ГОСТ Р ИСО 18629-41—2011
< occurrencejiteral > ::= (occurrence < variable > < term >)
(subactivity_occurrence <variable > <variable >)
<occurrence_formula > ::= < occurrencejiteral > |
(and <occurrencejiteral >*)
< occurrence_sentence > := (exists (< variable >*)
<occurrencejormula >)
< branch_spec > ::= (and (sameJree < variable > ?occ)+
(not (= < variable > ?occ))+)
7 Недетерминированные действия: складная структура ветвей
Данный раздел характеризует все определения, обусловленные недетерминированными действия
ми: складнаяструктура ветвей.
7.1 Примитивная лексика складной структуры ветвей
Лексика складной структуры ветвей не требует примитивных соотношений.
7.2 Определяемая лексика понятий для складной структуры ветвей
Вданном подразделе определены нижеследующие соотношения:
-(branch_homomorphic?occ1 ?осс2);
- (folded ?а);
- (nondctJolded ?а):
- (partial Jolded ?а);
-(rigid ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
7.3 Теории, обусловленные складной структурой ветвей
Для данной теории необходимы:
- act_occ.th;
- complex.th:
- atomic.th;
-subactivity.th;
- occtree.th;
- psl_core.th.
7.4Дофинициональные расширения, обусловленные складной структурой ветвей
Для складной структуры ветвей дефинициоиальныо расширения нетребуются.
7.5 Определения складной структуры ветвей
Для складной структуры ветвей определены нижеследующие понятия.
7.5.1 Branch_homomorphic
Одна ветвь минимального дерева действий является гомоморфической для другой ветви тогда и
только тогда, когда существует отображение набора событий на одной ветви внутрь заданного набора
событий надругой ветви.
(forall (?осс1 ?occ2)(iffbranch_homomorphic?occ1 ?осс2)
(and (same_grove ?осс1 ?осс2)
(forall (?s1 ?а)
(implies (and (occurrence_of ?ocd ?a)
(subactivity_occurrence ?s1 ?occ1))
(exists (?s2)
(subactivity_occurrence?s2 ?occ2)
(hom ?s1 ?s2 ?a)))))))
7.5.2 Folded
Некоторое действие является сложенным тогда итолько тогда, когдасуществует единственная ветвь,
для которой наборсобытий на каждой ветви минимального деревадействий является перестановкой набо
ра событий на указанной единственной ветви.
8