Редактирование: ВПнМ, примеры задач/Задача 5
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 125: | Строка 125: | ||
В одной итерации вычисления между метками Start и End операция R всегда предшествует (не обязательно непосредственно) выполнению операции S (полученное свойство должно быть инвариантным к прореживанию). | В одной итерации вычисления между метками 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 === | === Задача 4 === |