ГОСТ Р ИСО 18629-44 - 2011
- complex.th;
- subactivity.th;
- occtree.th;
- disc.state.th;
- psl..core.th.
9.4 Дефинициональные расширения для действий, обусловленных
набором ресурсов
Для данного расширения необходимо нижеследующее дефинициональное
расширение:
- strong poset.def.
9.5 Определения для действий, обусловленных набором ресурсов
Длядействий,обусловленныхнаборомресурсов,определены
нижеследующие понятия.
9.5.1 nondet_select
Некотороедействиеявляется действиемснедетерминированным
выбором по отношению к какому-либо набору ресурсов ?г1 тогда и только тогда,
когда выполнение данного действия эквивалентно выполнению поддействия,
требующегокакой-либоресурс,являющийсяэлементомнабора,
ассоциированного с набором ?г1.
(forall (?а1 ?г1) (iff (nondet_select ?a1 ?rl)
(forall (?occ)
(iff (occurrence_of ?occ ?a1)
(exists (?r2 ?i ?a2 ?occ2)
(and (subactivity ?a2 ?a1)
(holds (resource_set ?i ?П) (root_occ ?occ))
(holds (in ?r2 ?i) (root_occ ?occ))
(res_requires ?a2 ?r2)
(occurrence_of ?occ2 ?a2)
(subactivity_occurrence ?occ2 ?occ)))))))
9.5.2 nondet_set select
Некоторое действие является действием с недетерминированным
выбором набора по отношению к какому-либо набору ресурсов ?г1 тогда и
только тогда, когда выполнение данного действия эквивалентно выполнению
поддействия, требующего поднабор ресурсов, включающий элементы набора,
23