Commit 59f4a482 authored by Markus Klinik's avatar Markus Klinik
Browse files

labels for line numbers

parent 89f531a7
......@@ -161,31 +161,31 @@ Given a list of action definitions, our preprocessor generates a stepping functi
\begin{example}
\label{ex:stepFunction}
(Making coffe, continued)
An excerpt of the step function, generated from the coffee actions, looks as follows.
\begin{CLEAN}[numbers=left]
:: Action = AddBeans Int | AddWater Int | MakeCoffee
step :: (State -> Bool) State Action -> [(State, [Bool])]
An excerpt of the code generated from the coffee actions looks as follows.
\begin{CLEAN}[numbers=left,escapechar=@]
:: Action = AddBeans Int | AddWater Int | MakeCoffee@\label{ex:stepFunction:action}@
step :: (State -> Bool) State Action -> [(State, [Bool])]@\label{ex:stepFunction:type}@
step pGoal state (AddWater amount)
| amount > 0
&& state.water + amount <= maxWater
| amount > 0@\label{ex:stepFunction:guard1}@
&& state.water + amount <= maxWater@\label{ex:stepFunction:guard2}@
= [(newState, [pGoal newState])]
where
newState = { state
& water = state.water + amount
& water = state.water + amount@\label{ex:stepFunction:recordUpdate}@
}
step _ state _ = [(state, [False])]
iut = \state action . ([False], state)
iut = \state action . ([False], state)@\label{ex:stepFunction:iut}@
\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}$) (line 2).
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}$) (\cref{ex:stepFunction:type}).
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 that indicates whether the returned state satisfies the goal predicate.
The arguments of actions are translated to constructor arguments for the \textsc{Action} data type (line 1).
The guard expressions are translated to guards (lines 4 and 5).
The effect statements are translated to record updates (line 9).
The arguments of actions are translated to constructor arguments for the \textsc{Action} data type (\cref{ex:stepFunction:action}).
The guard expressions are translated to guards (\cref{ex:stepFunction:guard1,ex:stepFunction:guard2}).
The effect statements are translated to record updates (\cref{ex:stepFunction:recordUpdate}).
The synthesizer uses the step function as model for Gast.
As IUT it uses a dummy that always outputs $\false$ (line 13).
As IUT it uses a dummy that always outputs $\false$ (\cref{ex:stepFunction:iut}).
\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