Spec 2:  Kurbel
---------------------

The second specification, the Kurbel box office, also allows customers
to book tickets in advance by telephone. However, at the Kurbel when a
customer phones, if there is an available ticket then this is simply
recorded. Only when the customer actually arrives at the box office,
is the ticket allocated.

In the Kurbel specification, $kpool$ is the pool of tickets and $bkd$
denotes whether a ticket has been booked. %Initially, $bkd$ is empty.
The operation $Book$ records a booking provided the customer has not
already booked.  The operation $Arrive$ allocates a ticket to a
customer who has a booking.

\[ Booked ::= yes \bbar no \]

\[ [ Ticket] \]

\begin{sidebyside}
\begin{schema}{Kurbel}
kpool:\pset Ticket\\
bkd: Booked
\end{schema}
\nextside
\begin{schema}{KInit}
Kurbel
\ST
bkd= no
\end{schema}
~
\end{sidebyside}

\begin{sidebyside}
\begin{schema}{KBook}
\Delta Kurbel
\ST
bkd = no\\
kpool \neq \emptyset\\
bkd'= yes \\
kpool' = kpool
\end{schema}
\nextside
\begin{schema}{KArrive}
\Delta Kurbel\\
t!:Ticket
\ST
bkd = yes\\
kpool \neq \emptyset\\
bkd' = no\\
t!\mem kpool\\
kpool'=kpool\setminus \{t!\}
\end{schema}
\end{sidebyside}