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

generated step function

parent 9e09bb1e
......@@ -85,11 +85,11 @@ The algorithm tries to find a plan that modifies the global state until the stat
This is done by using the model-based testing facility of Gast.
\paragraph{Model-Based Testing}
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}$.
Model-based testing checks whether an implementation adheres to a specification by repeatedly giving generated lists of input to both the implementation under test (IUT) and a model.
IUT 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.
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 yield different outputs.
A counterexample is a list of inputs that causes the IUT 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}
......@@ -152,4 +152,23 @@ The effect of \name{MakeCoffee} removes those units from the state and adds one
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.
In order to employ Gast, we need to take these components and construct an IUT and a model, to which Gast can feed the generated streams of input.
Given a list of action definitions, our preprocessor generates a stepping function that is suitable to be used as a model for Gast.
\begin{example}
(Making coffe, continued)
An excerpt of the step function, generated from the coffee actions, looks as follows.
\begin{CLEAN}
:: Action = AddBeans Int | AddWater Int | MakeCoffee
step :: (State -> Bool) State Action -> [(State, [Bool])]
step pGoal state (AddWater w)
| (w) > (0)
&& ((state.water) + (w)) <= (maxWater)
= [(newState, [pGoal newState])]
where
newState = { state
& water = (state.water) + (w)
}
\end{CLEAN}
\qed
\end{example}
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