ГОСТ Р ИСО 18629-41—2011
14 Встраивающие ограничения для действий
Данный разделхарактеризует все определения, обусловленные встраивающими ограничениями для
действий.
14.1 Примитивная лексика встраивающих ограничений для действий
Лексика встраивающих ограниченийдля действий не требует примитивных соотношений.
14.2 Определяемая лексика встраивающих ограничений для действий
В данном подразделеопределены нижеследующиесоотношения:
- (Iive_branch ?s1 ?s2 ?а):
- (embedded ?s1 ?s2 ?a):
- (dead_branch ?s1 ?s2 ?a);
- (dead_occurrence ?s1 ?s2 ?a);
- (embed_tree ?s1 ?s2 ?s3 ?a):
- (subocc_equiv ?s1 ?s2 ?s3 ?a);
- (unrestricted ?occ).
Каждое понятиеопределяется неформальной семантикой и аксиомой KIF.
14.3 Теории, обусловленные встраивающими ограничениями для действий
Для данной теории необходимы:
- act_occ.th;
- complex.th:
- atomic.th;
- subactivity.th:
- occtree.th:
- psl_core.th.
14.4 Дефинициональные расширения, обусловленные встраивающими ограничениями для
действий
Для встраивающих ограниченийдлядействийдефинициональные расширения нетребуются.
14.5 Определения встраивающих ограничений для действий
Для встраивающих ограничений для действийопределены нижеследующие понятия.
14.5.1 Live_branch
Событие?s2 находится на живой ветви некотороговстроенного дерева действийдля ?а скорнем ?s1
тогда и только тогда, когда оно является событием на указанной ветви.
(forall (?s1 ?s2 ?а) (iff(live_branch ?s1 ?s2 ?a)
(exists (?occ)
(and (occurrence_of ?occ ?a)
(root_occ ?s1 ?occ)
(min_precedes ?s1 ?s2 ?a)))))
14.5.2 Embedded
Событиеявляется элементом положительного максимальноговстроенногоподдерева тогдаитолько
тогда, когда оно является внешним событием, находящимся между двумя событиями на ветке дерева
событий.
(forall (?s1 ?s2 ?а) (iff(embedded ?s1 ?s2 ?a)
(exists (?s3)
(and (root ?s2?a)
(min_precedes ?s2 ?s3?a)
(precedes ?s2 ?s1)
(precedes ?s1 ?s3)
(not (min_precedes ?s1 ?s3 ?a)))))
22