Редактирование: ВПнМ, примеры задач/Задача 5

Материал из eSyr's wiki.

Версия от 14:23, 6 июня 2010; 84.51.102.21 (Обсуждение)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

== Как решать эти задачи? ==
Для решения этих задач '''обязательно''' знать '''[[ВПнМ/Теормин#.D0.9B.D0.BE.D0.B3.D0.B8.D0.BA.D0.B0_LTL._.D0.A1.D0.B8.D0.BD.D1.82.D0.B0.D0.BA.D1.81.D0.B8.D1.81_LTL._.D0.A1.D0.B5.D0.BC.D0.B0.D0.BD.D1.82.D0.B8.D0.BA.D0.B0_.D0.B2.D1.8B.D0.BF.D0.BE.D0.BB.D0.BD.D0.B8.D0.BC.D0.BE.D1.81.D1.82.D0.B8_.D1.84.D0.BE.D1.80.D0.BC.D1.83.D0.BB._.D0.A1.D0.B8.D0.BB.D1.8C.D0.BD.D1.8B.D0.B9_.D0.B8_.D1.81.D0.BB.D0.B0.D0.B1.D1.8B.D0.B9_until.|определения]]''', а так же следующие '''[http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml шаблоны].'''

Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.

'''Инвариантная к прореживанию''' формула - это такая формула, результат вычисления которой не меняется от того, применяется прореживание или нет. '''Прореживание''' - это сужение нескольких состояний до одного (а м.б. и расширение одного до нескольких - доподлинно неизвестно).

Будьте готовы к тому, что вам скажут, что в формуле '''применять слабый until нельзя''', поэтому здесь следующие форм-лы экв-ти:
 p W q = ([]p) | (p U q)
 p W q = <>(!p) -> (p U q)
 p W q = p U (q | []p)

== Задачи (не инв-ные) ==
Втаких задачах можно спокойно применять оператор Next (X).

=== Задача 1 ===

После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной y равно 5' наступает событие 'значение глобальной переменной x равно 3' (полученное свойство не обязательно может быть инвариантным к прореживанию)

#define p_begin (p@iter_begin)
 #define p_end (p@iter_end)
 #define global5 (g==5)
 #define global3 (g==3)

[](<>p_begin && p_begin -> X <> (global5 -> X global3 ))

TeX'ом:
 <math>\Box (\Diamond p \And p \rightarrow X \Diamond (g1 \rightarrow g2))</math>
(по-моему, в формуле вообще нету p_end. такого быть не должно.)

=== Задача 2  ===

До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза

#define state_leave (state==leave)
 #define p_sent (p@sent)

[](p_sent -> X (!p_sent U state_leave))

=== Задача 3 ===

Между событиями 'значение глобальной переменной state равно enter_critical' и 'значение глобальной переменной state равно leave_critical' верно: если наступило событие 'процесс p находится на метке lock', то до него было событие 'значение глобальной переменной state равно locked'

#define state_enter (state==enter_critical)
 #define state_leave (state==leave_critical)
 #define state_locked (state==locked)
 #define p_lock (p@lock)

[]( state_enter -> X((!p_lock U state_leave) || (<>p_lock && !p_lock U state_locked) )

=== Задача 4 ===

После наступления события 'значение глобальной переменной state равно enter_critical' верно:
событие 'процесс q находится на метке received' наступает ровно один раз

#define S "state == enter_critical"
 #define was_received Q@received

[](S -> (<>was_received && [](was_received -> X([]!was_received))))

=== Задача 5 ===

До наступления события 'значение глобальной переменной state равно leave' верно:
событие 'процесс p находится на метке sent' наступает не менее одного раза

#define R "state == leave"
 #define was_sent P@sent

([]!R) || (!R U (was_sent && !R))

== Задачи (инв-ные) ==
=== Задача 1 ===

После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно:
после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'

#define begin P@iter_begin
 #define end P@iter_end
 #define R ...@C_send_req
 #define S ...@D_send_ack

[]((begin) -> [](R -> (!end U (S && !end))))

=== Задача 2 ===
После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)

'''1й вариант''':

[] (p && !q -> !r W (q || (r W (q || !r W q))))

'''2й вариант''':
 <math>\Box \Biggl( p \rightarrow \biggl( \Bigl( r \rightarrow (\text{r U !r}) \Bigr) \ || \ \Bigl( \text{(!r U q) } || \text{ (!q U (r U (!r U q)))} \Bigr) \biggr) \Biggr) </math>

ps. пояснение формулы:
# до первого || — случай, когда q не факт, что произойдёт (после того, как произойдёт r, оно длится до тех пор, пока не прекратится)
# после первого || — случай, когда q обязательно произойдет
#* до второго || — r встречается 0 раз
#* после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков)

=== Задача 3 ===

В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).

<math>\Box \biggl( Start \And \ !End \And \Diamond End \biggr) \rightarrow \biggl( \Bigl( \text{(!S U R)} \And !(S \And R) \And !End \Bigr) \ || \ \text{(!R U End)} \biggr) </math>

=== Задача 4 ===
В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.

[] (START & !END & <>END -> ( (!P U END)||((P -> (!END U S))U END) )

=== Задача 5 ===

Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'

#define p_b p@iter_begin
 #define p_e p@iter_end
 #define c_r c!req
 #define d_a d?ack

[](  (p_b && !p_e && <>p_e) -> ((!c_r U p_e) || (!c_r U d_a))  )

(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)

=== Задача 6 ===

Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'

#define s_e state == enter
 #define s_l state == leave
 #define c_r c!req
 #define d_a d?ack

[](  (s_e && !s_l && <>s_l) -> ((!s_l U c_r) -> (!s_l U d_a))  )

(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)

=== Задача 7 ===

До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5'

#define p_e p@iter_end
 #define x_3 x == 3
 #define y_5 y == 5

(!p_e U x_3) -> (!p_e U y_5)

(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)

=== Задача 8 ===

После наступления события 'значение глобальной переменной state равно enter_critical' верно: всегда выполняется 'процесс p находится на метке unlock'

Решение.

формально: 
#define p 'значение глобальной переменной state равно enter_critical' 
#define q 'процесс p находится на метке unlock'

спин:
#define p (state == enter_critical)
#define q p@unlock

[](p -> []q)

(Источник: практикум, задание 4, вариант 24, сдано Савенкову)

=== Задача 9 ===

До наступления события 'значение глобальной переменной state равно leave_critical' верно: всегда выполняется 'значение глобальной переменной x равно 3'

Решение.
формально: 
#define p 'значение глобальной переменной state равно leave_critical'
#define q 'значение глобальной переменной x равно 3'

спин:
#define p (state == leave_critical)
#define q (x == 3)

( <> p -> ( q U p )  ) || [] q

(Источник: практикум, задание 4, вариант 24, сдано Савенкову)

=== Задача 10 ===

После события 'значение глобальной переменной state равно enter_critical' и до наступления события 'значение глобальной переменной state равно leave_critical' 
верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received'

Решение.
формально: 
#define a 'значение глобальной переменной state равно enter_critical'
#define b 'значение глобальной переменной state равно leave_critical'
#define p 'процесс p находится на метке sent'
#define q 'процесс q находится на метке received'

спин:
#define a (state == enter_critical)
#define b (state == leave_critical)
#define p p@sent
#define q q@received

[]( ( a && !b ) -> ( ( ( p -> (!b U q) ) U b ) || [](p -> (!b U q) ) )

(Источник: практикум, задание 4, вариант 24, сдано Савенкову)

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице: