Редактирование: ВПнМ, примеры задач/Задача 5

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

<div style="float:right">__TOC__</div>
== Как решать эти задачи? ==
Для решения этих задач '''обязательно''' знать '''[[ВПнМ/Теормин#.D0.9B.D0.BE.D0.B3.D0.B8.D0.BA.D0.B0_LTL._.D0.A1.D0.B8.D0.BD.D1.82.D0.B0.D0.BA.D1.81.D0.B8.D1.81_LTL._.D0.A1.D0.B5.D0.BC.D0.B0.D0.BD.D1.82.D0.B8.D0.BA.D0.B0_.D0.B2.D1.8B.D0.BF.D0.BE.D0.BB.D0.BD.D0.B8.D0.BC.D0.BE.D1.81.D1.82.D0.B8_.D1.84.D0.BE.D1.80.D0.BC.D1.83.D0.BB._.D0.A1.D0.B8.D0.BB.D1.8C.D0.BD.D1.8B.D0.B9_.D0.B8_.D1.81.D0.BB.D0.B0.D0.B1.D1.8B.D0.B9_until.|определения]]''', а так же следующие '''[http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml шаблоны].'''

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

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

Будьте готовы к тому, что вам скажут, что в формуле '''применять слабый 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 (g==5)
 #define d (g==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. Окончательный вариант.

=== Задача 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 когда-либо произойдет.

=== Задача 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 -> ( (!d U c) U b))

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

[]( (a & !b & <>b) -> (!d U (c | 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) // Потомкам: доказать что эта формула верна или нет:)

=== Задача 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) // Или так.

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

=== Задача 10 ===

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

Решение.
формально: 
#define a 'значение глобальной переменной state равно enter_critical'
#define b 'значение глобальной переменной state равно leave_critical'
#define p 'процесс p находится на метке sent'
#define q 'процесс q находится на метке received'

спин:
#define a (state == enter_critical)
#define b (state == leave_critical)
#define p p@sent
#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' наступает не менее одного раза

#define x3 (x == 3)
#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' наступает не менее одного раза

#define ent (state == enter)
#define leave (state == leave)
#define x3 (x == 3)

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

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

=== Задача 13 ===

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

#define leave (state == leave)
#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?

Авварон:
 ок
 #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 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))

Авварон:
 al-indigo, твое решение неверное. Квантор [] НЕ ограничивается Until'ом 
 #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 q state==enter
 #define p x==3
 [](!q) | <>(q & <>P))

al-indigo:
 ok?

Авварон:
 #define A state==enter
 #define B x==3
 [](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' наступает не более одного раза

#define S state == state_critical
#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))

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

==== Задача 2 ====

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

#define S state = leave_critical
#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'

#define A state == leave_critical
#define B c@req 
#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' (полученное свойство не обязательно может быть инвариантным к прореживанию)

#define p_iter_end (p@iter_end)
#define p_iter_unlock (p@iter_unlock)
#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' наступает не более одного раза

#define p_iter_begin(p@iter_begin)
#define p_iter_end((p@iter_end)
#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)))

Авварон:
 о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'

#define p_iter_begin(p@iter_begin)
#define p_iter_end((p@iter_end)
#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) )

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Шаблон:Курс ВПнМ

Получено с http://esyr.us/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_%D0%BF%D1%80%D0%B8%D0%BC%D0%B5%D1%80%D1%8B_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_5

Редактирование: ВПнМ, примеры задач/Задача 5

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

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 2: / Строка 2: @@
 == Как решать эти задачи? ==
 Для решения этих задач '''обязательно''' знать '''[[ВПнМ/Теормин#.D0.9B.D0.BE.D0.B3.D0.B8.D0.BA.D0.B0_LTL._.D0.A1.D0.B8.D0.BD.D1.82.D0.B0.D0.BA.D1.81.D0.B8.D1.81_LTL._.D0.A1.D0.B5.D0.BC.D0.B0.D0.BD.D1.82.D0.B8.D0.BA.D0.B0_.D0.B2.D1.8B.D0.BF.D0.BE.D0.BB.D0.BD.D0.B8.D0.BC.D0.BE.D1.81.D1.82.D0.B8_.D1.84.D0.BE.D1.80.D0.BC.D1.83.D0.BB._.D0.A1.D0.B8.D0.BB.D1.8C.D0.BD.D1.8B.D0.B9_.D0.B8_.D1.81.D0.BB.D0.B0.D0.B1.D1.8B.D0.B9_until.|определения]]''', а так же следующие '''[http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml шаблоны].'''
-Полезна также ссылка из шаблонов на то, что означают различные области[http://patterns.projects.cis.ksu.edu/documentation/patterns/scopes.shtml].
-Обратите внимание на "между Q и R", т.е. "Between Q and R" и на "после Q до R", т.е. "After Q, until R"
 Задачи, по сути делятся на инвариантные к прореживанию и не обязательно инвариантные.
@@ Строка 14: / Строка 11: @@
  p W q = <>(!p) -> (p U q)
  p W q = p U (q | []p)
 == Задачи (не инв-ные) ==
@@ Строка 24: / Строка 22: @@
  #define a (p@iter_begin)
  #define b (p@iter_end)
- #define c (y==5)
+ #define c (g==5)
- #define d (x==3)
+ #define d (g==3)
 [](a & !b -> (c & Xd & X !b) W b)
@@ Строка 78: / Строка 76: @@
 !a U (b && !b) // сильный или слабый Until зависит от прочтения задачи. Возможны оба варианта
-UPD: (b && !b) всегда false. Если наступление события означает, что условие стало верным, то ответ
-!a W b
-Если наступление события означает, что условие побыло истинным, а потом стало ложным, то ответ
-!a W (b && X!b)
 == Задачи (инв-ные) ==
@@ Строка 103: / Строка 93: @@
 []( (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 ===
@@ Строка 114: / Строка 100: @@
 []( (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 ===
@@ Строка 159: / Строка 139: @@
  #define d d?ack
-[](a -> ( (!c U d) U b))
+[](a -> ( (!d U c) U b))
-[]( (a & !b & <>b) -> ((!c U d) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
+[]( (a & !b & <>b) -> ((!d U c) U b) ) // Добавили то, что a и b не происходят одновременно и то, что b когда-либо произойдет.
-[]( (a & !b & <>b) -> (!c U (d | b)) ) // можно и так
+[]( (a & !b & <>b) -> (!d U (c | b)) ) // можно и так
 === Задача 6 ===
@@ Строка 191: / Строка 171: @@
 (!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 ===
@@ Строка 225: / Строка 195: @@
 Потомкам: понять разницу:)
-Teravisor: потомки говорят, между 2 и 3 формулами разницы нету. Объяснение: U требует выполнимости где-то второго аргумента, в данном случае "a", в случае если его нет, формула не выполняется. требование <>a-> может быть расценено лектором как избыточное, и вообщем то не хорошо. Вообще говоря вроде первая формула правильная, в отличие от последних двух, но и правильность последних можно доказать из утверждения "я так понял задание".
 === Задача 10 ===
@@ Строка 233: / Строка 201: @@
 верно: после события 'процесс p находится на метке sent' рано или поздно наступит событие 'процесс q находится на метке received'
- #define a (state == enter_critical)
+Решение.
- #define b (state == leave_critical)
+формально:
- #define c p@sent
+#define a 'значение глобальной переменной state равно enter_critical'
- #define d q@received
+#define b 'значение глобальной переменной state равно leave_critical'
+#define p 'процесс p находится на метке sent'
+#define q 'процесс q находится на метке received'
+спин:
+#define a (state == enter_critical)
+#define b (state == leave_critical)
+#define p p@sent
+#define q q@received
-[]( (a & !b & <>b) -> ((c -> (!b U d)) U b)  ) // Здесь U b можно заменить на W b (зависит от прочтения задачи)
+[]( ( a && !b ) -> ( ( ( p -> (!b U q) ) U b ) || [](p -> (!b U q) ) )
-Teravisor: то, же что и в задании 1. Комментарий это не можно, а нужно. И заменой U b на W b не всё исправится - надо еще <>b убрать вначале.
+(Источник: практикум, задание 4, вариант 24, сдано Савенкову)
+al-indigo:
+ Здесь какая-то неточность, непонятно, насколько существенная. В первой подформуле точняк должно быть ещё <>b, а его там нет.
 === Задача 11 ===
@@ Строка 246: / Строка 225: @@
 До наступления события 'процесс p находится на метке iter_end' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
- #define a (p@iter_end)
+#define x3 (x == 3)
- #define b (x == 3)
+#define iter (p@iter_end)
-!a W (b && !a) // В принципе, тут можно сильный Until поставить.
+([]!iter) || (!iter U (x3 && !iter))
-([]!a) || (!a U (b && !a)) // Расписан слабый Until
+Есть подозрение, что первая скобка не нужна, т.к. во второй тоже не гарантируется наступление "итер", но она полностью описывает условие.
+al-indigo:
+ А тут нужно учитывать, что iter_end может не наступить? Мне кажется, оно по условию всегда должно происходить в какой-то момент. И да -- само-то решение является правильным?
+ !iter U (x3 && !iter)
 === Задача 12 ===
@@ Строка 257: / Строка 240: @@
 Между событиями 'значение глобальной переменной state равно enter' и 'значение глобальной переменной state равно leave' верно: событие 'значение глобальной переменной x равно 3' наступает не менее одного раза
- #define a (state == enter)
- #define b (state == leave)
- #define c (x == 3)
-[]( a -> (!b U c) ) // "Простой" вариант.
+#define ent (state == enter)
+#define leave (state == leave)
+#define x3 (x == 3)
-[]( (a && !b && <>b) -> (!b U (c && !b)) ) // Окончательный.
+[]((ent && <>leave && !leave) -> (!leave U (x3 && !leave)))
+al-indigo:
+ не понимаю, что тут избыточного в решении, по-моему, самое то?
 === Задача 13 ===
@@ Строка 269: / Строка 254: @@
 До наступления события 'значение глобальной переменной state равно leave' верно: всегда выполняется 'в канал c отправляется сообщение req'
- #define a (state == leave)
+#define leave (state == leave)
- #define b (channel ! req)
+#define send (channel ! req)
-b W a
+(send U leave)||([]send)
-[]b || (b U a) // Расписан Weak.
+//Задачи 11-13 были отправлены по почте, оценка 5. Решение задачи 12 - избыточно.
+al-indigo:
+ красивое, понятное и наверное правильное решение :)
 === Вариант 110 ===
@@ Строка 281: / Строка 269: @@
 Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза
- #define a p@iter_begin
+ #define f_b p@iter_begin
- #define b p@iter_end
+ #define f_e p@iter_end
- #define c p@lock
+ #define f_lock p@lock
+ []( (f_b & !f_e && <>f_e) -> ( !f_e U ( f_lock & !f_e ) ) )
-[](a -> !b U c)
+al-indigo:
+ ok?
-[]( (a & !b && <>b) -> (!b U (c & !b)) ) // Окончательный вариант.
+Авварон:
+ ок
+ #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 f_b state==enter
- #define b state==leave
+ #define f_e state==leave
- #define c p@lock
+ #define f_lock p@lock
+ []((f_b && !f_e && <>f_e) -> (f_lock U f_e))
-[](a -> (c U b))
+al-indigo:
+ Может, избыточно, но кажется, так правильнее:
+ []((f_b && !f_e && <>f_e) -> ([]f_lock U f_e))
-[]( (a && !b && <>b) -> (c U b) )
+Авварон:
+ al-indigo, твое решение неверное. Квантор [] НЕ ограничивается Until'ом
+ #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 q state==enter
- #define b x==3
+ #define p x==3
+ [](!q) | <>(q & <>P))
-[](a -> <>b)
+al-indigo:
+ ok?
-[](!a) | <>(a & <>b)) // Потомкам: проверить правильность.
+Авварон:
+ #define A state==enter
+ #define B x==3
+ [](A -> <>B)
+ я бы написал так, а то что сверху имхо будет если развернуть импликацию. Могу ошибаться в своем варианте
 === Вариант 104 ===
@@ Строка 383: / Строка 394: @@
  По-моему, как-то уж очень избыточно
  []((P & !S & <>S) -> (!P U S))
- []((P & !S & <>S) -> (P U (!P U S)))         ( поправил al-indigo: P->!P - всегда false)
 Авварон:
@@ Строка 475: / Строка 484: @@
 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)
 Авварон: