Commit 45f279b1 authored by Markus Klinik's avatar Markus Klinik
Browse files

describe step function

parent 654f7eac
......@@ -173,5 +173,8 @@ An excerpt of the step function, generated from the coffee actions, looks as fol
& water = (state.water) + (w)
}
\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.
\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