Scheduled Embedding Constraints

Scheduled Embedding Constraints

Extension Name: schedule.def

Primitive Lexicon: None

Theories Required by this Extension: duration.th, 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: schedule.bnf

Definitions

Definition 1 An activity occurrence ?occ is scheduled if and only if every subactivity occurrence of ?occ is delay constrained. 
(forall (?occ) (iff (scheduled ?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)
			(delay_equiv ?s1 ?s2))
		  (subocc_equiv ?s1 ?s2 ?s3 ?a)))))
Definition 2 An activity occurrence ?occ is partially scheduled if and only if some subactivity occurrences of ?occ are delay constrained. 
(forall (?occ) (iff (partial_scheduled ?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)
					(delay_equiv ?s1 ?s2))
				  (subocc_equiv ?s1 ?s2 ?s ?a)))
		(subactivity_occurrence ?s3 ?occ)
		(iso_occ ?s3 ?s4 ?a)
		(delay_equiv ?s3 ?s4)
		(embed_tree ?s3 ?s4 ?s ?a)
		(not (subocc_equiv ?s3 ?s4 ?s ?a))))))
Definition 3 An activity occurrence ?occ is unscheduled if and only if none of the subactivity occurrences of ?occ are delay constrained. 
(forall (?occ) (iff (unscheduled ?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)
				(delay_equiv ?s1 ?s2)
				(not (subocc_equiv ?s1 ?s2 ?s ?a))))))))