ГОСТ Р ИСО 18629-42—2011
29.3 Теории, обусловленные встроенными действиями: временной разброс
Для данной теории необходимы:
- occtree.th;
- psl_core.th.
29.4 Дефинициональные расширения,обусловленные встроеннымидействиями:
временной разброс
Для данных расширений необходимы:
- occ_precond.def:
- state_precond.def;
- precond.def.
29.5 Определения встроенных действий: временной разброс
Для встроенных действий (временной разброс) определены нижеследующие понятия.
29.5.1 spread
Некоторое событие ?осс является разбросом тогда и только тогда, когда каждое событие ограничено
по времени.
(forall (?осс) (iff(spread ?осс)
(forall (?а ?s1 ?s2 ?s3)
(implies (and (occurrence_of ?occ ?a)
(root_occ ?s3 ?occ)
(subactivityoccurrence ?s1 ?occ)
(iso_occ ?S1 ?s2)
(embedjreo ?s1 ?s2 ?s3 ?a)
(begin_equiv ?s1 ?s2))
(subocc_eQuiv ?s1 ?s2 ?s3 ?a)))))
29.5.2 partial_sPr^ad
Некоторое событие ?occ является частичным разбросом тогда и только тогда, когда некоторые состав
ляющие действия события ?осс ограничены по времени.
(forall (?осс) (iff (partial_spfead ?осс)
(exists (?а ?s ?s1 ?s3 ?s4)
(and (occurrence_of ?occ ?a)
(rootjocc ?s ?occ)
(subactivity_occurrence ?s1 ?occ)
(forall (?s2)
(implies (and (iso_occ ?s1 ?s2)
(embed_tree ?s1 ?s2 ?s ?a)
(begin_equiv ?s1 ?s2))
(subocc_equiv ?s1 ?s2 ?s ?a))))
(subactivityoccurrence ?s3 ?occ)
(iso_occ ?s3 ?s4)
(begin_equiv ?s3 ?s4)
(embedjree ?s3 ?s4 ?s ?a)
(not (subocc_equiv ?s3 ?s4 ?s ?a))))))
29.5.3 tight
Некоторое событие occ? является частично плотным тогда и только тогда, когда ни одно изсоставля
ющих действий события ?осс не ограничено по времени.
(forall (?осс) (iff (tight ?осс)
(forall (?s ?s1 ?a)
(implies (and (occurrenceof?occ ?a)
(root_occ ?s ?occ)
{subactivityoccurrence ?s1 ?occ))
(exists (?s2)
(and (isoocc ?s1 ?s2)
(embedjree ?s1 ?s2 ?s ?a)
(beginoquw ?s1 ?s2)
(not (suboccoqurv ?s1 ?s2 ?s ?a))))))))
40