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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: === Задача 1 === После события 'процесс p находится на метке iter_begin' и до наступления события 'процесс p нах...)
Строка 34: Строка 34:
[]( state_enter -> X((!p_lock U state_leave) || (<>p_lock && !p_lock U state_locked) )
[]( state_enter -> X((!p_lock U state_leave) || (<>p_lock && !p_lock U state_locked) )
 +
 +
{{Курс ВПнМ}}

Версия 19:31, 21 мая 2009

Задача 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 ))


Задача 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) )


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


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 | Теормин

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