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

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

Версия от 17:33, 1 октября 2010; Авварон (Обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

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

ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 30 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.

<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 ===
После события p и до наступления события q событие r наступает не более одного раза. (полученное свойство должно быть инвариантным к прореживанию)

'''1й вариант''':

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

'''2й вариант''':
 <math>\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) </math>

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

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

Авварон:
 Предполагаю такой вариант:
 []( A -> ((C -> C U (!C U B)) U B) )

=== Задача 3 ===

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

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

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 подходит

al-indigo:
 и правда накосячил. Чёрт возьми, как же на пересдаче-то не ошибиться :(

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

Задача типа "недосамолет", аналогична 3ей
Решил переписать в "прямых" обозначениях (и исправить косяк с p_a): 
 #define A p@iter_begin
 #define B p@iter_end
 #define C c!req
 #define D d?ack
 []((A & !B & <>B) -> (!C U (D | B)))

=== Задача 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. Кто-нибудь может, кстати, "объяснить правильность формулы на трассе"? У меня просили что-то в таком духе, и у меня как-то ничего не вышло из этого

Авварон:
 прямые обозначения:
 #define A (P@iter_begin)
 #define B (P@iter_end)
 #define C (C!req)
 #define D (D?ack)
 урезанная: [](A -> (C -> ((!B U D) U B) 
 полная: []((A & !B & <>B) -> (C -> (!B U (D & !B))) U B)

=== Задача 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) //мой вариант, просто рассуждения

Авварон:
 первое хрень (оно ОЧЕНЬ похоже на правду, но я не могу доказать что она не верна. Препод похоже тоже не смог:)), 2е оба верны (во 2м !x_3 лишняя, тк "!x_3 | x_3 -> A" EQ "!x_3 | !x_3 | A")
 прямые обозначения:
 #define A p@iter_end
 #define B x == 3
 #define C y == 5
 урезанная: (B -> (!A U C)) U A
 полная: (B -> (!A U [C & !A])) U A
 <>A по желанию, зависит от того, хотим ли мы видеть А
 Задачу классифицирую как "самолет урезанный"

=== Задача 8 ===

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

Решение.

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

спин:
#define p (state == enter_critical)
#define q p@unlock

[](p -> []q)

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

al-indigo:
 ok?

Авварон:
 ок

=== Задача 9 ===

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

Решение.
формально: 
#define p 'значение глобальной переменной state равно leave_critical'
#define q 'значение глобальной переменной x равно 3'

спин:
#define p (state == leave_critical)
#define q (x == 3)

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

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

al-indigo:
 ok?

Авварон:
 Да, ок, но я бы написал тут и "простой" вариант:
 q W p

=== Задача 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:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

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

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

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