ГОСТР ИСО 18629-43—2011
14.4 Дефинициомальные расширения, обусловленные запланированными встраивающими
ограничениями
Для данного расширения необходимы нижеследующиедефинициональные расширения:
- embedding .def;
- time
_
precond.def.
14.5 Определения запланированных встраивающих ограничений
Для запланированных встраивающих ограничений определены нижеследующие понятия.
14.5.1 scheduled
Некоторое событие ?осс запланировано тогда итолькотогда, когда каждоесобытие из?оссограниче
но задержкой.
(forall (?осс) {iff(scheduled ?осс)
(forall (?а ?s1 ?s2 ?s3)
(implies (and (occurrence
_
of ?occ ?a)
(root
_
occ ?s3 ?occ)
(subactivity
_
occurrence ?s1 ?occ)
(iso
_
occ ?s1 ?s2)
(embedjree ?s1 ?s2 ?s3 ?a)
(delay
_
equiv?s1 ?s2))
(subocc
_
equiv?s1 ?s2 ?s3 ?a)))))
14.5.2 partial
_
scheduled
Некоторое событие ?occ запланировано частично тогда итолько тогда, когда некоторые подсобытия
из ?оссограничены задержкой.
(forall (?осс) (iff(partial
_
scheduled ?осс)
(exists (?а ?s ?s1 ?s3 ?s4)
(and (occurrence
_
of ?occ ?a)
(root
_
occ ?s ?occ)
(subactivity jiccurrence ?s1 ?occ)
(forall (?s2)
(implies (and (iso
_
occ ?s1 ?s2)
(embedjree ?s1 ?s2 ?s ?a)
(delay
_
equiv?s1 ?s2))
(subocc
_
equiv ?s1 ?s2 ?s ?a))))
(subactivity
_
occurrence ?s3 ?occ)
(iso
_
occ ?s3 ?s4)
(delay
_
equiv?s3 ?s4)
(embedjree ?s3 ?s4 ?s ?a)
(not (subocc
_
equiv?s3 ?s4 ?s ?a))))))
14.5.3 unscheduled
Некоторое событие ?occ не запланировано тогда итолькотогда, когда ниодно из подсобытий ?оссне
ограничено задержкой.
(forall (?осс) (iff(unscheduled ?осс)
(forall (?s ?s1 ?a)
(implies (and (occurrence
_
of ?occ ?a)
(root
_
occ ?s ?occ)
(subactivity
_
occurrence ?s1 ?occ))
(exists (?s2)
(and (iso
_
occ ?s1 ?s2)
(embed
_
tree ?s1 ?s2 ?s ?a)
(delay
_
equiv ?s1 ?s2)
(not (subocc
_
equiv ?s1 ?s2 ?s ?a))))))))
14.6 Грамматика запланированных встраивающих ограничений
Грамматика описаний процессадля запланированных встраивающихограничений:
< schedule
_
axiom > ::= (forall (?s ?осс < variable >*)
20