Commit ffef01a5 authored by Markus Klinik's avatar Markus Klinik
Browse files

making coffee

parent 54850716
......@@ -78,19 +78,31 @@ 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 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.
We used ideas from this paper 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}$.
Model-based testing checks whether an implementation adheres to a specification by repeatedly giving generated lists of input to both the system under test (SUT) and a model.
SUT and model must be state transformer functions of type $\textsc{State} \times \textsc{Input} \to \textsc{State} \times \textsc{Output}$.
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.
A counterexample is a list of inputs that causes the SUT and the model to yield different outputs.
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.
Our plan synthesis algorithm uses the ingredients of model-based testing to find a minimal partial-order plan that leads to a desirable state.
\begin{example}
(Making coffee)
The running example throughout this chapter will be the problem domain of preparing coffee.
A coffee machine needs to be filled with beans and water before it can prepare coffee.
There are three actions: \emph{addBeans}, \emph{addWater}, and \emph{makeCoffee}.
The planner should deduce that in order to have coffee, the plan must consist of first adding beans and water, in any order, and then make coffee.
\qed
\end{example}
We use the facilities of Gast in a creative way to let it compute plans in the following way.
An \textsc{Action} consists of a guarding \textsc{Expression} and a list of \textsc{Assignment}s to state variables.
The \textsc{State} is a record whose fields are different for each domain.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment