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

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

Перейти к: навигация, поиск

Содержание

Как решать эти задачи?

Для решения этих задач обязательно знать определения, а так же следующие шаблоны.

Полезна также ссылка из шаблонов на то, что означают различные области[1]. Обратите внимание на "между Q и R", т.е. "Between Q and R" и на "после Q до R", т.е. "After Q, until R"

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

Инвариантная к прореживанию формула - это такая формула, результат вычисления которой не меняется от того, применяется прореживание или нет. Прореживание - это сужение нескольких состояний до одного (а м.б. и расширение одного до нескольких - доподлинно неизвестно).

Будьте готовы к тому, что вам скажут, что в формуле применять слабый 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 a (p@iter_begin)
#define b (p@iter_end)
#define c (y==5)
#define d (x==3)

[](a & !b -> (c & Xd & X !b) W b)

Задача 2

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

#define a (state==leave)
#define b (p@sent)

<>a -> ((b -> b & X (!b U a)) U a)

Задача 3

Между событиями 'значение глобальной переменной state равно enter_critical' и 'значение глобальной переменной state равно leave_critical' верно: если наступило событие 'процесс p находится на метке lock', то до него было событие 'значение глобальной переменной state равно locked'

#define a (state==enter_critical)
#define b (state==leave_critical)
#define c (p@lock)
#define d (state==locked)

[]( a -> ((!c U d) U b) ) // Этот вариант не учитывает то, что b не может быть одновременно с a, и то, что b когда-либо наступит

[]( (a & !b & <>b) -> ((!c U d) U b) )

[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно объединить d и b - c не наступит, пока не наступит один из них

Задача 4

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

#define a "state == enter_critical"
#define b Q@received

[]( a -> ( <>b && [](b -> X[]!b) ) )

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

[]( a -> ( <>b && [](b -> (b U []!b)) ) )

Задача 5

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

#define a "state == leave"
#define b P@sent

!a W (b && !b)

!a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта

Задачи (инв-ные)

Задача 1

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

#define a P@iter_begin
#define b P@iter_end
#define c ...@C_send_req
#define d ...@D_send_ack

[]( a -> ( (c -> (!b U d)) U b) )

[]( (a & !b & <>b) -> ( (c -> (!b U d)) U b) ) // добавили то, что a и b не могут быть одновременно и то, что b когда-либо наступит

[]( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) ) // добавили то, что b не происходит одновременно с d. Окончательный вариант.

Teravisor: Все три три не верны потому, что формулировка "после ... до ..." подразумевает, что второе событие может не произойти. Моя версия(шаблон S responds to P After Q until R, раскрытие W): [](a && !b -> ( ((p -> (!b U (q && !b ))) U b) || ([](p -> (!b U (q && !b ))) )

Задача 2

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

[]( a -> ((c -> c U (!c U b)) U b) )

[]( (a & !b & <>b) -> ((c -> c U (!c U b)) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.


Teravisor: Та же самая ошибка, что и в задаче 1. Мой вариант(Заменить в 2й формуле последний U на W и раскрыть с небольшой правкой условия !c U b):

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

Задача 3

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

#define a Start
#define b End
#define c R
#define d S

[](a -> ( (!d U c) U b ))

[]( (a & !b & <>b) -> ( (!d U c) U b) ) // добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет

[]( (a & !b & <>b) -> ( !d U (c | b)) ) // можно и так

Задача 4

В ходе итерации, начинающейся меткой START и заканчивающейся меткой END, выполнение оператора x==1 всегда влечет за собой приём сообщения, помеченного меткой S.

#define a START
#define b END
#define c x==1
#define d S

[](a -> ( (c -> (!b U d)) U b)

[]( (a & !b & <>b) -> ( (c -> (!b U d)) U b) // добавили то, что a и b не происходят одновременно и что b когда-либо произойдет

[]( (a & !b & <>b) -> ( (c -> (!b U (d & !b))) U b) // добавили то, что b и d не происходят одновременно. Окончательный вариант.

Задача 5

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

#define a p@iter_begin
#define b p@iter_end
#define c c!req
#define d d?ack

[](a -> ( (!c U d) U b))

[]( (a & !b & <>b) -> ((!c U d) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.

[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно и так

Задача 6

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

#define a (state == enter)
#define b (state == leave)
#define c (с!req)
#define d (в?ack)

[](a -> (c -> ((!b U d) U b))

[]( (a & !b & <>b) -> (c -> (!b U (d & !b))) U b) ) // Добавили то, что a и b не могут происходить одновременно и аналогично d и b. Окончательный вариант.

Задача 7

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

#define a p@iter_end
#define b x == 3
#define c y == 5

(b -> (!a U c)) U a

<>a ->( (b -> (!a U (c & !a))) U a ) // Добавили то, что a когда-либо произойдет, и то, что c и a не происходят одновременно. Окончательный вариант.

(!a U b) -> (!a U c) // Потомкам: доказать что эта формула верна или нет:)

Teravisor: Потомки доказывают: третья не верная. Мы смотрим обе импликации(->) из начальной точки, т.е. нам подойдет

!a !a !a !a !a !a a

!b !b !b !b !b b b

!c c c c c c c

!a U c выполняется. => формула true, хотя условию не удовлетворяет. Если поставить [] перед всей формулой правильность не изменится. Кто хочет может сам доказать.

Задача 8

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

#define a (state == enter_critical)
#define b p@unlock

[](a -> []b)

Задача 9

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

#define a (state == leave_critical)
#define b (x == 3)

(b W a) // []b || (b U a) - Тоже самое, но через сильный Until.

(b U a) // Можно так.

<>a -> (b U a) // Или так.

Потомкам: понять разницу:)

Teravisor: потомки говорят, между 2 и 3 формулами разницы нету. Объяснение: U требует выполнимости где-то второго аргумента, в данном случае "a", в случае если его нет, формула не выполняется. требование <>a-> может быть расценено лектором как избыточное, и вообщем то не хорошо. Вообще говоря вроде первая формула правильная, в отличие от последних двух, но и правильность последних можно доказать из утверждения "я так понял задание".

Задача 10

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

#define a (state == enter_critical)
#define b (state == leave_critical)
#define c p@sent
#define d q@received

[]( (a & !b & <>b) -> ((c -> (!b U d)) U b) ) // Здесь U b можно заменить на W b (зависит от прочтения задачи)

Teravisor: то, же что и в задании 1. Комментарий это не можно, а нужно. И заменой U b на W b не всё исправится - надо еще <>b убрать вначале.

Задача 11

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

#define a (p@iter_end)
#define b (x == 3)

!a W (b && !a) // В принципе, тут можно сильный Until поставить.

([]!a) || (!a U (b && !a)) // Расписан слабый Until

Задача 12

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

#define a (state == enter)
#define b (state == leave)
#define c (x == 3)

[]( a -> (!b U c) ) // "Простой" вариант.

[]( (a && !b && <>b) -> (!b U (c && !b)) ) // Окончательный.

Задача 13

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

#define a (state == leave)
#define b (channel ! req)

b W a

[]b || (b U a) // Расписан Weak.

Вариант 110

Задача 1

Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза

#define a p@iter_begin
#define b p@iter_end
#define c p@lock

[](a -> !b U c)

[]( (a & !b && <>b) -> (!b U (c & !b)) ) // Окончательный вариант.

Задача 2

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

#define a state==enter
#define b state==leave
#define c p@lock

[](a -> (c U b))

[]( (a && !b && <>b) -> (c U b) )

Задача 3

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

#define a state==enter
#define b x==3

[](a -> <>b)

[](!a) | <>(a & <>b)) // Потомкам: проверить правильность.

Вариант 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)) )     )

al-indigo:

Фиг знает, что тут происходит, но мне кажется, что правильно будет так:
[](( a & !b & <>b ) -> (!b U (c -> [](!c))))

Авварон:

без Х не решается => все что сверху - туфта
с Х:
#define A p@iter_begin
#define B p@iter_end
#define C d?ack
[]( A -> (C -> X (!C U B)) ) // туплю - не надо ли 2ю импликацию сделать также U B ? вроде нет

Задача 2

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

#define d (state==enter)
#define e (state==leave)
#define f p@unlock
[] ( (d & (<>e) ) -> (!e U f) )

al-indigo:

Пропущено, что d и e не совпадают:
[] ( (d & (<>e) & !e ) -> (!e U f) )

Авварон:

#define A (state==enter)
#define B (state==leave)
#define C p@unlock
короткая: [](A -> (!B U C))
длинная: []( (A & !B & <>B) -> (!B U C) )

Задача 3

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

#define g (state==enter_critical)
#define h (state==unlocked)
[] ([]!g || (g -> []!h))

al-indigo:

ok?

Авварон:

Похоже на правду, но я бы писал так (используя шаблон из 8й лекции на стр 56):
#define A (state==enter_critical)
#define B (state==unlocked)
[](A -> []!B)
По идее будет то же самое после преобразований

Вариант 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, сдано Коннову)

al-indigo:

По-моему, как-то уж очень избыточно
[]((P & !S & <>S) -> (!P U S))
[]((P & !S & <>S) -> (P U (!P U S)))         ( поправил al-indigo: P->!P - всегда false)

Авварон:

#define A state == state_critical
#define B x = 3
[](B -> B U !B U A)
вроде так, проверьте)

Задача 2

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

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

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

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

al-indigo:

ок?

Авварон:

ага, но я бы писал так:
#define A state = leave_critical
#define B p@lock
через Weak, простая: !A W B
через Weak, сложная: !A W (B & !A)
через Until, сложная: []!A || (!A U (B & !A))
Эти 3 ф-лы эквивалентны, но W имхо читать проще

Задача 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, сдано Коннову)

al-indigo:

<>A -> (!B U (C | A))

Авварон:

согласен
малый фикс:
<>A -> (!B U C U A) 
в этом варианте проще добавить неодновременность, если преподу припрет изменить условие. Да, и <>A зависит от прочтения, тоже можно опустить (не факт что оно будет)

Вариант 29

Задача 1

До наступления события 'процесс p находится на метке iter_end' верно: сразу за событием 'значение глобальной переменной state равно unlocked'наступает событие 'процесс p находится на метке unlock' (полученное свойство не обязательно может быть инвариантным к прореживанию)

  1. define p_iter_end (p@iter_end)
  2. define p_iter_unlock (p@iter_unlock)
  3. define state (state=unlocked)

[](((state->X p_iter_unlocked) U p_iter_end))

al-indigo:

кажется, так
[](!p_iter_end U (p_iter_unlock -> X state))

Авварон:

al-indigo у тебя условие слабее - хотя бы 1 раз будет выполнено условие (а это не имелось ввиду, поэтому так). Можно перефразировать "за каким-то B будет С" (но не за всеми!)
#define A (p@iter_end)
#define B (p@iter_unlock)
#define C (state=unlocked)
(B -> X C) U A

Задача 2

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

  1. define p_iter_begin(p@iter_begin)
  2. define p_iter_end((p@iter_end)
  3. define c_S ...@C_send_req


[](p_iter_begin -> !p_iter_end || (!p_iter_end U (c_S U (!c_S U p_iter_end ))))

al-indigo:

[]((p_iter_begin & !p_iter_end & <>p_iter_end) -> (req -> (![]req U p_iter_end)))
[]((p_iter_begin & !p_iter_end & <>p_iter_end) -> (req -> (req U (!req U p_iter_end)))) (поправил al-indigo)

Авварон:

о5 задача не решается без X
#define A (p@iter_begin)
#define B ((p@iter_end)
#define C ...@C_send_req
[]( A -> { (C -> X[!C U B]) U B } )

Задача 3

Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно:всегда выполняется 'процесс p находится на метке lock'

  1. define p_iter_begin(p@iter_begin)
  2. define p_iter_end((p@iter_end)
  3. define p_lock(p@lock)

[](p_iter_begin & !p_iter_end & <>p_iter_end)->(p_lock U p_iter_end)

Сдавал не Коннову

al-indigo:

может быть избыточно, но должно быть правильно
[]((p_iter_begin & !p_iter_end & <>p_iter_end)->([]p_lock U p_iter_end))

Авварон:

#define A (p@iter_begin)
#define B ((p@iter_end)
#define C (p@lock)
простая: [](A -> (C U B))
сложная: []( (A & !B & <>B) -> (C U B) )


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


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

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