@@ -77,4 +77,20 @@ Our method relaxes constraints only when tasks are parallelizable.
\subsection{Plan Synthesis Using Generic Programming}
\citet{KoopmanP2009} use the generic programming facilities of the Clean \cite{Plasmeijer2002} programming language to synthesize functions that fulfil a given specification.
\citet{KoopmanP2009} use the generic programming facilities of the Clean programming language \cite{Plasmeijer2002} together with the test framework Gast \cite{Gast} to synthesize functions that fulfil a given specification.
We used the same ideas to synthesize plans, by regarding a plan as a special kind of program with actions in place of instructions.
Actions have an effect on the global state, and the synthesis algorithm uses as specification a predicate on the state.
The algorithm tries to find a plan that modifies the global state until the state fulfils the specification.
This is done by using the model-based testing facility of Gast.
\paragraph{Model-Based Testing}
Model-based testing tests adherence to a specification by repeatedly giving generated lists of input to both the system under test (SUT) and a model.
SUT and models must be state transformer functions of type $\mathit{State}\times\mathit{Input}\to\mathit{State}$.
A model is a reference implementation that implements one particular aspect of the specification.
The programmer has to provide a comparison function that compares two states for differences.
Testing stops when either the search space is exhausted or a counterexample has been found.
A counterexample is a list of inputs that causes the SUT and the model to lead to different states.
Once a counterexample has been found, Gast uses cycle detection and other heuristics to condense it as much as possible into a minimal counterexample.
\paragraph{Model-Based Synthesis}
Our plan synthesis algorithm uses the ingredients of model-based testing to find a minimal plan that leads to a desirable state.
