Spectrum and Subtree Containment

Spectrum and Subtree Containment

Extension Name: subtree.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: None

Grammar: subtree.bnf

Definitions

Definition 1 One minimal activity tree for ?a can be embedded into another as a subtree iff any atomic subactivity occurrence in the tree rooted in ?s1 can be mapped to an atomic subactivity occurrence in the tree rooted in ?s2 in such a way that the ordering is preserved. 
(forall (?s1 ?s2 ?a) (iff (subtree_embed ?s1 ?s2 ?a)
(forall (?s3)
        (if	  (min_precedes ?s1 ?s3 ?a)
                  (exists (?s4)
                        (and    (min_precedes ?s2 ?s4 ?a)
				(iso_occ ?s4 ?s3 ?a)))))))
Definition 2 An activity is multiple outcome iff any two activity trees can be embedded into one another. 
(forall (?a) (iff (multiple_outcome ?a)
(forall (?s1 ?s2)
	(if	  (and	(root ?s1 ?a)
			(root ?s2 ?a))
		  (or	(subtree_embed ?s1 ?s2 ?a)
			(subtree_embed ?s2 ?s1 ?a))))))
Definition 3 An activity ?a is weak outcome iff there exists a minimal activity tree that can be embedded into all other minimal activity trees of ?a. 
(forall (?a) (iff (weak_outcome ?a)
(exists (?s1)
	(and	(root ?s1 ?a)
		(forall (?s2)
			(if	  (root ?s2 ?a)
				  (subtree_embed ?s2 ?s1 ?a)))))))
Definition 4 An activity ?a has a nondeterministic outcome iff there exists a minimal activity tree that can be embedded into other minimal activity trees of ?a, and there also exists branches that cannot be embedded. 
(forall (?a) (iff (nondet_outcome ?a)
(exists (?s1 ?s2 ?s3)
	(and	(root ?s1 ?a)
		(root ?s2 ?a)
		(subtree_embed ?s2 ?s1 ?a)
		(root ?s3 ?a)
		(forall (?s4)
			(if	  (root ?s4 ?a)
				  (not (or	(subtree_embed ?s3 ?s4 ?a)
						(subtree_embed ?s4 ?s3 ?a)))))))))
Definition 5 An activity is imiscible iff no tree in the spectrum can be embedded into any other. 
(forall (?a) (iff (imiscible ?a)
(forall (?s1 ?s2)
	(if	  (and	(root ?s1 ?a)
			(root ?s2 ?a))
		  (not (or	(subtree_embed ?s1 ?s2 ?a)
				(subtree_embed ?s2 ?s1 ?a)))))))