ГОСТ Р ИСО 18629-41—2011
6 Недетерминированные действия: перестановочная структура ветвей
Данный раздел характеризует все определения, обусловленные недетерминированными действия
ми: перестановочнаяструктура ветвей.
6.1 Примитивная лексика перестановочной структуры ветвей
Лексика перестановочной структуры ветвей нетребует примитивных соотношений.
6.2 Определяемая лексика понятий перестановочной структуры ветвей
В данном разделеопределены нижеследующие соотношения:
-(branch_monomorphic?a?occ1 ?осс2);
- (branch_automorphic?а ?осс1 ?осс2);
- (permuted ?а);
-(r*ondet_permuted ?а);
-(partial_permuted ?а);
- (simple ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
6.3 Теории ядра, обусловленные перестановочной структурой ветвей
Для данных расширений необходимы:
- act_occ.th;
- complox.th;
- atomic.th;
- subactivity.th:
- occtree.th:
- psl_core.th.
6.4 Дефинициональныо расширения, обусловленные перестановочной структурой ветвей
Для перестановочнойструктуры ветвей дефинициональные расширения нетребуются.
6.5 Определения понятий для перестановочной структуры ветвей
Для перестановочной структуры ветвей определены нижеследующие понятия.
6.5.1 Branch_monomorphic
Одна ветвь минимального дерева действий является мономорфической для другой ветви тогда и
только тогда, когда набор событий наодной ветви может быть встроен внутрь набора событий надругой
ветви.
(forall (?ocd ?occ2)(iff(branch_monomorphic?occ1 ?осс2)
(forall (?s1 ?а)
(implies (and (occurrence_of ?occ1 ?a)
(subactivity_occurrence ?s1 ?occ1))
(exists (?s2)
(and (subactivity_occurrence ?s2 ?occ2)
(mono?s1 ?s2 ?a))))))))
6.5.2 Branch_automorphic
Две ветви минимальногодеревадействий являются автоморфическими поотношению друг кдругу
тогда и только тогда, когда набор событий на одной ветви является перестановкой набора событий на
другой ветви.
(forall (?осс
1
?occ2)(iff(brancfi_automorphic?occ1 ?осс2)
(and(branch_monomorphic?occ1 ?осс2)
(brancb_monomorphic ?осс2 ?осс1))))
6.5.3 Permuted
Событиеявляетсяперестановочным тогда и только тогда,когда набор событий на каждой ветви мини
мальногодеревадействийявляетсяперестановкой набора событий на всех прочих ветвях.
(forall (?осс) (iff(permuted ?осс)
(forall (?осс1 ?осс2)
6