stuff about the goal predicate

planning.tex

@@ -189,3 +189,9 @@ The synthesizer uses the step function as model for Gast.
 As IUT it uses a dummy that always outputs $\false$ (\cref{ex:stepFunction:iut}).
 \qed
 \end{example}
+
+With these components in place, the plan synthesizer algorithm works as follows.
+Given the step function and the IUT, Gast generates lists of actions of increasing length.
+It feeds each list to both the model and the IUT, and compares their outputs.
+The IUT always returns \false, while the model returns \false\ until the goal predicate is satisfied.
+Once the goal predicate is satisfied, Gast thinks that it found a counterexample and reports the list of actions that leads to the differing output.