Commit 654f7eac authored by Markus Klinik's avatar Markus Klinik
Browse files

wording

parent bb2365d1
......@@ -85,15 +85,18 @@ 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 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}$.
Model-based testing checks whether an implementation conforms 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}$, where \textsc{State}, \textsc{Input} and \textsc{Output} are different in different scenarios.
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 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}
Our plan synthesis algorithm uses the ingredients of model-based testing to find a minimal partial-order plan that leads to a desirable state.
Our plan synthesis algorithm uses the ingredients of model-based testing to find a partial-order plan that leads to a desirable state.
It works in two steps.
In the first step, model-based testing is used to find a valid plan.
In the second step, dependence analysis is used to relax the plan into a partial order plan.
\begin{example}
(Making coffee)
......@@ -107,14 +110,14 @@ The planner should deduce that in order to have coffee, the plan must consist of
We use the facilities of Gast creatively 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.
Actions are specified in a domain-specific language (DSL) so that they can easily be analyzed.
A pre-processing step translates them to Clean before the synthesis algorithm can be run.
A pre-processing step translates actions into Clean before the synthesis algorithm can be run.
The \textsc{State} is a record whose fields are different for each domain.
\begin{example}
(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.
The following code is a data type definition in Clean.
\begin{CLEAN}
:: State =
{ beans :: Int
......@@ -151,7 +154,7 @@ The effect of \name{MakeCoffee} removes those units from the state and adds one
\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.
A concrete \emph{planning problem} is defined by an initial state and a goal predicate inside a domain.
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.
......
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