Commit 9e09bb1e authored by Markus Klinik's avatar Markus Klinik
Browse files

domain vs problem

parent c66bc45b
......@@ -86,6 +86,7 @@
\newcommand{\todo}[1]{\textcolor{red}{\emph{Todo: #1}}}
\newcommand*{\name}[1]{\textit{#1}}
\newcommand*{\typename}[1]{\textsc{#1}}
% general math
\newcommand{\set}[1]{\{\,#1\,\}}
......
......@@ -99,7 +99,7 @@ Our plan synthesis algorithm uses the ingredients of model-based testing to find
(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: \name{addBeans}, \name{addWater}, and \name{makeCoffee}.
There are three actions: \name{AddBeans}, \name{AddWater}, and \name{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}
......@@ -111,7 +111,7 @@ A pre-processing step translates them to Clean before the synthesis algorithm ca
The \textsc{State} is a record whose fields are different for each domain.
\begin{example}
(Making coffee)
(Making coffee, continued)
The state in the coffee domain is a record with three fields.
They store the amount of beans and water present in the machine, and how many cups of coffee the machine has already dispensed.
The following code is its data type definition in Clean.
......@@ -125,27 +125,31 @@ The following code is its data type definition in Clean.
The three actions are defined as follows, described below.
They are given in our action description DSL, the format of which should be self-explanatory.
\begin{CLEAN}
Action addWater amount
Action AddWater amount :: Int
(amount > 0 && state.water + amount <= maxWater)
(state.water := state.water + amount)
Action addBeans amount
Action AddBeans amount :: Int
(amount > 0 && state.beans + amount <= maxBeans)
(state.beans := state.beans + amount)
Action makeCoffee
Action MakeCoffee
(state.water >= 2 && state.beans >= 1)
( state.water := state.water - 2
; state.beans := state.beans - 1
; state.haveCoffee := state.haveCoffee + 1
)
\end{CLEAN}
The action \name{addWater} takes one argument, \name{amount}.
The action \name{AddWater} takes one argument, \name{amount}, of type \typename{Int}.
The guard expression checks that the amount is greater than zero, and that adding the amount to the water currently held by the machine does not exceed \name{maxWater}, which is a globally defined constant.
The effect of \name{addWater} adds the given amount to the state's water level.
The effect of \name{AddWater} adds the given amount to the state's water level.
The action \name{addBeans} does the same as \name{addWater}, but for the coffee beans.
The action \name{AddBeans} does the same as \name{AddWater}, but for the coffee beans.
The action \name{makeCoffee} does not have arguments.
The action \name{MakeCoffee} does not have any arguments.
Its guard expression checks that there are at least two units of water and one unit of beans in the machine.
The effect of \name{makeCoffee} removes those units from the state and adds one coffee.
The effect of \name{MakeCoffee} removes those units from the state and adds one coffee.
\qed
\end{example}
The data type definition of a state, together with the actions define a problem \emph{domain}.
A concrete \emph{planning problem} is defined by an initial state and a goal predicate inside the domain.
In order to employ Gast, we need to take these components and construct a SUT and a model, to which Gast can feed the generated streams of input.
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