ВПнМ, примеры задач/Задача 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'ом:

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

(по-моему, в формуле вообще нету p_end. такого быть не должно.)

me thinks so:

\Box (pb \land \neg pe \to (g5 \land X g3 \land X \neg pe) W pe)

Задача 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й вариант:

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

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

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

Задача 3

В одной итерации вычисления между метками 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) 


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

Решение.

формально:

  1. define p 'значение глобальной переменной state равно enter_critical'
  2. define q 'процесс p находится на метке unlock'

спин:

  1. define p (state == enter_critical)
  2. define q p@unlock

[](p -> []q)

(Источник: практикум, задание 4, вариант 24, сдано Савенкову)

Задача 9

До наступления события 'значение глобальной переменной state равно leave_critical' верно: всегда выполняется 'значение глобальной переменной x равно 3'

Решение. формально:

  1. define p 'значение глобальной переменной state равно leave_critical'
  2. define q 'значение глобальной переменной x равно 3'

спин:

  1. define p (state == leave_critical)
  2. define q (x == 3)

( <> p -> ( q U p ) ) || [] q

(Источник: практикум, задание 4, вариант 24, сдано Савенкову)

Задача 10

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

Решение. формально:

  1. define a 'значение глобальной переменной state равно enter_critical'
  2. define b 'значение глобальной переменной state равно leave_critical'
  3. define p 'процесс p находится на метке sent'
  4. define q 'процесс q находится на метке received'

спин:

  1. define a (state == enter_critical)
  2. define b (state == leave_critical)
  3. define p p@sent
  4. define q q@received

[]( ( a && !b ) -> ( ( ( p -> (!b U q) ) U b ) || [](p -> (!b U q) ) )

(Источник: практикум, задание 4, вариант 24, сдано Савенкову)

Задача 11

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

  1. define x3 (x == 3)
  2. define iter (p@iter_end)

([]!iter) || (!iter U (x3 && !iter))

Есть подозрение, что первая скобка не нужна, т.к. во второй тоже не гарантируется наступление "итер", но она полностью описывает условие.

Задача 12

Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза


  1. define ent (state == enter)
  2. define leave (state == leave)
  3. define x3 (x == 3)

[]((ent && <>leave && !leave) -> (!leave U (x3 && !leave)))

Задача 13

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

  1. define leave (state == leave)
  2. 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' наступает не более одного раза

  1. define S state == state_critical
  2. 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' наступает не менее одного раза

  1. define S state = leave_critical
  2. define P p@lock

([]!S) || (!S U (P && !S))

(Источник: практикум, задание 4, вариант 32, сдано Коннову)

Задача 3

До наступления события 'значение глобальной переменной state равно leave_critical' верно: если наступило событие 'в канал c отправляется сообщение req', то до него было событие 'из канала d принимается сообщение ack'

  1. define A state == leave_critical
  2. define B c@req
  3. define C d@ack

((! B U A ) || ((!A && !B) U (C && (! A U B )))) || ( [] !B) || (!B U C)

(Источник: практикум, задание 4, вариант 32, сдано Коннову)


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


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

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