Temporal Spread

Embedded Activities: Temporal Spread

Extension Name: spread.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: embedding.def, time_precond.def

Grammar: spread.bnf

Definitions

Definition 1 An activity occurrence ?occ is spread if and only if every subactivity occurrence of ?occ is temporally constrained. 
(forall (?occ) (iff (spread ?occ)
(forall (?a ?s1 ?s2 ?s3)
	(if	  (and	(occurrence_of ?occ ?a)
			(= ?s3 (root_occ ?occ))
			(subactivity_occurrence ?s1 ?occ)
			(iso_occ ?s1 ?s2 ?a)
			(embed_tree ?s1 ?s2 ?s3 ?a)
			(begin_equiv ?s1 ?s2))
		  (subocc_equiv ?s1 ?s2 ?s3 ?a)))))
Definition 2 An activity occurrence ?occ is partially spread if and only if some subactivity occurrences of ?occ are temporally constrained. 
(forall (?occ) (iff (partial_spread ?occ)
(exists (?a ?s ?s1 ?s3 ?s4)
	(and 	(occurrence_of ?occ ?a)
		(= ?s (root_occ ?occ))
		(subactivity_occurrence ?s1 ?occ)
		(forall (?s2)
			(if	  (and	(iso_occ ?s1 ?s2 ?a)
					(embed_tree ?s1 ?s2 ?s ?a)
					(begin_equiv ?s1 ?s2))
				  (subocc_equiv ?s1 ?s2 ?s ?a)))
		(subactivity_occurrence ?s3 ?occ)
		(iso_occ ?s3 ?s4 ?a)
		(begin_equiv ?s3 ?s4)
		(embed_tree ?s3 ?s4 ?s ?a)
		(not (subocc_equiv ?s3 ?s4 ?s ?a))))))
Definition 3 An activity occurrence ?occ is partially tight if and only if none of the subactivity occurrences of ?occ are temporally constrained. 
(forall (?occ) (iff (tight ?occ)
(forall (?s ?s1 ?a)
	(if	  (and	(occurrence_of ?occ ?a)
			(= ?s (root_occ ?occ))
			(subactivity_occurrence ?s1 ?occ))
		  (exists (?s2)
			(and	(iso_occ ?s1 ?s2 ?a)
				(embed_tree ?s1 ?s2 ?s ?a)
				(begin_equiv ?s1 ?s2)
				(not (subocc_equiv ?s1 ?s2 ?s ?a))))))))