Substitutable Resources

Extension Name: subst_res.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:

(superpose_select ?a ?r)
(homogeneous_set ?r ?a)
(set_contention ?r)

Definitional Extensions Required by this Extension: res_set_action.def, states.def

Definitions

(forall (?a ?r) (iff (superpose_select ?a ?r) 
(forall (?a1 ?occ1)
        (if  (and	(occurrence_of ?occ1 ?a)
                        (subactivity ?a1 ?a)
                        (primitive ?a1))
                  (exists (?a2 ?r1 ?occ2)
                        (and    (subactivity ?a1 ?a2)
                                (subactivity ?a2 ?a)
				(occurrence_of ?occ2 ?a2)
                                (holds (resource_subset ?r1 ?r) (root_occ ?occ2))
                                (nondet_select ?a2 ?r1)))))))

A resource set is homogeneous iff it is required by a superpose_select activity.

(forall (?a ?r) (iff (homogeneous_set ?r ?a) 
(exists (?a2)
   	(and    (superpose_select ?a2 ?r)
                (subactivity ?a ?a2)))))

(forall (?a1 ?a2 ?occ)
        (iff    (occurs_over (set_contention ?r) ?occ)
                (if  (and	(subactivity ?a1 (set_contention ?r))
                                (subactivity ?a2 (set_contention ?r)))
                          (and  (requires_set ?a1 ?r)
                                (requires_set ?a2 ?r)
                                (concurrent_superpose (set_contention ?r))))))

(forall (?r ?s)
	(if  (poss (set_contention ?r) ?s)
		  (and	(forall (?a)
				(if  (subactivity ?a (set_contention ?a))
				     (homogeneous_set ?r ?a)))
			(holds (available ?r (set_contention ?r)) ?s))))