Capacity-based Concurrency

Classes of Activities and Resources for Capacity-based Concurrency

Extension Name: capacity.def

Primitive Lexicon: None

Defined Lexicon:

Definitional Extensions Required by this Extension: none

Theories Required by this Extension: requires.th, act_occ.th, complex.th, atomic.th, subactivity.th, disc_state.th, occtree.th, psl_core.th

Definitions

Definition 1 An activity is exclusive use for a resource iff its demand for the resource is equal to its resource point. 
(forall (?a ?r) (iff (exclusive_use ?a ?r)
(forall (?q1 ?q2 ?occ ?occp)
	(if  (and  (do ?a ?occ ?occp)
		   (holds (demand ?a ?r ?q1) ?occ)
		   (holds (resource_point ?r ?q2) ?occ))
	     (= ?q1 ?q2)))))
Definition 2 An activity is capacity-bsed for a resource iff its demand for the resource is less than its resource point. This allows the possibility that multiple activities can share the resource. 
(forall (?a ?r) (iff (capacity_based ?a ?r)
(forall (?q1 ?q2 ?occ ?occp)
	(if     (and    (do ?a ?occ ?occp)
			(holds (demand ?a ?r ?q1) ?occ)
			(holds (resource_point ?r ?q2) ?occ))
		(lesser ?q1 ?q2)))))
Definition 3 A resource is unary if all activities that require it are exclusive use. 
(forall (?r) (iff (unary_resource ?r)
(forall (?a)
	(if  (requires ?a ?r)
		  (exclusive_use ?a ?r)))))
Definition 4 A resource is capacitated if all activities that require it are capacity-based. 
(forall (?r) (iff (capacitated_resource ?r)
(forall (?a)
	(if  (requires ?a ?r)
		  (capacity_based ?a ?r)))))
Definition 5 An activity has uniform demand for a resource iff the demand for the resource is the same in all situations. 
(forall (?a ?r ?q) (iff (uniform_demand ?a ?r ?q) 
(forall (?occ)
	(holds (demand ?a ?r ?q) ?occ))))
Definition 6 An activity is a layout action for a resource iff the demand varies depending on the effects of other activities. 
(forall (?r ?a) (iff (layout ?r ?a)
(forall (?q ?occ1 ?occ2 ?ap)
	(if  (= ?occ2 (successor ?ap ?occ1))
	     (not (iff	(holds (demand ?r ?a ?q) ?occ2)
			(holds (demand ?r ?a ?q) ?occ1)))))))