Редактирование: ВПнМ, примеры задач/Задача 5
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 32 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 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 | + | #define p_begin (p@iter_begin) |
- | #define | + | #define p_end (p@iter_end) |
- | #define | + | #define global5 (g==5) |
- | #define | + | #define global3 (g==3) |
- | []( | + | [](<>p_begin && p_begin -> X <> (global5 -> X global3 )) |
+ | |||
+ | 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 === | ||
Строка 33: | Строка 48: | ||
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза | До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза | ||
- | #define | + | #define state_leave (state==leave) |
- | #define | + | #define p_sent (p@sent) |
- | + | [](p_sent -> X (!p_sent U state_leave)) | |
+ | |||
+ | 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 === | ||
Строка 42: | Строка 68: | ||
Между событиями 'значение глобальной переменной 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 ( | + | #define c (state==locked) |
- | #define d ( | + | #define d (p@lock) |
- | + | <math>\Box ((a \and \neg b \and \Diamond b) \to (\neg c \ U (d \or b)))</math> | |
- | []( (a & !b & <>b) -> | + | al-indigo: |
+ | []((a & !b & <>b) -> (!d U (c | b))) | ||
- | []( | + | Авварон: |
+ | обозначения я беру по порядку в тексте (то есть с предыдущими вариантами C и D наоборот) | ||
+ | [](A->((!C U D) U B)) | ||
+ | отличия от al-indigo: | ||
+ | 1) в моем случае, если Б не выполнено, то будет False. Но, имхо модель подразумевает что Б всегда есть - без разницы (о5 же вопрос понимания текста) | ||
+ | 2) я решил забить на написание A & !B, тк тогда по хорошему аналогичные отрицания надо писать и внутри Until'ов и формула будет слишком громоздкой | ||
+ | 3) можно заменить внутренний Until на Weak Until - зависит от того, ожидаем ли мы выполнение D или нет | ||
+ | а так, оба варианта имхо правильны | ||
=== Задача 4 === | === Задача 4 === | ||
Строка 58: | Строка 100: | ||
событие 'процесс q находится на метке received' наступает ровно один раз | событие 'процесс q находится на метке received' наступает ровно один раз | ||
- | #define | + | #define S "state == enter_critical" |
- | #define | + | #define Q Q@received |
- | []( | + | [](S -> (<>Q && [](Q -> X([]!Q)))) |
- | + | al-indigo: | |
+ | меня мучают особые сомнения, но кажется, так? | ||
+ | !S | [](<>S -> (Q -> X([]!Q))) | ||
- | + | Авварон: | |
+ | Нет, оригинал был правильный. 2я формула вообще инвертированная по-моему + напрягает !S в начале | ||
+ | |||
+ | al-indigo: | ||
+ | !S в начале -- я имел в виду случай, когда state==enter_critical вообще не наступает. В самой формуле я, может, ошибся, но вообще я вот сейчас смотрю, и вроде, мне кажется, что правильно. Ну то есть так примерно: "Либо S не наступает никогда, либо, если S когда-нибудь наступает, то всегда выполняется то, что Q наступает, и если оно наступает, что начиная со следующего состояния всегда !Q". Или я не так это читаю? | ||
=== Задача 5 === | === Задача 5 === | ||
Строка 72: | Строка 120: | ||
событие 'процесс p находится на метке sent' наступает не менее одного раза | событие 'процесс p находится на метке sent' наступает не менее одного раза | ||
- | #define | + | #define R "state == leave" |
- | #define | + | #define was_sent P@sent |
- | ! | + | ([]!R) || (!R U (was_sent && !R)) |
- | ! | + | al-indigo: |
+ | Может, здесь не слабый антил всё-таки? | ||
+ | !R U (was_sent && !R) | ||
- | + | Авварон: | |
- | + | Имхо без разницы слабый или сильный. Оба варианта ок | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
== Задачи (инв-ные) == | == Задачи (инв-ные) == | ||
Строка 93: | Строка 138: | ||
после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack' | после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack' | ||
- | #define | + | #define begin P@iter_begin |
- | #define | + | #define end P@iter_end |
- | #define | + | #define R ...@C_send_req |
- | #define | + | #define S ...@D_send_ack |
- | []( | + | []((begin) -> [](R -> (!end U (S && !end)))) |
- | []( ( | + | al-indigo: |
+ | Тут явно какая-то херня с двумя последними #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. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого | ||
- | + | Авварон: | |
- | + | это задача про самолет в чистом виде:) | |
- | + | вариант al-indigo верный, только <>end не нужен - тк он есть всегда по условию, то Future(end) всегда true и ни на что не влияет | |
- | + | Ну и о5 же я бы не писал невозможность одновременности состояний (begin & !end - они несут мало смысла:) | |
- | + | ||
=== Задача 2 === | === Задача 2 === | ||
- | После события | + | После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию) |
- | []( a -> ((c -> c U (!c U b)) U b) ) | ||
- | + | '''1й вариант''': | |
+ | [] (p && !q -> !r W (q || (r W (q || !r W q)))) | ||
- | + | '''2й вариант''': | |
- | + | <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> | |
- | + | ps. пояснение формулы: | |
+ | # до первого || — случай, когда q не факт, что произойдёт (после того, как произойдёт r, оно длится до тех пор, пока не прекратится) | ||
+ | # после первого || — случай, когда q обязательно произойдет | ||
+ | #* до второго || — r встречается 0 раз | ||
+ | #* после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков) | ||
+ | |||
+ | al-indigo: | ||
+ | адский ад какой-то, я так ничего и не понял тут, надо будет завтра ещё подумать :( | ||
+ | |||
+ | Авварон: | ||
+ | имхо, задача нерешаема) так как свойства, инвариантные по прореживанию, не могут отличить - было одно событие или два (одно это прореживание двух). | ||
=== Задача 3 === | === Задача 3 === | ||
Строка 125: | Строка 187: | ||
В одной итерации вычисления между метками 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> | |
- | + | ||
- | + | ||
- | + | ||
- | []( | + | al-indigo: |
+ | Кажется, вариант выше тоже *почти* правильный (не хватает ещё пары внешних скобок, вроде), но какой-то перегруженный. Вот мой: | ||
+ | []((start & !end & <>end) -> (!S U (R | end))) //Precedence between | ||
- | + | Авварон: | |
- | + | первый вариант не верен, если не встретится R - будет верна правая часть дизъюнкции и на левую мы кладем => свойство того, что должно быть !S, тупо не проверяется (противоречие с тем, что оно не должно появляться до R). | |
- | + | al-indigo - нормально, но о5 же - почему есть проверка неодновременности start и end, но нет аналогичной у Until (они в принципе не нужны, но если мы захотим добавить что-нибудь эдакое, то добавить будет сложно из-за дизъюнкции). Мой вариант: (аналогичный, и как обычно без !End & <>End) | |
+ | [](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) ) | |
- | + | ||
- | + | ||
- | + | ||
- | []( | + | al-indigo: |
+ | Хорошая тренировка -- найдите отличия (они есть). Единственное что -- странно, но случай, когда P не случается выглядит уместным (в решении выше), а у меня его нет -- в паттерне написано, как у меня. Кто-нибудь, прокомментируйте? Или из этого не следует, что P обязательно произойдёт? | ||
+ | [] ((Start & !End & <>End) -> (P -> (!End U (S & !End) U End)) | ||
- | []( ( | + | Авварон: |
+ | первый вариант верный, но там не нужна дизъюнкция вообще (вариант !P включается в P -> BLA ибо -> это !P || BLA) | ||
+ | al-indigo, ты накосячил со скобками, надо | ||
+ | [] ((Start & !End & <>End) -> ( {P -> (!End U (S & !End))} U End) | ||
+ | Из-за скобок и коммент неверный - в этом варианте !P подходит | ||
- | + | al-indigo: | |
+ | и правда накосячил. Чёрт возьми, как же на пересдаче-то не ошибиться :( | ||
=== Задача 5 === | === Задача 5 === | ||
Строка 154: | Строка 220: | ||
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack' | Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack' | ||
- | #define | + | #define p_b p@iter_begin |
- | #define | + | #define p_e p@iter_end |
- | #define | + | #define c_r c!req |
- | #define | + | #define d_a d?ack |
- | []( | + | []( (p_b && !p_e && <>p_e) -> ((!c_r U p_e) || (!c_r U d_a)) ) |
- | + | (Источник: практикум, задание 4, вариант 117, сдано не Савенкову) | |
- | []( ( | + | 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: | Строка 245: | ||
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack' | Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack' | ||
- | #define | + | #define s_e state == enter |
- | #define | + | #define s_l state == leave |
- | #define c | + | #define c_r c!req |
- | #define d | + | #define d_a d?ack |
- | []( | + | []( (s_e && !s_l && <>s_l) -> ((!s_l U c_r) -> (!s_l U d_a)) ) |
- | + | (Источник: практикум, задание 4, вариант 117, сдано не Савенкову) | |
- | + | 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 | + | al-indigo: |
- | #define | + | Это дублирование задачи один, повторюсь, чтобы можно было сравнить и понять, что всё-таки правильно. Кажется, первые два варината неправильные вообще. |
- | #define | + | И тут опять херня с #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. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого | ||
- | ( | + | Авварон: |
+ | прямые обозначения: | ||
+ | #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 === | |
- | + | До наступления события 'процесс p находится на метке iter_end' верно: после события 'значение глобальной переменной x равно 3' рано или поздно наступит событие 'значение глобальной переменной y равно 5' | |
- | + | #define p_e p@iter_end | |
+ | #define x_3 x == 3 | ||
+ | #define y_5 y == 5 | ||
- | ! | + | (!p_e U x_3) -> (!p_e U y_5) |
- | + | (Источник: практикум, задание 4, вариант 117, сдано не Савенкову) | |
- | ! | + | 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) //мой вариант, просто рассуждения | ||
- | + | Авварон: | |
+ | первое хрень (оно ОЧЕНЬ похоже на правду, но я не могу доказать что она не верна. Препод похоже тоже не смог:)), 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: | Строка 309: | ||
После наступления события 'значение глобальной переменной state равно enter_critical' верно: всегда выполняется 'процесс p находится на метке unlock' | После наступления события 'значение глобальной переменной state равно enter_critical' верно: всегда выполняется 'процесс p находится на метке unlock' | ||
- | + | Решение. | |
- | + | ||
- | []( | + | формально: |
+ | #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: | Строка 333: | ||
До наступления события 'значение глобальной переменной state равно leave_critical' верно: всегда выполняется 'значение глобальной переменной x равно 3' | До наступления события 'значение глобальной переменной state равно leave_critical' верно: всегда выполняется 'значение глобальной переменной x равно 3' | ||
- | + | Решение. | |
- | + | формально: | |
+ | #define p 'значение глобальной переменной state равно leave_critical' | ||
+ | #define q 'значение глобальной переменной x равно 3' | ||
- | ( | + | спин: |
+ | #define p (state == leave_critical) | ||
+ | #define q (x == 3) | ||
- | ( | + | ( <> p -> ( q U p ) ) || [] q |
- | + | (Источник: практикум, задание 4, вариант 24, сдано Савенкову) | |
- | + | al-indigo: | |
+ | ok? | ||
- | + | Авварон: | |
+ | Да, ок, но я бы написал тут и "простой" вариант: | ||
+ | q W p | ||
=== Задача 10 === | === Задача 10 === | ||
Строка 233: | Строка 358: | ||
верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received' | верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received' | ||
- | + | Решение. | |
- | + | формально: | |
- | + | #define a 'значение глобальной переменной state равно enter_critical' | |
- | + | #define b 'значение глобальной переменной state равно leave_critical' | |
+ | #define p 'процесс p находится на метке sent' | ||
+ | #define q 'процесс q находится на метке received' | ||
- | + | спин: | |
+ | #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) ) ) | |
+ | |||
+ | (Источник: практикум, задание 4, вариант 24, сдано Савенкову) | ||
+ | |||
+ | al-indigo: | ||
+ | Здесь какая-то неточность, непонятно, насколько существенная. В первой подформуле точняк должно быть ещё <>b, а его там нет. | ||
=== Задача 11 === | === Задача 11 === | ||
Строка 246: | Строка 382: | ||
До наступления события 'процесс 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: | Строка 397: | ||
Между событиями 'значение глобальной переменной 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: | Строка 411: | ||
До наступления события 'значение глобальной переменной 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: | Строка 426: | ||
Между событиями 'процесс 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 === | ||
Строка 322: | Строка 490: | ||
Фиг знает, что тут происходит, но мне кажется, что правильно будет так: | Фиг знает, что тут происходит, но мне кажется, что правильно будет так: | ||
[](( a & !b & <>b ) -> (!b U (c -> [](!c)))) | [](( 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==== | ====Задача 2==== | ||
Строка 342: | Строка 502: | ||
Пропущено, что 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==== | ||
Строка 359: | Строка 512: | ||
al-indigo: | al-indigo: | ||
ok? | ok? | ||
- | |||
- | Авварон: | ||
- | Похоже на правду, но я бы писал так (используя шаблон из 8й лекции на стр 56): | ||
- | #define A (state==enter_critical) | ||
- | #define B (state==unlocked) | ||
- | [](A -> []!B) | ||
- | По идее будет то же самое после преобразований | ||
=== Вариант 32 === | === Вариант 32 === | ||
Строка 383: | Строка 529: | ||
По-моему, как-то уж очень избыточно | По-моему, как-то уж очень избыточно | ||
[]((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 ==== | ||
Строка 406: | Строка 544: | ||
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 ==== | ||
Строка 432: | Строка 561: | ||
al-indigo: | al-indigo: | ||
<>A -> (!B U (C | A)) | <>A -> (!B U (C | A)) | ||
- | |||
- | Авварон: | ||
- | согласен | ||
- | малый фикс: | ||
- | <>A -> (!B U C U A) | ||
- | в этом варианте проще добавить неодновременность, если преподу припрет изменить условие. Да, и <>A зависит от прочтения, тоже можно опустить (не факт что оно будет) | ||
===Вариант 29=== | ===Вариант 29=== | ||
Строка 454: | Строка 577: | ||
кажется, так | кажется, так | ||
[](!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==== | ||
Строка 475: | Строка 591: | ||
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==== | ||
Строка 500: | Строка 607: | ||
может быть избыточно, но должно быть правильно | может быть избыточно, но должно быть правильно | ||
[]((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) ) | ||
{{Курс ВПнМ}} | {{Курс ВПнМ}} |