ГОСТ Р ИСО 18629-42—2011
составляющих действий в максимальном встроенном поддереве, которые также согласованы и между
собой.
(forall (?s) (iff (nondet_plan ?s)
(exists (?a ?s1 ?s3 ?s4)
(and (root ?s ?a)
(forall (?s2)
(implies (and (embed_tree ?s1 ?s2 ?s ?a)
(state_equiv ?s1 ?s2))
(subocc_equiv ?s1 ?s2 ?s ?a))))
(state_equiv ?s3 ?s4)
(embed_tree ?s3 ?s4 ?s5 ?a)
(not (subocc_equiv ?s3 ?s4 ?s5 ?a))))))
28.5.3 unplan
Некоторое дерево действий с корневым событием ?s является неплановым тогда и только тогда,
когдадля каждого согласованного по состоянию события существует другое событие, связанное с состав
ляющим действием, но отличное отуказанного.
(forall (?s) (iff(unplan ?s)
(forall (?s1 ?a)
(implies (root ?s ?a)
(exists (?s2)
(and (embed_tree ?s1 ?s2 ?s ?a)
(state_equiv?s1 ?s2)
(not (subocc_equiv ?s1 ?s2 ?s ?a))))))))
28.6 Грамматика описаний процесса для встроенных действий: планы
Нижеследующие грамматические утверждения определяют описания процесса, установленные в KIF
для встроенныхдействий: планов.
< p!an_axiom > ::= (forall (?s ?осс < variable >*)
< simple_plan_axiom >)
< nondet_plan_axiom > ::= (forall (?s ?occ < variable >+)
< nondet_plan_axiom >))
< plan_formula > ::= (implies < subocc_formula >
< simple_state_axiom >)
< simple_plan_axiom > ::= < plan_formula> |
(and < simple_plan_axiom > < simple_plan_axiom >+)
< nondet_plan_formula > ::= (implies < subocc_formula >
< state_axk>m >)
< nondet_plan_axiom > ::= < nondet_plan_formula> |
(and < nondet_plan_axiom > < nondet_plan_axiom >+)
29 Встроенные действия: временной разброс
Данный раздел характеризует все определения, обусловленные встроеннымидействиями: времен
ной разброс. Критерий, используемый для классификации указанных действий: зависят или нет события
некоторого комплексного действия от времени выполнения составляющихдействий в процессе выполне
ния указанного комплексного действия.
29.1 Примитивная лексика встроенных действий: временной разброс
Лексика встроенныхдействий (временной разброс) не требует примитивных соотношений.
29.2 Описываемые соотношения встроенных действий: временной разброс
В данном подразделе определены следующие соотношения:
- (preventable ?а):
- (possibly_preventable ?а);
- (unpreventable ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
39