Вариант 7

Задача 1

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

#define p_end (p@iter_end)
#define x_3 (x == 3)
!p_end U (x_3 && !p_end)

Задача 2

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

#define s_enter (state == enter)
#define s_leave (state == leave)
#define x_3 (x == 3)
[]((s_enter && <>s_leave) -> (!s_leave U (x_3 && !s_leave)))

Задача 3

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

#define s_leave (state == leave)
#define c_req (c!req)

(<>s_leave -> (c_req U s_leave)) || ([]c_req)