ГОСТ Р ИСО 18629-42—2011
(forall (?а) (iff(periodic ?а)
(forall (?s1 ?s2)
(implies (and
(occurrence ?s1 ?a)
(occurrence ?s2 ?a)
(begin_equiv ?s1 ?s2)
(tree_equiv ?s1 ?s2))
(legal_equiv ?s1 ?s2)))))
11.5.2 intermittent
Некоторое действие является перемежающимся тогда и только тогда, когда допустимые события
зависят от времени выполнения других действий.
(forall (?а) (iff (intermittent ?а)
(exists (?s1)
(and (occurrence ?s1 ?a)
(forall (?s2)
(implies (and
(occurrence ?s2 ?a)
(begin_equiv ?s1 ?s2)
(tree_equiv ?s1 ?s2))
(legal_equiv ?s1 ?s2)))))))
11.5.3 aperiodic
Некоторое действие является апериодическим тогда и только тогда, когда не существует связи меж
ду действительным событием и временем выполнения других действий.
(forall (?а) (iff(aperiodic ?а)
(forall (?s1)
(implies (occurrence ?s1 ?a)
(exists (?s2)
(and
(occurrence ?s2 ?a)
(begin_equiv ?s1 ?s2)
(tree_equiv ?s1 ?s2)
(not (legal_equiv ?s1 ?s2))))))))
11.6 Грамматика периодических входных условий выполнения действий
Следующие грамматические утверждения определяют описания процесса, установленные в KIF для
периодических входных условий выполнения действий.
< periodic_precond >
(forall <?s)
({implies | iff}
(and (occurrence ?s < term >)
(legal ?s)
(ubiquitous < term > < term >)
< simple_time_axiom >)
{< leaf_constrained_axiom > | < inner_constrained_axiom}))
< intermittent_precond > ::=
(forall (?s)
({implies | iff}
(and (occurrence ?s < term >)
(legal ?s)
(ubiquitous < term > < term >)
< time_axiom >)
{< leaf_constrained_axiom > | < inner_constrained_axiom}))
12Входные условия нарушения выполнения действий
Данный раздел характеризует все определения, обусловленные входными условиями нарушения
выполнения действий. Критерий, используемый для классификации указанных действий, зависит или нет
действительное выполнениедействий от состояния до выполнения действий, от времени выполнениядей
ствий и от выполнения других действий.
15