ГОСТ Р ИСО 18629-42—2011
7.3 Теории, обусловленные временными входными условиями выполнения действий
Для данныхтеорий необходимы:
- disc_state.th;
- occtree.th;
- psl_core.th.
7.4 Дефинициональныо расширения, обусловленные временными входными условиями
выполнения действий
Для временных входных условий действий требуются нижеследующие дефинициомальные
расширения:
- precond.def:
- start.def.
7.5 Определения временных входных условий выполнения действий
Нижеследующие понятия определены для временных входных условий выполнения действий.
7.5.1 begln_equiv
Два неделимых события эквивалентны по началу выполнения действия (приобретают характеристику
begin_equiv) тогда и только тогда, когда они имеютодинаковое время начала отсчета.
(forall (?s1 ?s2) (iff (begin_equiv ?s1 ?s2)
(= (beginof?s1)(beginof ?s2))))
7.5.2 time_procond
Некотороедействие являетсядействием с временными входными условиями при ограничении: если
два неделимых события на дереве событий согласуются по времени начала отсчета, то они согласуются и
по расширению возможности данногодействия.
(forall (?а) (iff(time_precond ?а)
(forall (?s1 ?s2)
(implies (begin_equiv ?s1 ?s2))
(poss_equiv ?a ?s1 ?s2)))))
7.5.3 partial_time_precond
Некоторое действие является частично ограниченным по времени тогда и только тогда, когда суще
ствуют сохраняющие событие перестановки.
(forall (?а) (iff (partial_time ?а)
(and (exists (?s1)
(forall (?s2)
(implies (begin_equiv?s1 ?s2)
(poss_equiv?a?s1 ?s2))))
(exists (?s3 ?s4)
(and (begin_equrv ?s3 ?s4)
(not (poss_equiv ?a ?s3 ?s4)))))))
7.5.4 rigid_timo
Некоторое действие является жестким временным действием тоща и только тогда, когда перестанов
ка по временной шкале, сохраняющая событие, является тривиальной.
(forall (?а) (iff(rigidjime ?а)
(forall (?s1)
(exists (?s2)
(and (begin_equiv ?s1 ?s2)
(not (poss_equiv ?a ?s1 ?s2)))))))
7.6 Грамматика описаний процесса для временных входных условий выполнения действий
Нижеследующие грамматические утверждения определяют описания процессов и вспомогательные
правила, установленные в KIF для временных входных условий выполнения действий.
< simple_time_precond > ::= (forall (?s)
(implies (and (occurrence ?s < term >)
(legal ?s))
< simple_time_axiom >))) |
8