ГОСТ Р ИСО 18629-44 - 2011
ассоциированного с ?г1.
(forall (?a1 ?r1) (iff (nondet_set_select ?а1 ?rl)
(forall (?occ)
(iff (occurrence_of ?occ ?a1)
(exists (?r2 ?a2)
(and (subactivity ?a2 ?a1)
(holds (resource_subset ?r2 ?rl) (root._occ ?occ))
(res_requires ?a2 ?r2)
(occurrence_of ?occ2 ?a2)
(subactivity_occurrence ?occ2 ?occ)))))))
9.5.3 nondet_quantity_select
Некотороедействиеявляется действиемснедетерминированным
выбором количества по отношению к какому-либо набору ресурсов ?г тогда и
только тогда, когда оно является действием с недетерминированным выбором
набора ресурсов и количество выбранных элементов поднабора равно ?q.
(forall (?а ?r ?q) (iff (nondet_quantity_select ?а ?r ?q)
(and (nondet_set_select ?a ?r)
(=?q (cardinality ?r)))))
9.5.4 requires_set
Некоторое действие требует набор ресурсов ?г тогда и только тогда, когда
каждое поддействие требует некоторый ресурс, являющийся элементом
набора, ассоциированного с ?г.
(forall (?а ?r) (iff (res_requires_set ?а ?г)
(forall (?осс1)
(iff (occurrence_of ?осс1 ?а)
(forall (?а1 ?i)
(implies (and (holds (resource_set ?i ?r) (root_occ ?occ))
(subactivity ?a1 ?a))
(exists (?r1 ?occ2 ?s2)
(and (occurrence_of ?occ2 ?a1)
(holds (in ?r1 ?i) (root_occ ?occ2))
(res_requires ?а1 ?П)
(subactivity_occurrence ?occ1 ?occ1)))))))))
9.5.5 requires_full_ set
Некоторое действие требует полный набор ресурсов ?г тогда и только
тогда, когда каждый ресурс, являющийся элементом набора, ассоциированного
с ?г, обусловлен некоторым поддействием.
(forall (?а ?r) (iff (res_requires_full_set ?а?г)
(forall (?осс1)
(iff (occurrence_of ?осс1 ?а)
(forall (?г1)
(implies (holds (in_resource_set ?r1 ?r) (root„occ ?occ1))
(exists (?al ?occ2)
(and (subactivity ?a1 ?a)
24