ГОСТ Р ИСО 18629-42—2011
- (interfering ?а);
- (imperial ?а);
- (gk>bal_interfere ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
32.3 Теории, обусловленные входными условиями совместных действий
Для данной теории необходимы:
- occtree.th;
- psl_core.th.
32.4 Дефинициональные расширения, обусловленные входными условиями совместных
действий
Для данных расширений необходимы;
- occ_precond.def,
- state_precond.def;
- precond.def.
32.5 Определения входных условий совместных действий
Для входных условий совместных действий определены нижеследующие понятия.
32.5.1 presorved_filter
Действия ?а и ?а1 являются элементами сохраненного фильтра тогда и только тогда, когда допусти
мые события какого-либо супердействия для ?а сохранены указанным составом совместных дей
ствий с ?а1.
(forall (?а ?а1 ?s) (iff (preserved_filter ?а ?а1 ?s)
(forall (?a2)
(implies (subactivity ?a ?a2)
(iff (poss ?a2 ?s)
(poss (cone ?a2 ?a1) ?s))))))
32.5.2 noninterforing
Некоторое действие является непрепятствующим тогда и только тогда, когда каждое неделимоедей
ствие является элементом сохраненного фильтра с ?а.
(forall (?а ?s) (iff (noninterfering ?а ?s>
(forall (?a1)
(implies (atomic ?a1)
(preserved_filter ?a ?a1 ?s)))))
32.5.3 interfering
Некоторое действие является препятствующим тогда и только тогда, когда существует некоторое
неделимое действие, не являющееся элементом некоторого сохраненного фильтра с ?а.
(forall (?а ?s) (iff (interfering ?а ?s)
(exists (?а1)
(and (atomic ?a1)
(not(preserved_filter?a ?a1 ?s))))))
32.5.4 imperial
Некоторое действие является имперским тогда и только тогда, когда не существует неделимогодей
ствия, являющегося элементом сохраненного фильтра с ?а.
(forall (?а ?s) (iff (imperial ?а ?s)
(forall (?а1)
(implies (atomic ?a1)
(not (preserved_filter ?a ?a1 ?s))))))
32.5.5 globaljntorfere
Некоторое действие является глобально препятствующим тогда и только тогда, когда все события
для ?а имеютодинаковые сохраненные фильтры для ?а.
(forall (?а ?s) (iff (global Jnterfere ?a)
(forall (?a1)
(implies (atomic ?a1)
(forall (?s1 ?s2)
(iff (preserved_filter?a?a1 ?s1)
(preserved_filter ?a ?a1 ?s2)))))))
49