ГОСТ Р ИС0 18629-41—2011
14.5.3 Dead_branch
Некоторое событие ?s2находится на мертвой ветви поотношению кнекоторому деревудействийдля
?а с корневым событием ?s1 тогда и только тогда, когда событие ?s2 находится на ветви, изоморфной
некоторой ветви встроенного дерева действий. Событие ?s2 является самым ранним мертвымсобытием по
отношению кдереву действийдля ?а с корневым событием ?s1 тогда итолько тогда, когда оно является
последующим элементом события, не являющегося листом надереве действий. При этом на дереве не
существует событий, происходящих позже, чем ?s2.
(forall (?s1 ?s2 ?a) (iff (dead_branch ?s1 ?s2 ?a)
(exists (?a1 ?s3)
(and (root ?s1 ?a)
(min_precedes ?s1 ?s3 ?a)
(not (leaf ?s3?a))
(= ?s2 (successor ?a1 ?s3))
(not (exists (?s4)
(and (precedes ?s3?s4)
(min_precedes?s3 ?s4 ?a))))))))
14.5.4 Dead_occurence
Событиедля внешнегодействия ?s2 является мертвым событием по отношению кдеревудействий
?а с корневым событием ?s1 тогда и только тогда, когда ?s2 находится междудвумя событиямидействий
на мертвой ветви ?а.
(forall (?s1 ?s2 ?а) (iff (dead_occurrence ?s1 ?s2 ?a)
(exists (?s3)
(and (dead_branch ?s1 ?s3 ?a)
(precedes ?s1 ?s2)
(precedes ?s2?s3)))))
14.5.5 Embed_treo
?s1 и ?s2 являются событиями поддействий ?a. которыеявляются элементами тогоже встроенного
дерева событийдля ?а с корнем ?s3.
(forall (?s1 ?s2 ?s3 ?a) (iff(embed_tree ?s1 ?s2 ?s3 ?a)
(exists (?a1 ?a2)
(and (subactivity ?a1 ?a)
(subactivity ?a2 ?a)
(occurrence_of ?s1 ?a1)
(occurrence_of ?s2 ?a2)
(or (live_branch ?s3 ?s1 ?a)
(dead_branch ?s3 ?s1 ?a))
(or (live_branch ?s3?s2 ?a)
(dead_branch ?s3 ?s2?a))))))
14.5.6 Subocc_equiv
Два события ?s1.?s2являются эквивалентными на уровне подсобытия в отношении ?а тогдаи только
тогда, когда они являются элементами тогоже максимально встроенногоподдерева ?ас корневым собы
тием ?s3. и они являются событиями поддействий и согласуются независимо от того, являются ли они
событиями поддействий события ?а.
(forall (?s1 ?s2 ?s3 ?a) (iff (subocc_equiv ?s1 ?s2 ?s3 ?a)
(and (embed_tree ?s1 ?s2 ?s3 ?a)
(iff(min_precedes ?s3 ?s1 ?a)
(min_precedes ?s3 ?s2 ?a))))
14.5.7 Unrestricted
Событие ?occ является несвязанным тогда и только тогда, когда каждая ветвь максимального
встроенного поддерева является живой.
(forall (?осс) (iffunrestricted ?осс)
(forall (?а ?s1 ?s2 ?s3)
(implies (and (occurrence_of ?occ ?a)
(root_occ ?s3 ?occ)
(embedjree ?s1 ?s2 ?s3 ?a))
(subocc_equiv?s1 ?s2 ?s3 ?a)))))
23