\documentclass[a4paper]{article}

\usepackage{zed-csp}


\begin{document}
\begin{titlepage}
	   \vspace*{\stretch{1.0}}
	\begin{center}
		\Huge\textbf{Z Specification Example}\\
		\huge\textit{Computer System  Version 1}
	\end{center}
	\vspace*{\stretch{2.0}}
\endtitlepage
	
\end{titlepage}

%Example X schema\\
%Here is a simple specification 


\section{Introduction}
A computer system that has multiple domains:
Admin, Purchase, Retail and Booking.  It also has multiple departments:
Estates, Sales, Management, Office. The following table defines which Department members can login to which Domain.
\begin{center}
	\begin{tabular}{ c c c c c }
		 & Admin & Purchase & Retail & Booking \\ 
		Estates & x & x &  &  \\  
		Sales &  & x & x & x \\
		Management & x & x & x & x \\
		Office & x & x & & \\    
	\end{tabular}
\end{center}
\section{Types}
[EMPLOYEE] set of all uniquely identifiable employees\\

\section{The State of the System}
\begin{schema}{Computer}
	users, loggedIn:\power EMPLOYEE
	\where
	loggedIn \subseteq users
\end{schema} 

\section{Initialisation}
\begin{schema}{InitComputer}
Computer'
\where
loggedIn' = \emptyset\\
users' = \emptyset
\end{schema}


\section{Change State Operations}
\textit{Partial} Operations defined here are:\\
i) Add User\\
ii) Remove User\\
iii) Log in\\
iv)  Log out
\pagebreak


\subsection{Add User}
Adds a new user. It specifies that p? is a member of staff and should not be a member of users before the operation.
It also specifies users' will include the new user, p?
Any implementation should also not allow a change to the loggedIn set after the operation.

\begin{schema}{AddUser}
	\Delta Computer\\
	p? :EMPLOYEE
	\where
	p? \nin users\\
	users' = users \cup \{p?\}\\
	loggedIn' = loggedIn
\end{schema}

\subsection{Remove User}
Removes a user. It specifies that p? is a member of staff and constrains p? to be a member of users before the operation.
It also specifies that p? will be removed from users'.
Any implementation should also ensure that p? is not logged in before the operation. Any implementation should also not allow a change to the loggedIn set after the operation.

\begin{schema}{RemoveUser}
	\Delta Computer\\
	p? :EMPLOYEE
	\where
	p? \in users\\
	users' = users \setminus \{p?\}\\
	p? \nin loggedIn\\
	loggedIn' = loggedIn
\end{schema}


\subsection{Log In}
The basic log in specification is logIn. It specifies that p? is a member of staff and should  be a member of users before the operation. It also specifies that p? should not be a member of loggedIn before the operation.
It also specifies loggedIn' will include the new user, p? after the operation


\begin{schema}{LogIn}
	\Delta Computer\\
	p? :EMPLOYEE
	\where
	p? \in users\\
	p? \nin loggedIn\\
    users' = users\\
    loggedIn'=loggedIn \cup \{p?\}\\
\end{schema}

\pagebreak
\subsection{Log Out}
The basic log out specification is logOut. It specifies that p? is a member of staff and should  be a member of users before the operation. It also specifies that p? should be a member of loggedIn before the operation.
It also specifies that p? will be removed from loggedIn' after the operation and that there will be no change in the set users' after the operation.


\begin{schema}{LogOut}
	\Delta Computer\\
	p? :EMPLOYEE
	\where
	p? \in users\\
	p? \in loggedIn\\
	users' = users\\
	loggedIn'=loggedIn \setminus \{p?\}\\
\end{schema}
\end{document}