ГОСТ Р ИСО 18629-42—2011
(exists (?а2 ?s3 ?s4)
(and (atomic ?a2)
(begin_equiv ?s3 ?s4)
(preserved_fdter ?a2 ?a ?s3)
(not (preserved_filter ?a2 ?a ?s4)))))))
34.5.6 rigidjntorfere
Некоторое действие препятствует жестко тогда и только тогда, когда для каких-либо согласованных
по времени начала отсчета событий существуют другие сохраненные фильтры.
(forall (?а) (iff(rigidJnterfere ?а)
(forall (?s1)
(exists (?a1 ?s2)
(and (atomic ?a1)
(begin_equtv?s1 ?s2)
(iff(preserved_filter ?a1 ?a ?s1)
(not (proserved_fitter ?a1 ?a ?s2))))))))
34.6 Грамматика описаний процесса для вариации препятствующих входных условий
Грамматика описаний технологического процесса для класса действий, описываемыхдля вариации
препятствующих входных условий, эквивалентна грамматике общего описания технологического процес
са в соответствии с ИСО 18629-11.
35 Вариация эффектов затирания полезных данных
Данный раздел характеризует все определения, обусловленные вариацией эффектов затирания
полезныхданных. Критерий, используемый для классификации указанныхдействий: сохраняются или нет
эффекты заданного неделимогодействия составом совместныхдействий, когда состояние, предшествую
щее выполнению действия, сохраняется.
35.1 Примитивная лексика вариации эффектов затирания полезных данных
Лексика вариации эффектов затирания полезныхданных нетребует примитивных соотношений.
35.2 Описываемые соотношения вариации эффектов затирания полезных данных
В данном подразделе определены следующие соотношения:
- (state_clobber ?а);
- (partial_dobber ?а);
- (unconditional_clobber ?а);
- (time_clobber ?а);
- (sometime_clobber ?а):
- (rig»d_ck>bber ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
35.3 Теории, обусловленные вариацией эффектов затирания полезных данных
Для данных теорий необходимы:
- occtree.th;
- psl_core.th.
35.4 Дсфинициональные расширения, обусловленные вариацией эффектов затирания
полезных данных
Для данных расширений необходимы:
- occ_precond.def;
- statejxecond.def;
- precond.def.
35.5 Определения вариации эффектов затирания полезных данных
Для вариации эффектов затирания полезных данных определены нижеследующие понятия.
35.5.1 state_clobber
Некотороедействие ?а затираетданные о состоянии тогда и только тогда, когда какие-либо согласо
ванные по состоянию события сохраняют те же эффекты.
53