{\small\sf class} $GetraenkeAutomat$
\par
\kTypes
\type{\kw{ }Money}{\Nat }
\kFunctions
\begin{fn}[e]{sum}%
\signature{\setof{\Natone } \To \Nat }
\parms*{\Lp s\Rp }
\annlab[o]{GetraenkeAutomat`sum}
\If s = \set{}
\Then \\
0
\Else \\
\Letbe* m \In s \Lin \\
m + \fnapply{sum}{s \Setdiff \set{m}}
\Fi
\end{fn}
\kTypes
\type{\kw{ }Coin}{\const{one} | \const{two} | \const{five} | \const{ten} | \const{twenty} | \const{fifty};}
\type{\kw{ }CoinValues}{Coin \Gmap Money}
\begin{invfn}{cv}\all{c : Coin}{c \In  \Dom cv}
\end{invfn}
\kValues
\val{CoinSet}[\setof{Coin}]{\set{\const{one},\const{two},\const{five},\const{ten},\const{twenty},\const{fifty}};}
\val{WORTH}[CoinValues]{\map{ \\
\const{one} \Mapsto 1,\const{two} \Mapsto 2, \\
\const{five} \Mapsto 5,\const{ten} \Mapsto 10, \\
\const{twenty} \Mapsto 20,\const{fifty} \Mapsto 50}}
\kTypes
\type{\kw{ }Cash}{Coin \Gmap \Nat }
\kFunctions
\begin{fn}[e]{valueOf}%
\signature{Cash \To Money}
\parms*{\Lp ca\Rp }
\annlab[o]{GetraenkeAutomat`valueOf}
\fnapply{sum}{\setcomp{\fnapply{WORTH}{co} \X \fnapply{ca}{co}}{co \In  \Dom ca}};
\end{fn}
\begin{fn}[e]{numOfCoinsInCash}%
\signature{Cash \X Coin \To \Nat }
\parms*{\Lp ca,co\Rp }
\annlab[o]{GetraenkeAutomat`numOfCoinsInCash}
\If co \In  \Dom ca
\Then \\
\fnapply{ca}{co}
\Else \\
0
\Fi;
\end{fn}
\begin{fn}[e]{possibleChanges}%
\signature{Cash \To \setof{Cash}}
\parms*{\Lp ch\Rp }
\annlab[o]{GetraenkeAutomat`possibleChanges}
\setcomp{c}{c : Cash}[\pex{ \Dom c \Subset  \Dom ch} \And  \\
\pex{\all{c-elem \In  \Dom c} \\
{\fnapply{c}{c-elem} \Le \fnapply{ch}{c-elem}}}];
\end{fn}
\begin{fn}[e]{coinCombinations}%
\signature{Money \To \setof{Cash}}
\parms*{\Lp m\Rp }
\annlab[o]{GetraenkeAutomat`coinCombinations}
\setcomp{c}{c : Cash}[\fnapply{valueOf}{c} = m]
\end{fn}
\kTypes
\type{\kw{ }Drink}{Tea-or-coffee | \const{chocolate};}
\begin{record}{Tea-or-coffee}flavor :{\const{tea} | \const{coffee}} \\
white :{\Bool } \\
sweet :{\Bool ; } \\
\end{record}
\type{\kw{ }Ingredient}{\const{tea} | \const{coffee} | \const{chocolate} | \const{milk} | \const{sugar} | \const{water};}
\type{\kw{ }Prices}{Drink \Gmap Money;}
\type{\kw{ }Stock}{Ingredient \Gmap \Nat }
\begin{invfn}{s}\all{i : Ingredient}{i \In  \Dom s}
\end{invfn}
\kValues
\val{Tea-or-coffeeSet}[\setof{Tea-or-coffee}]{\set{\reccons{\kw{mk-} Tea-or-coffee}{\const{tea},\False ,\False }, \\
\reccons{\kw{mk-} Tea-or-coffee}{\const{tea},\False ,\True }, \\
\reccons{\kw{mk-} Tea-or-coffee}{\const{tea},\True ,\False }, \\
\reccons{\kw{mk-} Tea-or-coffee}{\const{tea},\True ,\True }, \\
\reccons{\kw{mk-} Tea-or-coffee}{\const{coffee},\False ,\False }, \\
\reccons{\kw{mk-} Tea-or-coffee}{\const{coffee},\False ,\True }, \\
\reccons{\kw{mk-} Tea-or-coffee}{\const{coffee},\True ,\False }, \\
\reccons{\kw{mk-} Tea-or-coffee}{\const{coffee},\True ,\True }};}
\val{DrinkSet}[\setof{Drink}]{\set{\const{chocolate}} \Union Tea-or-coffeeSet;}
\val{IngredientSet}[\setof{Ingredient}]{\set{\const{tea},\const{coffee},\const{chocolate},\const{milk},\const{sugar},\const{water}};}
\val{INGREDIENTS}[Drink \Gmap \setof{Ingredient}]{\map{\const{chocolate} \Mapsto \set{\const{chocolate},\const{water}}} \Mapmerge  \\
\mapcomp{d \Mapsto  \\
\set{d.flavor,\const{water}} \Union  \\
\pex{\If d.white
\Then \\
\set{\const{milk}}
\Else \\
\set{}
\Fi} \Union  \\
\pex{\If d.sweet
\Then \\
\set{\const{sugar}}
\Else \\
\set{}
\Fi}} \\
{d \In Tea-or-coffeeSet}}
\kInstanceVarDef
\parlinebr
\begin{insvar}
\assdef{balance}{Money}[{0}]
\end{insvar}
\begin{insvar}
\assdef{stock}{Stock}[{\mapcomp{i \Mapsto 0}{i \In IngredientSet}}]
\end{insvar}
\begin{insvar}
\assdef{cups}{\Nat }[{0}]
\end{insvar}
\begin{insvar}
\assdef{takings}{Cash}[{\mapcomp{c \Mapsto 0}{c \In CoinSet}}]
\end{insvar}
\begin{insvar}
\assdef{prices}{Prices}[{\mapcomp{d \Mapsto 0}{d \In DrinkSet}}]
\end{insvar}
\par
\kOperations
\begin{op}[e]{do-service}%
\signature{Stock \X \Nat  \X Cash \X Prices \Oto ()}
\parms{newStock,newCups,newTakings,newPrices}
\annlab[o]{GetraenkeAutomat`do-service}
\isnotyetspec
\begin{precond}
balance = 0
\end{precond} \\

\post{stock = newStock \And  \\
cups = newCups \And  \\
takings = newTakings \And  \\
prices = newPrices}
\end{op}
\kValues
\val{c1}[\seqof*{\Char }]{\Dquote Eine\hspace{0.5em}Muenze\hspace{0.5em}einwerfen \Dquote }
\kOperations
\begin{op}[e]{insertCoin}%
\signature{Coin \Oto ()}
\parms{c}
\annlab[o]{GetraenkeAutomat`insertCoin}
\isnotyetspec
\begin{precond}
\True 
\end{precond} \\

\post{\pex{balance = \old{balance} + \fnapply{WORTH}{c}} \And  \\
\pex{takings = \old{takings} \Override \map{c \Mapsto \fnapply{\old{takings}}{c} + 1}}}
\end{op}
\kValues
\val{c2}[\seqof*{\Char }]{\Dquote Getraenke-Auswahlknopf\hspace{0.5em}betaetigen \Dquote }
\kOperations
\begin{op}[e]{getDrink}%
\signature{Drink \Oto Drink}
\parms{d}
\annlab[o]{GetraenkeAutomat`getDrink}
\isnotyetspec
\begin{precond}
\pex{balance \Ge \fnapply{prices}{d}} \And  \\
\pex{cups > 0} \And  \\
\pex{\all{i \In \fnapply{INGREDIENTS}{d}}{\fnapply{stock}{i} > 0}}
\end{precond} \\

\post{\pex{balance = \old{balance} \Minus \fnapply{prices}{d}} \And  \\
\pex{cups = \old{cups} \Minus 1} \And  \\
\pex{stock = \old{stock} \Override \mapcomp{i \Mapsto \fnapply{\old{stock}}{i} \Minus 1}{i \In \fnapply{INGREDIENTS}{d}}} \And  \\
\pex{RESULT = d}}
\end{op}
\kValues
\val{c3}[\seqof*{\Char }]{\Dquote Restgeld-Auswurfknopf\hspace{0.5em}betaetigen \Dquote }
\kOperations
\begin{op}[e]{getChange}%
\signature{() \Oto Cash}
\parms{}
\annlab[o]{GetraenkeAutomat`getChange}
\isnotyetspec
\begin{precond}
\fnapply{coinCombinations}{balance} \Inter \fnapply{possibleChanges}{takings} \Neq \set{}
\end{precond} \\

\post{\pex{RESULT \In \fnapply{coinCombinations}{balance} \Inter \fnapply{possibleChanges}{takings}} \And  \\
\pex{balance = 0} \And  \\
\pex{\all{c \In  \Dom RESULT}{\fnapply{RESULT}{c} + \fnapply{takings}{c} = \fnapply{\old{takings}}{c}}}}
\end{op}
{\small\sf end} {\it GetraenkeAutomat}

