Extension Name: state_distribution.def
Primitive Lexicon: None
Defined Lexicon:
Relations:
Definitional Extensions Required by this Extension: distribution.def, state_precond.def
Grammar: state_distribution.bnf
(forall (?a) (iff (trigger ?a) (forall (?occ1 ?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2)))))Definition 2 An activity is a partial trigger activity iff there exist occurrences that agree on state and on the occurrence of the activity.
(forall (?a) (iff (partial_trigger ?a) (and (exists (?occ1) (forall (?occ2) (if (and (profile ?occ1 ?a) (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2)) (root_equiv ?a ?occ1 ?occ2)))) (exists (?occ3 ?occ4) (and (profile ?occ3 ?a) (profile ?occ4 ?a) (state_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 fluent automorphism is the trivial one.
(forall (?a) (iff (nontrigger ?a) (forall (?occ1) (if (profile ?occ1 ?a) (exists (?occ2) (and (profile ?occ2 ?a) (state_equiv ?occ1 ?occ2) (not (root_equiv ?a ?occ1 ?occ2))))))))