ГОСТ Р ИСО 18629-42—2011
32.6 Грамматика описаний процесса для входных условий совместных действий
Грамматика описаний технологического процесса для классов действий, описываемых для вариации
входных условий совместныхдействий, эквивалентна грамматике общего описания технологического про
цесса в соответствии с ИСО 18629-11.
33 Эффекты совместных действий
Данный раздел характеризует все определения, обусловленные эффектами совместныхдействий.
Криторий. используемый для классификации указанныхдействий: сохранены или нет эффекты неделимых
действий составом совместныхдействий.
33.1 Примитивная лексика эффектов совместных действий
Лексика эффектов совместныхдействий не требует примитивных соотношений.
33.2 Описываемые соотношения эффектов совместных действий
В данном разделе определены следующие соотношения:
- (preserved_effect ?а ?а1 ?s);
- (nonclobbering ?а);
- (clobbering ?а):
-(meddling ?а):
- (g(obal_c!obber ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
33.3 Теории, обусловленные эффектами совместных действий
Для данной теории необходимы:
- occtree.th;
- psl_core.th.
33.4 Дефинициональные расширения, обусловленные эффектами совместных действий
Для данных расширений необходимы:
- occ_precond.def,
- state_precond.def;
- precond.def.
33.5 Определения эффектов совместных действий
Для эффектов совместныхдействий определены нижеследующие понятия.
33.5.1 proserved_effoct
Действия ?а и ?а1 сохраняют эффекты тогда и только тогда, когда указанные эффекты событий для
какого-либо супврдействия для ?а сохранены указанным составом совместныхдействий с ?а1.
(forall (?а ?а1 ?s) (iff( preserved_effects ?а ?а1 ?s)
(forall (?a2?f)
(implies (subactivity ?a ?a2)
(iff (holds ?f (successor ?a2 ?s))
(holds ?f (successor (cone ?a2 ?a1)?s))))))
33.5.2 nonclobbering
Некоторое действие ?a не затирает полезные данные тогда и только тогда, когда любое неделимое
действие сохраняет указанные эффекты для ?а.
(forall (?а ?s) (iff ( nondobbering ?а ?s)
(forall (?а1)
(implies (atomic ?a1)
(preserved_effects ?a ?a1 ?s))))
33.5.3 clobbering
Некоторое действие затирает полезные данные тогда и только тогда, когда существует некоторое
неделимое действие, несохраняющее эффекты для ?а.
50