Spec 1: Marlowe
-------------------------
The Marlowe box office allows customers to book tickets in advance by
telephone. When a customer calls, if there is an available ticket then one
is allocated and put to one side for the caller. When the customer arrives,
they are presented with this ticket. $Ticket$ is the set of all tickets, and a
free type adds a possibly null ticket:

\[ [Ticket] \\
 MTicket ::= null \bbar ticket \lang Ticket \rang
\]

The pool of tickets is denoted by $mpool$ and $tkt$ models which tickets have
been allocated. %Initially, no tickets have been allocated.
The operation $Book$ is feasible whenever there are still tickets available
($mpool\neq\emptyset$) and allocates a ticket to the customer.
The operation $Arrive$ issues the ticket but does not change the pool of
tickets.

\begin{sidebyside}
\begin{schema}{Marlowe}
mpool:\pset Ticket\\
tkt: MTicket
\end{schema}
\nextside
\begin{schema}{MInit}
Marlowe'
\ST
tkt' = null
\end{schema}
~
\end{sidebyside}

\begin{sidebyside}
\begin{schema}{MBook}
\Delta Marlowe
\ST
tkt = null\\
mpool\neq\emptyset\\
tkt' \neq null\\
ticket^{-1}(tkt') \in mpool \\
mpool' = mpool \setminus \{ticket^{-1}(tkt') \}
\end{schema}
\nextside
\begin{schema}{MArrive}
\Delta Marlowe\\
t!:Ticket
\ST
tkt \neq null\\
tkt' = null\\
t! = ticket^{-1}(tkt)\\
mpool' = mpool
\end{schema}
\end{sidebyside}