ВПнМ, примеры задач/Задача 5
Материал из eSyr's wiki.
(→Задачи (инв-ные)) |
(→Задача 1) |
||
| Строка 29: | Строка 29: | ||
<math>\Box (\Diamond p \And p \rightarrow X \Diamond (g1 \rightarrow g2))</math> | <math>\Box (\Diamond p \And p \rightarrow X \Diamond (g1 \rightarrow g2))</math> | ||
(по-моему, в формуле вообще нету p_end. такого быть не должно.) | (по-моему, в формуле вообще нету p_end. такого быть не должно.) | ||
| + | |||
| + | me thinks so: | ||
| + | <math>\Box (pb \land \neg pe \to (g5 \land X g3 \land X \neg pe) W pe)</math> | ||
=== Задача 2 === | === Задача 2 === | ||
Версия 21:03, 11 сентября 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 p_begin (p@iter_begin) #define p_end (p@iter_end) #define global5 (g==5) #define global3 (g==3)
[](<>p_begin && p_begin -> X <> (global5 -> X global3 ))
TeX'ом:
(по-моему, в формуле вообще нету p_end. такого быть не должно.)
me thinks so:
Задача 2
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не более одного раза
#define state_leave (state==leave) #define p_sent (p@sent)
[](p_sent -> X (!p_sent U state_leave))
Задача 3
Между событиями 'значение глобальной переменной 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) )
Задача 4
После наступления события 'значение глобальной переменной state равно enter_critical' верно: событие 'процесс q находится на метке received' наступает ровно один раз
#define S "state == enter_critical" #define was_received Q@received
[](S -> (<>was_received && [](was_received -> X([]!was_received))))
Задача 5
До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не менее одного раза
#define R "state == leave" #define was_sent P@sent
([]!R) || (!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))))
Задача 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 раз, записано с помощью трёх вложенных циклов (описание промежутков)
Задача 3
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).
Задача 4
В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.
[] (START & !END & <>END -> ( (!P U END)||((P -> (!END U S))U END) )
Задача 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, сдано не Савенкову)
Задача 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)))) )
Задача 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, сдано не Савенкову)
Задача 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, сдано Савенкову)
Задача 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, сдано Савенкову)
Задача 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, сдано Савенкову)
Задача 11
До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
- define x3 (x == 3)
- define iter (p@iter_end)
([]!iter) || (!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)))
Задача 13
До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
- define leave (state == leave)
- define send (channel ! req)
(send U leave)||([]send)
//Задачи 11-13 были отправлены по почте, оценка 5. Решение задачи 12 - избыточно.
Вариант 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 ) ) )
Задача 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))
Задача 3
После наступления события 'значение глобальной переменной state равно enter' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
#define q state==enter #define p x==3 [](!q) | <>(q & <>P))
Вариант 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)) ) )
Задача 2
Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке unlock' наступает не менее одного раза
#define d (state==enter) #define e (state==leave) #define f p@unlock [] ( (d & (<>e) ) -> (!e U f) )
Задача 3
После наступления события 'значение глобальной переменной state равно enter_critical' верно: никогда не выполняется 'значение глобальной переменной state равно unlocked'
#define g (state==enter_critical) #define h (state==unlocked) [] ([]!g || (g -> []!h))
Вариант 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, сдано Коннову)
Задача 2
До наступления события 'значение глобальной переменной state равно leave_critical' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
- define S state = leave_critical
- define P p@lock
([]!S) || (!S U (P && !S))
(Источник: практикум, задание 4, вариант 32, сдано Коннову)
Задача 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, сдано Коннову)
