Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 121: | Строка 121: | ||
* <math>S = Loc \times Eval(V_p)</math> (декартово произведение точек программы на всевозможные подстановки) | * <math>S = Loc \times Eval(V_p)</math> (декартово произведение точек программы на всевозможные подстановки) | ||
- | * <math>\rightarrow : S \times Act \times S </math> с соответствующим правилом вывода <math> \frac{l \overset{g:a}{\rightarrow} l | + | * <math>\rightarrow : S \times Act \times S </math> с соответствующим правилом вывода <math> \frac{l \overset{g:a}{\rightarrow} l \and (n \models g) }{\langle l,n \rangle \overset{a}{\rightarrow} \langle l',Effect(a,n) \rangle }</math> |
* Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы: | * Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы: | ||
- | ** <math>I= | + | ** <math>I={\langle l , n \rangle : l \in Loc_0 , n \models g_0 }</math> |
* Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы: | * Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы: | ||
** <math>AP=Loc \cup Cond(V_P) </math> | ** <math>AP=Loc \cup Cond(V_P) </math> | ||
* Состояния вида <math>\langle l,n \rangle</math> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке: | * Состояния вида <math>\langle l,n \rangle</math> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке: | ||
- | ** <math>L(\langle l , n \rangle)= | + | ** <math>L(\langle l , n \rangle)= (l) \cup (g \in Cond(V_P): n \models g ).</math> |