Embedding Constraints for Activities

Embedding Constraints for Activities

Extension Name: embedding.def

Primitive Lexicon: None

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

Defined Lexicon:

Predicates:

Definitional Extensions Required by this Extension: None

Definitions

Definition 1 An atomic activity occurrence ?s2 is on a live branch of an embedded activity tree for ?a with root ?s1 iff it is a subactivity occurrence on the branch. 
(forall (?s1 ?s2 ?a) (iff (live_branch ?s1 ?s2 ?a)
(exists (?occ)
	(and	(occurrence_of ?occ ?a)
		(= ?s1 (root_occ ?occ))
		(min_precedes ?s1 ?s2 ?a)))))
Definition 2 An activity occurrence is an element of the positive maximal embedded subtree iff it is an external activity occurrence that is between two subactivity occurrences on a branch of the occurrence tree. 
(forall (?s1 ?s2 ?a) (iff (embedded ?s1 ?s2 ?a)
(exists (?s3)
	(and	(root ?s2 ?a)
		(min_precedes ?s2 ?s3 ?a)
		(precedes ?s2 ?s1)
		(precedes ?s1 ?s3)
		(not (min_precedes ?s1 ?s3 ?a))))))
Definition 3 An occurrence ?s2 is on a dead branch with respect to an activity tree for ?a with root occurrence ?s1 iff ?s2 is on a branch that is occurrence isomorphic to a branch of the embedded activity tree. The activity occurrence ?s2 is the earliest dead occurrence with respect to the activity tree for ?a with root occurrence ?s1 if and only if it is the successor of a non-leaf subactivity occurrence in the activity tree but there are no subactivity occurrences of the tree that are later than ?s2. 
(forall (?s1 ?s2 ?a) (iff (dead_branch ?s1 ?s2 ?a)
(exists (?a1 ?s3)
	(and	(root ?s1 ?a)
		(min_precedes ?s1 ?s3 ?a)
		(not (leaf ?s3 ?a))
		(= ?s2 (successor ?a1 ?s3))
		(not (exists (?s4)
			(and	(precedes ?s3 ?s4)
				(min_precedes ?s3 ?s4 ?a))))))))
Definition 4 An external activity occurrence ?s2 is a dead occurrence with respect to the activity tree for ?a with root occurrence ?s1 iff ?s2 is between two activity occurrences on a dead branch for ?a. 
(forall (?s1 ?s2 ?a) (iff (dead_occurrence ?s1 ?s2 ?a)
(exists (?s3)
	(and	(dead_branch ?s1 ?s3 ?a)
		(precedes ?s1 ?s2)
		(precedes ?s2 ?s3)))))
Definition 5 ?s1 and ?s2 are occurrences of subactivities of ?a that are elements of the same embedded activity tree for ?a with root ?s3. 
(forall (?s1 ?s2 ?s3 ?a) (iff (embed_tree ?s1 ?s2 ?s3 ?a)
(exists (?a1 ?a2)
	(and	(subactivity ?a1 ?a)
		(subactivity ?a2 ?a)
		(occurrence_of ?s1 ?a1)
		(occurrence_of ?s2 ?a2)
		(or	(live_branch ?s3 ?s1 ?a)
			(dead_branch ?s3 ?s1 ?a))
		(or	(live_branch ?s3 ?s2 ?a)
			(dead_branch ?s3 ?s2 ?a))))))
Definition 6 Two activity occurrences ?s1,?s2 are subocc equivalent with respect to ?a iff they are elements of the same maximal embedded subtree for ?a with root occurrence ?s3, they are occurrences of subactivities, and they agree on whether or not they are subactivity occurrences of an occurrence of ?a. 
(forall (?s1 ?s2 ?s3 ?a) (iff (subocc_equiv ?s1 ?s2 ?s3 ?a)
(and	(embed_tree ?s1 ?s2 ?s3 ?a)
	(iff	(min_precedes ?s3 ?s1 ?a)
		(min_precedes ?s3 ?s2 ?a)))))
Definition 7 An activity occurrence ?occ is unrestricted iff every branch in the maximal embedded subtree is a live branch. 
(forall (?occ) (iff (unrestricted ?occ)
(forall (?a ?s1 ?s2 ?s3)
        (if	  (and    (occurrence_of ?occ ?a)
                          (= ?s3 (root_occ ?occ))
                          (embed_tree ?s1 ?s2 ?s3 ?a))
                  (subocc_equiv ?s1 ?s2 ?s3 ?a)))))