ВПнМ, примеры задач/Задача 5
Материал из eSyr's wiki.
(→Задача 3) |
(→Задача 3) |
||
| Строка 44: | Строка 44: | ||
#define c (p@lock) | #define c (p@lock) | ||
#define d (state==locked) | #define d (state==locked) | ||
| + | |||
[]( a -> ((!c U d) U b) ) // Этот вариант не учитывает то, что b не может быть одновременно с a, и то, что b когда-либо наступит | []( a -> ((!c U d) U b) ) // Этот вариант не учитывает то, что b не может быть одновременно с a, и то, что b когда-либо наступит | ||
| + | |||
[]( (a & !b & <>b) -> ((!c U d) U b) ) | []( (a & !b & <>b) -> ((!c U d) U b) ) | ||
| + | |||
[]( (a & !b & <>b) -> (!d U (c | b)) ) // можно объединить c и b - d не наступит, пока не наступит один из них | []( (a & !b & <>b) -> (!d U (c | b)) ) // можно объединить c и b - d не наступит, пока не наступит один из них | ||
Версия 17:08, 1 октября 2010
Содержание
|
Как решать эти задачи?
Для решения этих задач обязательно знать определения, а так же следующие шаблоны.
Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
Инвариантная к прореживанию формула - это такая формула, результат вычисления которой не меняется от того, применяется прореживание или нет. Прореживание - это сужение нескольких состояний до одного (а м.б. и расширение одного до нескольких - доподлинно неизвестно).
Будьте готовы к тому, что вам скажут, что в формуле применять слабый 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
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной y равно 5' наступает событие 'значение глобальной переменной x равно 3' (полученное свойство не обязательно может быть инвариантным к прореживанию)
#define a (p@iter_begin) #define b (p@iter_end) #define c (g==5) #define d (g==3)
[](a & !b -> (c & Xd & X !b) W b)
Задача 2
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза
#define a (state==leave) #define b (p@sent)
<>a -> ((b -> b & X (!b U a)) U a)
Задача 3
Между событиями 'значение глобальной переменной state равно enter_critical' и 'значение глобальной переменной state равно leave_critical' верно: если наступило событие 'процесс p находится на метке lock', то до него было событие 'значение глобальной переменной state равно locked'
#define a (state==enter_critical) #define b (state==leave_critical) #define c (p@lock) #define d (state==locked)
[]( a -> ((!c U d) U b) ) // Этот вариант не учитывает то, что b не может быть одновременно с a, и то, что b когда-либо наступит
[]( (a & !b & <>b) -> ((!c U d) U b) )
[]( (a & !b & <>b) -> (!d U (c | b)) ) // можно объединить c и b - d не наступит, пока не наступит один из них
Задача 4
После наступления события 'значение глобальной переменной state равно enter_critical' верно: событие 'процесс q находится на метке received' наступает ровно один раз
#define S "state == enter_critical" #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". Или я не так это читаю?
Авварон:
!S напрягло, ибо нет квантора времени. Если написать []!S, то этот случай будет включен в S-> у тебя формула проверяет ДО наступления S (ибо <>S возвращает True независимо от того, есть ли сейчас S (а от того, что оно будет). Это я подразумевал под инвертированностью. <> Надо убрать и думать дальше. Без <> импликация теряет свойство "продолжительности" - значит надо пофиксить это добавлением [] в правую ее часть. Плюс у тебя не учтено что Q наступит.
Итого:
#define A "state == enter_critical" #define B Q@received
[]( A -> ( <>B && [](B -> X[]!B) ) )
Задача 5
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не менее одного раза
#define R "state == leave" #define was_sent P@sent
([]!R) || (!R U (was_sent && !R))
al-indigo:
Может, здесь не слабый антил всё-таки? !R U (was_sent && !R)
Авварон: Имхо без разницы слабый или сильный. Оба варианта ок
Задачи (инв-ные)
Задача 1
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
#define begin P@iter_begin #define end P@iter_end #define R ...@C_send_req #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
После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)
1й вариант:
[] (p && !q -> !r W (q || (r W (q || !r W q))))
2й вариант:
ps. пояснение формулы:
- до первого || — случай, когда q не факт, что произойдёт (после того, как произойдёт r, оно длится до тех пор, пока не прекратится)
- после первого || — случай, когда q обязательно произойдет
- до второго || — r встречается 0 раз
- после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков)
al-indigo:
адский ад какой-то, я так ничего и не понял тут, надо будет завтра ещё подумать :(
Авварон:
Предполагаю такой вариант: []( A -> ((C -> C U (!C U B)) U B) )
Задача 3
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).
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
В ходе итерации, начинающейся меткой 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
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'
#define p_b p@iter_begin #define p_e p@iter_end #define c_r c!req #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
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
#define s_e state == enter #define s_l state == leave #define c_r c!req #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)))) )
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. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого
Авварон:
прямые обозначения: #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
После наступления события 'значение глобальной переменной 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
До наступления события 'значение глобальной переменной 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
После события 'значение глобальной переменной state равно enter_critical' и до наступления события 'значение глобальной переменной state равно leave_critical' верно: после события 'процесс 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
До наступления события 'процесс 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
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
- define ent (state == enter)
- define leave (state == leave)
- define x3 (x == 3)
[]((ent && <>leave && !leave) -> (!leave U (x3 && !leave)))
al-indigo:
не понимаю, что тут избыточного в решении, по-моему, самое то?
Задача 13
До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
- define leave (state == leave)
- define send (channel ! req)
(send U leave)||([]send)
//Задачи 11-13 были отправлены по почте, оценка 5. Решение задачи 12 - избыточно.
al-indigo:
красивое, понятное и наверное правильное решение :)
Вариант 110
Задача 1
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
#define f_b p@iter_begin #define f_e p@iter_end #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
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: всегда выполняется 'процесс p находится на метке lock'
#define f_b state==enter #define f_e state==leave #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
После наступления события 'значение глобальной переменной state равно enter' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
#define q state==enter #define p x==3 [](!q) | <>(q & <>P))
al-indigo:
ok?
Авварон:
#define A state==enter #define B x==3 [](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))
Авварон:
#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)))
Авварон:
о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) )
