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

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

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

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

<div style="float:right">__TOC__</div>
== Как решать эти задачи? ==
Для решения этих задач '''обязательно''' знать '''[[ВПнМ/Теормин#.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 шаблоны].'''

Полезна также ссылка из шаблонов на то, что означают различные области[http://patterns.projects.cis.ksu.edu/documentation/patterns/scopes.shtml].
Обратите внимание на "между Q и R", т.е. "Between Q and R" и на "после Q до R", т.е. "After Q, until R"

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

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

Будьте готовы к тому, что вам скажут, что в формуле '''применять слабый 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 a (p@iter_begin)
 #define b (p@iter_end)
 #define c (y==5)
 #define d (x==3)

[](a & !b -> (c & Xd & X !b) W b)

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

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

#define a (state==leave)
 #define b (p@sent)

<>a -> ((b -> b & X (!b U a)) U a)

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

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

#define a (state==enter_critical)
 #define b (state==leave_critical)
 #define c (p@lock)
 #define d (state==locked)

[]( a -> ((!c U d) U b) ) // Этот вариант не учитывает то, что b не может быть одновременно с a, и то, что b когда-либо наступит

[]( (a & !b & <>b) -> ((!c U d) U b) )

[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно объединить d и b - c не наступит, пока не наступит один из них

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

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

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

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

al-indigo:
 меня мучают особые сомнения, но кажется, так?
 !S | [](<>S -> (Q -> X([]!Q)))

Авварон:
Нет, оригинал был правильный. 2я формула вообще инвертированная по-моему + напрягает !S в начале

al-indigo:
!S в начале -- я имел в виду случай, когда state==enter_critical вообще не наступает. В самой формуле я, может, ошибся, но вообще я вот сейчас смотрю, и вроде, мне кажется, что правильно. Ну то есть так примерно: "Либо S не наступает никогда, либо, если S когда-нибудь наступает, то всегда выполняется то, что Q наступает, и если оно наступает, что начиная со следующего состояния всегда !Q". Или я не так это читаю?

Авварон:
 !S напрягло, ибо нет квантора времени. Если написать []!S, то этот случай будет включен в S->
 у тебя формула проверяет ДО наступления S (ибо <>S возвращает True независимо от того, есть ли сейчас S (а от того, что оно будет). Это я подразумевал под инвертированностью. <> Надо убрать и думать дальше. Без <> импликация теряет свойство "продолжительности" - значит надо пофиксить это добавлением [] в правую ее часть. Плюс у тебя не учтено что Q наступит.

Итого:
 #define A "state == enter_critical"
 #define B Q@received

[]( A -> ( <>B && [](B -> X[]!B) ) )

Если в условие задачи добавить инвариантность к прореживанию, то решение будет выглядеть так:

[]( a -> ( <>b && [](b -> (b U []!b)) ) )

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

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

#define a "state == leave"
 #define b P@sent

!a W (b && !b)

!a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта

UPD: (b && !b) всегда false. Если наступление события означает, что условие стало верным, то ответ

!a W b

Если наступление события означает, что условие побыло истинным, а потом стало ложным, то ответ

!a W (b && X!b)

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

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

#define a P@iter_begin
 #define b P@iter_end
 #define c ...@C_send_req
 #define d ...@D_send_ack

[]( a -> ( (c -> (!b U d)) U b) )

[]( (a & !b & <>b) -> ( (c -> (!b U d)) U b) ) // добавили то, что a и b не могут быть одновременно и то, что b когда-либо наступит

[]( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) ) // добавили то, что b не происходит одновременно с d. Окончательный вариант.

Teravisor:
Все три три не верны потому, что формулировка "после ... до ..." подразумевает, что второе событие может не произойти.
Моя версия(шаблон S responds to P After Q until R, раскрытие W): [](a && !b -> ( ((p -> (!b U (q && !b ))) U b) || ([](p -> (!b U (q && !b ))) )

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

[]( a -> ((c -> c U (!c U b)) U b) )

[]( (a & !b & <>b) -> ((c -> c U (!c U b)) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.

Teravisor: Та же самая ошибка, что и в задаче 1.
Мой вариант(Заменить в 2й формуле последний U на W и раскрыть с небольшой правкой условия !c U b):

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

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

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

#define a Start
 #define b End
 #define c R
 #define d S

[](a -> ( (!d U c) U b ))

[]( (a & !b & <>b) -> ( (!d U c) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет

[]( (a & !b & <>b) -> ( !d U (c | b)) ) // можно и так

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

#define a START
 #define b END
 #define c x==1
 #define d S

[](a -> ( (c -> (!b U d)) U b)

[]( (a & !b & <>b) -> ( (c -> (!b U d)) U b) // добавили то, что a и b не происходят одновременно и что b когда-либо произойдет

[]( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) // добавили то, что b и d не происходят одновременно. Окончательный вариант.

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

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

#define a p@iter_begin
 #define b p@iter_end
 #define c c!req
 #define d d?ack

[](a -> ( (!c U d) U b))

[]( (a & !b & <>b) -> ((!c U d) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.

[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно и так

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

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

#define a (state == enter)
 #define b (state == leave)
 #define c (с!req)
 #define d (в?ack)

[](a -> (c -> ((!b U d) U b))

[]( (a & !b & <>b) -> (c -> (!b U (d & !b))) U b) ) // Добавили то, что a и b не могут происходить одновременно и аналогично d и b. Окончательный вариант.

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

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

#define a p@iter_end
 #define b x == 3
 #define c y == 5

(b -> (!a U c)) U a

<>a ->(  (b -> (!a U (c & !a))) U a ) // Добавили то, что a когда-либо произойдет, и то, что c и a не происходят одновременно. Окончательный вариант.

(!a U b) -> (!a U c) // Потомкам: доказать что эта формула верна или нет:)

Teravisor: Потомки доказывают: третья не верная. Мы смотрим обе импликации(->) из начальной точки, т.е. нам подойдет

!a !a !a !a !a !a  a

!b !b !b !b !b  b  b

!c  c  c  c  c  c  c

!a U c выполняется. => формула true, хотя условию не удовлетворяет. Если поставить [] перед всей формулой правильность не изменится. Кто хочет может сам доказать.

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

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

#define a (state == enter_critical)
 #define b p@unlock

[](a -> []b)

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

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

#define a (state == leave_critical)
 #define b (x == 3)

(b W a) // []b || (b U a)  - Тоже самое, но через сильный Until.

(b U a) // Можно так.

<>a -> (b U a) // Или так.

Потомкам: понять разницу:)

Teravisor: потомки говорят, между 2 и 3 формулами разницы нету. Объяснение: U требует выполнимости где-то второго аргумента, в данном случае "a", в случае если его нет, формула не выполняется. требование <>a-> может быть расценено лектором как избыточное, и вообщем то не хорошо. Вообще говоря вроде первая формула правильная, в отличие от последних двух, но и правильность последних можно доказать из утверждения "я так понял задание".

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

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

#define a (state == enter_critical)
 #define b (state == leave_critical)
 #define c p@sent
 #define d q@received

[]( (a & !b & <>b) -> ((c -> (!b U d)) U b)  ) // Здесь U b можно заменить на W b (зависит от прочтения задачи)

Teravisor: то, же что и в задании 1. Комментарий это не можно, а нужно. И заменой U b на W b не всё исправится - надо еще <>b убрать вначале.

=== Задача 11 ===

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

#define a (p@iter_end)
 #define b (x == 3)

!a W (b && !a) // В принципе, тут можно сильный Until поставить.

([]!a) || (!a U (b && !a)) // Расписан слабый Until

=== Задача 12 ===

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

#define a (state == enter)
 #define b (state == leave)
 #define c (x == 3)

[]( a -> (!b U c) ) // "Простой" вариант.

[]( (a && !b && <>b) -> (!b U (c && !b)) ) // Окончательный.

=== Задача 13 ===

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

#define a (state == leave)
 #define b (channel ! req)

b W a

[]b || (b U a) // Расписан Weak.

=== Вариант 110 ===

==== Задача 1 ====
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза

#define a p@iter_begin
 #define b p@iter_end
 #define c p@lock

[](a -> !b U c)

[]( (a & !b && <>b) -> (!b U (c & !b)) ) // Окончательный вариант.

====Задача 2====
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: всегда выполняется 'процесс p находится на метке lock'

#define a state==enter
 #define b state==leave
 #define c p@lock

[](a -> (c U b))

[]( (a && !b && <>b) -> (c U b) )

====Задача 3====
После наступления события 'значение глобальной переменной state равно enter' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
 
 #define a state==enter
 #define b x==3

[](a -> <>b)

[](!a) | <>(a & <>b)) // Потомкам: проверить правильность.

=== Вариант 104 ===
==== Задача 1 ====
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: событие 'из канала d принимается сообщение ack' наступает ровно один раз

#define a p@iter_begin
 #define b p@iter_end
 #define c d?ack
 [] (  a -> ( <>b -> (!b&!c) U (c & !b U (!c & b) )   ||   []!b -> (!c U (c U !c)) )     )

al-indigo:
 Фиг знает, что тут происходит, но мне кажется, что правильно будет так:
 [](( a & !b & <>b ) -> (!b U (c -> [](!c))))

Авварон:
 без Х не решается => все что сверху - туфта
 с Х:
 #define A p@iter_begin
 #define B p@iter_end
 #define C d?ack
 []( A -> (C -> X (!C U B)) ) // туплю - не надо ли 2ю импликацию сделать также U B ? вроде нет

====Задача 2====
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке unlock' наступает не менее одного раза

#define d (state==enter)
 #define e (state==leave)
 #define f p@unlock
 [] ( (d & (<>e) ) -> (!e U f) )

al-indigo:
 Пропущено, что d и e не совпадают:
 [] ( (d & (<>e) & !e ) -> (!e U f) )

Авварон:
 #define A (state==enter)
 #define B (state==leave)
 #define C p@unlock
 короткая: [](A -> (!B U C))
 длинная: []( (A & !B & <>B) -> (!B U C) )

====Задача 3====
После наступления события 'значение глобальной переменной state равно enter_critical' верно: никогда не выполняется 'значение глобальной переменной state равно unlocked'

#define g (state==enter_critical)
 #define h (state==unlocked)
 [] ([]!g || (g -> []!h))

al-indigo:
 ok?

Авварон:
 Похоже на правду, но я бы писал так (используя шаблон из 8й лекции на стр 56):
 #define A (state==enter_critical)
 #define B (state==unlocked)
 [](A -> []!B)
 По идее будет то же самое после преобразований

=== Вариант 32 ===
==== Задача 1 ====

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

#define S state == state_critical
#define P x = 3

((!P U (S || (P U (S || (!P U S))))) || ([] !S && ( [] ! P) || [] P || P U ([] ! P) || !P U ( P U ([] !P)) )

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

al-indigo:
 По-моему, как-то уж очень избыточно
 []((P & !S & <>S) -> (!P U S))

[]((P & !S & <>S) -> (P U (!P U S)))         ( поправил al-indigo: P->!P - всегда false)

Авварон:
 #define A state == state_critical
 #define B x = 3
 [](B -> B U !B U A)
 вроде так, проверьте)

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

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

#define S state = leave_critical
#define P p@lock

([]!S) || (!S U (P && !S))

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

al-indigo:
 ок?

Авварон:
 ага, но я бы писал так:
 #define A state = leave_critical
 #define B p@lock
 через Weak, простая: !A W B
 через Weak, сложная: !A W (B & !A)
 через Until, сложная: []!A || (!A U (B & !A))
 Эти 3 ф-лы эквивалентны, но W имхо читать проще

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

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

#define A state == leave_critical
#define B c@req 
#define C d@ack

((! B U A ) || ((!A && !B) U (C && (! A U B )))) || ( [] !B) || (!B U C)

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

al-indigo:
 <>A -> (!B U (C | A))

Авварон:
 согласен
 малый фикс:
 <>A -> (!B U C U A) 
 в этом варианте проще добавить неодновременность, если преподу припрет изменить условие. Да, и <>A зависит от прочтения, тоже можно опустить (не факт что оно будет)

===Вариант 29===

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

До наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной state равно unlocked'наступает событие 'процесс p находится на метке unlock' (полученное свойство не обязательно может быть инвариантным к прореживанию)

#define p_iter_end (p@iter_end)
#define p_iter_unlock (p@iter_unlock)
#define state (state=unlocked)

[](((state->X p_iter_unlocked) U p_iter_end))

al-indigo:
 кажется, так
 [](!p_iter_end U (p_iter_unlock -> X state))

Авварон:
 al-indigo у тебя условие слабее - хотя бы 1 раз будет выполнено условие (а это не имелось ввиду, поэтому так). Можно перефразировать "за каким-то B будет С" (но не за всеми!)
 #define A (p@iter_end)
 #define B (p@iter_unlock)
 #define C (state=unlocked)
 (B -> X C) U A

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

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

#define p_iter_begin(p@iter_begin)
#define p_iter_end((p@iter_end)
#define c_S ...@C_send_req

[](p_iter_begin -> !p_iter_end || (!p_iter_end U (c_S U (!c_S U p_iter_end ))))

al-indigo:
 []((p_iter_begin & !p_iter_end & <>p_iter_end) -> (req -> (![]req U p_iter_end)))

[]((p_iter_begin & !p_iter_end & <>p_iter_end) -> (req -> (req U (!req U p_iter_end)))) (поправил al-indigo)

Авварон:
 о5 задача не решается без X
 #define A (p@iter_begin)
 #define B ((p@iter_end)
 #define C ...@C_send_req
 []( A -> { (C -> X[!C U B]) U B } )

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

Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно:всегда выполняется 'процесс p находится на метке lock'

#define p_iter_begin(p@iter_begin)
#define p_iter_end((p@iter_end)
#define p_lock(p@lock)

[](p_iter_begin & !p_iter_end & <>p_iter_end)->(p_lock U p_iter_end)

Сдавал не Коннову

al-indigo:
 может быть избыточно, но должно быть правильно
 []((p_iter_begin & !p_iter_end & <>p_iter_end)->([]p_lock U p_iter_end))

Авварон:
 #define A (p@iter_begin)
 #define B ((p@iter_end)
 #define C (p@lock)
 простая: [](A -> (C U B))
 сложная: []( (A & !B & <>B) -> (C U B) )

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

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

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

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

Шаблон:Курс ВПнМ

Получено с http://esyr.us/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_%D0%BF%D1%80%D0%B8%D0%BC%D0%B5%D1%80%D1%8B_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_5

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

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

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 58: / Строка 58: @@
 событие 'процесс q находится на метке received' наступает ровно один раз
- #define a "state == enter_critical"
+ #define S "state == enter_critical"
- #define b Q@received
+ #define Q Q@received
-[]( a -> ( <>b && [](b -> X[]!b) ) )
+ [](S -> (<>Q && [](Q -> X([]!Q))))
+al-indigo:
+ меня мучают особые сомнения, но кажется, так?
+ !S | [](<>S -> (Q -> X([]!Q)))
+Авварон:
+Нет, оригинал был правильный. 2я формула вообще инвертированная по-моему + напрягает !S в начале
+al-indigo:
+!S в начале -- я имел в виду случай, когда state==enter_critical вообще не наступает. В самой формуле я, может, ошибся, но вообще я вот сейчас смотрю, и вроде, мне кажется, что правильно. Ну то есть так примерно: "Либо S не наступает никогда, либо, если S когда-нибудь наступает, то всегда выполняется то, что Q наступает, и если оно наступает, что начиная со следующего состояния всегда !Q". Или я не так это читаю?
+Авварон:
+ !S напрягло, ибо нет квантора времени. Если написать []!S, то этот случай будет включен в S->
+ у тебя формула проверяет ДО наступления S (ибо <>S возвращает True независимо от того, есть ли сейчас S (а от того, что оно будет). Это я подразумевал под инвертированностью. <> Надо убрать и думать дальше. Без <> импликация теряет свойство "продолжительности" - значит надо пофиксить это добавлением [] в правую ее часть. Плюс у тебя не учтено что Q наступит.
+Итого:
+ #define A "state == enter_critical"
+ #define B Q@received
+ []( A -> ( <>B && [](B -> X[]!B) ) )
 Если в условие задачи добавить инвариантность к прореживанию, то решение будет выглядеть так: