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

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

Версия 20:11, 26 сентября 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'ом:

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

me thinks so:

al-indigo:

//неправильно! //[]((p_begin & !p_end & <>p_end) -> (global5 -> Xglobal3))

Авварон: я вывел формулу, которая под меткой "me thinks so:" (за исключением что я поставил сильный Until). Еще можно сделать !pe U g5 (те не выйдем, пока не найдем g5. Но это необязательно вариант al-indigo неверный, тк нет квантора времени на (global5 -> Xglobal3) (то есть оно выполнено не ПОСЛЕ начала, а во время начала)

al-indigo: Угу, ты прав

Задача 2

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

#define state_leave (state==leave)
#define p_sent (p@sent)

[](p_sent -> X (!p_sent U state_leave))

me thinks so:

al-indigo

<>state_leave -> (<>state_leave -> []!state_leave) U a)

Авварон: метка "me thinks so:" похожа на правду (можно убрать <>s - зависит от прочтения задачи) al-indigo во 1х нельзя написать свойство 1го раза без оператора Next (тк оно не инвариантно по прореживанию) во 2х <>A U B - это неправильно (тк Future действует на всем пути вычислений, независимо от наичия Until'а) и означает что-то типа ---BA

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

me thinks so:

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

al-indigo:

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

Авварон: обозначения я беру по порядку в тексте (то есть с предыдущими вариантами C и D наоборот)

[](A->((!C U D) U B))

отличия от al-indigo: 1) в моем случае, если Б не выполнено, то будет False. Но, имхо модель подразумевает что Б всегда есть - без разницы (о5 же вопрос понимания текста) 2) я решил забить на написание A & !B, тк тогда по хорошему аналогичные отрицания надо писать и внутри Until'ов и формула будет слишком громоздкой 3) можно заменить внутренний Until на Weak Until - зависит от того, ожидаем ли мы выполнение D или нет а так, оба варианта имхо правильны

Задача 4

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

#define S "state == enter_critical"
#define Q Q@received

[](S -> (<>Q && [](Q -> X([]!Q))))

al-indigo:

меня мучают особые сомнения, но кажется, так?
!S | [](<>S -> (Q -> X([]!Q)))

Авварон: Нет, оригинал был правильный. 2я формула вообще инвертированная по-моему + напрягает !S в начале

al-indigo: !S в начале -- я имел в виду случай, когда state==enter_critical вообще не наступает. В самой формуле я, может, ошибся, но вообще я вот сейчас смотрю, и вроде, мне кажется, что правильно. Ну то есть так примерно: "Либо S не наступает никогда, либо, если S когда-нибудь наступает, то всегда выполняется то, что Q наступает, и если оно наступает, что начиная со следующего состояния всегда !Q". Или я не так это читаю?

Задача 5

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

#define R "state == leave"
#define was_sent P@sent

([]!R) || (!R U (was_sent && !R))

al-indigo:

Может, здесь не слабый антил всё-таки?
!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))))

al-indigo:

Тут явно какая-то херня с двумя последними #define, хотя я и не уверен, что правильно у меня

#define begin (P@iter_begin)
#define end (P@iter_end)
#define R (C!req)
#define S (D?ack)
[]((begin & !end & <>end) -> (R -> (!end U (S & !end))) U end) 
//это паттерн response between. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого

Авварон: это задача про самолет в чистом виде:) вариант al-indigo верный, только <>end не нужен - тк он есть всегда по условию, то Future(end) всегда true и ни на что не влияет Ну и о5 же я бы не писал невозможность одновременности состояний (begin & !end - они несут мало смысла:)

Задача 2

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

1й вариант:

[] (p && !q -> !r W (q || (r W (q || !r W q))))

2й вариант:

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

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

al-indigo:

адский ад какой-то, я так ничего и не понял тут, надо будет завтра ещё подумать :(

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

Задача 3

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

al-indigo:

Кажется, вариант выше тоже *почти* правильный (не хватает ещё пары внешних скобок, вроде), но какой-то перегруженный. Вот мой:
[]((start & !end & <>end) -> (!S U (R | end))) //Precedence between

Авварон:

первый вариант не верен, если не встретится R - будет верна правая часть дизъюнкции и на левую мы кладем => свойство того, что должно быть !S, тупо не проверяется (противоречие с тем, что оно не должно появляться до R).
al-indigo - нормально, но о5 же - почему есть проверка неодновременности start и end, но нет аналогичной у Until (они в принципе не нужны, но если мы захотим добавить что-нибудь эдакое, то добавить будет сложно из-за дизъюнкции). Мой вариант: (аналогичный, и как обычно без !End & <>End)
[](Start->( (!S U R) U End))

Задача 4

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

[] (START & !END & <>END -> ( (!P U END)||((P -> (!END U S))U END) )

al-indigo:

Хорошая тренировка -- найдите отличия (они есть). Единственное что -- странно, но случай, когда P не случается выглядит уместным (в решении выше), а у меня его нет -- в паттерне написано, как у меня. Кто-нибудь, прокомментируйте? Или из этого не следует, что P обязательно произойдёт?
[] ((Start & !End & <>End) -> (P -> (!End U (S & !End) U End))

Авварон:

первый вариант верный, но там не нужна дизъюнкция вообще (вариант !P включается в P -> BLA ибо -> это !P || BLA)
al-indigo, ты накосячил со скобками, надо
[] ((Start & !End & <>End) -> ( {P -> (!End U (S & !End))} U End)
Из-за скобок и коммент неверный - в этом варианте !P подходит

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

al-indigo:

//абсолютно то же самое, шаблон precedence between/
[]((p_b & !p_e & <>p_e) -> (!c_r U (p_a | p_e)))

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

al-indigo:

Это дублирование задачи один, повторюсь, чтобы можно было сравнить и понять, что всё-таки правильно. Кажется, первые два варината неправильные вообще.
И тут опять херня с #define, хотя я снова не уверен, что правильно у меня
#define begin (P@iter_begin)
#define end (P@iter_end)
#define R (C!req)
#define S (D?ack)
[]((begin & !end & <>end) -> (R -> (!end U (S & !end))) U end) 
//это паттерн response between. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого

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

al-indigo:

<>p_e -> ((x_3 -> (!p_e U (y_5 & !p_e))) U p_e) // из паттернов. Но тут неясно -- может ли быть так, что х не будет равно 3?
<>p_e -> ((!x_3 | (x_3 -> (!p_e U (y_5 & !p_e)))) U p_e) //мой вариант, просто рассуждения

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

al-indigo:

ok?

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

al-indigo:

ok?

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

al-indigo:

Здесь какая-то неточность, непонятно, насколько существенная. В первой подформуле точняк должно быть ещё <>b, а его там нет.

Задача 11

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

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

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

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

al-indigo:

А тут нужно учитывать, что iter_end может не наступить? Мне кажется, оно по условию всегда должно происходить в какой-то момент. И да -- само-то решение является правильным?
!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)))

al-indigo:

не понимаю, что тут избыточного в решении, по-моему, самое то?

Задача 13

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

1. define leave (state == leave)
2. define send (channel ! req)

(send U leave)||([]send)

//Задачи 11-13 были отправлены по почте, оценка 5. Решение задачи 12 - избыточно.

al-indigo:

красивое, понятное и наверное правильное решение :)

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

al-indigo:

ok?

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

al-indigo:

Может, избыточно, но кажется, так правильнее:
[]((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))

al-indigo:

ok?

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

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

Задача 3

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

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

al-indigo:

ok?

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

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

ок?

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

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

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

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