ВПнМ, примеры задач/Задача 5
Материал из eSyr's wiki.
м (оформление + дополнение) |
м (→Задача 2 - добавлен шаблонный вариант) |
||
| Строка 88: | Строка 88: | ||
После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию) | После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию) | ||
| - | <math>\Box \Biggl( p \rightarrow \biggl( \Bigl( r \rightarrow ( | + | |
| + | '''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. пояснение формулы: | ps. пояснение формулы: | ||
| Строка 95: | Строка 101: | ||
#* до второго || — r встречается 0 раз | #* до второго || — r встречается 0 раз | ||
#* после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков) | #* после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков) | ||
| - | |||
=== Задача 3 === | === Задача 3 === | ||
Версия 16:23, 14 июня 2009
Содержание |
Как решать эти задачи?
Для решения этих задач обязательно знать определения, а так же следующие шаблоны.
Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
Инвариантная к прореживанию формула - это такая формула, результат вычисления которой не меняется от того, применяется прореживание или нет. Прореживание - это сужение нескольких состояний до одного (а м.б. и расширение одного до нескольких - доподлинно неизвестно).
Будьте готовы к тому, что вам скажут, что в формуле применять слабый 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. такого быть не должно.)
Задача 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
...
