Strong Partially Ordered Activities

Strong Partially Ordered Activities

Extension Name: strong_posets.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: None

Grammar: strongposets.bnf

Definitions

Definition 1 This relation is used to specify which subactivity occurrences are elements of the same AND-junction. 
(forall (?s1 ?s2 ?a) (iff (same_bag ?s1 ?s2 ?a)
(exists (?s3 ?s4)
	(and	(next_subocc ?s1 ?s3 ?a)
		(iso_occ ?s3 ?s2 ?a)
		(next_subocc ?s2 ?s4 ?a)
		(iso_occ ?s4 ?s1 ?a)))))
Definition 2 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of siblings for ?s. 
(forall (?s ?a) (iff (rotate ?s ?a)
(and	(forall (?s1)
		(if	  (next_subocc ?s ?s1 ?a)
			  (exists (?s2)
				(and	(sibling ?s ?s2 ?a)
					(iso_occ ?s1 ?s2 ?a)))))
	(forall (?s3)
		(if	  (sibling ?s ?s3 ?a)
			  (same_bag ?s ?s3 ?a))))))
Definition 3 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of successors of ?s in the subactivity occurrence ordering. 
(forall (?s ?a) (iff (reflect ?s ?a)
(forall (?s1)
	(iff	(next_subocc ?s ?s1 ?a)
		(next_soo (soomap ?s) (soomap ?s1) ?a)))))
Definition 4 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of successors of ?s in the subactivity occurrence ordering, together with a copy of the siblings of ?s. 
(forall (?s ?a) (iff (flip ?s ?a)
(forall (?s1)
	(iff	(next_subocc ?s ?s1 ?a)
		(or	(next_soo (soomap ?s) (soomap ?s1) ?a)
			(exists (?s2)
				(and	(sibling ?s ?s2 ?a)
					(iso_occ ?s1 ?s2 ?a))))))))
Definition 5 Within the activity tree for ?a containing ?s, the set of next subactivity occurrences is a copy of the set of successors of ?s in the subactivity occurrence ordering, together with a copy of the siblings of ?s that are in the same bag. 
(forall (?s ?a) (iff (turn ?s ?a)
(and	(exists (?s5)
		(and	(sibling ?s ?s5 ?a)
			(same_bag ?s ?s5 ?a)))
	(forall (?s1)
		(if	  (next_subocc ?s ?s1 ?a)
			  (or	(next_soo (soomap ?s) (soomap ?s1) ?a)
				(exists (?s2)
					(and	(sibling ?s ?s2 ?a)
						(iso_occ ?s1 ?s2 ?a)))))))))
Definition 6 A bag is an activity tree in which all elements are rotated. Intuitively, this corresponds to a process flow diagram which contains only AND junctions with no linear orderings. 
(forall (?occ) (iff (bag ?occ) 
(forall (?a ?s ?occ1)
	(if	  (and	(same_grove ?occ ?occ1)
			(occurrence_of ?occ ?a)
			(subactivity_occurrence ?s ?occ1))
		  (rotate ?s ?a)))))
Definition 7 A choice poset is an activity tree in which all elements are reflected. Intuitively, this corresponds to a process flow diagram which contains only OR junctions. 
(forall (?occ) (iff (choice_poset ?occ) 
(forall (?a ?s ?occ1)
	(if	  (and	(same_grove ?occ ?occ1)
			(occurrence_of ?occ ?a)
			(subactivity_occurrence ?s ?occ1))
		  (reflect ?s ?a)))))
Definition 8 A strong poset is an activity tree in which all elements are flipped. Intuitively, this corresponds to a process flow diagram which contains linear orderings within AND junctions. 
(forall (?occ) (iff (strong_poset ?occ) 
(forall (?a ?s ?occ1)
	(if	  (and	(same_grove ?occ ?occ1)
			(occurrence_of ?occ ?a)
			(subactivity_occurrence ?s ?occ1))
		  (flip ?s ?a)))))
Definition 9 A complex poset is an activity tree in which all elements are turned. Intuitively, this corresponds to a process flow diagram which contains both AND and OR junctions. 
(forall (?occ) (iff (complex_poset ?occ) 
(forall (?a ?s ?occ1)
	(if	  (and	(same_grove ?occ ?occ1)
			(occurrence_of ?occ ?a)
			(subactivity_occurrence ?s ?occ1))
		  (turn ?s ?a)))))