ВПнМ, примеры задач/Задача 5

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

Версия 11:55, 22 мая 2009

Вариант 1

Задача 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 ))

Задача 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) )

Вариант 2

Задача 1

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

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

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

Задача 2

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

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

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

Задача 3

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

#define was_iter_begin P@iter_begin
#define was_iter_end P@iter_end
#define was_req ...@C_send_req
#define was_ack ...@D_send_ack

[]((was_iter_begin) -> [](was_req -> (!was_iter_end U (was_ack && !was_iter_end))))