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

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

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

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

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

Текущая версия Ваш текст
Строка 2: Строка 2:
== Как решать эти задачи? ==
== Как решать эти задачи? ==
Для решения этих задач '''обязательно''' знать '''[[ВПнМ/Теормин#.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: Строка 11:
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)
 +
== Задачи (не инв-ные) ==
== Задачи (не инв-ные) ==
Строка 24: Строка 22:
#define a (p@iter_begin)
#define a (p@iter_begin)
#define b (p@iter_end)
#define b (p@iter_end)
-
#define c (y==5)
+
#define c (g==5)
-
#define d (x==3)
+
#define d (g==3)
[](a & !b -> (c & Xd & X !b) W b)
[](a & !b -> (c & Xd & X !b) W b)
Строка 78: Строка 76:
!a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта
!a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта
- 
-
UPD: (b && !b) всегда false. Если наступление события означает, что условие стало верным, то ответ
 
- 
-
!a W b
 
- 
-
Если наступление события означает, что условие побыло истинным, а потом стало ложным, то ответ
 
- 
-
!a W (b && X!b)
 
== Задачи (инв-ные) ==
== Задачи (инв-ные) ==
Строка 103: Строка 93:
[]( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) ) // добавили то, что b не происходит одновременно с d. Окончательный вариант.
[]( (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 ===
Строка 114: Строка 100:
[]( (a & !b & <>b) -> ((c -> c U (!c U b)) U b) ) // добавили то, что a и b не происходят одновременно и то, что 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 ===
=== Задача 3 ===
Строка 154: Строка 134:
Между событиями 'процесс 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)) ) // можно и так
+
al-indigo:
 +
//абсолютно то же самое, шаблон 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 ===
Строка 169: Строка 159:
Между событиями 'значение глобальной переменной 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 ===
+
upd: скорее всего, это решение неправильное. Варианты, скорее всего правильные:
 +
[]((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'
 
-
#define a p@iter_end
+
al-indigo:
-
#define b x == 3
+
Это дублирование задачи один, повторюсь, чтобы можно было сравнить и понять, что всё-таки правильно. Кажется, первые два варината неправильные вообще.
-
#define c y == 5
+
И тут опять херня с #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. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого
-
(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)
-
<>a ->( (b -> (!a U (c & !a))) U a ) // Добавили то, что a когда-либо произойдет, и то, что c и a не происходят одновременно. Окончательный вариант.
+
=== Задача 7 ===
-
(!a U b) -> (!a U c) // Потомкам: доказать что эта формула верна или нет:)
+
До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5'
-
Teravisor: Потомки доказывают: третья не верная. Мы смотрим обе импликации(->) из начальной точки, т.е. нам подойдет
+
#define p_e p@iter_end
 +
#define x_3 x == 3
 +
#define y_5 y == 5
-
!a !a !a !a !a !a a
+
(!p_e U x_3) -> (!p_e U y_5)
-
!b !b !b !b !b b b
+
(Источник: практикум, задание 4, вариант 117, сдано не Савенкову)
-
!c c c c c c c
+
al-indigo:
 +
<>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 ===
Строка 206: Строка 223:
После наступления события 'значение глобальной переменной 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 ===
Строка 215: Строка 247:
До наступления события 'значение глобальной переменной 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)
-
(b U a) // Можно так.
+
( <> p -> ( q U p ) ) || [] q
-
<>a -> (b U a) // Или так.
+
(Источник: практикум, задание 4, вариант 24, сдано Савенкову)
-
Потомкам: понять разницу:)
+
al-indigo:
 +
ok?
-
Teravisor: потомки говорят, между 2 и 3 формулами разницы нету. Объяснение: U требует выполнимости где-то второго аргумента, в данном случае "a", в случае если его нет, формула не выполняется. требование <>a-> может быть расценено лектором как избыточное, и вообщем то не хорошо. Вообще говоря вроде первая формула правильная, в отличие от последних двух, но и правильность последних можно доказать из утверждения "я так понял задание".
+
Авварон:
 +
Да, ок, но я бы написал тут и "простой" вариант:
 +
q W p
=== Задача 10 ===
=== Задача 10 ===
Строка 233: Строка 272:
верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received'
верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received'
-
#define a (state == enter_critical)
+
Решение.
-
#define b (state == leave_critical)
+
формально:
-
#define c p@sent
+
#define a 'значение глобальной переменной state равно enter_critical'
-
#define d q@received
+
#define b 'значение глобальной переменной state равно leave_critical'
 +
#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
-
Teravisor: то, же что и в задании 1. Комментарий это не можно, а нужно. И заменой U b на W b не всё исправится - надо еще <>b убрать вначале.
+
[]( ( a && !b ) -> ( ( ( p -> (!b U q) ) U b ) || [](p -> (!b U q) ) )
 +
 
 +
(Источник: практикум, задание 4, вариант 24, сдано Савенкову)
 +
 
 +
al-indigo:
 +
Здесь какая-то неточность, непонятно, насколько существенная. В первой подформуле точняк должно быть ещё <>b, а его там нет.
=== Задача 11 ===
=== Задача 11 ===
Строка 246: Строка 296:
До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
-
#define a (p@iter_end)
+
#define x3 (x == 3)
-
#define b (x == 3)
+
#define iter (p@iter_end)
-
!a W (b && !a) // В принципе, тут можно сильный Until поставить.
+
([]!iter) || (!iter U (x3 && !iter))
-
([]!a) || (!a U (b && !a)) // Расписан слабый Until
+
Есть подозрение, что первая скобка не нужна, т.к. во второй тоже не гарантируется наступление "итер", но она полностью описывает условие.
 +
 
 +
al-indigo:
 +
А тут нужно учитывать, что iter_end может не наступить? Мне кажется, оно по условию всегда должно происходить в какой-то момент. И да -- само-то решение является правильным?
 +
!iter U (x3 && !iter)
=== Задача 12 ===
=== Задача 12 ===
Строка 257: Строка 311:
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
-
#define a (state == enter)
 
-
#define b (state == leave)
 
-
#define c (x == 3)
 
-
[]( a -> (!b U c) ) // "Простой" вариант.
+
#define ent (state == enter)
 +
#define leave (state == leave)
 +
#define x3 (x == 3)
-
[]( (a && !b && <>b) -> (!b U (c && !b)) ) // Окончательный.
+
[]((ent && <>leave && !leave) -> (!leave U (x3 && !leave)))
 +
 
 +
al-indigo:
 +
не понимаю, что тут избыточного в решении, по-моему, самое то?
=== Задача 13 ===
=== Задача 13 ===
Строка 269: Строка 325:
До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
-
#define a (state == leave)
+
#define leave (state == leave)
-
#define b (channel ! req)
+
#define send (channel ! req)
-
b W a
+
(send U leave)||([]send)
-
[]b || (b U a) // Расписан Weak.
+
//Задачи 11-13 были отправлены по почте, оценка 5. Решение задачи 12 - избыточно.
 +
 
 +
al-indigo:
 +
красивое, понятное и наверное правильное решение :)
=== Вариант 110 ===
=== Вариант 110 ===
Строка 281: Строка 340:
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
-
#define a p@iter_begin
+
#define f_b p@iter_begin
-
#define b p@iter_end
+
#define f_e p@iter_end
-
#define c p@lock
+
#define f_lock p@lock
 +
[]( (f_b & !f_e && <>f_e) -> ( !f_e U ( f_lock & !f_e ) ) )
-
[](a -> !b U c)
+
al-indigo:
 +
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 a state==enter
+
#define f_b state==enter
-
#define b state==leave
+
#define f_e state==leave
-
#define c p@lock
+
#define f_lock p@lock
 +
[]((f_b && !f_e && <>f_e) -> (f_lock U f_e))
-
[](a -> (c U b))
+
al-indigo:
 +
Может, избыточно, но кажется, так правильнее:
 +
[]((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 a state==enter
+
#define q state==enter
-
#define b x==3
+
#define p x==3
 +
[](!q) | <>(q & <>P))
-
[](a -> <>b)
+
al-indigo:
 +
ok?
-
[](!a) | <>(a & <>b)) // Потомкам: проверить правильность.
+
Авварон:
 +
#define A state==enter
 +
#define B x==3
 +
[](A -> <>B)
 +
я бы написал так, а то что сверху имхо будет если развернуть импликацию. Могу ошибаться в своем варианте
=== Вариант 104 ===
=== Вариант 104 ===
Строка 383: Строка 465:
По-моему, как-то уж очень избыточно
По-моему, как-то уж очень избыточно
[]((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)
 
Авварон:
Авварон:
Строка 475: Строка 555:
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)
 
Авварон:
Авварон:

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

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

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