Mixed Distribution of Complex Activities

Mixed Distribution of Complex Activities

Extension Name: mixed_distribution.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

Definitional Extensions Required by this Extension: distribution.def, precond.def, start.def

Grammar: mixed_distribution.bnf

Definitions

Definition 1 An activity is a conditional launch activity if and only if whenever two occurrences agree on state and their beginof timepoints, then they agree on the occurrences of the activity. 
 
(forall (?a) (iff (conditional_launch ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(profile ?occ1 ?a)
			(profile ?occ2 ?a)
			(state_equiv ?occ1 ?occ2)
			(begin_equiv ?occ1 ?occ2))
		  (root_equiv ?a ?occ1 ?occ2)))))
Definition 2 An activity is a partial conditional launch activity if and only if there exist occurrences such that whenever they agree on state and their beginof timepoints, then they also agree on the occurrences of the activity. 
 
(forall (?a) (iff (partial_conditional_launch ?a)
(and    (exists (?occ1)
                (forall (?occ2)
                        (if	  (and	(profile ?occ1 ?a)
					(profile ?occ2 ?a)
					(state_equiv ?occ1 ?occ2)
					(begin_equiv ?occ1 ?occ2))
                                  (root_equiv ?a ?occ1 ?occ2))))
        (exists (?occ3 ?occ4)
                (and    (profile ?occ3 ?a)
			(profile ?occ4 ?a)
			(state_equiv ?occ3 ?occ4)
			(begin_equiv ?occ3 ?occ4)
                        (not (root_equiv ?a ?occ3 ?occ4)))))))
Definition 3 An activity is a nontrigger activity if and only if the only occurrence-preserving automorphism that also preserves both state and time is the trivial one. 
(forall (?a) (iff (unconditional_launch ?a)
(forall (?occ1)
	(if	  (profile ?occ1 ?a)
        	  (exists (?occ2)
                	(and    (profile ?occ2 ?a)
				(state_equiv ?occ1 ?occ2)
				(begin_equiv ?occ1 ?occ2)
                        	(not (root_equiv ?a ?occ1 ?occ2))))))))