Commit 89f531a7 authored by Markus Klinik's avatar Markus Klinik
Browse files

code example line numbers

parent a65b3d40
......@@ -165,27 +165,27 @@ An excerpt of the step function, generated from the coffee actions, looks as fol
\begin{CLEAN}[numbers=left]
:: Action = AddBeans Int | AddWater Int | MakeCoffee
step :: (State -> Bool) State Action -> [(State, [Bool])]
step pGoal state (AddWater w)
| (w) > (0)
&& ((state.water) + (w)) <= (maxWater)
step pGoal state (AddWater amount)
| amount > 0
&& state.water + amount <= maxWater
= [(newState, [pGoal newState])]
where
newState = { state
& water = (state.water) + (w)
& water = state.water + amount
}
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}$).
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).
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 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.
The guard expressions are translated to guards.
The effect statements are translated to record updates.
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 synthesizer gives the step function as model to Gast.
As IUT it uses a dummy that always outputs $\false$.
The synthesizer uses the step function as model for Gast.
As IUT it uses a dummy that always outputs $\false$ (line 13).
\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