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

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

Перейти к: навигация, поиск

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

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

Текущая версия Ваш текст
Строка 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"
 
Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
Строка 14: Строка 10:
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)
 +
== Задачи (не инв-ные) ==
== Задачи (не инв-ные) ==
Строка 22: Строка 19:
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной y равно 5' наступает событие 'значение глобальной переменной x равно 3' (полученное свойство не обязательно может быть инвариантным к прореживанию)
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной y равно 5' наступает событие 'значение глобальной переменной x равно 3' (полученное свойство не обязательно может быть инвариантным к прореживанию)
-
#define a (p@iter_begin)
+
#define p_begin (p@iter_begin)
-
#define b (p@iter_end)
+
#define p_end (p@iter_end)
-
#define c (y==5)
+
#define global5 (g==5)
-
#define d (x==3)
+
#define global3 (g==3)
-
[](a & !b -> (c & Xd & X !b) W b)
+
[](<>p_begin && p_begin -> X <> (global5 -> X global3 ))
 +
 
 +
TeX'ом:
 +
<math>\Box (\Diamond p \And p \rightarrow X \Diamond (g1 \rightarrow g2))</math>
 +
(по-моему, в формуле вообще нету p_end. такого быть не должно.)
=== Задача 2 ===
=== Задача 2 ===
Строка 33: Строка 34:
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза
-
#define a (state==leave)
+
#define state_leave (state==leave)
-
#define b (p@sent)
+
#define p_sent (p@sent)
-
<>a -> ((b -> b & X (!b U a)) U a)
+
[](p_sent -> X (!p_sent U state_leave))
=== Задача 3 ===
=== Задача 3 ===
Строка 42: Строка 43:
Между событиями 'значение глобальной переменной state равно enter_critical' и 'значение глобальной переменной state равно leave_critical' верно: если наступило событие 'процесс p находится на метке lock', то до него было событие 'значение глобальной переменной state равно locked'
Между событиями 'значение глобальной переменной state равно enter_critical' и 'значение глобальной переменной state равно leave_critical' верно: если наступило событие 'процесс p находится на метке lock', то до него было событие 'значение глобальной переменной state равно locked'
-
#define a (state==enter_critical)
+
#define state_enter (state==enter_critical)
-
#define b (state==leave_critical)
+
#define state_leave (state==leave_critical)
-
#define c (p@lock)
+
#define state_locked (state==locked)
-
#define d (state==locked)
+
#define p_lock (p@lock)
-
[]( a -> ((!c U d) U b) ) // Этот вариант не учитывает то, что b не может быть одновременно с a, и то, что b когда-либо наступит
+
[]( state_enter -> X((!p_lock U state_leave) || (<>p_lock && !p_lock U state_locked) )
-
 
+
-
[]( (a & !b & <>b) -> ((!c U d) U b) )
+
-
 
+
-
[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно объединить d и b - c не наступит, пока не наступит один из них
+
=== Задача 4 ===
=== Задача 4 ===
Строка 58: Строка 55:
событие 'процесс q находится на метке received' наступает ровно один раз
событие 'процесс q находится на метке received' наступает ровно один раз
-
#define a "state == enter_critical"
+
#define S "state == enter_critical"
-
#define b Q@received
+
#define was_received Q@received
-
[]( a -> ( <>b && [](b -> X[]!b) ) )
+
[](S -> (<>was_received && [](was_received -> X([]!was_received))))
-
 
+
-
Если в условие задачи добавить инвариантность к прореживанию, то решение будет выглядеть так:
+
-
 
+
-
[]( a -> ( <>b && [](b -> (b U []!b)) ) )
+
=== Задача 5 ===
=== Задача 5 ===
Строка 72: Строка 65:
событие 'процесс p находится на метке sent' наступает не менее одного раза
событие 'процесс p находится на метке sent' наступает не менее одного раза
-
#define a "state == leave"
+
#define R "state == leave"
-
#define b P@sent
+
#define was_sent P@sent
-
!a W (b && !b)
+
([]!R) || (!R U (was_sent && !R))
-
 
+
-
!a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта
+
-
 
+
-
UPD: (b && !b) всегда false. Если наступление события означает, что условие стало верным, то ответ
+
-
 
+
-
!a W b
+
-
 
+
-
Если наступление события означает, что условие побыло истинным, а потом стало ложным, то ответ
+
-
 
+
-
!a W (b && X!b)
+
== Задачи (инв-ные) ==
== Задачи (инв-ные) ==
Строка 93: Строка 76:
после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
-
#define a P@iter_begin
+
#define begin P@iter_begin
-
#define b P@iter_end
+
#define end P@iter_end
-
#define c ...@C_send_req
+
#define R ...@C_send_req
-
#define d ...@D_send_ack
+
#define S ...@D_send_ack
-
 
+
-
[]( a -> ( (c -> (!b U d)) U b) )
+
-
[]( (a & !b & <>b) -> ( (c -> (!b U d)) U b) ) // добавили то, что a и b не могут быть одновременно и то, что b когда-либо наступит
+
[]((begin) -> [](R -> (!end U (S && !end))))
-
[]( (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 ===
=== Задача 2 ===
-
После события a и до наступления события b событие c наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)
+
После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)
-
[]( a -> ((c -> c U (!c U b)) U b) )
 
-
[]( (a & !b & <>b) -> ((c -> c U (!c U b)) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
+
'''1й вариант''':
 +
[] (p && !q -> !r W (q || (r W (q || !r W q))))
-
Teravisor: Та же самая ошибка, что и в задаче 1.
+
'''2й вариант''':
-
Мой вариант(Заменить в 2й формуле последний U на W и раскрыть с небольшой правкой условия !c U b):
+
<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>
-
[]( a && !b -> ( ((c -> c U (!c U b)) U b) || [](c -> c U ([](!c && !b))) ) )
+
ps. пояснение формулы:
 +
# до первого || — случай, когда q не факт, что произойдёт (после того, как произойдёт r, оно длится до тех пор, пока не прекратится)
 +
# после первого || — случай, когда q обязательно произойдет
 +
#* до второго || — r встречается 0 раз
 +
#* после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков)
=== Задача 3 ===
=== Задача 3 ===
Строка 125: Строка 106:
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).
-
#define a Start
+
<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 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 ===
=== Задача 4 ===
В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.
В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.
-
#define a START
+
[] (START & !END & <>END -> ( (!P U END)||((P -> (!END U S))U END) )
-
#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 ===
=== Задача 5 ===
Строка 154: Строка 119:
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'
-
#define a p@iter_begin
+
#define p_b p@iter_begin
-
#define b p@iter_end
+
#define p_e p@iter_end
-
#define c c!req
+
#define c_r c!req
-
#define d d?ack
+
#define d_a d?ack
-
[](a -> ( (!c U d) U b))
+
[]( (p_b && !p_e && <>p_e) -> ((!c_r U p_e) || (!c_r U d_a)) )
-
[]( (a & !b & <>b) -> ((!c U d) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
+
(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)
-
[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно и так
 
=== Задача 6 ===
=== Задача 6 ===
Строка 169: Строка 133:
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
-
#define a (state == enter)
+
#define s_e state == enter
-
#define b (state == leave)
+
#define s_l state == leave
-
#define c (с!req)
+
#define c_r c!req
-
#define d (в?ack)
+
#define d_a d?ack
-
[](a -> (c -> ((!b U d) U b))
+
[]( (s_e && !s_l && <>s_l) -> ((!s_l U c_r) -> (!s_l U d_a)) )
-
[]( (a & !b & <>b) -> (c -> (!b U (d & !b))) U b) ) // Добавили то, что a и b не могут происходить одновременно и аналогично d и b. Окончательный вариант.
+
(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)
=== Задача 7 ===
=== Задача 7 ===
Строка 182: Строка 146:
До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5'
До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5'
-
#define a p@iter_end
+
#define p_e p@iter_end
-
#define b x == 3
+
#define x_3 x == 3
-
#define c y == 5
+
#define y_5 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_e U x_3) -> (!p_e U y_5)
-
может быть избыточно, но должно быть правильно
+
-
[]((p_iter_begin & !p_iter_end & <>p_iter_end)->([]p_lock U p_iter_end))
+
-
Авварон:
+
(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)
-
#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.name/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
Разделы