ГОСТ Р ИС0 18629-41—2011
13.5.1 Subtree_embed
Одно минимальноедереводействийдля ?а может быть встроено вдругое поддерево тогда и только
тогда, когда какой-либо набор событий на дереве с корнями в ?s1 может быть отображен на какой-либо
набор событий на дереве с корнями в ?s2 так. что упорядочивание сохраняется.
(forall (?s1 ?s2 ?а) (iff(subtree_embed ?s1 ?s2 ?a)
(forall (?s3)
(implies (min_precedes ?s1 ?s3 ?a)
(exists (?s4)
(and (min_precedes ?s2 ?s4 ?a)
(iso_occ ?s4 ?s3)))))))
13.5.2 Multiple_outcome
Некотороедействиеявляется многозначным тогда итолько тогда, когда какие-либо два деревадей
ствий могут быть встроены одновдругое.
(forall (?а) (iff(multiple_outcome?а)
(forall (?s1 ?s2)
(implies (and (root ?s1 ?a)
(root ?s2 ?a))
(or (subtree_embed ?s1 ?s2 ?a)
(subtree_ombed ?s2 ?s1 ?a))))))
13.5.3 Weak_outcome
Некоторое действие ?a является слабым тогда и только тогда, когдасуществует минимальное дерево
действий, которое может быть встроено во все прочие минимальныедеревьядействийдля ?а.
(forall (?а) (iff(weak_outcome ?а)
(exists (?s1)
(and (root ?s1 ?a)
(forall (?s2)
(implies(root ?s2 ?a)
(subtree_embed ?s2 ?s1 ?a)))))))
13.5.4 Nondet_outcome
Некоторое действие ?a имеет недетерминированный результат тогдаитолько тогда, когдасуществует
минимальноедереводействий, которое может быть встроено внутрь других минимальныхдеревьевдей
ствий для ?а. При этом существуют отдельныеневстраиваемые ветви.
(forall (?а) (iff(nondet_outcome ?а)
(exists (?s1 ?s2 ?s3)
(and (root ?s1 ?a)
(root ?s2 ?a)
(subtree_embed ?s2 ?s1 ?a)
(root ?s3 ?a)
(forall (?s4)
(implies (root ?s4 ?a)
(not (or (subtree_embed ?s3 ?s4 ?a)
(subtree_embed ?s4 ?s3?a)))))))))
13.5.5 immiscible
Некоторое действие является несмешиваемым тогда итолько тогда, когда никакое издеревьевспек
тра не может быть встроено в какое-либодругоедерево.
(forall (?а) (iff(imiscible ?а)
(forall (?s1 ?s2)
(implies (and (root ?s1 ?a)
(root ?s2 ?a))
(not (or (subtree_embed ?s1 ?s2 ?a)
(subtree_embed ?s2 ?s1 ?a)))))))
13.6 Грамматика перестановочной структуры ветвей
Грамматика описаний процессадля перестановочной структуры ветвей эквивалентна грамматике ут
верждений общего описания технологического процесса в соответствии с ИСО 18629-11.
21