2.5 Asserting, Clobbering, Achieving, and Undoing

Conventional planning literature often speaks of clobbering and achieving preconditions of plans [Weld, 1994]. In CHiPs, these notions are slightly different since inconditions can clobber and be clobbered, as seen in the previous section. Formalizing these concepts and another, undoing postconditions, helps us define summary conditions (in Section 3.2). However, it will be convenient to define first what it means to assert a condition. Figure 5 gives examples of executions involved in these interactions, and we define these terms as follows:

Definition 2   $$\begin{array}{@{}l@{}l@{}l} asserts(e_p,\ell,t,h) \equiv &(&... ...ge t = t_f(e_p)) \wedge \\ &(&r(t,h) \vdash \ell) \end{array}$$

Definition 2 states that an execution $e_p$ in a history $h$ asserts a literal at time $t$ if that literal is an effect of $p$ that holds in the state at $t$. Note that that from this point on, beginning in Definition 3, we use brackets [ ] as a shorthand when defining similar terms and procedures. For example, saying ``[$a$, $b$] implies [$c$, $d$]'' means $a$ implies $c$, and $b$ implies $d$. This shorthand will help us avoid repetition, at the cost of slightly more difficult parsing.

Definition 3   $$\begin{array}{@{}l@{}l@{}l} [ach&ieves,clobbers] \_precondit... ...{p''},\neg\ell,t'',h)) \wedge t<t''\leq t_s(e_{p'}) \end{array}$$

Definition 4   $$\begin{array}{@{}l@{}l@{}l} clob&bers\_[in,post]condition(e_... ...] \wedge [t_s(e_{p'})<t<t_s(e_{p'}), t=t_f(e_{p'})] \end{array}$$

Definition 5   $$\begin{array}{@{}l@{}l@{}l} undo&es(e_p,\ell,e_{p'},t,h) \eq... ...'},\neg\ell,t'',h)) \wedge t_f(e_{p'}) \leq t'' < t \end{array}$$

So, an execution achieves or clobbers a precondition if it is the last (or one of the last) to assert the condition or its negation (respectively) before it is required. Likewise, an execution undoes a postcondition if it is the first (or one of the first) to assert the negation of the condition after the condition is asserted. An execution $e$ clobbers an incondition or postcondition of $e'$ if $e$ asserts the negation of the condition during or at the end (respectively) of $e'$. Achieving effects (inconditions and postconditions) does not make sense for this formalism, so it is not defined. Figure 5 shows different ways an execution $e$ achieves, clobbers, and undoes an execution $e'$. $\ell$ and $\neg\ell$ point to where they are asserted or required to be met.

Figure 5: Interval interactions of plan steps