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

step and iut

parent 953f4b4d
......@@ -100,7 +100,7 @@
% expression syntax
\newcommand{\midd}{\ \mid\ }
\newcommand{\kw}[1]{\mathbf{#1}}
\newcommand{\kw}[1]{\text{\normalfont\sffamily #1}}
\newcommand{\fn}[2]{\kw{fn}\,#1.#2}
\newcommand{\fix}[3]{\kw{fix}\,#1 #2.#3}
\newcommand{\ite}[3]{\kw{if}\ #1\ \kw{then}\ #2\ \kw{else}\ #3}
......
......@@ -159,9 +159,10 @@ In order to employ Gast, we need to take these components and construct an IUT a
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}
\label{ex:stepFunction}
(Making coffe, continued)
An excerpt of the step function, generated from the coffee actions, looks as follows.
\begin{CLEAN}
\begin{CLEAN}[numbers=left]
:: Action = AddBeans Int | AddWater Int | MakeCoffee
step :: (State -> Bool) State Action -> [(State, [Bool])]
step pGoal state (AddWater w)
......@@ -172,9 +173,19 @@ An excerpt of the step function, generated from the coffee actions, looks as fol
newState = { state
& water = (state.water) + (w)
}
step _ state _ = [(state, [False])]
iut = \state action . ([False], state)
\end{CLEAN}
Given a goal predicate ($\textsc{State} \to \textsc{Bool}$) as first argument, the step function becomes a state transformer as required by Gast ($\textsc{State} \times \textsc{Action} \to \textsc{State} \times \textsc{Bool}$).
For technical reasons the step function actually returns a list of states with a list of outputs, but we use it with singleton results, so it should be seen as returning $\textsc{State} \times \textsc{Bool}$.
The output is a Boolean which indicates whether the returned state satisfies the goal predicate.
The arguments of actions are translated to constructor arguments for the \textsc{Action} data type.
The guard expressions are translated to guards.
The effect statements are translated to record updates.
The synthesizer gives the step function as model to Gast.
As IUT it uses a dummy that always outputs $\false$.
\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