Plans

Embedded Activities: Plans

Extension Name: plan.def

Primitive Lexicon: None

Theories Required by this Extension: 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, state_precond.def

Grammar: plan.bnf

Definitions

Definition 1 An activity tree with root occurrence ?s is a plan if and only if all occurrences of subactivities in the maximal embedded subtree that agree on state also agree on being subactivity occurrences. 
(forall (?s) (iff (plan ?s)
(forall (?a ?s1 ?s2)
	(if	  (and	(root ?s ?a)
			(embed_tree ?s1 ?s2 ?s ?a)
			(state_equiv ?s1 ?s2))
		  (subocc_equiv ?s1 ?s2 ?s ?a)))))
Definition 2 An activity tree with root occurrence ?s is a nondeterministic plan if and only if there exist occurrences of subactivities in the maximal embedded subtree that agree on state and that also agree on being subactivity occurrences. 
(forall (?s) (iff (nondet_plan ?s)
(exists (?a ?s1 ?s3 ?s4)
	(and 	(root ?s ?a)
		(forall (?s2)
			(if	  (and	(embed_tree ?s1 ?s2 ?s ?a)
					(state_equiv ?s1 ?s2))
				  (subocc_equiv ?s1 ?s2 ?s ?a)))
		(state_equiv ?s3 ?s4)
		(embed_tree ?s3 ?s4 ?s ?a)
		(not (subocc_equiv ?s3 ?s4 ?s ?a))))))
Definition 3 An activity tree with root occurrence ?s is an unplan if and only if for every subactivity occurrence, there exists another occurrence of the subactivity that agrees on state but that is not a subactivity occurrence. 
(forall (?s) (iff (unplan ?s)
(forall (?s1 ?a)
	(if	  (root ?s ?a)
		  (exists (?s2)
			(and	(embed_tree ?s1 ?s2 ?s ?a)
				(state_equiv ?s1 ?s2)
				(not (subocc_equiv ?s1 ?s2 ?s ?a))))))))