ГОСТ Р ИСО 18629-42—2011
21.2 Описываемые соотношения основанного на состоянии распределения комплексных
действий
В данном подразделе определены следующие соотношения:
- (trigger ?а);
- (partialjrigger ?а);
- (nontrigger?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
21.3 Теории, обусловленные основанным на состоянии распределением комплексных
действий
Для данной теории необходимы:
- occtree.th;
- psl_core.th.
21.4 Дефинициональные расширения, обусловленные основанным на состоянии
распределением комплексных действий
Для данных расширений необходимы:
- occ_precond.def;
- state_precond.def;
- precond.def.
21.5 Определения основанного на состоянии распределения комплексных действий
Для основанного на состоянии распределения комплексныхдействий определены нижеследующие
понятия.
21.5.1 trigger
Некоторое действие является инициирующим при условии, что если когда-либо два события согласу
ются по состоянию, то они согласуются и по событиям.
(forall (?а) (iff(trigger ?а)
(forall (?осс1 ?осс2)
(implies (and (profile ?осс1 ?а)
(profile ?осс2 ?а)
(state_equiv ?осс1 ?осс2))
(root_equiv ?а ?осс1 ?осс2)))))
21.5.2 partialjrigger
Некоторое действие является частично инициирующим при условии, что существуют события, согла
сующиеся как по состоянию, так и по событиям.
(forall (?а) (iff (partialjrigger ?а)
(and (exists (?ocd)
(forall (?осс2)
(implies (and (profile ?occ1 ?a)
(profile ?occ2 ?a)
(state_equiv ?occ1 ?occ2))
(root_equiv ?a ?occ1 ?occ2))))
(exists (?occ3 ?occ4)
(and (profile ?occ3 ?a)
(profile ?occ4 ?a)
(state_equiv ?occ3 ?occ4)
(not (root_equiv ?a ?occ3 ?occ4)))))))
21.5.3 nontrigger
Некоторое действие является неинициирующим тогда и только тогда, когда сохраняющая события
перестановка переменных является тривиальной.
(forall (?а) (iff(nontrigger ?а)
(forall (?осс1)
(implies (profile ?ocd ?а)
(exists (?осс2)
28