ГОСТ Р ИС0 18629-41—2011
(precedes ?s5?s6)
(iso_occ ?s4 ?s1)
(iso_occ ?s5 ?s3)
(iso_occ ?s6 ?s3)
(dead_branch ?s1 ?s4 ?a)
(dead_branch ?s1 ?s6 ?a)))))))
15.5.3 Free
Событиеявляется свободным тогда итолько тогда, когда наэтом жедереве существуют какрасплав
ленные события, так инерасплавленные события. Это все равно что несуществуют необходимые внешние
события.
(forall (?осс) (iff(free ?осс)
(exists (?осс1 ?осс2)
(and (same_tree ?осс?осс1)
(samejree ?осс ?осс2)
(not (fused ?осс1))
(fused ?осс2)))))
15.5.4Assisted
Событие является ассистированным тогда итолько тогда,когда каждое событие на этом же деревене
расплавлено. Это все равночтосуществуют необходимые внешниесобытия.
(forall (?осс) (iff (assisted ?осс)
(forall (?ocd)
(implies (samejree ?осс ?ocd)
(not (fused ?осс1))))))
15.5.5 Helploss
Некоторое действие является беспомощным тогда итолько тогда, когда между какими-либодвумя
событиями существует внешнее событие. Это всеравно когда внешниедействия всегда необходимы,
(forall (?осс) (iff(helpless ?осс)
(forall (?s1 ?s2)
(implies (next_subocc ?s1 ?s2 ?occ)
(exists (?s3)
(and (precedes ?s1 ?s3)
(precedes ?s3 ?s2)
(not (subactivity_occurrence ?s3 ?occ))))))))
15.5.6 Unbound
Событие является несвязанным тогда итолько тогда, когданиодно изсобытий наэтом жедерево не
может быть встроено внутрь мертвой ветви. Это все равно когда запрещенные внешние действия отсут
ствуют.
(forall (?осс) (iff(unbound ?осс)
(forall (?ocd)
(implies (samejree ?ocd ?осс)
(not (embed_occ ?ocd))))))
15.5.7 Bound
Событие является связанным тогда и только тогда, когда на этом же дереве существуют события,
которые могутбыть встроены внутрьмертвой ветви. Это всеравночто существуют запрещенные внешние
действия.
(forall (?осс) (iff(bound ?осс)
(exists (?осс1 ?осс2)
(and (samejree ?осс1 ?осс)
(not (embed_occ ?ocd))
(samejree ?осс2 ?осс)
(embed_occ?осс2)))))
15.5.8 Strict
Событие является строгим тогда итолько тогда, когда все события наэтом жедереве расплавлены.
Это все равночто все внешние события запрещены.
25