Duration based on State and Time

Duration based on State and Time

Extension Name: mixed_dur.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: actdur.def, time_precond.def, state_precond.def

Grammar: mixed_dur.bnf

Definitions

Definition 1 An activity is a mixed duration activity iff whenever two occurrences agree on fluents and their beginof timepoints, then they agree on duration. 
(forall (?a) (iff (mixed_duration ?a) 
(forall (?occ1 ?occ2)
        (if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(state_equiv ?occ1 ?occ2)
			(begin_equiv ?occ1 ?occ2))
                  (dur_equiv ?occ1 ?occ2)))))
Definition 2 An activity is a nondeterministically mixed duration activity if and only if there exist fluent and beginof automorphisms that are also duration-preserving. 
(forall (?a) (iff (nondet_mixed_duration ?a) 
(and 	(exists (?occ1) 
		(forall (?occ2)
			(if	  (and	(occurrence_of ?occ1 ?a)
					(occurrence_of ?occ2 ?a)
					(state_equiv ?occ1 ?occ2)
					(begin_equiv ?occ1 ?occ2))
				  (dur_equiv ?occ1 ?occ2))))
	(exists (?occ3 ?occ4)
		(and	(occurrence_of ?occ3 ?a)
			(occurrence_of ?occ4 ?a)
			(begin_equiv ?occ3 ?occ4)
			(state_equiv ?occ3 ?occ4)
			(not (dur_equiv ?occ3 ?occ4)))))))
Definition 3 An activity is a rigid mixed duration activity if and only if the only duration-preserving beginof and fluent automorphism is the trivial one. 
(forall (?a) (iff (rigid_mixed_duration ?a) 
(forall (?occ1)
	(if	  (occurrence_of ?occ1 ?a)
		  (exists (?occ2)
			(and	(occurrence_of ?occ2 ?a)
				(begin_equiv ?occ1 ?occ2)
				(state_equiv ?occ1 ?occ2)
				(not (dur_equiv ?occ1 ?occ2))))))))