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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Задача 1)
(Задача 5)
 
(72 промежуточные версии не показаны)
Строка 1: Строка 1:
 +
<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 шаблоны].'''
Для решения этих задач '''обязательно''' знать '''[[ВПнМ/Теормин#.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"
Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
Строка 10: Строка 14:
p W q = <>(!p) -> (p U q)
p W q = <>(!p) -> (p U q)
p W q = p U (q | []p)
p W q = p U (q | []p)
- 
== Задачи (не инв-ные) ==
== Задачи (не инв-ные) ==
Строка 19: Строка 22:
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной y равно 5' наступает событие 'значение глобальной переменной x равно 3' (полученное свойство не обязательно может быть инвариантным к прореживанию)
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной y равно 5' наступает событие 'значение глобальной переменной x равно 3' (полученное свойство не обязательно может быть инвариантным к прореживанию)
-
#define p_begin (p@iter_begin)
+
#define a (p@iter_begin)
-
#define p_end (p@iter_end)
+
#define b (p@iter_end)
-
#define global5 (g==5)
+
#define c (y==5)
-
#define global3 (g==3)
+
#define d (x==3)
-
[](<>p_begin && p_begin -> X <> (global5 -> X global3 ))
+
[](a & !b -> (c & Xd & X !b) W b)
-
 
+
-
TeX'ом:
+
-
<math>\Box (\Diamond p \And p \rightarrow X \Diamond (g1 \rightarrow g2))</math>
+
-
(по-моему, в формуле вообще нету p_end. такого быть не должно.)
+
-
 
+
-
me thinks so:
+
-
<math>\Box (pb \land \neg pe \to (g5 \land X g3 \land X \neg pe) W pe)</math>
+
-
 
+
-
 
+
-
al-indigo:
+
-
//неправильно! //[]((p_begin & !p_end & <>p_end) -> (global5 -> Xglobal3))
+
-
 
+
-
Авварон:
+
-
я вывел формулу, которая под меткой "me thinks so:" (за исключением что я поставил сильный Until). Еще можно сделать !pe U g5 (те не выйдем, пока не найдем g5. Но это необязательно
+
-
вариант al-indigo неверный, тк нет квантора времени на (global5 -> Xglobal3) (то есть оно выполнено не ПОСЛЕ начала, а во время начала)
+
-
 
+
-
al-indigo:
+
-
Угу, ты прав
+
=== Задача 2 ===
=== Задача 2 ===
Строка 48: Строка 33:
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза
-
#define state_leave (state==leave)
+
#define a (state==leave)
-
#define p_sent (p@sent)
+
#define b (p@sent)
-
[](p_sent -> X (!p_sent U state_leave))
+
<>a -> ((b -> b & X (!b U a)) U a)
-
 
+
-
me thinks so:
+
-
<math>\diamond s \to ((p \to X(\neg p\ U s))\ U s)</math>
+
-
 
+
-
al-indigo
+
-
<>state_leave -> (<>state_leave -> []!state_leave) U a)
+
-
 
+
-
Авварон:
+
-
метка "me thinks so:" похожа на правду (можно убрать <>s - зависит от прочтения задачи)
+
-
al-indigo во 1х нельзя написать свойство 1го раза без оператора Next (тк оно не инвариантно по прореживанию)
+
-
во 2х <>A U B - это неправильно (тк Future действует на всем пути вычислений, независимо от наичия Until'а) и означает что-то типа ---BA
+
=== Задача 3 ===
=== Задача 3 ===
Строка 68: Строка 42:
Между событиями 'значение глобальной переменной state равно enter_critical' и 'значение глобальной переменной state равно leave_critical' верно: если наступило событие 'процесс p находится на метке lock', то до него было событие 'значение глобальной переменной state равно locked'
Между событиями 'значение глобальной переменной 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) )
 
- 
-
me thinks so:
 
#define a (state==enter_critical)
#define a (state==enter_critical)
#define b (state==leave_critical)
#define b (state==leave_critical)
-
#define c (state==locked)
+
#define c (p@lock)
-
#define d (p@lock)
+
#define d (state==locked)
-
<math>\Box ((a \and \neg b \and \Diamond b) \to (\neg c \ U (d \or b)))</math>
+
[]( a -> ((!c U d) U b) ) // Этот вариант не учитывает то, что b не может быть одновременно с a, и то, что b когда-либо наступит
-
al-indigo:
+
[]( (a & !b & <>b) -> ((!c U d) U b) )
-
[]((a & !b & <>b) -> (!d U (c | b)))
+
-
Авварон:
+
[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно объединить d и b - c не наступит, пока не наступит один из них
-
обозначения я беру по порядку в тексте (то есть с предыдущими вариантами C и D наоборот)
+
-
[](A->((!C U D) U B))
+
-
отличия от al-indigo:
+
-
1) в моем случае, если Б не выполнено, то будет False. Но, имхо модель подразумевает что Б всегда есть - без разницы (о5 же вопрос понимания текста)
+
-
2) я решил забить на написание A & !B, тк тогда по хорошему аналогичные отрицания надо писать и внутри Until'ов и формула будет слишком громоздкой
+
-
3) можно заменить внутренний Until на Weak Until - зависит от того, ожидаем ли мы выполнение D или нет
+
-
а так, оба варианта имхо правильны
+
=== Задача 4 ===
=== Задача 4 ===
Строка 100: Строка 58:
событие 'процесс q находится на метке received' наступает ровно один раз
событие 'процесс q находится на метке received' наступает ровно один раз
-
#define S "state == enter_critical"
+
#define a "state == enter_critical"
-
#define Q Q@received
+
#define b Q@received
-
[](S -> (<>Q && [](Q -> X([]!Q))))
+
[]( a -> ( <>b && [](b -> X[]!b) ) )
-
al-indigo:
+
Если в условие задачи добавить инвариантность к прореживанию, то решение будет выглядеть так:
-
меня мучают особые сомнения, но кажется, так?
+
-
!S | [](<>S -> (Q -> X([]!Q)))
+
-
Авварон:
+
[]( a -> ( <>b && [](b -> (b U []!b)) ) )
-
Нет, оригинал был правильный. 2я формула вообще инвертированная по-моему + напрягает !S в начале
+
-
 
+
-
al-indigo:
+
-
!S в начале -- я имел в виду случай, когда state==enter_critical вообще не наступает. В самой формуле я, может, ошибся, но вообще я вот сейчас смотрю, и вроде, мне кажется, что правильно. Ну то есть так примерно: "Либо S не наступает никогда, либо, если S когда-нибудь наступает, то всегда выполняется то, что Q наступает, и если оно наступает, что начиная со следующего состояния всегда !Q". Или я не так это читаю?
+
=== Задача 5 ===
=== Задача 5 ===
Строка 120: Строка 72:
событие 'процесс p находится на метке sent' наступает не менее одного раза
событие 'процесс p находится на метке sent' наступает не менее одного раза
-
#define R "state == leave"
+
#define a "state == leave"
-
#define was_sent P@sent
+
#define b P@sent
-
([]!R) || (!R U (was_sent && !R))
+
!a W (b && !b)
-
al-indigo:
+
!a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта
-
Может, здесь не слабый антил всё-таки?
+
-
!R U (was_sent && !R)
+
-
Авварон:
+
UPD: (b && !b) всегда false. Если наступление события означает, что условие стало верным, то ответ
-
Имхо без разницы слабый или сильный. Оба варианта ок
+
 
 +
!a W b
 +
 
 +
Если наступление события означает, что условие побыло истинным, а потом стало ложным, то ответ
 +
 
 +
!a W (b && X!b)
== Задачи (инв-ные) ==
== Задачи (инв-ные) ==
Строка 138: Строка 93:
после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
-
#define begin P@iter_begin
+
#define a P@iter_begin
-
#define end P@iter_end
+
#define b P@iter_end
-
#define R ...@C_send_req
+
#define c ...@C_send_req
-
#define S ...@D_send_ack
+
#define d ...@D_send_ack
-
[]((begin) -> [](R -> (!end U (S && !end))))
+
[]( a -> ( (c -> (!b U d)) U b) )
-
al-indigo:
+
[]( (a & !b & <>b) -> ( (c -> (!b U d)) U b) ) // добавили то, что a и b не могут быть одновременно и то, что b когда-либо наступит
-
Тут явно какая-то херня с двумя последними #define, хотя я и не уверен, что правильно у меня
+
-
+
-
#define begin (P@iter_begin)
+
-
#define end (P@iter_end)
+
-
#define R (C!req)
+
-
#define S (D?ack)
+
-
[]((begin & !end & <>end) -> (R -> (!end U (S & !end))) U end)
+
-
//это паттерн response between. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого
+
-
Авварон:
+
[]( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) ) // добавили то, что b не происходит одновременно с d. Окончательный вариант.
-
это задача про самолет в чистом виде:)
+
 
-
вариант al-indigo верный, только <>end не нужен - тк он есть всегда по условию, то Future(end) всегда true и ни на что не влияет
+
Teravisor:
-
Ну и о5 же я бы не писал невозможность одновременности состояний (begin & !end - они несут мало смысла:)
+
Все три три не верны потому, что формулировка "после ... до ..." подразумевает, что второе событие может не произойти.
 +
Моя версия(шаблон S responds to P After Q until R, раскрытие W): [](a && !b -> ( ((p -> (!b U (q && !b ))) U b) || ([](p -> (!b U (q && !b ))) )
=== Задача 2 ===
=== Задача 2 ===
-
После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)
+
После события a и до наступления события b событие c наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)
 +
[]( a -> ((c -> c U (!c U b)) U b) )
-
'''1й вариант''':
+
[]( (a & !b & <>b) -> ((c -> c U (!c U b)) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
-
[] (p && !q -> !r W (q || (r W (q || !r W q))))
 
-
'''2й вариант''':
+
Teravisor: Та же самая ошибка, что и в задаче 1.
-
<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>
+
Мой вариант(Заменить в 2й формуле последний U на W и раскрыть с небольшой правкой условия !c U b):
-
ps. пояснение формулы:
+
[]( a && !b -> ( ((c -> c U (!c U b)) U b) || [](c -> c U ([](!c && !b))) ) )
-
# до первого || — случай, когда q не факт, что произойдёт (после того, как произойдёт r, оно длится до тех пор, пока не прекратится)
+
-
# после первого || — случай, когда q обязательно произойдет
+
-
#* до второго || — r встречается 0 раз
+
-
#* после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков)
+
-
 
+
-
al-indigo:
+
-
адский ад какой-то, я так ничего и не понял тут, надо будет завтра ещё подумать :(
+
-
 
+
-
Авварон:
+
-
имхо, задача нерешаема) так как свойства, инвариантные по прореживанию, не могут отличить - было одно событие или два (одно это прореживание двух).
+
=== Задача 3 ===
=== Задача 3 ===
Строка 187: Строка 125:
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).
В одной итерации вычисления между метками 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>
+
#define a Start
 +
#define b End
 +
#define c R
 +
#define d S
-
al-indigo:
+
[](a -> ( (!d U c) U b ))
-
Кажется, вариант выше тоже *почти* правильный (не хватает ещё пары внешних скобок, вроде), но какой-то перегруженный. Вот мой:
+
-
[]((start & !end & <>end) -> (!S U (R | end))) //Precedence between
+
-
Авварон:
+
[]( (a & !b & <>b) -> ( (!d U c) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет
-
первый вариант не верен, если не встретится R - будет верна правая часть дизъюнкции и на левую мы кладем => свойство того, что должно быть !S, тупо не проверяется (противоречие с тем, что оно не должно появляться до R).
+
 
-
al-indigo - нормально, но о5 же - почему есть проверка неодновременности start и end, но нет аналогичной у Until (они в принципе не нужны, но если мы захотим добавить что-нибудь эдакое, то добавить будет сложно из-за дизъюнкции). Мой вариант: (аналогичный, и как обычно без !End & <>End)
+
[]( (a & !b & <>b) -> ( !d U (c | b)) ) // можно и так
-
[](Start->( (!S U R) U End))
+
=== Задача 4 ===
=== Задача 4 ===
В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.
В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.
-
[] (START & !END & <>END -> ( (!P U END)||((P -> (!END U S))U END) )
+
#define a START
 +
#define b END
 +
#define c x==1
 +
#define d S
-
al-indigo:
+
[](a -> ( (c -> (!b U d)) U b)
-
Хорошая тренировка -- найдите отличия (они есть). Единственное что -- странно, но случай, когда P не случается выглядит уместным (в решении выше), а у меня его нет -- в паттерне написано, как у меня. Кто-нибудь, прокомментируйте? Или из этого не следует, что P обязательно произойдёт?
+
-
[] ((Start & !End & <>End) -> (P -> (!End U (S & !End) U End))
+
-
Авварон:
+
[]( (a & !b & <>b) -> ( (c -> (!b U d)) U b) // добавили то, что a и b не происходят одновременно и что b когда-либо произойдет
-
первый вариант верный, но там не нужна дизъюнкция вообще (вариант !P включается в P -> BLA ибо -> это !P || BLA)
+
-
al-indigo, ты накосячил со скобками, надо
+
-
[] ((Start & !End & <>End) -> ( {P -> (!End U (S & !End))} U End)
+
-
Из-за скобок и коммент неверный - в этом варианте !P подходит
+
-
al-indigo:
+
[]( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) // добавили то, что b и d не происходят одновременно. Окончательный вариант.
-
и правда накосячил. Чёрт возьми, как же на пересдаче-то не ошибиться :(
+
=== Задача 5 ===
=== Задача 5 ===
Строка 220: Строка 154:
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'
-
#define p_b p@iter_begin
+
#define a p@iter_begin
-
#define p_e p@iter_end
+
#define b p@iter_end
-
#define c_r c!req
+
#define c c!req
-
#define d_a d?ack
+
#define d d?ack
-
[]( (p_b && !p_e && <>p_e) -> ((!c_r U p_e) || (!c_r U d_a)) )
+
[](a -> ( (!c U d) U b))
-
(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)
+
[]( (a & !b & <>b) -> ((!c U d) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
-
al-indigo:
+
[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно и так
-
//абсолютно то же самое, шаблон precedence between/
+
-
[]((p_b & !p_e & <>p_e) -> (!c_r U (p_a | p_e)))
+
-
 
+
-
Задача типа "недосамолет", аналогична 3ей
+
-
Решил переписать в "прямых" обозначениях (и исправить косяк с p_a):
+
-
#define A p@iter_begin
+
-
#define B p@iter_end
+
-
#define C c!req
+
-
#define D d?ack
+
-
[]((A & !B & <>B) -> (!C U (D | B)))
+
=== Задача 6 ===
=== Задача 6 ===
Строка 245: Строка 169:
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
-
#define s_e state == enter
+
#define a (state == enter)
-
#define s_l state == leave
+
#define b (state == leave)
-
#define c_r c!req
+
#define c !req)
-
#define d_a d?ack
+
#define d ?ack)
-
[]( (s_e && !s_l && <>s_l) -> ((!s_l U c_r) -> (!s_l U d_a)) )
+
[](a -> (c -> ((!b U d) U b))
-
(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)
+
[]( (a & !b & <>b) -> (c -> (!b U (d & !b))) U b) ) // Добавили то, что a и b не могут происходить одновременно и аналогично d и b. Окончательный вариант.
-
upd: скорее всего, это решение неправильное. Варианты, скорее всего правильные:
+
=== Задача 7 ===
-
[]((s_e && !s_l) -> ((c_r -> (!s_l U d_a)) U s_l) )
+
-
[]((s_e && !s_l && <>s_l) -> (( <>c_r -> !s_l U (c_r && (!s_l U d_a)))) )
+
 +
До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5'
-
al-indigo:
+
#define a p@iter_end
-
Это дублирование задачи один, повторюсь, чтобы можно было сравнить и понять, что всё-таки правильно. Кажется, первые два варината неправильные вообще.
+
#define b x == 3
-
И тут опять херня с #define, хотя я снова не уверен, что правильно у меня
+
#define c y == 5
-
#define begin (P@iter_begin)
+
-
#define end (P@iter_end)
+
-
#define R (C!req)
+
-
#define S (D?ack)
+
-
[]((begin & !end & <>end) -> (R -> (!end U (S & !end))) U end)
+
-
//это паттерн response between. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого
+
-
Авварон:
+
(b -> (!a U c)) U a
-
прямые обозначения:
+
-
#define A (P@iter_begin)
+
-
#define B (P@iter_end)
+
-
#define C (C!req)
+
-
#define D (D?ack)
+
-
урезанная: [](A -> (C -> ((!B U D) U B)
+
-
полная: []((A & !B & <>B) -> (C -> (!B U (D & !B))) U B)
+
-
=== Задача 7 ===
+
<>a ->( (b -> (!a U (c & !a))) U a ) // Добавили то, что a когда-либо произойдет, и то, что c и a не происходят одновременно. Окончательный вариант.
-
До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5'
+
(!a U b) -> (!a U c) // Потомкам: доказать что эта формула верна или нет:)
-
#define p_e p@iter_end
+
Teravisor: Потомки доказывают: третья не верная. Мы смотрим обе импликации(->) из начальной точки, т.е. нам подойдет
-
#define x_3 x == 3
+
-
#define y_5 y == 5
+
-
(!p_e U x_3) -> (!p_e U y_5)
+
!a !a !a !a !a !a a
-
(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)
+
!b !b !b !b !b b b
-
al-indigo:
+
!c c c c c c c
-
<>p_e -> ((x_3 -> (!p_e U (y_5 & !p_e))) U p_e) // из паттернов. Но тут неясно -- может ли быть так, что х не будет равно 3?
+
-
<>p_e -> ((!x_3 | (x_3 -> (!p_e U (y_5 & !p_e)))) U p_e) //мой вариант, просто рассуждения
+
-
Авварон:
+
!a U c выполняется. => формула true, хотя условию не удовлетворяет. Если поставить [] перед всей формулой правильность не изменится. Кто хочет может сам доказать.
-
первое хрень (оно ОЧЕНЬ похоже на правду, но я не могу доказать что она не верна. Препод похоже тоже не смог:)), 2е оба верны (во 2м !x_3 лишняя, тк "!x_3 | x_3 -> A" EQ "!x_3 | !x_3 | A")
+
-
прямые обозначения:
+
-
#define A p@iter_end
+
-
#define B x == 3
+
-
#define C y == 5
+
-
урезанная: (B -> (!A U C)) U A
+
-
полная: (B -> (!A U [C & !A])) U A
+
-
<>A по желанию, зависит от того, хотим ли мы видеть А
+
-
Задачу классифицирую как "самолет урезанный"
+
=== Задача 8 ===
=== Задача 8 ===
Строка 309: Строка 206:
После наступления события 'значение глобальной переменной state равно enter_critical' верно: всегда выполняется 'процесс p находится на метке unlock'
После наступления события 'значение глобальной переменной state равно enter_critical' верно: всегда выполняется 'процесс p находится на метке unlock'
-
Решение.
+
#define a (state == enter_critical)
 +
#define b p@unlock
-
формально:
+
[](a -> []b)
-
#define p 'значение глобальной переменной state равно enter_critical'
+
-
#define q 'процесс p находится на метке unlock'
+
-
 
+
-
спин:
+
-
#define p (state == enter_critical)
+
-
#define q p@unlock
+
-
 
+
-
[](p -> []q)
+
-
 
+
-
(Источник: практикум, задание 4, вариант 24, сдано Савенкову)
+
-
 
+
-
al-indigo:
+
-
ok?
+
-
 
+
-
Авварон:
+
-
ок
+
=== Задача 9 ===
=== Задача 9 ===
Строка 333: Строка 215:
До наступления события 'значение глобальной переменной state равно leave_critical' верно: всегда выполняется 'значение глобальной переменной x равно 3'
До наступления события 'значение глобальной переменной state равно leave_critical' верно: всегда выполняется 'значение глобальной переменной x равно 3'
-
Решение.
+
#define a (state == leave_critical)
-
формально:
+
#define b (x == 3)
-
#define p 'значение глобальной переменной state равно leave_critical'
+
-
#define q 'значение глобальной переменной x равно 3'
+
-
спин:
+
(b W a) // []b || (b U a) - Тоже самое, но через сильный Until.
-
#define p (state == leave_critical)
+
-
#define q (x == 3)
+
-
( <> p -> ( q U p ) ) || [] q
+
(b U a) // Можно так.
-
(Источник: практикум, задание 4, вариант 24, сдано Савенкову)
+
<>a -> (b U a) // Или так.
-
al-indigo:
+
Потомкам: понять разницу:)
-
ok?
+
-
Авварон:
+
Teravisor: потомки говорят, между 2 и 3 формулами разницы нету. Объяснение: U требует выполнимости где-то второго аргумента, в данном случае "a", в случае если его нет, формула не выполняется. требование <>a-> может быть расценено лектором как избыточное, и вообщем то не хорошо. Вообще говоря вроде первая формула правильная, в отличие от последних двух, но и правильность последних можно доказать из утверждения "я так понял задание".
-
Да, ок, но я бы написал тут и "простой" вариант:
+
-
q W p
+
=== Задача 10 ===
=== Задача 10 ===
Строка 358: Строка 233:
верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received'
верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received'
-
Решение.
+
#define a (state == enter_critical)
-
формально:
+
#define b (state == leave_critical)
-
#define a 'значение глобальной переменной state равно enter_critical'
+
#define c p@sent
-
#define b 'значение глобальной переменной state равно leave_critical'
+
#define d q@received
-
#define p 'процесс p находится на метке sent'
+
-
#define q 'процесс q находится на метке received'
+
-
спин:
+
[]( (a & !b & <>b) -> ((c -> (!b U d)) U b) ) // Здесь U b можно заменить на W b (зависит от прочтения задачи)
-
#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) ) )
+
Teravisor: то, же что и в задании 1. Комментарий это не можно, а нужно. И заменой U b на W b не всё исправится - надо еще <>b убрать вначале.
-
 
+
-
(Источник: практикум, задание 4, вариант 24, сдано Савенкову)
+
-
 
+
-
al-indigo:
+
-
Здесь какая-то неточность, непонятно, насколько существенная. В первой подформуле точняк должно быть ещё <>b, а его там нет.
+
=== Задача 11 ===
=== Задача 11 ===
Строка 382: Строка 246:
До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
-
#define x3 (x == 3)
+
#define a (p@iter_end)
-
#define iter (p@iter_end)
+
#define b (x == 3)
-
([]!iter) || (!iter U (x3 && !iter))
+
!a W (b && !a) // В принципе, тут можно сильный Until поставить.
-
Есть подозрение, что первая скобка не нужна, т.к. во второй тоже не гарантируется наступление "итер", но она полностью описывает условие.
+
([]!a) || (!a U (b && !a)) // Расписан слабый Until
-
 
+
-
al-indigo:
+
-
А тут нужно учитывать, что iter_end может не наступить? Мне кажется, оно по условию всегда должно происходить в какой-то момент. И да -- само-то решение является правильным?
+
-
!iter U (x3 && !iter)
+
=== Задача 12 ===
=== Задача 12 ===
Строка 397: Строка 257:
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
 +
#define a (state == enter)
 +
#define b (state == leave)
 +
#define c (x == 3)
-
#define ent (state == enter)
+
[]( a -> (!b U c) ) // "Простой" вариант.
-
#define leave (state == leave)
+
-
#define x3 (x == 3)
+
-
[]((ent && <>leave && !leave) -> (!leave U (x3 && !leave)))
+
[]( (a && !b && <>b) -> (!b U (c && !b)) ) // Окончательный.
-
 
+
-
al-indigo:
+
-
не понимаю, что тут избыточного в решении, по-моему, самое то?
+
=== Задача 13 ===
=== Задача 13 ===
Строка 411: Строка 269:
До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
-
#define leave (state == leave)
+
#define a (state == leave)
-
#define send (channel ! req)
+
#define b (channel ! req)
-
(send U leave)||([]send)
+
b W a
-
//Задачи 11-13 были отправлены по почте, оценка 5. Решение задачи 12 - избыточно.
+
[]b || (b U a) // Расписан Weak.
-
 
+
-
al-indigo:
+
-
красивое, понятное и наверное правильное решение :)
+
=== Вариант 110 ===
=== Вариант 110 ===
Строка 426: Строка 281:
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
-
#define f_b p@iter_begin
+
#define a p@iter_begin
-
#define f_e p@iter_end
+
#define b p@iter_end
-
#define f_lock p@lock
+
#define c p@lock
-
[]( (f_b & !f_e && <>f_e) -> ( !f_e U ( f_lock & !f_e ) ) )
+
-
al-indigo:
+
[](a -> !b U c)
-
ok?
+
-
Авварон:
+
[]( (a & !b && <>b) -> (!b U (c & !b)) ) // Окончательный вариант.
-
ок
+
-
#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====
====Задача 2====
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: всегда выполняется 'процесс p находится на метке lock'
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: всегда выполняется 'процесс p находится на метке lock'
-
#define f_b state==enter
+
#define a state==enter
-
#define f_e state==leave
+
#define b state==leave
-
#define f_lock p@lock
+
#define c p@lock
-
[]((f_b && !f_e && <>f_e) -> (f_lock U f_e))
+
-
al-indigo:
+
[](a -> (c U b))
-
Может, избыточно, но кажется, так правильнее:
+
-
[]((f_b && !f_e && <>f_e) -> ([]f_lock U f_e))
+
-
Авварон:
+
[]( (a && !b && <>b) -> (c U b) )
-
al-indigo, твое решение неверное. Квантор [] НЕ ограничивается Until'ом
+
-
#define A state==enter
+
-
#define B state==leave
+
-
#define C p@lock
+
-
короткая: [](A -> (C U B))
+
-
полная: []((A && !B && <>B) -> (C U B))
+
====Задача 3====
====Задача 3====
После наступления события 'значение глобальной переменной state равно enter' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
После наступления события 'значение глобальной переменной state равно enter' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
-
#define q state==enter
+
#define a state==enter
-
#define p x==3
+
#define b x==3
-
[](!q) | <>(q & <>P))
+
-
al-indigo:
+
[](a -> <>b)
-
ok?
+
-
Авварон:
+
[](!a) | <>(a & <>b)) // Потомкам: проверить правильность.
-
#define A state==enter
+
-
#define B x==3
+
-
[](A -> <>B)
+
-
я бы написал так, а то что сверху имхо будет если развернуть импликацию. Могу ошибаться в своем варианте
+
=== Вариант 104 ===
=== Вариант 104 ===
Строка 510: Строка 342:
Пропущено, что d и e не совпадают:
Пропущено, что d и e не совпадают:
[] ( (d & (<>e) & !e ) -> (!e U f) )
[] ( (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====
====Задача 3====
Строка 520: Строка 359:
al-indigo:
al-indigo:
ok?
ok?
 +
 +
Авварон:
 +
Похоже на правду, но я бы писал так (используя шаблон из 8й лекции на стр 56):
 +
#define A (state==enter_critical)
 +
#define B (state==unlocked)
 +
[](A -> []!B)
 +
По идее будет то же самое после преобразований
=== Вариант 32 ===
=== Вариант 32 ===
Строка 537: Строка 383:
По-моему, как-то уж очень избыточно
По-моему, как-то уж очень избыточно
[]((P & !S & <>S) -> (!P U S))
[]((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 ====
==== Задача 2 ====
Строка 552: Строка 406:
al-indigo:
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 ====
==== Задача 3 ====
Строка 569: Строка 432:
al-indigo:
al-indigo:
<>A -> (!B U (C | A))
<>A -> (!B U (C | A))
 +
 +
Авварон:
 +
согласен
 +
малый фикс:
 +
<>A -> (!B U C U A)
 +
в этом варианте проще добавить неодновременность, если преподу припрет изменить условие. Да, и <>A зависит от прочтения, тоже можно опустить (не факт что оно будет)
===Вариант 29===
===Вариант 29===
Строка 585: Строка 454:
кажется, так
кажется, так
[](!p_iter_end U (p_iter_unlock -> X state))
[](!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====
====Задача 2====
Строка 599: Строка 475:
al-indigo:
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 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====
====Задача 3====
Строка 615: Строка 500:
может быть избыточно, но должно быть правильно
может быть избыточно, но должно быть правильно
[]((p_iter_begin & !p_iter_end & <>p_iter_end)->([]p_lock U p_iter_end))
[]((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) )
{{Курс ВПнМ}}
{{Курс ВПнМ}}

Текущая версия

Содержание

[править] Как решать эти задачи?

Для решения этих задач обязательно знать определения, а так же следующие шаблоны.

Полезна также ссылка из шаблонов на то, что означают различные области[1]. Обратите внимание на "между 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 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' наступает не более одного раза

  1. define S state == state_critical
  2. 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' наступает не менее одного раза

  1. define S state = leave_critical
  2. 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'

  1. define A state == leave_critical
  2. define B c@req
  3. 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' (полученное свойство не обязательно может быть инвариантным к прореживанию)

  1. define p_iter_end (p@iter_end)
  2. define p_iter_unlock (p@iter_unlock)
  3. 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' наступает не более одного раза

  1. define p_iter_begin(p@iter_begin)
  2. define p_iter_end((p@iter_end)
  3. 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'

  1. define p_iter_begin(p@iter_begin)
  2. define p_iter_end((p@iter_end)
  3. 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) )


Верификация программ на моделях


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин

Личные инструменты
Разделы