ГОСТ Р ИСО 18629-42—2011
23.4 Дефинициональные расширения, обусловленные смешанным распределением
комплексных действий
Для данных расширений необходимы:
- occ_precond.def,
- state_precond.def:
- precond.def.
23.5 Определения смешанного распределения комплексных действий
Определены нижеследующие понятия для смешанного распределения комплексныхдействий.
23.5.1 conditionaljaunch
Некоторое действие является условно запускающим действием при условии, что если и только если
когда-либо два события согласуются по состоянию и по времени начала отсчета, то они согласуются и по
событиям.
(forall (?а) (iff(conditionaljaunch ?а)
(forall (?осс1 ?осс2)
(implies (and (profile ?осс1 ?а)
(profile ?осс2 ?а)
(state_equiv ?осс1 ?осс2)
(begin_equiv ?осс1 ?осс2))
(root_equiv ?а ?осс1 ?осс2)))))
23.5.2 partial_conditional_launch
Некоторое действие является частично условно запускающим действием при условии, что если и
только если существуют события, согласованные по состоянию и по времени начала отсчета, то они также
согласуются и по событиям.
(forall (?а) (iff(partial_conditionalJaunch ?а)
(and (exists (?ocd)
(forall (?осс2)
(implies (and (profile ?occ1 ?a)
(profile ?occ2 ?a)
(state_equiv ?occ1 ?occ2)
(begin_equiv?occ1 ?occ2))
(root_equiv ?a ?occ1 ?occ2))))
(exists (?occ3 ?occ4)
(and (profile ?occ3 ?a)
(profile ?occ4 ?a)
(state_equiv ?occ3 ?occ4)
(begin_equiv ?occ3 ?occ4)
(not (root_equiv ?a ?occ3 ?occ4)))))))
23.5.3 unconditionaljaunch
Некоторое действие является безусловно запускающим тогда и только тогда, когда сохраняющая
событие перестановка, сохраняющая также состояние и время, является тривиальной.
(forall (?а) (iff(unconditionaljaunch ?а)
(forall (?осс1)
(implies (profile ?ocd ?а)
(exists (?осс2)
(and (profile ?осс2 ?а)
(state_equiv ?осс1 ?осс2)
(begin_equiv ?осс1 ?осс2)
(not (root_equiv ?а ?осс1 ?осс2)))))))
23.6 Грамматика описаний процесса для смешанного распределения комплексных действий
Нижеследующие грамматические утверждения определяют описания процесса, установленные в KIF
для смешанного распределения комплексных действий.
< conditionalJaunch_activitiy > ::= (forall (?s ?s2)
(implies < simple_mix_axiom >
<distributionJormula>))
31