Текущая версия |
Ваш текст |
Строка 1: |
Строка 1: |
- | <div style="float:right">__TOC__</div>
| + | == Вариант 1 == |
- | == Как решать эти задачи? == | + | |
- | Для решения этих задач '''обязательно''' знать '''[[ВПнМ/Теормин#.D0.9B.D0.BE.D0.B3.D0.B8.D0.BA.D0.B0_LTL._.D0.A1.D0.B8.D0.BD.D1.82.D0.B0.D0.BA.D1.81.D0.B8.D1.81_LTL._.D0.A1.D0.B5.D0.BC.D0.B0.D0.BD.D1.82.D0.B8.D0.BA.D0.B0_.D0.B2.D1.8B.D0.BF.D0.BE.D0.BB.D0.BD.D0.B8.D0.BC.D0.BE.D1.81.D1.82.D0.B8_.D1.84.D0.BE.D1.80.D0.BC.D1.83.D0.BB._.D0.A1.D0.B8.D0.BB.D1.8C.D0.BD.D1.8B.D0.B9_.D0.B8_.D1.81.D0.BB.D0.B0.D0.B1.D1.8B.D0.B9_until.|определения]]''', а так же следующие '''[http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml шаблоны].'''
| + | |
- | | + | |
- | Полезна также ссылка из шаблонов на то, что означают различные области[http://patterns.projects.cis.ksu.edu/documentation/patterns/scopes.shtml].
| + | |
- | Обратите внимание на "между Q и R", т.е. "Between Q and R" и на "после Q до R", т.е. "After Q, until R"
| + | |
- | | + | |
- | Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
| + | |
- | | + | |
- | '''Инвариантная к прореживанию''' формула - это такая формула, результат вычисления которой не меняется от того, применяется прореживание или нет. '''Прореживание''' - это сужение нескольких состояний до одного (а м.б. и расширение одного до нескольких - доподлинно неизвестно).
| + | |
- | | + | |
- | Будьте готовы к тому, что вам скажут, что в формуле '''применять слабый until нельзя''', поэтому здесь следующие форм-лы экв-ти:
| + | |
- | p W q = ([]p) | (p U q)
| + | |
- | p W q = <>(!p) -> (p U q)
| + | |
- | p W q = p U (q | []p)
| + | |
- | | + | |
- | == Задачи (не инв-ные) ==
| + | |
- | Втаких задачах можно спокойно применять оператор Next (X).
| + | |
| | | |
| === Задача 1 === | | === Задача 1 === |
Строка 22: |
Строка 5: |
| После события 'процесс 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) |
| + | |
| + | [](<>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. такого быть не должно.) |
| | | |
| === Задача 2 === | | === Задача 2 === |
Строка 33: |
Строка 20: |
| До наступления события 'значение глобальной переменной 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: |
Строка 29: |
| Между событиями 'значение глобальной переменной 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) )
| + | == Вариант 2 == |
| | | |
- | []( (a & !b & <>b) -> (!c U (d | b)) ) // можно объединить d и b - c не наступит, пока не наступит один из них
| + | === Задача 1 === |
- | | + | |
- | === Задача 4 === | + | |
| | | |
| После наступления события 'значение глобальной переменной state равно enter_critical' верно: | | После наступления события 'значение глобальной переменной state равно enter_critical' верно: |
| событие 'процесс 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)))) |
| | | |
- | Если в условие задачи добавить инвариантность к прореживанию, то решение будет выглядеть так:
| + | === Задача 2 === |
- | | + | |
- | []( a -> ( <>b && [](b -> (b U []!b)) ) )
| + | |
- | | + | |
- | === Задача 5 === | + | |
| | | |
| До наступления события 'значение глобальной переменной state равно leave' верно: | | До наступления события 'значение глобальной переменной state равно leave' верно: |
| событие 'процесс 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. Если наступление события означает, что условие стало верным, то ответ
| + | === Задача 3 === |
- | | + | |
- | !a W b
| + | |
- | | + | |
- | Если наступление события означает, что условие побыло истинным, а потом стало ложным, то ответ
| + | |
- | | + | |
- | !a W (b && X!b)
| + | |
- | | + | |
- | == Задачи (инв-ные) ==
| + | |
- | === Задача 1 === | + | |
| | | |
| После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: | | После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: |
| после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack' | | после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack' |
| | | |
- | #define a P@iter_begin | + | #define was_iter_begin P@iter_begin |
- | #define b P@iter_end | + | #define was_iter_end P@iter_end |
- | #define c ...@C_send_req | + | #define was_req ...@C_send_req |
- | #define d ...@D_send_ack | + | #define was_ack ...@D_send_ack |
| | | |
- | []( a -> ( (c -> (!b U d)) U b) ) | + | []((was_iter_begin) -> [](was_req -> (!was_iter_end U (was_ack && !was_iter_end)))) |
| | | |
- | []( (a & !b & <>b) -> ( (c -> (!b U d)) U b) ) // добавили то, что a и b не могут быть одновременно и то, что b когда-либо наступит | |
| | | |
- | []( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) ) // добавили то, что b не происходит одновременно с d. Окончательный вариант.
| + | == Вариант 3 == |
| | | |
- | Teravisor:
| + | === Задача 1 === |
- | Все три три не верны потому, что формулировка "после ... до ..." подразумевает, что второе событие может не произойти.
| + | После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию) |
- | Моя версия(шаблон S responds to P After Q until R, раскрытие W): [](a && !b -> ( ((p -> (!b U (q && !b ))) U b) || ([](p -> (!b U (q && !b ))) )
| + | |
| | | |
- | === Задача 2 ===
| + | <math>\Box</math> |
- | После события a и до наступления события b событие c наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)
| + | |
| | | |
- | []( a -> ((c -> c U (!c U b)) U b) )
| + | === Задача 4 === |
| | | |
- | []( (a & !b & <>b) -> ((c -> c U (!c U b)) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
| + | В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S |
| | | |
- | | + | <math>[](Start && !End && <>End) -> (((!S U R) && !(S && R) && !End) || (!R U End))</math> |
- | 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 === |
- | | + | Пишите какие у вас задачи были. |
- | В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).
| + | |
- | | + | |
- | #define a Start
| + | |
- | #define b End
| + | |
- | #define c R
| + | |
- | #define d S
| + | |
- | | + | |
- | [](a -> ( (!d U c) U b ))
| + | |
- | | + | |
- | []( (a & !b & <>b) -> ( (!d U c) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет
| + | |
- | | + | |
- | []( (a & !b & <>b) -> ( !d U (c | b)) ) // можно и так
| + | |
- | | + | |
- | === Задача 4 ===
| + | |
- | В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.
| + | |
- | | + | |
- | #define a START
| + | |
- | #define b END
| + | |
- | #define c x==1
| + | |
- | #define d S
| + | |
- | | + | |
- | [](a -> ( (c -> (!b U d)) U b)
| + | |
- | | + | |
- | []( (a & !b & <>b) -> ( (c -> (!b U d)) U b) // добавили то, что a и b не происходят одновременно и что b когда-либо произойдет
| + | |
- | | + | |
- | []( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) // добавили то, что b и d не происходят одновременно. Окончательный вариант.
| + | |
- | | + | |
- | === Задача 5 ===
| + | |
- | | + | |
- | Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'
| + | |
- | | + | |
- | #define a p@iter_begin
| + | |
- | #define b p@iter_end
| + | |
- | #define c c!req
| + | |
- | #define d d?ack
| + | |
- | | + | |
- | [](a -> ( (!c U d) U b))
| + | |
- | | + | |
- | []( (a & !b & <>b) -> ((!c U d) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
| + | |
- | | + | |
- | []( (a & !b & <>b) -> (!c U (d | b)) ) // можно и так
| + | |
- | | + | |
- | === Задача 6 ===
| + | |
- | | + | |
- | Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
| + | |
- | | + | |
- | #define a (state == enter)
| + | |
- | #define b (state == leave)
| + | |
- | #define c (с!req)
| + | |
- | #define d (в?ack)
| + | |
- | | + | |
- | [](a -> (c -> ((!b U d) U b))
| + | |
- | | + | |
- | []( (a & !b & <>b) -> (c -> (!b U (d & !b))) U b) ) // Добавили то, что a и b не могут происходить одновременно и аналогично d и b. Окончательный вариант.
| + | |
- | | + | |
- | === Задача 7 ===
| + | |
- | | + | |
- | До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5'
| + | |
- | | + | |
- | #define a p@iter_end
| + | |
- | #define b x == 3
| + | |
- | #define c y == 5
| + | |
- | | + | |
- | (b -> (!a U c)) U a
| + | |
- | | + | |
- | <>a ->( (b -> (!a U (c & !a))) U a ) // Добавили то, что a когда-либо произойдет, и то, что c и a не происходят одновременно. Окончательный вариант.
| + | |
- | | + | |
- | (!a U b) -> (!a U c) // Потомкам: доказать что эта формула верна или нет:)
| + | |
- | | + | |
- | Teravisor: Потомки доказывают: третья не верная. Мы смотрим обе импликации(->) из начальной точки, т.е. нам подойдет
| + | |
- | | + | |
- | !a !a !a !a !a !a a
| + | |
- | | + | |
- | !b !b !b !b !b b b
| + | |
- | | + | |
- | !c c c c c c c
| + | |
- | | + | |
- | !a U c выполняется. => формула true, хотя условию не удовлетворяет. Если поставить [] перед всей формулой правильность не изменится. Кто хочет может сам доказать.
| + | |
- | | + | |
- | === Задача 8 ===
| + | |
- | | + | |
- | После наступления события 'значение глобальной переменной state равно enter_critical' верно: всегда выполняется 'процесс p находится на метке unlock'
| + | |
- | | + | |
- | #define a (state == enter_critical)
| + | |
- | #define b p@unlock
| + | |
- | | + | |
- | [](a -> []b)
| + | |
- | | + | |
- | === Задача 9 ===
| + | |
- | | + | |
- | До наступления события 'значение глобальной переменной state равно leave_critical' верно: всегда выполняется 'значение глобальной переменной x равно 3'
| + | |
- | | + | |
- | #define a (state == leave_critical)
| + | |
- | #define b (x == 3)
| + | |
- | | + | |
- | (b W a) // []b || (b U a) - Тоже самое, но через сильный Until.
| + | |
- | | + | |
- | (b U a) // Можно так.
| + | |
- | | + | |
- | <>a -> (b U a) // Или так.
| + | |
- | | + | |
- | Потомкам: понять разницу:)
| + | |
- | | + | |
- | Teravisor: потомки говорят, между 2 и 3 формулами разницы нету. Объяснение: U требует выполнимости где-то второго аргумента, в данном случае "a", в случае если его нет, формула не выполняется. требование <>a-> может быть расценено лектором как избыточное, и вообщем то не хорошо. Вообще говоря вроде первая формула правильная, в отличие от последних двух, но и правильность последних можно доказать из утверждения "я так понял задание".
| + | |
- | | + | |
- | === Задача 10 ===
| + | |
- | | + | |
- | После события 'значение глобальной переменной state равно enter_critical' и до наступления события 'значение глобальной переменной state равно leave_critical'
| + | |
- | верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received'
| + | |
- | | + | |
- | #define a (state == enter_critical)
| + | |
- | #define b (state == leave_critical)
| + | |
- | #define c p@sent
| + | |
- | #define d q@received
| + | |
- | | + | |
- | []( (a & !b & <>b) -> ((c -> (!b U d)) U b) ) // Здесь U b можно заменить на W b (зависит от прочтения задачи)
| + | |
- | | + | |
- | Teravisor: то, же что и в задании 1. Комментарий это не можно, а нужно. И заменой U b на W b не всё исправится - надо еще <>b убрать вначале.
| + | |
- | | + | |
- | === Задача 11 ===
| + | |
- | | + | |
- | До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
| + | |
- | | + | |
- | #define a (p@iter_end)
| + | |
- | #define b (x == 3)
| + | |
- | | + | |
- | !a W (b && !a) // В принципе, тут можно сильный Until поставить.
| + | |
- | | + | |
- | ([]!a) || (!a U (b && !a)) // Расписан слабый Until
| + | |
- | | + | |
- | === Задача 12 ===
| + | |
- | | + | |
- | Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
| + | |
- | | + | |
- | #define a (state == enter)
| + | |
- | #define b (state == leave)
| + | |
- | #define c (x == 3)
| + | |
- | | + | |
- | []( a -> (!b U c) ) // "Простой" вариант.
| + | |
- | | + | |
- | []( (a && !b && <>b) -> (!b U (c && !b)) ) // Окончательный.
| + | |
- | | + | |
- | === Задача 13 ===
| + | |
- | | + | |
- | До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
| + | |
- | | + | |
- | #define a (state == leave)
| + | |
- | #define b (channel ! req)
| + | |
- | | + | |
- | b W a
| + | |
- | | + | |
- | []b || (b U a) // Расписан Weak.
| + | |
- | | + | |
- | === Вариант 110 ===
| + | |
- | | + | |
- | ==== Задача 1 ====
| + | |
- | Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
| + | |
- | | + | |
- | #define a p@iter_begin
| + | |
- | #define b p@iter_end
| + | |
- | #define c p@lock
| + | |
- | | + | |
- | [](a -> !b U c)
| + | |
- | | + | |
- | []( (a & !b && <>b) -> (!b U (c & !b)) ) // Окончательный вариант.
| + | |
- | | + | |
- | ====Задача 2====
| + | |
- | Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: всегда выполняется 'процесс p находится на метке lock'
| + | |
- | | + | |
- | #define a state==enter
| + | |
- | #define b state==leave
| + | |
- | #define c p@lock
| + | |
- | | + | |
- | [](a -> (c U b))
| + | |
- | | + | |
- | []( (a && !b && <>b) -> (c U b) )
| + | |
- | | + | |
- | ====Задача 3====
| + | |
- | После наступления события 'значение глобальной переменной state равно enter' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
| + | |
- |
| + | |
- | #define a state==enter
| + | |
- | #define b x==3
| + | |
- | | + | |
- | [](a -> <>b)
| + | |
- | | + | |
- | [](!a) | <>(a & <>b)) // Потомкам: проверить правильность.
| + | |
- | | + | |
- | === Вариант 104 ===
| + | |
- | ==== Задача 1 ====
| + | |
- | После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: событие 'из канала d принимается сообщение ack' наступает ровно один раз
| + | |
- | | + | |
- | #define a p@iter_begin
| + | |
- | #define b p@iter_end
| + | |
- | #define c d?ack
| + | |
- | [] ( a -> ( <>b -> (!b&!c) U (c & !b U (!c & b) ) || []!b -> (!c U (c U !c)) ) )
| + | |
- | | + | |
- | al-indigo:
| + | |
- | Фиг знает, что тут происходит, но мне кажется, что правильно будет так:
| + | |
- | [](( a & !b & <>b ) -> (!b U (c -> [](!c))))
| + | |
- | | + | |
- | Авварон:
| + | |
- | без Х не решается => все что сверху - туфта
| + | |
- | с Х:
| + | |
- | #define A p@iter_begin
| + | |
- | #define B p@iter_end
| + | |
- | #define C d?ack
| + | |
- | []( A -> (C -> X (!C U B)) ) // туплю - не надо ли 2ю импликацию сделать также U B ? вроде нет
| + | |
- | | + | |
- | ====Задача 2====
| + | |
- | Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке unlock' наступает не менее одного раза
| + | |
- | | + | |
- | #define d (state==enter)
| + | |
- | #define e (state==leave)
| + | |
- | #define f p@unlock
| + | |
- | [] ( (d & (<>e) ) -> (!e U f) )
| + | |
- | | + | |
- | al-indigo:
| + | |
- | Пропущено, что d и e не совпадают:
| + | |
- | [] ( (d & (<>e) & !e ) -> (!e U f) )
| + | |
- | | + | |
- | Авварон:
| + | |
- | #define A (state==enter)
| + | |
- | #define B (state==leave)
| + | |
- | #define C p@unlock
| + | |
- | короткая: [](A -> (!B U C))
| + | |
- | длинная: []( (A & !B & <>B) -> (!B U C) )
| + | |
- | | + | |
- | ====Задача 3====
| + | |
- | После наступления события 'значение глобальной переменной state равно enter_critical' верно: никогда не выполняется 'значение глобальной переменной state равно unlocked'
| + | |
- | | + | |
- | #define g (state==enter_critical)
| + | |
- | #define h (state==unlocked)
| + | |
- | [] ([]!g || (g -> []!h))
| + | |
- | | + | |
- | al-indigo:
| + | |
- | ok?
| + | |
- | | + | |
- | Авварон:
| + | |
- | Похоже на правду, но я бы писал так (используя шаблон из 8й лекции на стр 56):
| + | |
- | #define A (state==enter_critical)
| + | |
- | #define B (state==unlocked)
| + | |
- | [](A -> []!B)
| + | |
- | По идее будет то же самое после преобразований
| + | |
- | | + | |
- | === Вариант 32 ===
| + | |
- | ==== Задача 1 ====
| + | |
- | | + | |
- | До наступления события 'значение глобальной переменной state равно leave_critical'
| + | |
- | верно: событие 'значение глобальной переменной x равно 3' наступает не более одного раза
| + | |
- | | + | |
- | #define S state == state_critical
| + | |
- | #define P x = 3
| + | |
- | | + | |
- | ((!P U (S || (P U (S || (!P U S))))) || ([] !S && ( [] ! P) || [] P || P U ([] ! P) || !P U ( P U ([] !P)) )
| + | |
- | | + | |
- | (Источник: практикум, задание 4, вариант 32, сдано Коннову)
| + | |
- | | + | |
- | al-indigo:
| + | |
- | По-моему, как-то уж очень избыточно
| + | |
- | []((P & !S & <>S) -> (!P U S))
| + | |
- | | + | |
- | []((P & !S & <>S) -> (P U (!P U S))) ( поправил al-indigo: P->!P - всегда false)
| + | |
- | | + | |
- | Авварон:
| + | |
- | #define A state == state_critical
| + | |
- | #define B x = 3
| + | |
- | [](B -> B U !B U A)
| + | |
- | вроде так, проверьте)
| + | |
- | | + | |
- | ==== Задача 2 ====
| + | |
- | | + | |
- | До наступления события 'значение глобальной переменной state равно leave_critical'
| + | |
- | верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
| + | |
- | | + | |
- | #define S state = leave_critical
| + | |
- | #define P p@lock
| + | |
- | | + | |
- | ([]!S) || (!S U (P && !S))
| + | |
- | | + | |
- | (Источник: практикум, задание 4, вариант 32, сдано Коннову)
| + | |
- | | + | |
- | al-indigo:
| + | |
- | ок?
| + | |
- | | + | |
- | Авварон:
| + | |
- | ага, но я бы писал так:
| + | |
- | #define A state = leave_critical
| + | |
- | #define B p@lock
| + | |
- | через Weak, простая: !A W B
| + | |
- | через Weak, сложная: !A W (B & !A)
| + | |
- | через Until, сложная: []!A || (!A U (B & !A))
| + | |
- | Эти 3 ф-лы эквивалентны, но W имхо читать проще
| + | |
- | | + | |
- | ==== Задача 3 ====
| + | |
- | | + | |
- | До наступления события 'значение глобальной переменной state равно leave_critical'
| + | |
- | верно: если наступило событие 'в канал c отправляется сообщение req',
| + | |
- | то до него было событие 'из канала d принимается сообщение ack'
| + | |
- | | + | |
- | #define A state == leave_critical
| + | |
- | #define B c@req
| + | |
- | #define C d@ack
| + | |
- | | + | |
- | ((! B U A ) || ((!A && !B) U (C && (! A U B )))) || ( [] !B) || (!B U C)
| + | |
- | | + | |
- | (Источник: практикум, задание 4, вариант 32, сдано Коннову)
| + | |
- | | + | |
- | al-indigo:
| + | |
- | <>A -> (!B U (C | A))
| + | |
- | | + | |
- | Авварон:
| + | |
- | согласен
| + | |
- | малый фикс:
| + | |
- | <>A -> (!B U C U A)
| + | |
- | в этом варианте проще добавить неодновременность, если преподу припрет изменить условие. Да, и <>A зависит от прочтения, тоже можно опустить (не факт что оно будет)
| + | |
- | | + | |
- | ===Вариант 29===
| + | |
- | | + | |
- | ====Задача 1====
| + | |
- | | + | |
- | До наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной state равно unlocked'наступает событие 'процесс p находится на метке unlock' (полученное свойство не обязательно может быть инвариантным к прореживанию)
| + | |
- | | + | |
- | #define p_iter_end (p@iter_end)
| + | |
- | #define p_iter_unlock (p@iter_unlock)
| + | |
- | #define state (state=unlocked)
| + | |
- | | + | |
- | [](((state->X p_iter_unlocked) U p_iter_end))
| + | |
- | | + | |
- | al-indigo:
| + | |
- | кажется, так
| + | |
- | [](!p_iter_end U (p_iter_unlock -> X state))
| + | |
- | | + | |
- | Авварон:
| + | |
- | al-indigo у тебя условие слабее - хотя бы 1 раз будет выполнено условие (а это не имелось ввиду, поэтому так). Можно перефразировать "за каким-то B будет С" (но не за всеми!)
| + | |
- | #define A (p@iter_end)
| + | |
- | #define B (p@iter_unlock)
| + | |
- | #define C (state=unlocked)
| + | |
- | (B -> X C) U A
| + | |
- | | + | |
- | ====Задача 2====
| + | |
- | | + | |
- | Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно:событие 'в канал c отправляется сообщение req' наступает не более одного раза
| + | |
- | | + | |
- | #define p_iter_begin(p@iter_begin)
| + | |
- | #define p_iter_end((p@iter_end)
| + | |
- | #define c_S ...@C_send_req
| + | |
- | | + | |
- | | + | |
- | [](p_iter_begin -> !p_iter_end || (!p_iter_end U (c_S U (!c_S U p_iter_end ))))
| + | |
- | | + | |
- | al-indigo:
| + | |
- | []((p_iter_begin & !p_iter_end & <>p_iter_end) -> (req -> (![]req U p_iter_end)))
| + | |
- | | + | |
- | []((p_iter_begin & !p_iter_end & <>p_iter_end) -> (req -> (req U (!req U p_iter_end)))) (поправил al-indigo)
| + | |
- | | + | |
- | Авварон:
| + | |
- | о5 задача не решается без X
| + | |
- | #define A (p@iter_begin)
| + | |
- | #define B ((p@iter_end)
| + | |
- | #define C ...@C_send_req
| + | |
- | []( A -> { (C -> X[!C U B]) U B } )
| + | |
- | | + | |
- | ====Задача 3====
| + | |
- | | + | |
- | Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно:всегда выполняется 'процесс p находится на метке lock'
| + | |
- | | + | |
- | #define p_iter_begin(p@iter_begin)
| + | |
- | #define p_iter_end((p@iter_end)
| + | |
- | #define p_lock(p@lock)
| + | |
- | | + | |
- | [](p_iter_begin & !p_iter_end & <>p_iter_end)->(p_lock U p_iter_end)
| + | |
- | | + | |
- | Сдавал не Коннову
| + | |
- | | + | |
- | al-indigo:
| + | |
- | может быть избыточно, но должно быть правильно
| + | |
- | []((p_iter_begin & !p_iter_end & <>p_iter_end)->([]p_lock U p_iter_end))
| + | |
- | | + | |
- | Авварон:
| + | |
- | #define A (p@iter_begin)
| + | |
- | #define B ((p@iter_end)
| + | |
- | #define C (p@lock)
| + | |
- | простая: [](A -> (C U B))
| + | |
- | сложная: []( (A & !B & <>B) -> (C U B) )
| + | |
| | | |
| {{Курс ВПнМ}} | | {{Курс ВПнМ}} |