\documentstyle[12pt,zed-csp]{article}
%\input{big}
\textwidth=6in
\textheight=9in
\oddsidemargin=0.0in
\newcommand{\dfrac}{\displaystyle\frac}
\newcommand{\dint}{\displaystyle\int}
\newcommand{\tendsto}{\rightarrow}
\newcommand{\qu}[1]{\item[{\large\bf#1.}]\hspace{4pt}}
\begin{document}
\thispagestyle{empty}
\begin{center}
\large CT216\hfill TUTORIAL 1\hfill INTRODUCTION TO Z
\end{center}
\begin{center}
{\tt http://www.it.nuigalway.ie/\~{}gettrick/courses/CT216/t1.html }
\end{center}
\hrule
\small
\begin{enumerate}

\qu{1}
Develop a Z specification for bank accounts. Include operations
to make deposits and withdrawals, open and close an account, and
query the balance of an account.

\qu{2} 
Model the booking system for a particular flight. The 
aeroplane has a limited capacity and the flight should not be 
overbooked. The operations should include: a passenger booking
onto the flight; a passenger cancelling his booking; a 
query of how many seats are still available; the production of a 
passenger list. Use the given set [PERSON].

\qu{3} 
A certain brokerage firm specialises in buying and selling 
companies. At a given time, its portfolio of investments is the
set of companies it owns. Based on the State Schema
\begin{schema}{Portfolio}
portfolio: \power COMPANY\\
portfolioSize: \num
\where
portfolioSize = \# portfolio 
\end{schema}
write down schemas for {\tt (i)} buying a company,
{\tt (ii)} selling a company, {\tt (iii)} a combined
operation where we buy one company and sell a different one.



\qu{4}
An antique shop buys and sells items. Model the collection
of antiques in the shop at a given time, and describe operations
to buy and sell antiques, using the basic type $[ANTIQUE]$.

\qu{5}
In the parking example discussed in class, with basic types
$ [PERSON, PARKING\_SLOT] $ our State Schema had the form
\begin{schema}{Parking}
staff: \power PERSON\\
assigned\_to: PARKING\_SLOT \rel PERSON\\
available, occupied: \power PARKING\_SLOT
\where
\ran assigned\_to \subseteq staff
\also
available \cap occupied = \emptyset
\end{schema}
Write schema (with appropriate error handling) to
{\tt (i)} find all parking slots assigned to a particular
person, {\tt (ii)} find all staff that share a particular
parking slot.


\qu{6}
In a certain US city, parking permission requires that the car
is registered and has a parking permit. A parking permit is only
issued to registered cars. Starting with the specification

\begin{zed}
[CAR]
\also
STATUS::= noRegistration | registeredCar | permitHolder
\also
REPORT::= success | alreadyRegistered 
 | permitCancelledAlso | notRegistered \\
\t3 | noPermitsLeft | permitAlready | notPermitHolder
\end{zed}
\begin{axdef}
permitLimit:\nat
\end{axdef}
and the State Schema
\begin{schema}{Reg}
registered, permits: \finset CAR
\where
permits \subseteq registered\\
\#permits \leq permitLimit
\end{schema}
develop schema for each of the following ($\finset$ above stands
for a {\bf finite subset}):

\begin{enumerate}

\item
Registration of a car. Write here 3 schema $ RegOK, Success,
AlreadyRegistered $ with the overall 
structure
\begin{zed}
Registration \defs RegOK \land Success \lor AlreadyRegistered
\end{zed}

\item
Deregistration of a car (4 schema: $ DeregOK, Success, 
DeregPlusPermit, NotRegistered $) 
\begin{zed}
DeRegistration \defs DeregOK \land Success \lor
DeregPlusPermit \lor NotRegistered
\end{zed}

\item
Issuing of a permit:
\begin{zed}
Permit \defs PermitOK \land Success \lor NotRegistered
\lor PermitAlready \lor NoPermitsLeft
\end{zed}

\item
Cancelling a permit:
\begin{zed}
CancelPermit \defs CancelPermitOK \land Success \lor
NotPermitHolder  \lor NotRegistered 
\end{zed}

\item
Enquiring about the status of a car:
\begin{zed}
Enquire \defs (RegisteredOnly \lor PermitHolder \lor
Unregistered) \land Success
\end{zed}


\end{enumerate}


\end{enumerate}
\end{document}