ГОСТР ИС0 18629-43—2011
(and (occurrence
_
of ?s2 ?а)
(delay
_
equiv ?s1 ?s2)
(tree
_
equiv ?s1 ?s2)
(not (legal
_
equiv?s1 ?s2))))))))
13.6 Грамматика описаний процесса для входных условий нарушения выполнения действий
Грамматика описаний процессадля входных условий нарушения выполнения действий.
<occ
_
constrained
_
precond > ::=
(forall (?s)
({implies | iff} (and (occurrence ?s < term >)
(legal ?s)
(ubiquitous < term > < term >))
{< leaf
_
delay
_
axiom > |< inner
_
delay
_
axiom}))
< leaf
_
delay
_
formula > ::= (exists (?occ ?s1)
(and (occurrence ?occ < term >)
(leaf
_
occ?s1 ?occ)
< delayJiteral >
(= ?s (successor < term > ?s1))))
< leaf
_
delay
_
axiom > ::= < leaf
_
delay
_
formula > |
(not <leaf
_
delay
_
formula >)
< inner
_
delay
_
formula > ::= (exists (?occ ?s1 ?s2)
(and (occurrence ?occ <term >)
< delay
_
fiteral >
(subactivity
_
occurrence ?s1 ?occ)
(subactivity
_
occurrence ?s2 ?occ)
(precedes ?s1 ?s)
(precedes ?s ?s2)))
< inner
_
delay
_
axiom > ::= < inner
_
delay
_
formula > |
(not <inner
_
delay
_
formula >)
14 Запланированные встраивающие ограничения
Данный раздел характеризует все определения, обусловленные запланированными встраивающими
ограничениями.
14.1 Примитивная лексика запланированных встраивающих ограничений
Л
ексика запланированныхвстраивающих ограничений не требует никаких примитивных соотноше
ний.
14.2 Описываемая лексика запланированных встраивающих ограничений
Вданном подразделе определены нижеследующие соотношения:
- (scheduled ?осс):
- (partial
_
scheduled ?осс);
- (unscheduled ?осс).
Каждое понятиеопределяется неформальной семантикой и аксиомами KIF.
14.3 Теории ядра, обусловленные запланированными встраивающими ограничениями
Дляданной теории необходимы:
-duration.th;
- act
_
occ.th;
- complex.th;
- atomic .th;
- subactivity.th:
- occtree.th;
- psl
_
core.th.
19