Редактирование: ВПнМ, примеры задач/Задача 5
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 281: | Строка 281: | ||
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза | Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится на метке iter_end' верно: событие 'процесс p находится на метке lock' наступает не менее одного раза | ||
- | #define | + | #define f_b p@iter_begin |
- | #define | + | #define f_e p@iter_end |
- | #define | + | #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==== | ====Задача 2==== |