ГОСТ Р ИСО 18629-42—2011
8.5.1 mixed_precond
Некоторое действие является смешанным действием для заданных входных условий при ограниче
нии. если два события согласуются по состоянию и времени начала отсчета, то они согласуются и по
расширениию возможности действий.
(forall (?а) (iff (mixed_precond ?а)
(forall (?s1 ?s2)
(implies (and(state_equiv ?s1 ?s2)
(begin_equiv?s1 ?s2))
(poss_equiv ?a ?s1 ?s2)))))
8.5.2 partial_mixed
Некоторое действие является частично смешанным ограниченным действием тогда и только тогда,
когда существуют сохраняющие событие перестановки.
(forall (?а) (iff(partial_mixed ?а)
(and (exists (?s1)
(forall (?s2)
(implies (and (state_equiv ?s1 ?s2)
(begin_equiv?s1 ?s2))
(poss_equiv?a?s1 ?s2))))
(exists (?s3 ?s4)
(arvd(state_equiv ?s3 ?s4)
(begin_equiv ?s3 ?s4)
(not (poss_equiv ?a ?s3 ?s4)))))))
8.5.3 rigid_mixod
Некоторое действие является жестким смешанным действием тогда и только тогда, когда сохраняю
щая событие перестановка (которая является сразу как текущей перестановкой, так и перестановкой по
временной шкале) является тривиальной.
(forall (?а) (iff(rigid_mixed ?а)
(forall (?s1)
(exists (?s2)
(and (state_equiv ?s1 ?s2)
(begin_equiv ?s1 ?s2)
(not(poss_equiv?a?s1 ?s2)))))))
8.6 Грамматика временных и основанных на состоянии входных условий
Нижеследующие грамматические утверждения определяют описания процесса и вспомогательные
правила, установленные в KIF для временных и основанных на состоянии входных условий.
< simple_mix_precond > ::= (forall (?s)
(implies (and (occurrence ?s < term >)
(legal ?s))
< simple_mix_axiom >))) |
(forall (?s)
(implies (and (legal ?s)
< simple_mix_axiom >)
(legal (successor < term > ?s))))
< mix_precond > .:= (forall (?s)
(implies (and (occurrence ?s < term >)
(legal ?s))
< mix_formula >)))
(= (beginof ?s) < term >) (prior ?s)
(and < simple_mix_literal >*)
({forall | exists} < vanable >*) < simple_mix_formula >)
< simple_mixjiteral > |
(before (beginof ?s) < term >) (prior < term > ?s) |
(before < term > (beginof ?s)) (prior < term > ?s)
<ordered_mix_literal > |
(not < mix_formula >) |
< simple_mix_literal > ::=
< simp»e_mix_formula >
< simple_mix_axiom > ::=
< ordered mix Gteral > ::=
< mix formula > ::=
10