Resource Paths

Resource Paths

Extension Name: res_path.def

Primitive Lexicon: None

Defined Lexicon:

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

Definitional Extensions Required by this Extension: processor.def

Definitions

Definition 1 An activity occurrence ?occ2 is the next processor subactivity occurrence after ?occ1 in an activity ?a iff the output material of ?a1 is the input material of ?a2, and there is no other processor subactivity of ?a which consumes the output material from ?a1, and which occurs between ?a1 and ?a2. 
(forall (?occ1 ?occ2 ?a) (iff (next_processor_path ?occ1 ?occ2 ?a) 
(and	(next_subactivity ?occ1 ?occ2 ?a)
	(exists (?a1 ?a2 ?r)
		(and	(occurrence_of ?occ1 ?a1)
			(occurrence_of ?occ2 ?a2)
			(processor_activity ?a1)
			(processor_activity ?a2)
			(output_material ?r ?a1)
			(input_material ?r ?a2))))))
Definition 2 pro_precedes is a partial ordering over the processor subactivity occurrences of ?a with respect to resource flow. 
(forall (?occ1 ?occ2 ?a) (iff (pro_precedes ?occ1 ?occ2 ?a) 
(and	(soo_precedes ?occ1 ?occ2 ?a)
	(forall (?occ3)
		(if  (and	(soo_precedes ?occ1 ?occ3 ?a)
				(soo_precedes ?occ3 ?occ2 ?a))
			  (exists (?occ4 ?occ5)
				(and	(next_processor_path ?occ4 ?occ3 ?a)
					(next_processor_path ?occ3 ?occ5 ?a))))))))
Definition 3 An activity is a resource path iff the subactivity occurrence ordering is equivalent to the material flow ordering. 
(forall (?a) (iff (resource_path ?a) 
(forall (?occ1 ?occ2)
	(iff	(soo_precedes ?occ1 ?occ2 ?a)
		(pro_precedes ?occ1 ?occ2 ?a)))))
Definition 4 An occurrence is initial processor activity occurrence in an activity ?a iff ?a is a resource path and the occurrence is the root of the subactivity occurrence ordering. 
(forall (?occ ?a) (iff (initial_processor_path ?occ ?a) 
(and	(resource_path ?a)
	(root_soo ?occ ?a))))
Definition 5 An occurrence is a final processor activity occurrence in an activity ?a iff ?a is a resource path and the occurrence is the leaf of the subactivity occurrence ordering. 
(forall (?occ ?a) (iff (final_processor_path ?occ ?a) 
(and	(resource_path ?a)
	(leaf_soo ?occ ?a))))