Duration Constraints on Activity Occurrences

Duration Constraints on Activity Occurrences

Extension Name: actdur.def

Primitive Lexicon: None

Theories Required by this Extension: duration.th, psl_core.th

Defined Lexicon:

Functions:

Predicates: Definitional Extensions Required by this Extension: None

Grammar: actdur.bnf

Definitions

Definition 1 The dur function is the duration between the beginof an activity occurrence and the endof an activity occurrence. 
(forall (?occ) 
	(= (dur ?occ) (duration (beginof ?occ) (endof ?occ))))
Definition 2 The delay function is the duration between the beginof one activity occurrence and the beginof another activity occurrence. 
(forall (?occ1 ?occ2) 
	(= (delay ?occ1 ?occ2) (duration (beginof ?occ1) (beginof ?occ2))))
Definition 3 Two occurrences are duration-equivalent if and only if they have the same duration. 
(forall (?occ1 ?occ2) (iff (dur_equiv ?occ1 ?occ2) 
(= (dur ?occ1) (dur ?occ2))))
Definition 4 Two activity occurrences are delay-equivalent if and only if there exists another activity occurrence with equal delay to the two occurrences. 
(forall (?occ1 ?occ2) (iff (delay_equiv ?occ1 ?occ2)
(exists (?occ)
	(= (delay ?occ ?occ1) (delay ?occ ?occ2)))))
Definition 5 An activity is constant if and only if all occurences have the same duration. 
(forall (?a) (iff (constant ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a))
		  (dur_equiv ?occ1 ?occ2)))))
Definition 6 An activity is interval duration if and only if there exist occurences have the same duration. 
(forall (?a) (iff (interval_duration ?a)
(forall (?occ1)
	(if	  (occurrence_of ?occ1 ?a)
		  (exists (?occ2)
			(and	(occurrence_of ?occ2 ?a)
				(dur_equiv ?occ1 ?occ2)))))))
Definition 7 An activity is variable if and only if all occurrences of the activity that have unequal durations. 
(forall (?a) (iff (variable ?a)
(not (exists (?occ1 ?occ2)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
		(dur_equiv ?occ1 ?occ2))))))