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

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

Содержание 1 Вариант 1 1.1 Задача 1 1.2 Задача 2 1.3 Задача 3 2 Вариант 2 2.1 Задача 1 2.2 Задача 2 2.3 Задача 3 3 Вариант 3 3.1 Задача 1 3.2 Задача 2 3.3 Задача 3

Вариант 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 ))

TeX'ом:

(по-моему, в формуле вообще нету 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) )

Вариант 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))))

Вариант 3

Задача 1

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

ps. пояснение формулы:

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

Задача 2

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

[](Start && !End && <>End) -> (((!S U R) && !(S && R) && !End) || (!R U End))

Задача 3

Пишите какие у вас задачи были.