ВПнМ, примеры задач/Задача 5

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
(Задача 1 - доп. пояснение)
(Задача 2 - преобразована в TeX)
Строка 87: Строка 87:
=== Задача 2 ===
=== Задача 2 ===
-
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S
+
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).
-
[](Start && !End && <>End) -> (((!S U R) && !(S && R) && !End) || (!R U End))
+
<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>
=== Задача 3 ===
=== Задача 3 ===

Версия 20:30, 24 мая 2009

Содержание

Вариант 1

Задача 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'ом:

\Box (\Diamond p \And p \rightarrow X \Diamond (g1 \rightarrow g2))

(по-моему, в формуле вообще нету 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) )

Вариант 2

Задача 1

После наступления события 'значение глобальной переменной state равно enter_critical' верно: событие 'процесс q находится на метке received' наступает ровно один раз

#define S "state == enter_critical"
#define was_received Q@received
[](S -> (<>was_received && [](was_received -> X([]!was_received))))

Задача 2

До наступления события 'значение глобальной переменной state равно leave' верно: событие 'процесс p находится на метке sent' наступает не менее одного раза

#define R "state == leave"
#define was_sent P@sent
([]!R) || (!R U (was_sent && !R))


Задача 3

После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p находится на метке iter_end' верно: после события 'в канал c отправляется сообщение req' рано или поздно наступит событие 'из канала d принимается сообщение ack'

#define was_iter_begin P@iter_begin
#define was_iter_end P@iter_end
#define was_req ...@C_send_req
#define was_ack ...@D_send_ack
[]((was_iter_begin) -> [](was_req -> (!was_iter_end U (was_ack && !was_iter_end))))


Вариант 3

Задача 1

После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)

\Box \Biggl( p \rightarrow \biggl( \Bigl( r \rightarrow (\Box \text{r U !r}) \Bigr) \ || \ \Bigl( \text{(!r U q) } || \text{ (!q U (r U (!r U q)))} \Bigr) \biggr) \Biggr) 

ps. пояснение формулы:

  1. до первого || — случай, когда q не факт, что произойдёт (после того, как произойдёт r, оно длится до тех пор, пока не прекратится)
  2. после первого || — случай, когда q обязательно произойдет
    • до второго || — r встречается 0 раз
    • после второго || — r встречается 1 раз, записано с помощью трёх вложенных циклов (описание промежутков)

Задача 2

В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию).

\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) 

Задача 3

Пишите какие у вас задачи были.


Верификация программ на моделях


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин

Личные инструменты
Разделы