Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 412: | Строка 412: | ||
* <math>I(tr') = \langle\mathbb{N}, \leqslant, \xi'\rangle, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math> | * <math>I(tr') = \langle\mathbb{N}, \leqslant, \xi'\rangle, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math> | ||
- | Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \ | + | Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \leqslant tr'</math>), если |
# <math>AP' \subseteq AP</math> | # <math>AP' \subseteq AP</math> | ||
# <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что | # <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что | ||
Строка 425: | Строка 425: | ||
''' Необходимое и достаточное условие корректности модели:''' | ''' Необходимое и достаточное условие корректности модели:''' | ||
- | Модель <math>M</math> системы <math>P</math> корректна тогда и только тогда, когда <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \ | + | Модель <math>M</math> системы <math>P</math> корректна тогда и только тогда, когда <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr'</math>. |
''(для проверки такого условия нужно рассмотреть все трассы исходной системы, допускает, что в модели | ''(для проверки такого условия нужно рассмотреть все трассы исходной системы, допускает, что в модели | ||
больше состояний )'' | больше состояний )'' |