ГОСТР ИС0 18629-43—2011
(implies (and (occurrence ?осс1 ?а)
(occurrence ?осс2 ?а)
(same
_
grove ?осс1 ?осс2)
(branch
_
automorphic ?осс1 ?осс2))
(duralton
_
equiv ?осс1 ?осс2)))))
12.5.2 partial
_
embod
_
duration
Некотороедействие имеет частично встроенную продолжительность тогда итолько тогда, когдасу
ществуют события, для которых все ветви автоморфныхсобытийэтогожедерева имеют одинаковую про
должительность.
(forall (?а) (iff(partial
_
embed
_
duration ?а)
(and (exists (?осс1)
(forall (?осс2)
(implies (and (occurrence ?occ1 ?a)
(occurrence ?occ2 ?a)
(same
_
grove?occ1 ?occ2)
(branch
_
automorphic?occ1 ?occ2))
(dur
_
equiv?occ1 ?occ2))))
(exists (?occ3 ?occ4)
(and (occurrence ?occ3 ?a)
(occurrence ?occ3 ?a)
(same
_
grove ?occ1 ?occ2)
(branch
_
automorphic ?occ1 ?occ2)
(not (dur
_
oquiv ?occ3 ?occ4)))))))
12.5.3 nonembed
_
duration
Некоторое действие имеет невстроенную продолжительность тогда и только тогда, когдадля какого-
либособытия существуют ветви автоморфных событий этого жедерева, имеющие разную продолжитель
ность.
(forall (?а) (iff(nonembed
_
duration ?а)
(exists (?осс1 ?осс2)
(and (occurrence ?осс1 ?а)
(occurrence ?осс2 ?а)
(same
_
grove ?осс1 ?осс2)
(branch
_
automorphic?осс1 ?осс2)
(not (duration
_
equiv ?осс1 ?осс2))))))
12.6 Грамматика упорядочивания и ограничений продолжительности встроенных событий
Грамматика описаний процессадля упорядочивания иограничений продолжительности встроенных
событий.
<embed
_
dur__spec > ::= (forall (?осс)
(implies (and (occurrence ?ccc < term >)
(samejree <variable > ?occ))
<durationjiteral >))
<embed
_
interval
_
spec > ::= (forall (?occ)
(implies (and (occurrence ?occ < term >)
(samejree <variable > ?occ))
< interval
_
axiom >))
13 Входные условия нарушения выполнения действий
Данный раздел характеризует все определения, обусловленные входными условиями нарушения
выполнения действий.
13.1 Примитивная лексика входных условий нарушения выполнения действий
Л
ексика входных условий нарушения выполнениядействий нетребует никаких примитивных соотно
шений.
17