\begin{zed}
  ID ::= a | b | unknown
\end{zed}

\begin{circus}
\circchannel enter, leave
\end{circus}

\begin{circus}
\circchannel cash, ticket, change : ID
\end{circus}

\begin{circus}
\circprocess MACHINE \circdef \circbegin \\
	MAC \circdef cash?ident \then ticket.ident \then change.ident \then MAC \\
	\circspot MAC \\
\circend
\end{circus}

\begin{circus}
\circprocess CUSTOMER \circdef ide : ID \circspot \circbegin 
	CUST \circdef iden : ID \circspot (enter \then cash.ide \then (ticket.ide \then change.ide \then \Skip
                                    \extchoice change.ide \then ticket.ide \then \Skip)) \circseq
                leave \then CUST(iden) \\
	\circspot CUST (ide)\\
	\circend
\end{circus}

\begin{circus}
\circprocess CUSTOMERS \circdef CUSTOMER(a) \interleave (CUSTOMER(b) \interleave CUSTOMER(unknown))
\end{circus}

\begin{circus}
\circprocess PAIDPARKINGSPOT \circdef (CUSTOMERS \lpar \lchanset cash, ticket, change \rchanset \rpar MACHINE) 
	\circhide \lchanset cash, ticket, change \rchanset
\end{circus}
