The Candymachine was learned using LearnLib. Figure~\ref{fig:candy} shows the 
learned model. In this Figure S0 is the initial state. 

\begin{figure}[H]
	\includegraphics[width=1.7\textwidth,natwidth=2389,natheight=891]{1candyfig.png} 
	\caption{Learned model of the candy machine}
	\label{fig:candy}
\end{figure}

\begin{description} 
	\item[Can you always insert every coin?] Yes, all states have outgoing 
			transitions for \texttt{COIN5} and \texttt{COIN10}.
	\item[How much do you need to pay for a single mars?] 15 coins (S0 to S1 
			with \texttt{COIN10}, S1 to S4 with \texttt{COIN5}, S4 to S0 for a
			Mars).
	\item[How much do you need to pay for a single Snickers?] 15 coins (S0 to S1 
			with \texttt{COIN10}, S1 to S3 with \texttt{COIN10}, S3 to S5 for a
			Snickers, S5 to S1 with \texttt{COIN5}, S5 to S1 for a refund which
			would then equal 10 coins, since S0 to S1 equals 10 coins.).
	\item[How much do you need to pay for a single Bounty?] 20 coins (S0 to S1 
			with \texttt{COIN10}, S1 to S3 with \texttt{COIN10}, S3 to S0 for a
			Bounty).
	\item[Which is the minimum amount of money that you need for TWO Snickers 
			AND a Bounty?] 50 coins (S0 to S1 
			with \texttt{COIN10}, S1 to S3 with \texttt{COIN10}, S3 to S5 for a
			Snickers, S5 to S1 with \texttt{COIN5}, S1 to S3 with 
			\texttt{COIN10}, S3 to S5 for a Snickers, S5 to S1 with 
			\texttt{COIN5}, S1 to S3 with \texttt{COIN10}, S3 to S0 for a
			Bounty)
\end{description}
