ГОСТ Р ИСО 18629-42—2011
({and | or} < mix_formula >*) |
({implies | iff) < mix_formula >)
< mix_axiom > ::=({forall | exists} < variable >*) < mix_formula >)
9 Событийные входные условия выполнения действий
Данный раздел характеризует все определения, обусловленные событийными входными условиями
выполнения действий. Критерий, используемыйдля классификации указанныхдействий: зависит или нет
реальное выполнение некоторогодействия от выполнениядругих действий.
9.1 Примитивная лексика событийных входных условий выполнения действий
В лексике событийных входных условий выполнения действий примитивные соотношения не исполь
зуются.
9.2 Описываемые соотношения событийных входных условий выполнения действий
В данном подразделе определены следующие соотношения:
- (tree_equiv ?s1 ?s2);
- (occurrence_constrained ?a);
- (occurrence_dependent ?a):
- (occurrencejndependent ?a).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
9.3 Теории, обусловленные событийными входными условиями выполнения действий
Для данной теории необходимы:
- occtree.th;
- psl_core.th.
9.4Дефинициональныо расширения, обусловленные событийными входными условиями
выполнения действий
Для событийных входных условий выполнения действий необходимо нижеследующее дефиницио-
нальное расширение:
- precond.def.
9.5 Определения событийных входных условий выполнения действий
Для событийных входных условий выполнения действий определены нижеследующие понятия.
9.5.1 tree_equiv
Два события эквивалентны на дереве событий тогда и только тогда, когда они отображаются друг на
друга путем некоторого преобразования дерева событий.
(forall {?a?s1 ?s2)
(iff (tree_equiv (successor ?a ?s1)(successor ?a ?s2))
(and (legal_equiv ?s1 ?s2)
(or(tree_equiv?s1 ?s2)
(initial ?s1)
(initial ?s2)))))
9.5.2 occurrence_constrained
Некотороедействие является событийно ограниченным тогда и только тогда, когда все преобразова
ния дерева событий сохраняютдействительное выполнениеданногодействия.
(forall (?а) (iff(occurrence_constrained ?а)
(forall (?s1 ?s2)
(implies (and (occurrence ?s1 ?a)
(occurrence ?s2 ?a)
(tree_equiv?s1 ?s2))
(legal_equiv ?s1 ?s2)))))
9.5.3 occurrence_dependent
Некоторое действие является зависящим отсобытия тогда и только тогда, когда существует преобра
зование дерева событий, сохраняющеедействительное выполнение действия.
11