Resource Set-based Activities

Resource Set-based Activities

Extension Name: res_set_action.def

Primitive Lexicon: none

Theories Required by this Extension: res_set.th, requires.th, psl_core.th, act_occ.th, subactivity.th,interval.th, complex_act.th, sitcalc.th

Defined Lexicon:

Definitional Extensions Required by this Extension: states.def

Definitions

An activity is a nondeterministic selection activity with respect to a resource set ?r1 iff the occurrence of the activity is equivalent to the occurrence of a subactivity which requires a resource that is an element of the set associated with ?r1. 
(forall (?a1 ?r1) (iff (nondet_select ?a1 ?r1) 
(forall (?occ)
	(iff	(occurrence_of ?occ ?a1)
		(exists (?r2 ?i ?a2 ?occ2)
			(and	(subactivity ?a2 ?a1)
				(holds (resource_set ?i ?r1) (root_occ ?occ))
				(holds (in ?r2 ?i) (root_occ ?occ))
				(requires ?a2 ?r2)
				(occurrence_of ?occ2 ?a2)
				(subactivity_occurrence ?occ2 ?occ)))))))
An activity is a nondeterministic set selection activity with respect to a resource set ?r1 iff the occurrence of the activity is equivalent to the occurrence of a subactivity which requires a subset of resources that are elements of the set associated with ?r1. 
(forall (?a1 ?r1) (iff (nondet_set_select ?a1 ?r1) 
(forall (?occ)
	(iff	(occurrence_of ?occ ?a1)
		(exists (?r2 ?a2 ?occ2)
			(and	(subactivity ?a2 ?a1)
				(holds (resource_subset ?r2 ?r1) (root_occ ?occ))
				(requires ?a2 ?r2)
				(occurrence_of ?occ2 ?a2)
				(subactivity_occurrence ?occ2 ?occ)))))))
An activity is a nondeterministic quantity selection activity with respect to a resource set ?r iff it is a nondeterministic set selection activity, and the cardinality of the selected subset is equal to ?q. 
(forall (?a ?r ?q) (iff (nondet_quantity_select ?a ?r ?q) 
(and	(nondet_set_select ?a ?r)
	(= ?q (cardinality ?r)))))
An activity requires the resource set ?r iff every subactivity requires some resource which is an element of the set associated with ?r. 
(forall (?a ?r) (iff (requires_set ?a ?r) 
(forall (?occ1)
	(iff	(occurrence_of ?occ1 ?a)
		(forall (?a1 ?i)
			(if  (and	(holds (resource_set ?i ?r) (root_occ ?occ1))
					(subactivity ?a1 ?a))
			     (exists (?r1 ?occ2)
				(and	(occurrence_of ?occ2 ?a1)
					(holds (in ?r1 ?i) (root_occ ?occ2))
					(requires ?a1 ?r1)
					(subactivity_occurrence ?occ1 ?occ1)))))))))
An activity requires the full resource set ?r iff every resource which is an element of the set associated with ?r is required by some subactivity . 
(forall (?a ?r) (iff (requires_full_set ?a ?r) 
(forall (?occ1)
	(iff	(occurrence_of ?occ1 ?a)
		(forall (?r1)
			(if  (holds (in_resource_set ?r1 ?r) (root_occ ?occ1))
			     (exists (?a1 ?occ2)
				(and	(subactivity ?a1 ?a)
					(requires ?a1 ?r1)
					(occurrence_of ?occ2 ?a1)
					(subactivity_occurrence ?occ2 ?occ1)))))))))
An activity is a nondeterministic resource activity iff the reason that the activity is nondeterministic is because it is a nondeterministic selection activity with respect to some resource set. 
(forall (?a) (iff (nondet_res_activity ?a) 
(if  (nondet_choice ?a)
     (exists (?r1)
	(nondet_select ?a ?r1)))))