ВПнМ, примеры задач/Задача 5
Материал из eSyr's wiki.
(→Задача 2) |
(→Задача 2) |
||
| Строка 37: | Строка 37: | ||
<>a -> ((b -> b & X (!b U a)) U a) | <>a -> ((b -> b & X (!b U a)) U a) | ||
| - | |||
| - | Формула выше означает, что событие b может продолжаться только в течение одного состояния. Я думаю, подразумевается, что событие может наступить и продолжаться. Опираясь на паттерн bounded existence: | ||
| - | |||
| - | <>a -> (!b & !a) U (a | ((b & !a) U (a | ((!b U a)))) | ||
=== Задача 3 === | === Задача 3 === | ||
Версия 14:35, 8 сентября 2011
Содержание
|
Как решать эти задачи?
Для решения этих задач обязательно знать определения, а так же следующие шаблоны.
Полезна также ссылка из шаблонов на то, что означают различные области[1]. Обратите внимание на "между 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
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной y равно 5' наступает событие 'значение глобальной переменной x равно 3' (полученное свойство не обязательно может быть инвариантным к прореживанию)
#define a (p@iter_begin) #define b (p@iter_end) #define c (y==5) #define d (x==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) -> (!c U (d | b)) ) // можно объединить d и b - c не наступит, пока не наступит один из них
Задача 4
После наступления события 'значение глобальной переменной state равно enter_critical' верно: событие 'процесс q находится на метке received' наступает ровно один раз
#define a "state == enter_critical" #define b Q@received
[]( a -> ( <>b && [](b -> X[]!b) ) )
Если в условие задачи добавить инвариантность к прореживанию, то решение будет выглядеть так:
[]( a -> ( <>b && [](b -> (b U []!b)) ) )
Задача 5
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не менее одного раза
#define a "state == leave" #define b P@sent
!a W (b && !b)
!a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта
Задачи (инв-ные)
Задача 1
После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'
#define a P@iter_begin #define b P@iter_end #define c ...@C_send_req #define d ...@D_send_ack
[]( 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. Окончательный вариант.
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
После события a и до наступления события b событие c наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)
[]( a -> ((c -> c U (!c U b)) U 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
В одной итерации вычисления между метками 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))
Авварон:
#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) )
