ГОСТР ИСО 18629-43—2011
9.5.1 rushhour
Некоторое действие является пиковым при условии: если когда-либо два события согласованы по
моментам времени их начала, то они согласованы ипо продолжительности.
(forall (?а) (iff{rushhour ?а)
(forall (?осс1 ?осс2)
(implies (and (occurrence ?ocd ?а)
(occurrence ?осс2 ?а)
(begin
_
equiv ?осс1 ?осс2))
(dur
_
equiv ?осс1 ?осс2))))
9.5.2 weekend
Некоторое действие является сверхурочным тогда итолько тогда, когда существуют сохраняющие
продолжительность автоморфизмы начала.
(forall (?а) (iff(weekend ?а)
(and (exists (?осс1)
(forall (?осс2)
(implies (and (occurrence ?occ1 ?a)
(occurrence ?occ2 ?a)
(begin
_
equiv?occ1 ?occ2))
(dur
_
equiv ?occ1 ?occ2))))
(exists (?occ3 ?occ4)
(and (occurrence ?occ3 ?a)
(occurrence ?occ3 ?a)
(begin
_
equiv?occ3?occ4)
(not (dur
_
equiv ?occ3 ?occ4)))))))
9.5.3 gridlock
Некоторое действие является тупиковым тогда и только тогда, когда сохраняющий продолжитель
ностьавтоморфизм началаявляется тривиальным.
(forall (?а) (iff(gridlock ?а)
(forall (?ocd)
(implies (occurrence ?ccd ?а)
(exists (?осс2)
(and (occurrence ?осс2?а)
(begin
_
equiv ?осс1 ?осс2)
(not (dur
_
equiv ?осс1 ?осс2))))))))
9.6 Грамматика описаний процесса для временной продолжительности
Нижеследующие грамматические утверждениядаютописания технологического процесса, опреде
ленные в KIFдля временной продолжительности.
< rushhour
_
spec >(forall (?осс)
(implies (and (occurrence ?occ < term >)
< simple
_
time
_
axtom >)
< durationjiteral >))
<weekend
_
spec > ::= (forall (?occ)
(implies (and (occurrence ?occ < term >)
< time
_
axiom >)
< durationJiteral >))|
(forall (?occ)
(implies (and (occurrence ?occ < term >)
<simple
_
time
_
axiom >)
< intervaljiteral >))
10 Временная продолжительность и продолжительность, основанная на
состоянии
Данный раздел характеризует все определения, обусловленные временной продолжительностью и
продолжительностью, основанной насостоянии.
12