Редактирование: ВПнМ, примеры задач/Задача 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 ( | + | #define c (g==5) |
- | #define d ( | + | #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 === | ||
Строка 159: | Строка 139: | ||
#define d d?ack | #define d d?ack | ||
- | [](a -> ( (! | + | [](a -> ( (!d U c) U b)) |
- | []( (a & !b & <>b) -> ((! | + | []( (a & !b & <>b) -> ((!d U c) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет. |
- | []( (a & !b & <>b) -> (! | + | []( (a & !b & <>b) -> (!d U (c | b)) ) // можно и так |
=== Задача 6 === | === Задача 6 === | ||
Строка 191: | Строка 171: | ||
(!a U b) -> (!a U c) // Потомкам: доказать что эта формула верна или нет:) | (!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 === | === Задача 8 === | ||
Строка 225: | Строка 195: | ||
Потомкам: понять разницу:) | Потомкам: понять разницу:) | ||
- | |||
- | Teravisor: потомки говорят, между 2 и 3 формулами разницы нету. Объяснение: U требует выполнимости где-то второго аргумента, в данном случае "a", в случае если его нет, формула не выполняется. требование <>a-> может быть расценено лектором как избыточное, и вообщем то не хорошо. Вообще говоря вроде первая формула правильная, в отличие от последних двух, но и правильность последних можно доказать из утверждения "я так понял задание". | ||
=== Задача 10 === | === Задача 10 === | ||
Строка 239: | Строка 207: | ||
[]( (a & !b & <>b) -> ((c -> (!b U d)) U b) ) // Здесь U b можно заменить на W b (зависит от прочтения задачи) | []( (a & !b & <>b) -> ((c -> (!b U d)) U b) ) // Здесь U b можно заменить на W b (зависит от прочтения задачи) | ||
- | |||
- | Teravisor: то, же что и в задании 1. Комментарий это не можно, а нужно. И заменой U b на W b не всё исправится - надо еще <>b убрать вначале. | ||
=== Задача 11 === | === Задача 11 === | ||
Строка 246: | Строка 212: | ||
До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза | До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза | ||
- | + | #define x3 (x == 3) | |
- | + | #define iter (p@iter_end) | |
- | ! | + | ([]!iter) || (!iter U (x3 && !iter)) |
- | + | Есть подозрение, что первая скобка не нужна, т.к. во второй тоже не гарантируется наступление "итер", но она полностью описывает условие. | |
+ | |||
+ | al-indigo: | ||
+ | А тут нужно учитывать, что iter_end может не наступить? Мне кажется, оно по условию всегда должно происходить в какой-то момент. И да -- само-то решение является правильным? | ||
+ | !iter U (x3 && !iter) | ||
=== Задача 12 === | === Задача 12 === | ||
Строка 257: | Строка 227: | ||
Между событиями 'значение глобальной переменной 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) | |
+ | #define leave (state == leave) | ||
+ | #define x3 (x == 3) | ||
- | []( ( | + | []((ent && <>leave && !leave) -> (!leave U (x3 && !leave))) |
+ | |||
+ | al-indigo: | ||
+ | не понимаю, что тут избыточного в решении, по-моему, самое то? | ||
=== Задача 13 === | === Задача 13 === | ||
Строка 269: | Строка 241: | ||
До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req' | До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req' | ||
- | + | #define leave (state == leave) | |
- | + | #define send (channel ! req) | |
- | + | (send U leave)||([]send) | |
- | + | //Задачи 11-13 были отправлены по почте, оценка 5. Решение задачи 12 - избыточно. | |
+ | |||
+ | al-indigo: | ||
+ | красивое, понятное и наверное правильное решение :) | ||
=== Вариант 110 === | === Вариант 110 === | ||
Строка 281: | Строка 256: | ||
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза | Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза | ||
- | #define | + | #define f_b p@iter_begin |
- | #define | + | #define f_e p@iter_end |
- | #define | + | #define f_lock p@lock |
+ | []( (f_b & !f_e && <>f_e) -> ( !f_e U ( f_lock & !f_e ) ) ) | ||
- | + | al-indigo: | |
+ | ok? | ||
- | []( ( | + | Авварон: |
+ | ок | ||
+ | #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 | + | #define f_b state==enter |
- | #define | + | #define f_e state==leave |
- | #define | + | #define f_lock p@lock |
+ | []((f_b && !f_e && <>f_e) -> (f_lock U f_e)) | ||
- | []( | + | al-indigo: |
+ | Может, избыточно, но кажется, так правильнее: | ||
+ | []((f_b && !f_e && <>f_e) -> ([]f_lock U f_e)) | ||
- | []( ( | + | Авварон: |
+ | 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 | + | #define q state==enter |
- | #define | + | #define p x==3 |
+ | [](!q) | <>(q & <>P)) | ||
- | + | al-indigo: | |
+ | ok? | ||
- | []( | + | Авварон: |
+ | #define A state==enter | ||
+ | #define B x==3 | ||
+ | [](A -> <>B) | ||
+ | я бы написал так, а то что сверху имхо будет если развернуть импликацию. Могу ошибаться в своем варианте | ||
=== Вариант 104 === | === Вариант 104 === | ||
Строка 383: | Строка 381: | ||
По-моему, как-то уж очень избыточно | По-моему, как-то уж очень избыточно | ||
[]((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: | Строка 471: | ||
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) | ||
Авварон: | Авварон: |