ГОСТ Р ИСО 18629-42—2011
(forall (?а ?s) (iff ( clobbering ?а ?s)
(exists (?a1)
(and (atomic ?a1)
(not(preserved_effects?a?a1 ?s)))))
33.5.4 meddling
Некоторое действие является вмешивающимся тогда и только тогда,когда не существует некоторого
неделимогодействия, сохраняющего эффекты для ?а.
(forall (?а ?s) (iff ( meddling ?а ?s)
(forall (?а1)
(implies (atomic ?a1)
(not (preserved_effects ?a ?a1 ?s)))))
33.5.5 global_clobber
(defrelation global_dobber (?a) :=
(forall (?a1)
(implies (atomic ?a1)
(forall (?s1 ?s2)
(iff (preserved_effects?a?a1 ?s1)
(preserved_effects ?a ?a1 ?s2))))))
33.6 Грамматика описаний процесса для эффектов совместных действий
Грамматика описаний технологического процесса для классов действий, описываемых эффектами
совместных действий, эквивалентна грамматике общего описания технологического процесса в соответ
ствии с ИСО 18629-11.
34 Вариация препятствующих входных условий
Данный раздел характеризует все определения, обусловленные вариацией препятствующих вход
ных условий. Критерий, используемый для классификации указанных действий: сохраняются или нет вход
ные условия заданного неделимого действия составом совместных действий, если сохраняется состоя
ние. предшествующее выполнению данных действий.
34.1 Примитивная лексика вариации препятствующих входных условий
Лексика вариации препятствующих входных условий не требует примитивных соотношений.
34.2 Описываемые соотношения вариации препятствующих входных условий
В данном подразделе определены следующие соотношения:
- (state„interfere ?а);
- (partialjnterfere ?а):
- (unconditionaljnterfere ?а);
- (timejnterfere ?а);
- (sometimejnterfere ?а);
- (rigidJnterfere ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
34.3 Теории, обусловленные вариацией препятствующих входных условий
Для данной теории необходимы:
- occtree.th;
- psl_core.th.
34.4 Дсфинициональные расширения, обусловленные вариацией препятствующих входных
условий
Для данных расширений необходимы:
- occ_precond.def:
- state_precond.def:
- precond.def.
51