\documentstyle[fuzz,italian]{article}
\marginparwidth 0pt
\oddsidemargin -0.2in
\evensidemargin -0.2in
\marginparsep 0pt
\topmargin -0.9in
\textwidth 6.75in
\textheight 9.8in

\begin{document}

\title{CHESSNET - specifiche Z}
\author{Gruppo 3}
\date {}
\maketitle
\begin{center}
{\large
Moris Bellavista, Paolo Gruppioni, \\
Alberto Montresor, Roberto Poggi} \\
\bigskip
a.a. 1993/94
\end{center}
\bigskip
\tableofcontents
\newpage

% ---------------------------------------------------------------------------
\section{Introduzione}
% ---------------------------------------------------------------------------

Questo documento fornisce le specifiche formali in linguaggio {\bf Z} del
sistema {\it ChessNet} a partire dalla descrizione in linguaggio naturale.
Il sistema {\bf \it ChessNet}  \`e un servizio distribuito di ausilio ai
giocatori di scacchi collegati ad Internet. Il sistema \`e stato diviso in
moduli indipendenti che si integrano negli schemi che descrivono i comandi
disponibili. L'elenco dei moduli comprende l'archivio storico delle partite, il
database degli utenti registrati, la gestione della comunicazione fra {\it client}
e {\it server}, la gestione del {\it client} e la gestione del {\it server}.

In questo documento sono stati volutamente omessi gli invarianti negli schemi
che modificano gli stati.

% ---------------------------------------------------------------------------
\section{Definizioni base}
% ---------------------------------------------------------------------------

I tipi $BOOL$ e $STRINGA$ rappresentano l'insieme dei valori booleani e
l'insieme delle stringhe rappresentabili a video. Il tipo $REPORT$ definisce
invece tutti i possibili messaggi di errore. $Successo$ \`e lo schema che
riporta incondizionatamente il buon esito di qualsiasi operazione.
\begin{zed}
  [STRINGA] 
\end{zed}
\begin{syntax}
  	BOOL &::=& TRUE | FALSE\\
	REPORT 	&::=& Utente\_gia\_presente | Utente\_non\_trovato |
			Risultato\_indeterminato | Messaggio\_vuoto \\
		& | & Client\_gia\_collegato | Identificatore\_del\_server\_errato |
			Collegamento\_inesistente \\ 
		& | & Broadcast\_non\_consentito | Comando\_non\_Trovato | Nessun\_Messaggio \\
		& | & Mossa\_Errata | Turno\_sbagliato | Ok
\end{syntax}
\begin{schema}{Successo}
  rep!: REPORT
\where
  rep! = Ok
\end{schema}

Il tipo $SEMIMOSSA$ codifica la semimossa di un giocatore in notazione
algebrica, mentre il tipo $MOSSE$ identifica una sequenza di semimosse.
Sia $POSIZIONE$ l'insieme di tutte le possibili configurazioni della
scacchiera e $STATOSCACCHIERA$ il tipo necessario a descrivere eventuali
condizioni non rappresentabili da una scacchiera (ad es. possibilit\`a di
arrocco). Il tipo $COLORE$ identifica i due colori possibili.
Sia $TEMPO$ il tipo che identifica gli intervalli di tempo calcolati
in secondi, mentre $DATA$ identifica temporalmente ogni partita. Il tipo
$RISULTATO$ descrive il risultato di una partita. \\
Sia $StandardPos$ la posizione che rappresenta la configurazione
iniziale della scacchiera. $IndTempo$ rappresenta un intervallo 
indeterminato di tempo.

\begin{zed}
	[SEMIMOSSA, POSIZIONE, STATOSCACCHIERA, DATA]
\also
	INDICEPARTITA == \nat \\
	MOSSE == \seq SEMIMOSSA \\
	COLORE ::= Bianco | Nero | IndColore \\
	TEMPO == \num \\
	RISULTATO ::= VittoriaBianco | VittoriaNero | Patta | IndRisultato
\end{zed}
\begin{axdef}
	StandardPos: POSIZIONE \\
	IndTempo: TEMPO \\
\end{axdef}

$IND\_POSTA$ \`e l'insieme dei possibili indirizzi {\it Internet} completi
sufficienti per inviare partite o altri messaggi agli utenti registrati
utilizzando la posta elettronica (E-Mail). $ID$ \`e invece un identificatore
univoco dei processi {\it client} o {\it server}, necessario per le comunicazioni
fra essi. $CONTENUTO$ \`e l'insieme delle possibili comunicazioni che avvengono
fra {\it Client} e {\it Server}.\\
Sia $Void$ il contenuto di messaggio vuoto.

\begin{zed}
	[IND\_POSTA, ID, CONTENUTO]
\end{zed}

\begin{axdef}
	Void: CONTENUTO
\end{axdef}

%	VOID &::=& Void \\

$USERNAME$ \`e l'insieme dei possibili {\it username} del servizio. $ELO$ \`e
l'insieme dei possibili punteggi {\it Elo} dei giocatori registrati. Sia
$DATI\_AUX$ l'insieme dei possibili dati ausiliari necessari alla fatturazione
del tempo di collegamento. $EloIniziale$ \`e il punteggio di un utente all'atto
della registrazione, mentre $NonAssegnato$ \`e uno speciale valore che viene
attribuito agli utenti non registrati nell'output di alcuni comandi.

\begin{zed}
	[USERNAME, DATI\_AUX]
\also
	ELO == \num
\end{zed}
\begin{axdef}
	EloIniziale: ELO \\
	NonAssegnato: ELO
\end{axdef}

\subsection{Servizi di sistema}

Si assumono presenti nel sistema tre servizi dipendenti dallo stato 
della macchina. Questi servizi possono essere rappresentati come 
funzioni che non richiedono parametri in input, ma non essendo possibile
in Z definire questo tipo di funzioni, sono state specificate come 
variabili. $WhoAmI$ \`e in grado di determinare l'identificatore del
processo che la chiama; $DataAttuale$ e $OraAttuale$ restituiscono data e
ora attuali.
\begin{axdef}
	WhoAmI: ID \\
	DataAttuale: DATA \\
	OraAttuale: TEMPO
\end{axdef}

% ---------------------------------------------------------------------------
\section{Gestione delle partite}
% ---------------------------------------------------------------------------

Introduciamo in questa sezione gli schemi e le funzioni necessarie per
la gestione delle partite. Innanzitutto, sono necessarie alcune
funzioni base:

Controllo della legalit\`a di una serie di mosse a partire dalla
posizione standard della scacchiera:
\begin{axdef}
  MosseLegali: MOSSE \fun BOOL
\end{axdef}

Introduciamo lo schema $Partita$ che raccoglie le informazioni relative ad
una partita: sequenza delle mosse, username dei giocatori, tempi di sfida
e di gioco, data di inizio ed eventuale risultato

\begin{schema}{Partita}
  Mosse: MOSSE \\
  Giocatori: USERNAME \pinj COLORE \\
  T1, T2: TEMPO \\
  Tempi: USERNAME \pfun TEMPO \\
  Risultato: RISULTATO \\
  Data: DATA
\where
  \#(\dom Giocatori) = 2 \land \dom Giocatori = \dom Tempi \\
  MosseLegali(Mosse) = TRUE
\end{schema}

% ---------------------------------------------------------------------------
\section{Db storico}
% ---------------------------------------------------------------------------

In questa sezione viene introdotto l'archivio $DbStorico$, in cui vengono
memorizzate le partite giocate da coppie di utenti registrati. Su questo
archivio storico \`e possibile effettuare interrogazioni sul nome di uno
o due giocatori.

% ***************************************************************************
\subsection{Definizioni di base}
% ***************************************************************************

Utilizzando lo schema $Partita$ possiamo creare lo schema $DbStorico$
che costituisce l'archivio storico di partite del servizio. Esso non \`e
altro che un insieme di partite registrate, il cui unico vincolo \`e che siano
tutte terminate. Lo schema di inizializzazione consiste semplicemente di un
insieme di partite vuoto.

\begin{schema}{DbStorico}
  Partite: \finset Partita
\where
  \forall p: Partita | p \in Partite @ p.Risultato \neq IndRisultato
\end{schema}

\begin{zed}
  InitDbStorico \defs [DbStorico' | Partite' = \emptyset]
\end{zed}


% ***************************************************************************
\subsection{Inserimento partite nel Db storico}
% ***************************************************************************

Una delle operazioni previste dalla nostra specifica \`e l'inserimento di una
partita nell'archivio storico. Prende in input una $Partita$, che si assumono
essere tutte diverse per la presenza del campo $Data$. Per questo motivo non
vi sono possibili errori.

\begin{schema}{InserisciPartita}
  \Delta DbStorico \\
  NuovaPartita?: Partita
\where
  Partite' = Partite \cup \{NuovaPartita?\}
\end{schema}


% **************************************************************************
\subsection{Reperimento delle partite soddisfacenti una query}
% **************************************************************************

Le query esprimibili nel sistema sono di due tipi: ricerca per singolo
utente e ricerca per coppia di utenti. La nostra specifica prevede un solo
schema a due parametri; nel caso si voglia effettuare una ricerca per
singolo utente \`e sufficiente utilizzare due volte lo stesso $USERNAME$.
\begin{schema}{SearchGames}
  \Xi DbStorico \\
  Sender?: USERNAME \\
  User_1?, User_2?: USERNAME \\
  DestPosta!: \finset USERNAME \\
  Posta!: \finset Partita
\where
  DestPosta! = \{Sender?\} \\
  Posta! = \{~ x:Partita | x \in Partite \land \{User_1?,User_2?\} \subseteq \dom
  x.Giocatori~\}
\end{schema}


% ---------------------------------------------------------------------------
\section{Database degli utenti registrati}
% ---------------------------------------------------------------------------

Questo database contiene le informazioni relative agli
utenti registrati; da esso dipende la gestione del rating e, in parte, la
fatturazione del tempo di collegamento.

% **************************************************************************
\subsection{Definizioni di base}
% **************************************************************************

Il DB degli utenti registrati si avvale di due schemi base; il primo,
$UtenteRegistrato$, contiene le informazioni relative ad un singolo utente,
cio\`e l'indirizzo di posta elettronica, la password, il rating, alcuni dati
ausiliari e il tempo totale di collegamento (gli ultimi due necessari per la
fatturazione); il secondo, $DbRegistrati$, contiene una funzione che mappa gli
$USERNAME$ nell'insieme degli utenti registrati. $PasswordNulla$ rappresenta
l'omissione dell'inserimento della password.

\begin{axdef}
	PasswordNulla: STRINGA
\end{axdef}
\begin{schema}{UtenteRegistrato}
	IndPosta: IND\_POSTA \\
	Password: STRINGA \\
	Elo: ELO \\
	DatiAux: DATI\_AUX \\
	Tempo: TEMPO
\where
	Password \neq PasswordNulla
\end{schema}

\begin{schema}{DbRegistrati}
	Dati: USERNAME \pfun UtenteRegistrato
\end{schema}

\begin{zed}
InitDbRegistrati \defs [DbRegistrati' | Dati' = \emptyset]
\end{zed}

% **************************************************************************
\subsection{Inserimento di un nuovo utente}
% **************************************************************************

Una funzione importante per il Db \`e l'operazione di inserimento, che modifica
la funzione $Dati$ aggiungendo un nuovo $Username$ al suo dominio; questo \`e
espresso nello schema $AddRegistratoOk$, che prende in input i dati relativi
all'utente, tranne il rating iniziale che \`e definito dalla costante $EloIniziale$.\\
L'unico errore che si pu\`o verificare \`e che lo username che si vuole inserire
sia gi\`a presente; questo viene intercettato dallo schema $UtentePresente$.
\begin{schema}{UtentePresente}
  \Xi DbRegistrati \\
  Username?: USERNAME \\
  rep!: REPORT
\where
  Username? \in \dom Dati \\
  rep! = Utente\_gia\_presente
\end{schema}

\begin{schema}{AddRegistratoOk}
  \Delta DbRegistrati \\
  Username?: USERNAME \\
  IndPosta?: IND\_POSTA \\
  Password?: STRINGA \\
  DatiAux?: DATI\_AUX
\where
  Username? \notin \dom Dati \\
  Password? \neq PasswordNulla
\also
  \exists_1 r:UtenteRegistrato | r.Elo = EloIniziale \land r.IndPosta = IndPosta? \land {} \\
\t1	r.Password = Password? \land r.DatiAux = DatiAux? \land r.Tempo = 0 @ {} \\
\t2		Dati' = Dati \cup \{ Username? \mapsto r \}
\end{schema}

\begin{zed}
AddRegistrato \defs (AddRegistratoOk \land Successo) \lor UtentePresente
\end{zed}


% **************************************************************************
\subsection{Aggiornamento del punteggio ELO}
% **************************************************************************

Al termine di una partita i cui giocatori sono entrambi registrati i rating
devono essere aggiornati; questo viene effettuato nello schema $AggiornaEloOk$.
Il calcolo dei nuovi punteggi \`e realizzato dalla funzione $CalcolaElo$, che
\`e definita in modo assiomatico. Per modificare il punteggio ELO di un utente
si utilizza la funzione $ModificaElo$, che prende in input un $UtenteRegistrato$
e un punteggio Elo e restituisce un $UtenteRegistrato$ identico al primo, tranne
nel campo $Elo$ che assume il nuovo valore. \\
Gli errori possibili sono: gli utenti non sono registrati e il risultato della
partita \`e indeterminato, rappresentati negli schemi $UtenteAssente$ e
$RisultatoIndeterminato$.

\begin{axdef}
  CalcolaElo: ELO \cross ELO \cross RISULTATO \pfun ELO \cross ELO
\where
  \forall x:ELO @ (NonAssegnato,x) \notin \ran CalcolaElo \land
  (x,NonAssegnato) \notin \ran CalcolaElo
\end{axdef}

\begin{axdef}
  ModificaElo: UtenteRegistrato \cross ELO \pfun UtenteRegistrato
\where
  \forall x: UtenteRegistrato; Elo:ELO | Elo \neq NonAssegnato @ (\exists y: UtenteRegistrato @ \\
\t1	y.IndPosta = x.IndPosta \land y.Password = x.Password \land y.DatiAux =	x.DatiAux \land {}\\
\t1	y.Tempo = x.Tempo \land y.Elo = Elo \land ModificaElo(x,Elo) = y)
\end{axdef}

\begin{schema}{AggiornaEloOk}
  \Delta DbRegistrati \\
  Risultato?: RISULTATO \\
  UserB?, UserN?: USERNAME
\where
  \{ UserB?, UserN? \} \subseteq \dom Dati \\
  Risultato? \neq IndRisultato
\also
  \exists EloB, EloN: ELO | \\
\t1	CalcolaElo((Dati(UserB?)).Elo, (Dati(UserN?)).Elo, Risultato?) = (EloB, EloN) @ \\
\t2 		Dati' = Dati \oplus \{ UserB? \mapsto ModificaElo(Dati(UserB?), EloB), \\
\t6		UserN? \mapsto ModificaElo(Dati(UserN?), EloN) \}
\end{schema}

\begin{schema}{UtenteAssente}
  \Xi DbRegistrati \\
  Username?: USERNAME \\
  rep!: REPORT
\where
  Username? \notin \dom Dati \\
  rep! = Utente\_non\_trovato
\end{schema}

\begin{schema}{RisultatoIndeterminato}
  \Xi DbRegistrati \\
  Risultato?: RISULTATO \\
  rep!: REPORT
\where
  Risultato? = IndRisultato \\
  rep! = Risultato\_indeterminato
\end{schema}

\begin{zed}
AggiornaElo \defs (AggiornaEloOk \land Successo) \lor RisultatoIndeterminato \lor {} \\
	\t1 UtenteAssente[UserB?/Username?] \lor UtenteAssente[UserN?/Username?]
\end{zed}


% **************************************************************************
\subsection{Aggiornamento del tempo globale di collegamento}
% **************************************************************************

Alla chiusura di un collegamento, \`e necessario incrementare il tempo totale
di utilizzo del sistema da parte dell'utente. Si introduce cos\`i lo schema
$AggiornaTempoOk$, che prende in input lo username dell'utente che ha chiuso
il collegamento e la durata dello stesso; se l'utente \`e registrato, il campo
$Tempo$ viene aumentato del necessario. Per effettuare la modifica si utilizza
la funzione $ModificaTempo$, simile alla $ModificaElo$ vista in precedenza.

\begin{axdef}
  ModificaTempo: UtenteRegistrato \cross TEMPO \pfun UtenteRegistrato
\where
  \forall x: UtenteRegistrato; AddTempo: TEMPO | AddTempo \neq IndTempo
		@ (\exists y:UtenteRegistrato @ \\
\t1	y.IndPosta = x.IndPosta \land y.Password = x.Password \land y.DatiAux = x.DatiAux \land {} \\
\t1	y.Elo = x.Elo \land y.Tempo = x.Tempo + AddTempo \land ModificaTempo(x,AddTempo) = y)
\end{axdef}

\begin{schema}{AggiornaTempoOk}
  \Delta DbRegistrati \\
  Username?: USERNAME \\
  Tempo?: TEMPO
\where
  Username? \in \dom Dati \\
  Dati' = Dati \oplus
	\{ Username? \mapsto ModificaTempo(Dati(Username?), Tempo?) \}
\end{schema}

\begin{zed}
AggiornaTempo \defs (AggiornaTempoOk \land Successo) \lor UtenteAssente
\end{zed}

% **************************************************************************
\subsection{Lettura della Toplist}
% **************************************************************************

Il Db degli utenti registrati permette anche di estrarre una graduatoria
dei primi cento punteggi $ELO$ presenti in archivio. La lista estratta ha
cardinalit\`a cento se nell'archivio vi sono pi\`u di cento utenti,
altrimenti comprende tutti gli utenti nell'archivio.

\begin{schema}{TopList}
  \Xi DbRegistrati \\
  Lista!: \seq (USERNAME \cross ELO)
\where
	Lista! = \{~f: \seq (USERNAME \cross ELO); x_1, x_2: USERNAME;
		y_1, y_2: ELO; i,j: \nat | \\
\t1	\{x_1,x_2\} \subseteq \dom Dati \land (Dati(x_1)).Elo = y_1 \land
		(Dati(x_2)).Elo = y_2 \land {} \\
\t1	(i<j) \land (f(i)=(x_1,y_1)) \land (f(j)=(x_2,y_2)) \land 
	(y_1 > y_2) \land i \in 1 \upto 100 @ i \mapsto (x_1,y_1)~\}
\end{schema}

% **************************************************************************
\subsection{Lettura dati in fase di connessione}
% **************************************************************************

In fase di connessione verranno eseguiti due controlli sul Db degli utenti
registrati: uno la presenza di un certo $USERNAME$, l'altro \`e la
corrispondenza della Password digitata dall'utente con quella registrata.
{\it ConsultaDbRegistrati} viene utilizzato per leggere le informazioni di un
insieme di giocatori.

\begin{schema}{Registrato}
  \Xi DbRegistrati \\
  Username?,Username!: USERNAME \\
  Presente!: BOOL
\where
  Username! = Username? \\
  Presente! = \IF Username? \in \dom Dati \THEN TRUE \ELSE FALSE
\end{schema}

\begin{schema}{VerificaPass}
  \Xi DbRegistrati \\
  Username?: USERNAME \\
  Passwd?: STRINGA ; Corretta!: BOOL
\where
  Corretta! = \IF Username? \in \dom Dati \land (Dati(Username?)).Password = Passwd? \\
\t5		\THEN TRUE \ELSE FALSE
\end{schema}

\begin{schema}{ConsultaDbRegistrati}
  \Xi DbRegistrati \\
  Nomi?: \finset USERNAME \\
  Info!: USERNAME \pfun UtenteRegistrato
\where
  Info! = Nomi? \dres Dati
\end{schema}


% ---------------------------------------------------------------------------
\section{COMUNICAZIONE}
% ---------------------------------------------------------------------------

\subsection{Definizioni di base}

La comunicazione mediante la rete viene vista a questo livello come uno spazio
condiviso dove ogni macchina ({\it client} o {\it server} indifferentemente)
pu\`o scrivere
o leggere messaggi. Ogni messaggio \`e una tripla ordinata dove la prima
componente individua il mittente, la seconda il destinatario e la terza il
contenuto vero e proprio.
\begin{zed}
	MESSAGGI == ID \cross ID \cross CONTENUTO
\end{zed}
Si utilizza un buffer condiviso dove i messaggi sono collegati
in sequenza in modo da mantenere un ordinamento FIFO fra gli stessi.
L'ordinamento \`e rilevante solamente per i messaggi che hanno la stessa coppia
($mittente$, $destinatario$).
I messaggi possono essere scambiati solamente fra macchine collegate.
Il collegamento fra le macchine viene espresso mediante un insieme di
coppie ordinate che ad ogni istante esprime fra quali macchine \`e
stato aperto il collegamento. La prima componente individua il {\it server}
mentre la seconda individua il {\it client}.
\begin{zed}
	COLLEGAMENTI == ID \cross ID
\end{zed}
Definiamo inoltre le funzioni $MsgSender$, $MsgReceiver$ e $MsgText$ che
restituiscono rispettivamente il mittente, il destinatario e il contenuto di
uno specifico messaggio.
\begin{axdef}
	MsgSender: MESSAGGI \fun ID \\
	MsgReceiver: MESSAGGI \fun ID \\
	MsgText: MESSAGGI \fun CONTENUTO
\where
	\forall m: MESSAGGI; s,r: ID; c: CONTENUTO | m = (s,r,c) @ \\
\t2		MsgSender(m) = s \land MsgReceiver(m) = r \land MsgText(m) = c
\end{axdef}
Sia inoltre $Collegati$ una funzione che dati due identificatori di processi
restituisce $TRUE$ se i due processi sono in collegamento.
\begin{axdef}
	Collegati: ID \cross ID \cross \finset COLLEGAMENTI \surj BOOL
\where
	\forall id1,id2: ID ; coll: \finset COLLEGAMENTI @ \\
\t1		Collegati(id1,id2,coll) =
			\IF (id1,id2) \in coll \lor (id2,id1) \in coll \THEN
TRUE \ELSE FALSE
\end{axdef}
Definiamo infine uno schema che identifica la condizione di messaggio vuoto.
\begin{schema}{MessaggioVuoto}
	Contenuto?: CONTENUTO \\
	rep!: REPORT
\where
	Contenuto? = Void \\
	rep! = Messaggio\_vuoto
\end{schema}



Lo schema di comunicazione \`e il seguente:
\begin{schema}{Comunicazione}
	Mailbox: \seq MESSAGGI \\
	Collegamenti: \finset COLLEGAMENTI
\where
	\forall s_1,s_2,c : ID | \{(s_1,c), (s_2,c)\} \subseteq Collegamenti @ s_1 = s_2
\land s_1 \neq c \\
	\forall s,c : ID | (s,c) \in Collegamenti @ (c,s) \notin
Collegamenti \\
	\forall l : \seq MESSAGGI; r : \seq_1 MESSAGGI | l \cat r = Mailbox @ \\
\t1		Collegati(MsgSender(head(r)),MsgReceiver(head(r)),Collegamenti)
= TRUE
\end{schema}
Lo stato iniziale della comunicazione prevede che non ci siano collegamenti
aperti e che non ci siano quindi messaggi in attesa di essere recapitati.
\begin{zed}
	InitComunicazione \defs [Comunicazione' | Mailbox' = \langle \rangle
		\land Collegamenti' = \emptyset]
\end{zed}


\subsection{Apertura del collegamento}

Per aprire il collegamento fra un {\it client} e un {\it server} \`e sufficiente
inserire la nuova coppia in $Collegamenti$. Si ricorda che la prima componente
della coppia deve essere sempre il {\it server}. Si noti inoltre che il
collegamento \`e sempre aperto dal {\it client} quando
vuole collegarsi ad un {\it server}, pertanto l'identificatore del primo viene
determinato mediante $WhoAmI$.
\begin{schema}{ApriCollegamentoOk}
	\Delta Comunicazione \\
	Server?: ID
\where
	\forall s,c: ID | (s,c) \in Collegamenti @ WhoAmI \notin \{s,c\} \\
	Collegamenti' = Collegamenti \cup \{~(Server?, WhoAmI)~\}
\end{schema}
L'apertura del collegamento pu\`o fallire qualora sia gi\`a stato aperto
precedentemente, o si vogliano aprire pi\`u collegamenti da parte dello stesso
programma {\it client}. Inoltre $Server?$ non pu\`o essere gi\`a utilizzato
come {\it client}.
\begin{schema}{CollegamentoPresente}
	\Xi Comunicazione \\
	rep!: REPORT
\where
	\exists s: ID @ Collegati(s,WhoAmI,Collegamenti) = TRUE \\
	rep! = Client\_gia\_collegato
\end{schema}

\begin{schema}{CollegamentoNonAmmesso}
	\Xi Comunicazione \\
	Server?: ID \\
	rep!: REPORT
\where
	Server? \in \{~s,c: ID | (s,c) \in Collegamenti @ c~\} \\
	rep! = Identificatore\_del\_server\_errato
\end{schema}

Lo schema completo per l'apertura del collegamento risulta quindi essere
il seguente:
\begin{zed}
	ApriCollegamento \defs \\
\t1		(ApriCollegamentoOk \land Successo) \lor CollegamentoPresente
\lor CollegamentoNonAmmesso
\end{zed}


\subsection{Chiusura del collegamento}

La chiusura del collegamento fra un programma {\it client} e un programma 
{\it server} avviene semplicemente eliminando la coppia opportuna da 
$Collegamenti$. Il collegamento pu\`o essere chiuso indifferentemente dal 
{\it client} o dal {\it server}. L'identificatore del programma con il 
quale si sta colloquiando \`e rappresentato da $Partner?$.

\begin{schema}{ChiudiCollegamentoOk}
	\Delta Comunicazione \\
	Partner?: ID
\where
	Collegati(WhoAmI,Partner?,Collegamenti) = TRUE \\
	Mailbox' = Mailbox \filter \{~ind_1,ind_2:ID; c:CONTENUTO | \\
\t1	      \{ind_1,ind_2\} \neq \{WhoAmI, Partner?\} @ (ind_1,ind_2,c)~\} \\
	Collegamenti' = Collegamenti \setminus \{~(WhoAmI, Partner?),
(Partner?,WhoAmI)~\}
\end{schema}
La chiusura del collegamento pu\`o fallire qualora non sia mai stato aperto
o comunque sia gi\`a stato chiuso.
\begin{schema}{CollegamentoAssente}
	\Xi Comunicazione \\
	Partner?: ID\\
	rep!: REPORT
\where
	Collegati(WhoAmI,Partner?,Collegamenti) = FALSE \\
	rep! = Collegamento\_inesistente
\end{schema}
Lo schema completo per la chiusura del collegamento risulta quindi essere
il seguente:
\begin{zed}
	ChiudiCollegamento \defs (ChiudiCollegamentoOk \land Successo) \lor
CollegamentoAssente
\end{zed}


\subsection{Broadcast di messaggi da parte del {\it server}}

Per {\em broadcast} di un messaggio intendiamo l'invio dello stesso messaggio
ad un gruppo di uno o pi\`u processi collegati al processo emittente.
Il processo che intende effettuare l'invio del messaggio deve essere un
processo {\it server}. I processi {\it client}, come si vedr\`a pi\`u avanti,
possono inviare solamente un messaggio al {\it server} al quale sono
collegati.
Per il {\it server} che esegue il {\em broadcast}, l'insieme dei riceventi
\`e un qualsiasi sottoinsieme dell'insieme dei {\it client} ad esso collegati.

Si noti che non \`e considerato errore n\'e l'invio di un messaggio ad un
insieme vuoto di riceventi, n\'e l'invio di un messaggio a qualche processo
non collegato. Queste operazioni comportano solamente la mancata spedizione
del messaggio ai destinatari non riconosciuti (eventualmente anche a tutti.
\`E per\`o considerato errore l'invio del messaggio vuoto.

Lo schema che segue verifica che il processo che vuole eseguire il {\em
broadcast} sia un processo {\it server}. Inoltre filtra dall'insieme dei
riceventi tutti gli identificatori di processi a lui non collegati.
\begin{schema}{toSend}
	\Xi Comunicazione \\
	Receivers?, Receivers!: \finset ID \\
	Contenuto?, Contenuto!: CONTENUTO
\where
	\exists c: ID @ (WhoAmI,c) \in Collegamenti \\
	Contenuto? \neq Void \\
	Receivers! = Receivers? \cap \{~c:ID | (WhoAmI,c) \in Collegamenti~\} \\
	Contenuto! = Contenuto?
\end{schema}
Il {\em broadcast} vero e proprio del messaggio viene eseguito nello schema
che segue. Le condizioni che vi compaiono esprimono nell'ordine che:
\begin{itemize}
\item tutti i messaggi ancora da recapitare vengono mantenuti;
\item i nuovi messaggi spediti vengono aggiunti in coda al $Mailbox$ 
preservando l'ordinamento FIFO
\item ogni nuovo messaggio spedito viene inviato ad uno dei processi
dell'insieme $Receivers?$
\item allo stesso utente viene spedito un solo messaggio nuovo 
\end{itemize}
\begin{schema}{MessageBroadcasting}
	\Delta Comunicazione \\
	Receivers?: \finset ID \\
	Contenuto?: CONTENUTO
\where
	Mailbox \prefix Mailbox' \\
	\forall s: \seq_1 MESSAGGI | s \suffix Mailbox' @ \\
\t1	    (\exists s_2: \seq_1 MESSAGGI | s_2 \suffix Mailbox @ s_2 \prefix s)
\lor {} \\
\t1	    ((\exists r: ID | r \in Receivers? @ (WhoAmI,r,Contenuto?) =
head(s) \land {} \\
\t2	    (\forall s_2: \seq MESSAGGI | s_2 \suffix s \land s_2 \neq s @
MsgReceiver(head(s_2)) \neq r)))
\end{schema}
Parallelamente lo schema seguente segnala la presenza di un errore nel caso
che chi esegue il {\em broadcast} sia un {\it client} o comunque non sia
collegato con nessun altro processo.
\begin{schema}{BroadcastNonAutorizzato}
	\Xi Comunicazione \\
	Receivers?: \finset ID \\
	Contenuto?: CONTENUTO \\
	rep!: REPORT
\where
	\forall c: ID @ (WhoAmI,c) \notin Collegamenti \\
	Contenuto? \neq Void \\
	rep! = Broadcast\_non\_consentito
\end{schema}
Per concludere lo schema completo per il {\em broadcast} risulta essere il
seguente:
\begin{zed}
	Broadcast \defs \\
\t1		(toSend \pipe MessageBroadcasting \land Successo) \lor
		BroadcastNonAutorizzato \lor MessaggioVuoto
\end{zed}


\subsection{Invio di messaggi ad un processo singolo}

In questa sezione si esamina l'invio di messaggi nella comunicazione uno a
uno. Questo tipo di comunicazione \`e l'unica consentita per il {\it client}
ma viene utilizzata anche dal {\it server}. Si fa nuovamente uso dello schema
$MessageBroadcasting$ dove per\`o si forza l'invio del messaggio ad un
solo ricevente. In questo contesto l'unica condizione di errore \`e che il
collegamento con il ricevente non sia ancora stato aperto.
\begin{schema}{SpedisciOk}
	\Xi Comunicazione \\
	Receiver?: ID \\
	Receivers!: \finset ID \\
	Contenuto?, Contenuto!: CONTENUTO
\where
	Collegati(WhoAmI,Receiver?,Collegamenti) = TRUE \\
	Contenuto? \neq Void \\
	Receivers! = \{Receiver?\} \\
	Contenuto! = Contenuto?
\end{schema}
Utilizzando anche altri schemi precedentemente definiti, lo schema completo
per l'invio dei messaggi risulta essere il seguente:
\begin{zed}
	Spedisci \defs (SpedisciOk \pipe MessageBroadcasting \land Successo) \lor {} \\
\t1		CollegamentoAssente[Receiver?/Partner?] \lor MessaggioVuoto
\end{zed}


\subsection{Ricezione di messaggi}

La ricezione di messaggi prevede che venga restituito il primo messaggio
contenuto nel $Mailbox$ che ha come destinatario colui che lo vuol ricevere.
Se sono presenti pi\`u messaggi diretti allo stesso destinatario
viene restituito solamente il primo di essi (seguendo una politica FIFO). Se
non vi sono messaggi per il destinatario o non esistono processi ad esso
collegati viene restituito uno speciale messaggio vuoto. Non sono previste
condizioni di errore.
\begin{schema}{RiceviOk}
	\Delta Comunicazione \\
	Sender!: ID \\
	Contenuto!: CONTENUTO
\where
	(\LET Messaggi == Mailbox \filter \{~s: ID; c: CONTENUTO @ (s,
WhoAmI, c)~\} @ \\
\t1		Messaggi \neq \langle \rangle \land Sender! =
MsgSender(head(Messaggi)) \land {} \\
\t1		Contenuto! = MsgText(head(Messaggi)) \land {}
\also
\t1		(\exists l: \seq MESSAGGI; r: \seq_1 MESSAGGI |
		   head(r) = head(Messaggi) \land l \cat r = Mailbox \land {} \\
\t2		   (\forall l_1: \seq_1 MESSAGGI| l_1 \suffix l @ head(l_1) \neq
head(r)) @ \\
\t3			Mailbox' = l \cat tail(r)))
\end{schema}

\begin{schema}{ZeroMessaggi}
	\Xi Comunicazione \\
	Sender!: ID \\
	Contenuto!: CONTENUTO
\where
	Mailbox \filter \{~s: ID; c: CONTENUTO @ (s, WhoAmI, c)~\} = \langle
\rangle \\
	Sender! = WhoAmI \\
	Contenuto! = Void
\end{schema}

Lo schema completo per la ricezione dei messaggi risulta essere il seguente:
\begin{zed}
	Ricevi \defs (RiceviOk \lor ZeroMessaggi) \land Successo
\end{zed}

% ---------------------------------------------------------------------------
\section{Client}
% ---------------------------------------------------------------------------

In questa sezione, definiamo lo stato e le operazioni del programma
di interfaccia fra {\it client} e {\it server}.

% ***************************************************************************
\subsection{Definizioni di base}
% ***************************************************************************

$VIDEO$ \`e il tipo che rappresenta l'insieme delle informazioni
visualizzabili.
\begin{zed}
	[VIDEO]
\end{zed}

Lo schema seguente \`e il tipo che rappresenta una scacchiera.

\begin{schema}{StatoScacchiera}
	Scacchiera      : POSIZIONE\\
	DeveMuovere     : COLORE\\
	StatoPartita    : STATOSCACCHIERA\\
	TempoB		: TEMPO \\
	TempoN		: TEMPO
\end{schema}

\begin{axdef}
	PosIniziale : StatoScacchiera\\
	IndPos : StatoScacchiera
\end{axdef}

Le seguenti funzioni servono per:

testare la possibilit\`a di effettuare una mossa a partire da una data
posizione:
\begin{axdef}
	ControllaMossa: StatoScacchiera \cross SEMIMOSSA \surj BOOL
\end{axdef}

determinare lo stato della scacchiera successivo data una posizione ed una 
mossa; aggiorna la scacchiera, cambia il colore di chi deve muovere ed
eventualmente modifica lo stato della partita:
\begin{axdef}
	AggiornaPosizione: StatoScacchiera \cross SEMIMOSSA \pfun StatoScacchiera
\end{axdef}

determinare la posizione raggiunta attraverso una sequenza di mosse:
\begin{axdef}
  TrovaPosizione: StatoScacchiera \cross MOSSE \pfun StatoScacchiera
\where
  \forall p: StatoScacchiera; m: MOSSE \spot \\
\t1	((\#m = 0) \implies TrovaPosizione(p,m) = p \lor \\
\t1	(\#m > 0) \implies TrovaPosizione(p,m) = \\
\t2		AggiornaPosizione(TrovaPosizione(p,front(m)),last(m)))
\end{axdef}


Definiamo una funzione che trasforma le informazioni relative allo stato
della scacchiera in un oggetto di tipo $VIDEO$.

\begin{axdef}
	visual : StatoScacchiera \cross COLORE \cross \seq STRINGA \fun VIDEO
\end{axdef}

Definiamo ora il tipo astratto dello stato dell'editor, il quale \`e composto
dalla posizione attuale della partita che si sta giocando, il colore
attribuito al cliente, i tempi attuali di gioco, un box dove vengono
inseriti i messaggi per il cliente ed infine un video nel quale vengono
visualizzate tutte le informazioni attraverso la funzione visual.\\
Da notare che, innanzitutto, la posizione attuale deve essere una posizione
raggiungibile per qualche sequenza di mosse, in pi\`u il video deve sempre
essere aggiornato con la funzione visual.

\begin{schema}{StatoEditor}
	PosAttuale	: StatoScacchiera \\
	MyColor		: COLORE \\
	PartiteOsservate : INDICEPARTITA \pfun StatoScacchiera \\
	BoxMsg		: \seq STRINGA \\
	Video		: VIDEO
\where
	\exists s : MOSSE @ (\forall l,r:MOSSE | \#r > 0 \land l\cat r = s @ \\
\t1		ControllaMossa(PosIniziale,head(r))=TRUE) \land {} \\
\t1		PosAttuale = TrovaPosizione(PosIniziale,s) \\
	Video = visual(PosAttuale,MyColor,BoxMsg)
\end{schema}

Ora arriviamo a definire lo stato vero e proprio del programma cliente,
che contiene lo stato dell'editor pi\`u l'indirizzo del server a cui il
cliente \`e collegato.

\begin{schema}{Cliente}
	server	: ID \\
	StatoEditor
\end{schema}

L'inizializzazione pone tutto a indeterminato o a vuoto tranne che l'$ID$ del
{\it server} che viene posto uguale all'indirizzo del {\it client}. Questo sta
a significare che l'utente non \`e collegato a nessun {\it server}.

\begin{schema}{InitCliente}
	Cliente'
\where
	server' = WhoAmI \land PosAttuale' = IndPos \land MyColor' = IndColore \\
	PartiteOsservate' = \emptyset \land BoxMsg' = \langle \rangle
\end{schema}

% ***************************************************************************
\subsection{Inserimento di un comando}
% ***************************************************************************

L'inserimento di un comando da parte del cliente \`e specificato con gli
schemi seguenti. Per prima cosa si controlla che il comando sia ammissibile,
poi se non \`e la richiesta di collegamento con un server, si spedisce un
messaggio al server che penser\`a a gestire il comando; altrimenti se \`e
un comando telnet, prima di spedire la richiesta di connessione al {\it server}
occorre aprire il collegamento.

La funzione $InSetComandi$ controlla che il comando sia ammissibile,
mentre la funzione {\it IsTelnet} controlla che il comando sia Telnet.
Le ultime due funzioni servono per la conversione di tipi.

\begin{axdef}
	InSetComandi: STRINGA \surj BOOL \\
	IsTelnet: STRINGA \surj BOOL \\
	ConvertiInContenuto: STRINGA \fun CONTENUTO \\
	ConvertiInId: STRINGA \fun ID
\end{axdef}

$MsgConnessione$ \`e il messaggio di richiesta di connessione da parte
del cliente per il server.

\begin{axdef}
	MsgConnessione: CONTENUTO
\end{axdef}

Se il comando non \`e ne sbagliato ne un comando telnet, allora lo si
spedisce al server.

\begin{schema}{InsertComandoOk}
	\Xi Cliente \\
	Comando? : STRINGA \\
	Receiver! : ID \\
	Contenuto! : CONTENUTO
\where
	InSetComandi(Comando?) = TRUE\\
	IsTelnet(Comando?) = FALSE \\
	Receiver! = server \\
	Contenuto! = ConvertiInContenuto(Comando?)
\end{schema}

Il prossimo schema \`e lo schema d'errore per l'inserimento di un comando.

\begin{schema}{ComandoNonTrovato}
	Comando? : STRINGA \\
	rep! : REPORT
\where
	InSetComandi(Comando?) = FALSE \\
	rep! = Comando\_non\_Trovato
\end{schema}

Il comando {\bf telnet} viene esaminato dal seguente schema, che estrae il
nome del server.

\begin{schema}{TelnetOk}
	\Delta Cliente \\
	Comando?: STRINGA\\
	Server!: ID\\
\where
	IsTelnet(Comando?)=TRUE \\
	server' = ConvertiInId(Comando?)\\
	Server! = server'\\
\end{schema}

I prossimi due schemi servono per controllare il risultato dell'operazione
di apertura del collegamento.

\begin{schema}{ServerKo}
	\Delta Cliente \\
	rep? : REPORT
\where
	rep? \neq Ok \\
	server' = WhoAmI
\end{schema}

\begin{schema}{ServerOk}
	\Xi Cliente \\
	rep? : REPORT\\
	Receiver!: ID \\
	Contenuto!: CONTENUTO
\where
	rep? = Ok \\
	Receiver! = server \\
	Contenuto! = MsgConnessione
\end{schema}

Il comando {\bf telnet} viene esaminato dallo schema $TelnetOk$, viene
aperto il collegamento, e se tutto \`e andato bene si spedisce la richiesta
di connessione al server. Invece lo schema finale $InsertComando$ prevede la
spedizione del comando al {\it server}, oppure un comando {\it telnet}, oppure
un caso di errore; i tre casi sono mutuamente esclusivi.

\begin{zed}
  Telnet \defs TelnetOk \pipe ApriCollegamento \pipe 
		((ServerOk \pipe Spedisci) \lor ServerKo)
\also
  InsertComando \defs ((InsertComandoOk \pipe Spedisci) \land 
		Successo) \lor ComandoNonTrovato \lor Telnet
\end{zed}

% ***************************************************************************
\subsection{Ricezione e gestione di un messaggio}
% ***************************************************************************

Il cliente pu\`o ricevere messaggi da parte del server che richiedono il
cambiamento dello stato del cliente. Non sono previsti casi di errore.
Iniziamo specificando tutti i tipi di messaggi che possono arrivare al
cliente:

\begin{syntax}
	MSGCLIENTE &::=& mossaavversario | nuovomatch | finematch |
		   	 visualmessaggio | visualpartita \\
		   & | & finevisualpartita | richiestausername |
			 richiestapassword 
\end{syntax}

La funzione $IsNewMsg$ prende il contenuto di un messaggio, un possibile
tipo di messaggio e restituisce vero se il messaggio \`e proprio di quel
tipo.

\begin{axdef}
	IsNewMsg: CONTENUTO \cross MSGCLIENTE \surj BOOL \\
\end{axdef}

Le funzioni seguenti servono per convertire i contenuti dei messaggi a
seconda del tipo di messaggio.

\begin{axdef}
	ConvertiInMossa: CONTENUTO \pinj SEMIMOSSA \cross TEMPO \cross TEMPO \\
	ConvertiInNuovoMatch: CONTENUTO \pinj COLORE \cross StatoScacchiera \\
	ConvertiInUltimaMossa: CONTENUTO \pinj SEMIMOSSA \cross COLORE \\
	ConvertiInStringa: CONTENUTO \pinj STRINGA \\
	ConvertiInPartita: CONTENUTO \pinj INDICEPARTITA \cross StatoScacchiera \\
	ConvertiInIndice: CONTENUTO \pinj INDICEPARTITA \\
\end{axdef}

Le funzioni seguenti servono per creare un messaggio da spedire al server
in risposta a qualche richiesta.

\begin{axdef}
	MsgUserName: USERNAME \inj CONTENUTO \\
	MsgPassword: STRINGA \inj CONTENUTO
\end{axdef}

Di seguito sono definiti due messaggi per la vittoria o la sconfitta.

\begin{axdef}
	MsgHaiVinto: STRINGA \\
	MsgHaiPerso: STRINGA
\end{axdef}

Iniziamo analizzando tutte le azioni dovute ai diversi messaggi.

Se il messaggio \`e una mossa dell'avversario, si aggiorna semplicemente
lo stato della scacchiera.

\begin{schema}{MossaAvversario}
	\Delta Cliente \\
	Contenuto? : CONTENUTO
\where
	IsNewMsg(Contenuto?,mossaavversario) = TRUE \\
	\exists mossa: SEMIMOSSA; T_1,T_2: TEMPO |
		ConvertiInMossa(Contenuto?) = (mossa,T_1,T_2) @ \\
\t1	PosAttuale' = AggiornaPosizione(PosAttuale,mossa) \land {} \\
\t1	PosAttuale'.TempoB = T_1 \land PosAttuale'.TempoN = T_2
\end{schema}

Se il messaggio contiene gli estremi per un nuovo match si inizializza la
posizione attuale e il proprio colore.

\begin{schema}{NuovoMatch}
	\Delta Cliente \\
	Contenuto? : CONTENUTO
\where
	IsNewMsg(Contenuto?,nuovomatch) = TRUE \\
	\exists c: COLORE; Stato: StatoScacchiera |
		ConvertiInNuovoMatch(Contenuto?) = (c,Stato) @ \\
\t2	PosAttuale' = Stato \land MyColor' = c
\end{schema}

In caso di fine match viene comunicato il risultato e viene aggiornata
l'ultima mossa.

\begin{schema}{FineMatch}
	\Delta Cliente \\
	Contenuto? : CONTENUTO
\where
	IsNewMsg(Contenuto?,finematch) = TRUE \\
	\exists m:SEMIMOSSA; vinc: COLORE | \\
\t1		ConvertiInUltimaMossa(Contenuto?) = (m,vinc) @ \\
\t2	BoxMsg' = BoxMsg \cat \langle \IF vinc = MyColor \THEN MsgHaiVinto
		\ELSE MsgHaiPerso \rangle \land {} \\
\t2	PosAttuale' = AggiornaPosizione(PosAttuale,m) \\
	MyColor' = IndColore \\
	PosAttuale'.TempoB = IndTempo \\
	PosAttuale'.TempoN = IndTempo
\end{schema}

Se il messaggio arrivato \`e proprio un messaggio  da visualizzare viene
messo nel box dei messaggi.

\begin{schema}{VisualMessaggio}
	\Delta Cliente \\
	Contenuto?: CONTENUTO
\where
	IsNewMsg(Contenuto?,visualmessaggio) = TRUE \\
	\exists s: STRINGA | ConvertiInStringa(Contenuto?) = s @ BoxMsg' =
BoxMsg \cat \langle s \rangle
\end{schema}

In caso che sia stata modificata una partita che stiamo osservando,
viene aggiornata la funzione {\it PartiteOsservate}.

\begin{schema}{VisualPartita}
	\Delta Cliente \\
	Contenuto?: CONTENUTO
\where
	IsNewMsg(Contenuto?,visualpartita) = TRUE \\
	\exists s: StatoScacchiera; c: INDICEPARTITA |
		ConvertiInPartita(Contenuto?) = (c,s) @ \\
\t1		PartiteOsservate' = PartiteOsservate \oplus \{c \mapsto s\}
\end{schema}

Il prossimo schema specifica la chiusura dell'osservazione di una partita.

\begin{schema}{FineVisualPartita}
	\Delta Cliente \\
	Contenuto?: CONTENUTO
\where
	IsNewMsg(Contenuto?,finevisualpartita) = TRUE \\
	\exists i: INDICEPARTITA | ConvertiInIndice(Contenuto?) = i @ \\
\t1		PartiteOsservate' = \{i\} \ndres PartiteOsservate
\end{schema}

I prossimi due schemi servono per rispondere alla richiesta dell'username
o della password da parte del server.

\begin{schema}{RichiestaUserName}
	\Xi Cliente \\
	Contenuto?: CONTENUTO\\
	User?: USERNAME\\
	Receiver!: ID\\
	Contenuto!: CONTENUTO
\where
	IsNewMsg(Contenuto?,richiestausername) = TRUE \\
	Receiver! = server\\
	Contenuto! = MsgUserName(User?)
\end{schema}

\begin{schema}{RichiestaPassword}
	\Xi Cliente \\
	Contenuto?: CONTENUTO\\
	Password?: STRINGA\\
	Receiver!: ID\\
	Contenuto!: CONTENUTO
\where
	IsNewMsg(Contenuto?,richiestapassword) = TRUE \\
	Receiver! = server\\
	Contenuto! = MsgPassword(Password?)
\end{schema}

In caso che non ci sia nessun messaggio, non facciamo niente.

\begin{schema}{NessunMessaggio}
	Contenuto? : CONTENUTO\\
	rep! : REPORT
\where
	Contenuto? = Void \\
	rep! = Nessun\_Messaggio
\end{schema}

$ConsumaMessaggio$ ha in alternativa tutte le possibili azioni associate ad un
messaggio, solo {\it RichiestaUserName} e {\it RichiestaPassword} devono spedire una
risposta al {\it server}; mentre {\it RiceviMessaggio} guarda se ci sono
messaggi, in questo caso consuma il primo altrimenti non fa niente.

\begin{zed}
  ConsumaMessaggio \defs VisualMessaggio \lor MossaAvversario \lor NuovoMatch
\lor FineMatch \lor {} \\
\t1	VisualPartita \lor FineVisualPartita \lor ((RichiestaUserName \lor
RichiestaPassword) \pipe Spedisci)
\also
  RiceviMessaggio \defs ((Ricevi \pipe ConsumaMessaggio) \land
		Successo) \lor NessunMessaggio
\end{zed}

% ***************************************************************************
\subsection{Introduzione di una mossa}
% ***************************************************************************

Quando l'utente introduce una mossa, si controlla che sia il turno giusto e
che la mossa sia corretta, quindi si aggiorna la posizione e si spedisce
al server un messaggio contenente la mossa, convertendola con la funzione
$MossaInMessaggio$.

\begin{axdef}
	MossaInMessaggio : SEMIMOSSA \inj CONTENUTO
\end{axdef}

\begin{schema}{MyMossaOk}
	\Delta Cliente \\
	Mossa? : SEMIMOSSA\\
	Receiver!: ID\\
	Contenuto!: CONTENUTO
\where
	MyColor = PosAttuale.DeveMuovere \\
	ControllaMossa(PosAttuale,Mossa?) = TRUE
\also
	PosAttuale' = AggiornaPosizione(PosAttuale,Mossa?)\\
	Receiver! = server\\
	Contenuto! = MossaInMessaggio(Mossa?)
\end{schema}

\begin{schema}{MossaSbagliata}
	\Xi Cliente \\
	Mossa? : SEMIMOSSA\\
	rep! : REPORT
\where
	MyColor = PosAttuale.DeveMuovere\\
	ControllaMossa(PosAttuale,Mossa?) = FALSE \\
	rep! = Mossa\_Errata
\end{schema}

\begin{schema}{TurnoSbagliato}
	\Xi Cliente \\
	rep! : REPORT
\where
	MyColor \neq PosAttuale.DeveMuovere \\
	rep! = Turno\_sbagliato
\end{schema}

Lo schema finale per l'introduzione di una mossa \`e il seguente:

\begin{zed}
  MyMossa \defs (MyMossaOk \pipe Spedisci) \lor MossaSbagliata \lor
TurnoSbagliato
\end{zed}


% ---------------------------------------------------------------------------
\section{Server}
% ---------------------------------------------------------------------------

% ***************************************************************************
\subsection{Definizioni di base}
% ***************************************************************************

Viste le definizioni delle sezioni precedenti, definiamo i tipi e gli schemi
necessari alla specifica dello stato astratto del server. \\
Introduciamo il tipo $FLAG$ e da questo definiamo il tipo $STATUS$, che
rappresentano lo stato dell'utente. Il valore $Connessione$ \`e utilizzato
durante la fase di connessione e il valore $Regis$ \`e utilizzato per
indicare che un utente \`e registrato. Si noti che alcuni $FLAG$ sono
mutuamente esclusivi. Introduciamo inoltre il tipo $STATOPARTITA$ per
tenere memoria della richiesta di patta o di sospensione.

\begin{zed}
  STATOPARTITA ::= PropostaPatta | PropostaSosp \\
  FLAG  ::=  Open | Close | Gioca | Connessione | Regis | NonCollegato \\
  STATUS == \{~x: \finset FLAG | \#(x \cap \{Open, Close, Gioca, Connessione\}) = 1 \land NonCollegato \notin x~\}
\end{zed}

Per la gestione delle partite, introduciamo lo schema $PartitaInCorso$
che include lo schema $Partita$ visto nella sezione relativa alle partite e
aggiunge informazioni relative alle osservazioni delle partite, allo stato
della partita (in caso che un giocatore abbia proposto la patta o la
sospensione), al tempo in cui \`e stata effettuata l'ultima mossa e al colore
del giocatore a cui tocca muovere.
Introduciamo inoltre il tipo $COPPIAGIOCATORI$, intesa come una coppia non
ordinata di giocatori diversi. Per la gestione delle sfide introduciamo lo
schema $Sfida$, che contiene le informazioni relative ad una sfida lanciata
con il comando {\bf match}

\begin{schema}{PartitaInCorso}
  Partita \\
  Osservatori: \finset USERNAME \\
  Stato: STATOPARTITA \pfun COLORE \\
  UltimaMossa: TEMPO \\
  DeveMuovere: COLORE 
\where
  DeveMuovere \neq IndColore \\
  DeveMuovere = \IF \#(\ran Mosse) \mod 2 = 0 \THEN Bianco \ELSE Nero
\end{schema}

\begin{zed}
  COPPIAGIOCATORI == \{~x,y: USERNAME | x \neq y @ \{x,y\}~\}
\end{zed}

\begin{schema}{Sfida}
  Sfidante, Sfidato: USERNAME \\
  T1, T2: TEMPO
\end{schema}

Infine, introduciamo due tipi utilizzati per identificare univocamente una
partita in corso e un canale di comunicazione fra utenti (la costante $NumCanali$
indica il numero massimo di canali presenti).

\begin{axdef}
  NumCanali: \nat
\end{axdef}

\begin{zed}
  CANALE == 1 \upto NumCanali
\end{zed}

A questo punto possiamo introdurre lo schema $Server$, che rappresenta lo
stato astratto di un singolo server. I campi $IdUtente$, $StatoUtente$,
$TempoUtente$ associano ad ogni utente collegato un indirizzo, uno stato ed un
contatore di inizio di collegamento; il campo $Sospese$
associa a coppie di utenti una partita sospesa in cui stavano giocando; la
funzione $InCorso$ utilizza un identificatore univoco per ogni partita e si
assicura che ogni giocatore giochi al pi\`u una partita.
Il campo $Sfide$ \`e un insieme di $Sfida$ dove \`e garantito che ogni
giocatore sfidi al pi\`u un altro giocatore e che non vi siano sfide incrociate
o con tempi diversi fra due giocatori; inoltre tutte gli sfidanti e gli sfidati
devono essere collegati.
L'ultimo campo \`e $Canali$, che ad ogni canale associa un insieme di utenti
connessi.

\begin{schema}{Server}
  IdUtente: USERNAME \pinj ID \\
  StatoUtente: USERNAME \pfun STATUS \\
  TempoUtente: USERNAME \pfun TEMPO \\
  Sospese: COPPIAGIOCATORI \pinj Partita \\
  InCorso: INDICEPARTITA \pfun PartitaInCorso \\
  Sfide: \finset Sfida \\
  Canali: CANALE \fun \finset USERNAME
\where
  \dom IdUtente = \dom StatoUtente \land \dom IdUtente = \dom TempoUtente \\
  \forall x: COPPIAGIOCATORI | x \in \dom Sospese @ x = \dom
(Sospese(x)).Giocatori \\
  \forall n,m: INDICEPARTITA | n \neq m \land \{n,m\} \subseteq \dom InCorso @ \\
	\t1 \dom (InCorso(n)).Giocatori \cap \dom (InCorso(m)).Giocatori = \emptyset \land {}\\
	\t1 \dom (InCorso(n)).Giocatori \subseteq \dom IdUtente \\
  \forall x,y: Sfida | x \neq y @ \{x,y\} \subseteq Sfide \land \{x.Sfidante,
x.Sfidato\} \neq \{y.Sfidante, y.Sfidato\} \land {}\\
	\t1 x.Sfidante \neq y.Sfidante \land \{x.Sfidante, x.Sfidato\} \subseteq
\dom IdUtente \\
  \forall c: CANALE @ Canali(c) \subseteq \dom IdUtente
\end{schema}

\begin{schema}{InitServer}
  Server'
\where
  Sospese' = \emptyset \land InCorso' = \emptyset \land Sfide' = \emptyset \land (\forall c:CANALE @ Canali'(c) = \emptyset) \\
  IdUtente' = \emptyset \land StatoUtente' = \emptyset \land TempoUtente' = \emptyset \\
\end{schema}


\section{GESTIONE COMANDI DA PARTE DEL SERVER}

In questa sezione vengono esaminati uno ad uno tutti i comandi che pu\`o
eseguire il {\it server}. Per tutti si utilizza una struttura analoga dove si
vuole in ingresso il contenuto di un messaggio proveniente da un {\it
client}, si verifica che si tratti di un comando corretto e in tal caso si
restituisce il risultato dell'esecuzione sotto forma di contenuto di un
messaggio da inviare a chi di dovere. Il formato di questi messaggi scambiati
non viene analizzato in dettaglio; si assume invece di avere a disposizione un
certo numero di funzioni in grado di elaborarli.

Si noti che alcuni comandi non prevedono output.


\subsection{Definizioni di base}

Definiamo gli schemi XiComando e DeltaComando, che devono essere inclusi
in ogni comando; prendono in input un comando e il suo mittente (output
dell'operazione $Ricevi$ del modulo di comunicazione) e verificano la
presenza dell'$ID$ nel codominio di $IdUtente$, la cui inversa viene
successivamente utilizzata per conoscere lo $USERNAME$.
Nello schema $DeltaComando$ gli invarianti sono volutamente omessi.
Si suppone vengano inseriti negli schemi dove {\it DeltaComando} \`e
incluso. $Connessione$ \`e un flag che indica se l'utente \`e in fase di
connessione (deve ancora inserire la password).

\begin{schema}{XiComando}
  \Xi Server \\
  Comando?: CONTENUTO \\
  Sender?: ID \\
  User: USERNAME
\where
  Sender? \in \ran IdUtente  \\
  User = IdUtente \inv (Sender?) \\
  Connessione \notin StatoUtente(User)
\end{schema}

\begin{schema}{DeltaComando}
  \Delta Server \\
  Comando?: CONTENUTO \\
  Sender?: ID \\
  User: USERNAME
\where
  Sender? \in \ran IdUtente  \\
  User = IdUtente \inv (Sender?) \\
  Connessione \notin StatoUtente(User)
\end{schema}

Definiamo inoltre alcune costanti per lo scambio di messaggi con il {\it
client}.
\begin{axdef}
	ComandoNonConsentito, UtenteNonCollegato, NumCanaleNonConosciuto : CONTENUTO
\end{axdef}

Definiamo lo schema $NonConsentito$, utilizzato in tutte quelle situazioni
in cui il comando non \`e consentito all'utente.

\begin{schema}{NonConsentito}
  XiComando \\
  Receiver!: ID \\
  Contenuto!: CONTENUTO
\where
  Receiver! = Sender? \\
  Contenuto! = ComandoNonConsentito
\end{schema}

$COMANDO$ \`e un insieme di costanti che identificano i vari comandi.
\begin{syntax}
	COMANDO	&::=& SpedUsername | SpedPassword | Who | Players |
Games \\
		& | & Stat | StatUtente | Free | SetOpen | SetClose | ObserveId
| ObserveName \\
		& | & MatchConTempi | MatchSenzaTempi | Accept | Decline |
Resign \\
		& | & Flag | ProposeDraw | AcceptDraw | Adjourn | AcceptAdjourn
\\
		& | & Mossa | Toplist | Shout | Tell | InChannel | OutChannel
| Channels \\
		& | & Searchgames | IndComando | Exit
\end{syntax}

Sia $is$ una funzione in grado di determinare il tipo del comando in base alla
sintassi del messaggio che si riceve.
\begin{axdef}
	is : CONTENUTO \cross COMANDO \surj BOOL
\end{axdef}

% ***************************************************************************
\subsection{Gestione della connessione}
% ***************************************************************************

\subsubsection{Apertura della connessione}

Prima di esporre gli schemi della specifica dell'operazione di connessione
introduciamo alcune funzioni e costanti utilizzate nel seguito:
{\it TrasformaMsgCliente} prende in input un $MSGCLIENTE$ definito nella sezione
del {\it client} e restituisce un $CONTENUTO$. Le tre costanti {\it
ClienteGiaPresente}, {\it UsernameGiaUtilizzato} e {\it
ErroreRicezionePassword} corrispondono ad altrettanti
messaggi di errore, mentre $Benvenuto$ \`e un messaggio di ingresso.
Definiamo infine le funzioni $EstraiNomeUtente$ e $EstraiPassword$.

\begin{axdef}
  TrasformaMsgCliente: MSGCLIENTE \fun CONTENUTO \\
  ClienteGiaPresente: CONTENUTO \\
  UsernameGiaUtilizzato: CONTENUTO \\
  ErroreRicezionePassword: CONTENUTO \\
  Benvenuto: CONTENUTO
\also
  EstraiNomeUtente: CONTENUTO \pfun USERNAME \\
  EstraiPassword: CONTENUTO \pfun STRINGA
\end{axdef}

La funzione $CopiaPartita$ trasforma una partita in corso in una partita
da registrare.

\begin{axdef}
	CopiaPartita: PartitaInCorso \pfun Partita \\
\where
	\forall P1: PartitaInCorso @ (\exists P2: Partita @
		P2.Giocatori = P1.Giocatori \land {} \\
	\t1 P2.Mosse = P1.Mosse \land
		P2.T1 = P1.T1 \land P2.T2 = P1.T2 \land {} \\
	\t1 P2.Tempi = P1.Tempi \land
		P2.Risultato = P1.Risultato \land {} \\
		\t2 CopiaPartita(P1) = P2)
\end{axdef}

L'apertura della connessione da parte del server avviene attraverso uno
scambio di messaggi con il cliente composto di tre fasi:
\begin{enumerate}
\item il cliente spedisce una richiesta di collegamento ed ottiene come risposta
il messaggio di login, a meno che non sia gi\`a collegato, nel qual caso
ottiene un messaggio di errore.

\begin{schema}{RichiestaCollegamentoOk}
  \Xi Server \\
  Comando?, Contenuto!: CONTENUTO \\
  Sender?, Receiver!: ID
\where
  Comando? = MsgConnessione \\
  Sender? \notin \ran IdUtente
\also
  Receiver! = Sender? \\
  Contenuto! = TrasformaMsgCliente(richiestausername)
\end{schema}

\begin{schema}{ClientePresente}
  \Xi Server \\
  Comando?, Contenuto!: CONTENUTO \\
  Sender?, Receiver!: ID
\where
  Comando? = MsgConnessione \\
  Sender? \in \ran IdUtente
\also
  Receiver! = Sender? \\
  Contenuto! = ClienteGiaPresente
\end{schema}

\begin{zed}
  RichiestaCollegamento \defs (RichiestaCollegamentoOk \lor ClientePresente) \pipe Spedisci
\end{zed}

\item il cliente spedisce lo username e si controlla una sua eventuale
registrazione; nel caso sia registrato, viene richiesta una password;

\begin{schema}{UsernameNuovo}
  \Delta Server \\
  Comando?, Contenuto!: CONTENUTO \\
  Sender?, Sender!: ID \\
  Username!: USERNAME
\where
  is(Comando?, SpedUsername) = TRUE \\
  Sender? \notin \ran IdUtente \\
  EstraiNomeUtente(Comando?) \notin \dom IdUtente
\also
  Username! = EstraiNomeUtente(Comando?) \\
  Sender! = Sender?
\end{schema}

\begin{schema}{VerificaRegistrato}
  Registrato \\
  Sender?, Sender!: ID
\where
  Sender! = Sender?
\end{schema}

\begin{schema}{ControllaRegistrazione}
  \Delta Server \\
  Presente?: BOOL \\
  Contenuto!: CONTENUTO \\
  Sender?, Receiver!: ID \\
  Username?: USERNAME
\where
  IdUtente' = IdUtente \cup \{Username? \mapsto Sender?\} \\
  StatoUtente' = \IF Presente? = TRUE \THEN StatoUtente \cup \{Username? \mapsto \{Connessione\}\} \\
\t8					\ELSE StatoUtente \cup \{Username? \mapsto \{Close\} \} \\
  TempoUtente' = TempoUtente \cup \{Username? \mapsto OraAttuale\} \\
  Receiver! = Sender? \\
  Contenuto! = \IF Presente? = TRUE \THEN TrasformaMsgCliente(richiestapassword) \\
\t8					\ELSE Benvenuto
\end{schema}

\begin{schema}{UsernameUtilizzato}
  \Xi Server \\
  Comando?, Contenuto!: CONTENUTO \\
  Sender?, Receiver!: ID \\
  Username?: USERNAME
\where
  is(Comando?, SpedUsername) = TRUE \\
  EstraiNomeUtente(Comando?) \in \dom IdUtente \\
  Receiver! = Sender? \\
  Contenuto! = UsernameGiaUtilizzato
\end{schema}

\begin{zed}
  RicezioneUsername \defs ((UsernameNuovo \pipe VerificaRegistrato \pipe ControllaRegistrazione) \lor {}\\
\t5		UsernameUtilizzato) \pipe Spedisci
\end{zed}

\item se \`e stata richiesta la password, questa viene spedita dal cliente
al servente, che la controlla; in caso di password errata il collegamento
viene interrotto. In caso di password indeterminata la procedura di
registrazione riparte da capo.

\begin{schema}{LeggiPass}
  \Delta Server \\
  Comando?: CONTENUTO \\
  Sender?: ID \\
  User: USERNAME \\
  Username!: USERNAME \\
  Password!: STRINGA
\where
  Sender? \in \ran IdUtente \\
  User = IdUtente \inv (Sender?) \\
  is(Comando?, SpedPassword) = TRUE \\
  StatoUtente(User) = \{Connessione\} \\
  Password! = EstraiPassword(Comando?) \\
  Username! = User
\end{schema}

\begin{schema}{PassOk}
  DeltaComando \\
  Corretta?: BOOL
\where
  Corretta? = TRUE
\also
  StatoUtente' = StatoUtente \oplus \{User \mapsto \{Close, Regis\} \} \\
  TempoUtente' = TempoUtente \oplus \{User \mapsto OraAttuale\} \\
\end{schema}

\begin{schema}{PassKo}
  DeltaComando \\
  Corretta?: BOOL \\
\where
  Corretta? = FALSE
\end{schema}

\begin{schema}{ElimUser}
  \Delta Server \\
  Username?,Username!: USERNAME \\
  Partner!: ID \\
  Tempo!: TEMPO
\where
  IdUtente' = \{Username?\} \ndres IdUtente \\
  StatoUtente' = \{Username?\} \ndres StatoUtente \\
  TempoUtente' = \{Username?\} \ndres TempoUtente \\
  InCorso' = \{~i:INDICEPARTITA | Username? \in \dom (InCorso(i)).Giocatori~\} \ndres InCorso \\
  Sospese' = Sospese \oplus \{i: INDICEPARTITA | Username? \in \dom (InCorso(i)).Giocatori \land {} \\
\t1	(\forall U:USERNAME | U \in \dom (InCorso(i)).Giocatori @ Regis \in StatoUtente(U)) @ \\
\t2		\dom (InCorso(i)).Giocatori \mapsto CopiaPartita(InCorso(i)) \} \\
  Sfide' = Sfide \setminus \{~x: Sfida | Username? \in \{x.Sfidante, x.Sfidato\}~\} \\
  \forall c:CANALE @ \\
	\t1 Canali' = Canali \oplus \{c \mapsto Canali(c) \setminus \{Username?\} \} \\
  Username! = Username? \\
  Tempo! = OraAttuale - TempoUtente(Username?) \\
  Partner! = IdUtente(Username?)
\end{schema}

\begin{schema}{PassNonRichiesta}
  XiComando \\
  Receiver!: ID \\
  Contenuto!: CONTENUTO
\where
  is(Comando?, SpedPassword) = TRUE \\
  StatoUtente(User) \neq \{Connessione\}
\also
  Receiver! = Sender? \\
  Contenuto! = ErroreRicezionePassword
\end{schema}

\begin{schema}{PassNulla}
  DeltaComando \\
  Receiver!: ID \\
  Contenuto!: CONTENUTO
\where
  is(Comando?, SpedPassword) = TRUE \\
  StatoUtente(User) = \{Connessione\} \\
  EstraiPassword(Comando?) = PasswordNulla \\
\also
  IdUtente' = \{User\} \ndres IdUtente \\
  StatoUtente' = \{User\} \ndres StatoUtente \\
  TempoUtente' = \{User\} \ndres TempoUtente \\
  Receiver!= Sender? \\
  Contenuto!= TrasformaMsgCliente(richiestausername)
\end{schema}

\begin{zed}
  RicezionePassword \defs \\
\t1	(LeggiPass \pipe VerificaPass \pipe (PassOk \lor ((PassKo \land ElimUser) \pipe ChiudiCollegamento))) \\
\t1	\lor ((PassNulla \lor PassNonRichiesta) \pipe Spedisci)
\end{zed}

\end{enumerate}

\subsubsection{Chiusura della connessione}

La chiusura del collegamento pu\`o avvenire spontaneamente o tramite il
comando {\bf exit}. Da parte
del server le eventuali partite in corso vengono salvate fra quelle sospese,
se questo \`e possibile. Nello schema $FineCollegamento$ si utilizza lo schema
$ElimUsername$ definito in precedenza.

\begin{schema}{ExitOk}
  DeltaComando
\where
  is(Comando?, Exit) = TRUE \\
\end{schema}

\begin{zed}
  FineCollegamento \defs ElimUser \pipe (AggiornaTempo \land ChiudiCollegamento)
\also
  ComandoExit \defs ExitOk \land FineCollegamento
\end{zed}

% ***************************************************************************
\subsection{Visualizzazione informazioni sullo stato del Server}
% ***************************************************************************

Si suppongono date le seguenti funzioni che manipolano i messaggi sia
in ingresso che in uscita eseguendo le conversioni opportune.

\begin{axdef}
	EstraiTesto: CONTENUTO \pfun STRINGA \\
	EstraiCanale: CONTENUTO \psurj CANALE \\
	EstraiPartita: CONTENUTO \psurj INDICEPARTITA
\also
	RisultatoTopList: \seq (USERNAME \cross ELO) \inj CONTENUTO \\
	RisultatoWho: \finset (USERNAME \cross BOOL) \inj CONTENUTO \\
	RisultatoPlayersFree: \finset (USERNAME \cross ELO) \inj CONTENUTO \\
	RisultatoGames: \finset (INDICEPARTITA \cross PartitaInCorso) \inj
CONTENUTO \\
	RisultatoStat: USERNAME \cross ELO \cross FLAG \inj CONTENUTO \\
\end{axdef}

\subsubsection{Comando TOPLIST}

Il comando {\bf toplist} \`e realizzato utilizzando lo schema $TopList$
definito nel database degli utenti registrati.

\begin{schema}{MsgTopList}
  XiComando \\
  topList?: \seq (USERNAME \cross ELO) \\
  Receiver!: ID ; Contenuto!: CONTENUTO
\where
  is(Comando?, Toplist) = TRUE \\
  Receiver! = Sender? \\
  Contenuto! = RisultatoTopList(topList?)
\end{schema}

\begin{zed}
  ComandoTopList \defs TopList \pipe MsgTopList \pipe Spedisci
\end{zed}

\subsubsection{Comando WHO}

Il comando {\bf who} permette ad un utente di visualizzare i nomi degli utenti
connessi. Per ogni utente viene specificato mediante un flag se l'utente \`e
registrato o meno. Non vi sono casi di errore.
\begin{schema}{ComandoWhoOk}
	XiComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?, Who) = TRUE
\also
	Receiver! = Sender? \\
	Contenuto! = RisultatoWho(\{~u:USERNAME | u \in \dom IdUtente \spot \\
\t2		(u, \IF Regis \in StatoUtente(u) \THEN TRUE \ELSE
FALSE)~\})
\end{schema}

\begin{zed}
	ComandoWho \defs ComandoWhoOk \pipe Spedisci
\end{zed}

\subsubsection{Comandi PLAYERS e FREE}

Racchiudiamo in questa sezione i due comandi {\bf players} e {\bf free} in
quanto a parte la selezione dei nomi per i quali visualizzare il risultato,
il tipo di operazioni necessarie alla visualizzazione \`e comune ad entrambi.

Il comando {\bf players} permette ad un utente di visualizzare i nomi degli
utenti che stanno giocando ed il relativo rating; mentre
il comando {\bf free} permette ad un utente di visualizzare le stesse
informazioni ma per i nomi degli utenti disposti a giocare.
Non vi sono casi di errore.
\begin{schema}{ComandoPlayersOk}
	XiComando \\
	Receiver!: ID \\
	Nomi!: \finset USERNAME
\where
	is(Comando?, Players) = TRUE
\also
	Receiver! = Sender? \\
	Nomi! = \{~id: INDICEPARTITA; n: USERNAME | \\
\t2		id \in \dom InCorso \land n \in \dom (InCorso(id)).Giocatori
\spot n~\}
\end{schema}

\begin{schema}{ComandoFreeOk}
	XiComando \\
	Receiver!: ID \\
	Nomi!: \finset USERNAME
\where
	is(Comando?, Free) = TRUE
\also
	Receiver! = Sender? \\
	Nomi! = \{~n: USERNAME | n \in \dom StatoUtente \land Open \in
StatoUtente(n) ~\}
\end{schema}

\begin{schema}{LeggiDbRegistrati}
	ConsultaDbRegistrati \\
	Receiver?, Receiver!: ID \\
	Nomi!: \finset USERNAME
\where
	Receiver! = Receiver? \\
	Nomi! = Nomi?
\end{schema}

\begin{schema}{FinePlayersFree}
	\Xi Server \\
	Nomi?: \finset USERNAME \\
	Info?: USERNAME \pfun UtenteRegistrato \\
	Receiver?, Receiver!: ID \\
	Contenuto! : CONTENUTO
\where
	Receiver! = Receiver? \\
	Contenuto! = RisultatoPlayersFree(\{~n: USERNAME| n \in Nomi? \spot \\
\t2	    (n, \IF n \in \dom Info? \THEN (Info?(n)).Elo \ELSE NonAssegnato)~\})
\end{schema}

\begin{zed}
	ComandoPlayers \defs ComandoPlayersOk \pipe LeggiDbRegistrati \pipe
		FinePlayersFree \pipe Spedisci
\also
	ComandoFree \defs ComandoFreeOk \pipe LeggiDbRegistrati \pipe
		FinePlayersFree \pipe Spedisci
\end{zed}

\subsubsection{Comando GAMES}

Il comando {\bf games} permette ad un utente di visualizzare dati sulle partite
in corso. Per ciascuna partita vengono visualizzati i seguenti dati:
numero identificativo della partita, username dei giocatori (prima il bianco
poi il nero); i tempi T1 (dotazione iniziale) e T2 (incremento); il tempo
ancora disponibile per ciascun giocatore; il numero dell'ultima mossa
effettuata; a chi sta la mossa.  Non vi sono casi di errore.
\begin{schema}{ComandoGamesOk}
	XiComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?, Games) = TRUE
\also
	Receiver! = Sender? \\
	Contenuto! = RisultatoGames(\{~ip:INDICEPARTITA | ip \in \dom InCorso
\spot (ip, InCorso(ip))~\})
\end{schema}

\begin{zed}
	ComandoGames \defs ComandoGamesOk \pipe Spedisci
\end{zed}

\subsubsection{Comando STAT}

Il comando {\bf stat} permette ad un utente di visualizzare informazioni su un
singolo giocatore (senza parametri descrive i dati del giocatore stesso). Ogni
giocatore \`e descritto dai seguenti dati: nome, rating, status (sta giocando,
\`e disposto a giocare, non vuol giocare, non connesso).
Non vi sono casi di errore. Se l'utente specificato non \`e registrato viene
visualizzato il valore di rating $NonAssegnato$.

La presenza del parametro \`e discriminata dalla funzione $is$, quindi
descriviamo il comando mediante due schemi distinti.
\begin{schema}{StatOk}
	XiComando \\
	Receiver!: ID \\
	Nomi!: \finset USERNAME
\where
	is(Comando?, Stat) = TRUE \\
	Receiver! = Sender? \\
	Nomi! = \{User\}
\end{schema}

\begin{schema}{StatUtenteOk}
	XiComando \\
	Receiver!: ID \\
	Nomi!: \finset USERNAME
\where
	is(Comando?, StatUtente) = TRUE \\
	Receiver! = Sender? \\
	Nomi! = \{EstraiNomeUtente(Comando?)\}
\end{schema}

\begin{schema}{FineStatRegistrato}
	\Xi Server \\
	Nomi?: \finset USERNAME \\
	Info?: USERNAME \pfun UtenteRegistrato \\
	Receiver?, Receiver!: ID \\
	Contenuto!: CONTENUTO
\where
	Receiver! = Receiver? \\
	\exists_1 n: USERNAME; c:FLAG | n \in \dom Info? \spot Contenuto! =
RisultatoStat(n, (Info?(n)).Elo, \\
\t1	    \IF n \in \dom IdUtente \land c \in (StatoUtente(n)
\setminus \{Regis\}) \THEN c \ELSE NonCollegato)
\end{schema}

\begin{schema}{FineStatNonRegistrato}
	\Xi Server \\
	Nomi?: \finset USERNAME \\
	Info?: USERNAME \pfun UtenteRegistrato \\
	Receiver?, Receiver!: ID \\
	Contenuto!: CONTENUTO
\where
	Receiver! = Receiver? \\
	\dom Info? = \emptyset \\
	\exists_1 n: USERNAME; c:FLAG | n \in Nomi? \spot Contenuto! = RisultatoStat(n,
NonAssegnato, \\
\t1	    \IF n \in \dom IdUtente \land c \in StatoUtente(n)
\THEN c \ELSE NonCollegato)
\end{schema}

\begin{zed}
	ComandoStat \defs (StatOk \lor StatUtenteOk) \pipe LeggiDbRegistrati
\pipe {} \\
\t1		(FineStatRegistrato \lor FineStatNonRegistrato) \pipe Spedisci
\end{zed}

\subsubsection{Comando SET}

Il comando {\bf set} permette ad un utente di cambiare il proprio status
dichiarandosi disposto o non disposto a giocare. Non vi sono casi di errore.
Lo stato nel quale si vuole porre l'utente \`e discriminato dalla funzione
$is$.
\begin{schema}{ComandoSetOpenOk}
	DeltaComando
\where
	is(Comando?, SetOpen) = TRUE
\also
	StatoUtente' = StatoUtente \oplus
		\{User \mapsto ((StatoUtente(User) \setminus \{Close\})
\cup \{Open\})\} \\
\end{schema}

\begin{schema}{ComandoSetCloseOk}
	DeltaComando
\where
	is(Comando?, SetClose) = TRUE
\also
	StatoUtente' = StatoUtente \oplus
		\{User \mapsto ((StatoUtente(User) \setminus \{Open\})
\cup \{Close\})\} \\
	Sfide' = Sfide \setminus \{~x : Sfida | x \in Sfide \land User \in \{x.Sfidante,x.Sfidato\}~\}
\end{schema}

\begin{zed}
	ComandoSet \defs ComandoSetOpenOk \lor ComandoSetCloseOk
\end{zed}

\subsubsection{Comando OBSERVE}

Il comando {\bf observe} permette ad un utente di porsi in osservazione di una
nuova partita. Si pu\`o specificare o il numero della partita, oppure il nome
di uno dei giocatori che vi partecipano. Al solito la distinzione fra i due
casi viene fatta dalla funzione $is$. Poich\'e il numero massimo di partite
osservabili da un utente \`e limitato, se si cerca di osservare troppe partite
si ha una segnalazione di errore. Una segnalazione analoga avviene se si
specifica una partita non in corso o un utente che non sta giocando.
\begin{axdef}
	AggiungiOsservatore: PartitaInCorso \cross USERNAME \fun PartitaInCorso
\end{axdef}

$NumOsservabili$ \`e il numero di partite osservabili.
\begin{axdef}
	NumOsservabili : \nat
\end{axdef}

\begin{schema}{ComandoObserveIdOk}
	DeltaComando
\where
	is(Comando?, ObserveId) = TRUE \\
	EstraiPartita(Comando?) \in \dom InCorso \\
	\#\{~id : INDICEPARTITA | id \neq EstraiPartita(Comando?) \land \\
\t1		id \in \dom InCorso \land User \in (InCorso(id)).Osservatori~\} <
NumOsservabili
\also
	InCorso' = InCorso \oplus \{~EstraiPartita(Comando?) \mapsto {} \\
\t1		AggiungiOsservatore(InCorso(EstraiPartita(Comando?)), User)~\}
\end{schema}

\begin{schema}{ComandoObserveNameOk}
	DeltaComando
\where
	is(Comando?, ObserveName) = TRUE \\
	\exists nuova: INDICEPARTITA| nuova \in \dom InCorso \land {} \\
\t1	    EstraiNomeUtente(Comando?) \in \dom ((InCorso(nuova)).Giocatori) \spot
\\
\t2		((\#\{~id : INDICEPARTITA | id \neq nuova \land id \in \dom
InCorso \land {} \\
\t4		    User \in (InCorso(id)).Osservatori~\} <
NumOsservabili) \land {}
\also
	InCorso' = InCorso \oplus \{~nuova \mapsto {} \\
\t1		AggiungiOsservatore(InCorso(nuova), User)~\})
\end{schema}

\begin{schema}{ObserveIdErrata}
	XiComando \\
\where
	is(Comando?, ObserveId) = TRUE \\
	(EstraiPartita(Comando?) \notin \dom InCorso \lor {} \\
\t1	\#\{~id : INDICEPARTITA | id \neq EstraiPartita(Comando?) \land \\
\t2		id \in \dom InCorso \land User \in (InCorso(id)).Osservatori~\}
\geq NumOsservabili)
\end{schema}

\begin{schema}{ObserveNameErrata}
	XiComando
\where
	is(Comando?, ObserveName) = TRUE \\
	((\forall id: INDICEPARTITA| id \in \dom InCorso \spot \\
\t2		EstraiNomeUtente(Comando?) \notin \dom (InCorso(id)).Giocatori)
\lor {} \\
\t1	(\exists nuova: INDICEPARTITA| nuova \in \dom InCorso \land {} \\
\t2	    EstraiNomeUtente(Comando?) \in \dom (InCorso(nuova)).Giocatori \spot
\\
\t3	    \#\{~id : INDICEPARTITA | id \neq nuova \land id \in \dom InCorso
\land {} \\
\t4		User \in (InCorso(id)).Osservatori~\} \geq NumOsservabili))
\end{schema}

\begin{zed}
	ComandoObserve \defs ComandoObserveIdOk \lor ComandoObserveNameOk \lor
{} \\
\t1		(((ObserveIdErrata \lor ObserveNameErrata) \land NonConsentito)
\pipe Spedisci)
\end{zed}

% ***************************************************************************
\subsection{Comandi di comunicazione fra utenti}
% ***************************************************************************

Si suppongono date le seguenti funzioni che manipolano i messaggi sia
in ingresso che in uscita eseguendo le conversioni opportune.

\begin{axdef}
	RisultatoShout: USERNAME \cross STRINGA \inj CONTENUTO \\
	RisultatoTell: USERNAME \cross STRINGA \inj CONTENUTO \\
	RisultatoChannels: (CANALE \fun \finset USERNAME) \inj CONTENUTO
\end{axdef}

\subsubsection{Comando SHOUT}

Il comando {\bf shout} permette ad un utente di spedire un
messaggio testuale a tutti gli utenti collegati al suo stesso {\it server}.
Se l'utente che esegue {\bf shout} \`e in un canale il messaggio viene inviato
solamente agli altri utenti che
appartengono allo stesso canale. Se invece l'utente non \`e in un canale pu\`o
eseguire {\bf shout} solamente se \`e registrato. In tal caso il suo messaggio
viene inviato a tutti gli utenti collegati a quel {\it server}.

Distinguiamo il caso di utenti registrati e non con due schemi distinti.
\begin{schema}{ShoutRegistratoOk}
	XiComando \\
	Receivers!: \finset ID ; Contenuto!: CONTENUTO
\where
	is(Comando?, Shout) = TRUE \\
	Regis \in StatoUtente(User)
\also
	\exists can:\finset CANALE; ins: \finset ID @ (\forall c: CANALE | c \in can @ User \in Canali(c)) \land {} \\
\t2	ins = \bigcup \{~c: CANALE | c \in can @ IdUtente\limg Canali(c) \rimg~\} \land {} \\
\t2	Receivers! = (\IF ins = \emptyset \THEN (\ran IdUtente) \ELSE ins) \setminus \{~Sender?~\} \\ 
	Contenuto! = RisultatoShout(User, EstraiTesto(Comando?))
\end{schema}

\begin{schema}{ShoutNonRegistratoOk}
	XiComando \\
	Receivers!: \finset ID ; Contenuto!: CONTENUTO
\where
	is(Comando?,Shout) = TRUE \\
	Regis \notin StatoUtente(User) \\
	\exists can:\finset CANALE | can \neq \emptyset @ (\forall c: CANALE | c \in can @ User \in Canali(c)) \land {} \\
\t2	Receivers! = \bigcup \{~c: CANALE | c \in can @ IdUtente\limg Canali(c) \setminus \{User\} \rimg~\} \land {} \\
\t2		Contenuto! = RisultatoShout(User,EstraiTesto(Comando?))
\end{schema}

\begin{schema}{ShoutNonConsentito}
	NonConsentito
\where
	is(Comando?,Shout) = TRUE \\
	Regis \notin StatoUtente(User) \\
	\forall c:CANALE @ User \notin Canali(c)
\end{schema}

Lo schema finale per il comando {\bf shout} \`e il seguente.
\begin{zed}
	ComandoShout \defs ((ShoutRegistratoOk \lor ShoutNonRegistratoOk) \pipe
Broadcast) \lor {} \\
\t1		(ShoutNonConsentito \pipe Spedisci)
\end{zed}


\subsubsection{Comando TELL}

Un utente pu\`o comunicare direttamente con un altro utente collegato allo
stesso sito mediante il comando {\bf tell}. Se l'utente sta giocando una
partita si omette nel comando lo {\it username} dell'utente con il quale si
vuol colloquiare e si assume che tale utente sia il suo avversario.

Distinguiamo il caso in cui l'utente sta giocando una partita mediante due
schemi distinti. Come caso di errore \`e previsto che si chieda di comunicare
con un utente non collegato.
\begin{schema}{TellAChiunqueOk}
	XiComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?, Tell) = TRUE \\
	\forall p: PartitaInCorso | p \in \ran InCorso @ User \notin \dom p.Giocatori \\
	EstraiNomeUtente(Comando?) \in \dom IdUtente
\also
	Receiver! = IdUtente(EstraiNomeUtente(Comando?)) \\
	Contenuto! = RisultatoTell(User, EstraiTesto(Comando?))
\end{schema}

\begin{schema}{TellAvversarioOk}
	XiComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?,Tell) = TRUE \\
	\exists p: PartitaInCorso | p \in \ran InCorso \land User \in \dom
p.Giocatori @ \\
\t2		\exists_1 g:USERNAME | g \in \dom p.Giocatori \setminus \{User\}
@ \\
\t3		Receiver! = IdUtente (g) \land {} \\
\t2		Contenuto! = RisultatoTell(User, EstraiTesto(Comando?))
\end{schema}

\begin{schema}{TellASconosciuto}
	XiComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?,Tell) = TRUE \\
	\forall p: PartitaInCorso | p \in \ran InCorso @ User \notin \dom
p.Giocatori \\
	EstraiNomeUtente(Comando?) \notin \dom IdUtente \\
	Receiver! = Sender? \\
	Contenuto! = UtenteNonCollegato
\end{schema}

Lo schema finale per il comando {\bf tell} \`e il seguente.
\begin{zed}
	ComandoTell \defs (TellAChiunqueOk \lor TellAvversarioOk \lor
TellASconosciuto) \pipe Spedisci
\end{zed}


\subsubsection{Comando INCHANNEL}

Gruppi di utenti possono stabilire comunicazioni riservate al gruppo entrando
in un canale; i canali sono distinti per numero. Per entrare in un canale si
usa il comando {\bf inchannel} dove come parametro si comunica il numero del
canale nel quale si vuole entrare. Tutti gli utenti sono abilitati ad eseguire
questa operazione. L'unica condizione di errore \`e se si specifica un numero
di canale inesistente. Un utente pu\`o anche entrare in pi\`u canali. Se si
\`e gi\`a nel canale dove si richiede di entrare il comando non ha effetto.
\begin{schema}{ComandoInChannelOk}
	DeltaComando
\where
	is(Comando?,InChannel) = TRUE \\
	EstraiCanale(Comando?) \in \dom Canali
\also
	Canali' = Canali \oplus \{EstraiCanale(Comando?) \mapsto
		(Canali(EstraiCanale(Comando?)) \cup \{User\})\}
\end{schema}

Descriviamo quindi lo schema per il caso di errore definendo anche lo schema
$CanaleSconosciuto$ che utilizzeremo anche per il prossimo comando. Questo
schema riporta un errore se il numero di canale specificato \`e errato.
\begin{schema}{CanaleSconosciuto}
	XiComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	EstraiCanale(Comando?) \notin \dom Canali
\also
	Receiver! = Sender? \\
	Contenuto! = NumCanaleNonConosciuto
\end{schema}

\begin{schema}{InChannelNonValida}
	CanaleSconosciuto
\where
	is(Comando?,InChannel) = TRUE
\end{schema}

Lo schema finale per il comando {\bf inchannel} \`e il seguente.
\begin{zed}
	ComandoInChannel \defs ComandoInChannelOk \lor (InChannelNonValida
\pipe Spedisci)
\end{zed}


\subsubsection{Comando OUTCHANNEL}

Per uscire da un canale si
usa il comando {\bf outchannel} dove come parametro si comunica il numero del
canale dal quale si vuole uscire. Tutti gli utenti sono abilitati ad eseguire
questa operazione. L'unica condizione di errore \`e se si specifica un numero
di canale inesistente. Se un utente esce da un canale nel quale non era
entrato il comando non ha alcun effetto ma non \`e considerata una condizione
di errore.
\begin{schema}{ComandoOutChannelOk}
	DeltaComando
\where
	is(Comando?,OutChannel) = TRUE \\
	EstraiCanale(Comando?) \in \dom Canali
\also
	Canali' = Canali \oplus \{EstraiCanale(Comando?) \mapsto
		(Canali(EstraiCanale(Comando?)) \setminus \{User\})\}
\end{schema}

\begin{schema}{OutChannelNonValida}
	CanaleSconosciuto
\where
	is(Comando?,OutChannel) = TRUE
\end{schema}

Lo schema finale per il comando {\bf outchannel} \`e il seguente.
\begin{zed}
	ComandoOutChannel \defs ComandoOutChannelOk \lor (OutChannelNonValida \pipe Spedisci)
\end{zed}


\subsubsection{Comando CHANNELS}

Il comando {\bf channels} visualizza i canali attivi e gli utenti che vi sono
collegati. Tutti gli utenti sono abilitati ad eseguire
questa operazione. Non sono previste condizioni di errore.
\begin{schema}{ComandoChannelsOk}
	XiComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?,Channels) = TRUE \\
\also
	Receiver! = Sender? \\
	Contenuto! = RisultatoChannels(Canali)
\end{schema}
Lo schema finale per il comando {\bf channels} \`e il seguente.
\begin{zed}
	ComandoChannels \defs ComandoChannelsOk \pipe Spedisci
\end{zed}


% ***************************************************************************
\subsection{Gestione delle sfide e delle partite}
% ***************************************************************************

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{funzioni per la gestione delle partite}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

A partire dallo schema $PartitaInCorso$ possiamo definire alcune funzioni per
manipolare le partite in corso: $NuovaPartita$ prende in input il nome dei
giocatori e i tempi della sfida ed restituisce una partita in Corso;
$NuovoMossa$ prende in input una $PartitaInCorso$, una $SEMIMOSSA$ ed
restituisce una $PartitaInCorso$ aggiornando anche i tempi di gioco in base
a quando \`e avvenuta l'ultima mossa ($UltimaMossa$).

\begin{axdef}
  NuovaPartita: USERNAME \cross USERNAME \cross TEMPO \cross TEMPO \pfun PartitaInCorso
\where
  \forall U1,U2: USERNAME; T1,T2: TEMPO @ (\exists P:PartitaInCorso @ \\
	\t1 P.Giocatori = \{U1 \mapsto Bianco, U2 \mapsto Nero\} \land {} \\
	\t1 P.Tempi = \{U1 \mapsto 60*T1, U2 \mapsto 60*T1\} \land {} \\
	\t1 P.T1 = T1 \land P.T2 = T2 \land {} \\
	\t1 P.Mosse = \langle \rangle \land {} \\
	\t1 P.Risultato = IndRisultato \land P.Data = DataAttuale \land {} \\
	\t1 P.Stato = \emptyset \land {} \\
	\t1 P.Osservatori = \emptyset \land {} \\
	\t1 P.UltimaMossa = OraAttuale \land {} \\
	\t1 P.DeveMuovere = Bianco \land {} \\
		\t2 NuovaPartita(U1, U2, T1, T2) = P)
\end{axdef}

\begin{axdef}
  NuovaMossa: PartitaInCorso \cross SEMIMOSSA \pfun PartitaInCorso
\where
  \forall P1: PartitaInCorso; M: SEMIMOSSA @ (\exists P2: PartitaInCorso @ \\
	\t1 P2.Mosse = P1.Mosse \cat \langle M \rangle \land {} \\
	\t1 MosseLegali(P2.Mosse) = TRUE \land {} \\
	\t1 P2.Giocatori = P1.Giocatori \land {} \\
	\t1 P2.T1 = P1.T1 \land P2.T2 = P1.T2 \land P2.Data = P1.Data \land {} \\
	\t1 P2.Risultato = P1.Risultato \land {} \\
	\t1 P2.Tempi = P1.Tempi \oplus \\
\t2		\{P1.Giocatori \inv (P1.DeveMuovere) \mapsto
		(P1.Tempi(P1.Giocatori \inv (P1.DeveMuovere)) + {} \\
	\t5 OraAttuale - P1.UltimaMossa + P1.T2)\} \land {} \\
	\t1 P2.Osservatori = P1.Osservatori \land {} \\
	\t1 P2.UltimaMossa = OraAttuale \land {} \\
	\t1 P2.DeveMuovere = \IF P1.DeveMuovere = Bianco \THEN Nero \ELSE Bianco \land {} \\
		\t2 NuovaMossa(P1, M) = P2)
\end{axdef}

Le seguenti funzioni estraggono dal contenuto del messaggio i parametri
per i relativi comandi:

\begin{axdef}
	EstraiMatch: CONTENUTO \inj USERNAME \cross TEMPO \cross TEMPO \\
	EstraiMatchSenzaTempi: CONTENUTO \inj USERNAME \\
	EstraiAccept: CONTENUTO \inj USERNAME \\
	EstraiMossa: CONTENUTO \inj SEMIMOSSA
\end{axdef}

I comandi di gestione delle sfide e delle partite devono spedire un
messaggio all'utente coinvolto, quindi le seguenti funzioni costruiscono
il messaggio in maniera differente da comando a comando.

\begin{axdef}
	MsgSfida: USERNAME \cross TEMPO \cross TEMPO \inj CONTENUTO \\
	MsgSfidaSospesa: USERNAME \inj CONTENUTO \\
	MsgPartita: PartitaInCorso \inj CONTENUTO \\
	MsgDecline: USERNAME \inj CONTENUTO \\
	MsgPartitaTerminata: Partita \surj CONTENUTO \\
	MsgPropostaPatta: USERNAME \inj CONTENUTO \\
	MsgPropostaSospensione: USERNAME \inj CONTENUTO \\
	MsgMossa: SEMIMOSSA \cross TEMPO \cross TEMPO \inj CONTENUTO \\
	MsgOsservatori: PartitaInCorso \cross INDICEPARTITA \inj CONTENUTO
\also
	MsgMatchSbagliato,MsgAcceptSbagliato, MsgAcceptDrawSbagliato : CONTENUTO \\
	MsgNonStaGiocando, MsgFlagSbagliato: CONTENUTO
\end{axdef}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Comando MATCH}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Il comando {\bf Match} \`e specificato con due schemi diversi, il primo
per gestire il caso che nel comando ci siano i tempi di gioco, il secondo
per riprendere una partita sospesa.
I due schemi sono abbastanza simili, quello che devono fare \`e creare una
nuova sfida, eliminando quelle in pi\`u (ad esempio se si vogliono proporre
tempi di gioco differenti, la precedente sfida decade).
Le precondizioni sono che i due utenti non stiano gi\`a giocando e che siano
disposti a giocare.
Entrambi gli schemi spediscono un messaggio all'utente sfidato.

\begin{schema}{MatchConTempiOk}
	DeltaComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?, MatchConTempi) = TRUE\\
	StatoUtente(User) \cap \{Gioca, Close\} = \emptyset
\also
	\exists U2: USERNAME; T1,T2: TEMPO; oldsf: \finset Sfida; s: Sfida |\\
	\t1 EstraiMatch(Comando?) = (U2, T1, T2) \land U2 \in \dom(IdUtente) \land {} \\
	\t1 StatoUtente(U2) \cap \{Gioca, Close\} = \emptyset \land {} \\
	\t1 s.Sfidante = User \land s.Sfidato = U2 \land s.T1 = T1 \land s.T2 = T2 \land {} \\
	\t1 oldsf = \{x: Sfida | x \in Sfide \land (x.Sfidante = User \lor {} \\
	\t1 \{x.Sfidante , x.Sfidato\} = \{User, U2\})\} @ 
		Sfide' = (Sfide \setminus oldsf) \cup \{s\} \land {}\\
		\t2 Receiver! = IdUtente(U2) \land {} \\
		\t2 Contenuto! = MsgSfida(User, T1, T2)
\end{schema}

\begin{schema}{MatchSenzaTempiOk}
	DeltaComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?, MatchSenzaTempi) = TRUE \\
	StatoUtente(User) \cap \{Gioca, Close\} = \emptyset
\also
	\exists U2: USERNAME; oldsf: \finset Sfida; s: Sfida | \\
	\t1 EstraiMatchSenzaTempi(Comando?) = U2 \land U2 \in \dom(IdUtente) \land {} \\
	\t1 StatoUtente(U2) \cap \{Gioca, Close\} = \emptyset \land {} \\
	\t1 s.Sfidante = User \land s.Sfidato = U2 \land s.T1 = IndTempo \land s.T2 = IndTempo \land {} \\
	\t1 oldsf = \{x: Sfida | x \in Sfide \land {} \\
	\t3 (x.Sfidante = User \lor \{x.Sfidante , x.Sfidato\} = \{User, U2\})\} @ \\
\t2 			Sfide' = (Sfide \setminus oldsf) \cup \{s\} \land {} \\
\t2 			Receiver! = IdUtente(U2)  \land {} \\
\t2 			Contenuto! = MsgSfidaSospesa(User)
\end{schema}

I prossimi due schemi gestiscono il caso di errore nel comando match con i
tempi e match senza tempi.

\begin{schema}{MatchConKo}
	XiComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?, MatchConTempi) = TRUE \\
	StatoUtente(User) \cap \{Gioca, Close\} \neq \emptyset \lor {} \\
\t1	(\forall U2: USERNAME; T1,T2: TEMPO | EstraiMatch(Comando?) =
(U2, T1, T2) @ \\
	\t2 U2 \notin \dom(IdUtente) \lor StatoUtente(U2) \cap \{Gioca, Close\} \neq \emptyset)
\also
	Receiver! = IdUtente(User) \\
	Contenuto! = MsgMatchSbagliato
\end{schema}

\begin{schema}{MatchSenzaKo}
	XiComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?, MatchSenzaTempi) = TRUE \\
	StatoUtente(User) \cap \{Gioca, Close\} \neq \emptyset \lor {} \\
	(\forall U2: USERNAME | EstraiMatchSenzaTempi(Comando?) = U2 @ \\
	\t1 U2 \notin \dom(IdUtente) \lor StatoUtente(U2) \cap \{Gioca, Close\} \neq \emptyset)
\also
	Receiver! = IdUtente(User) \\
	Contenuto! = MsgMatchSbagliato
\end{schema}

Lo schema finale per il comando {\bf match} \`e il seguente:

\begin{zed}
  ComandoMatch \defs (MatchConTempiOk \lor MatchSenzaTempiOk \lor {} \\
  \t1 MatchConKo \lor MatchSenzaKo) \pipe Spedisci
\end{zed}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Comando ACCEPT}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Il comando {\bf accept} controlla che esista una sfida in corso, e
in questo caso cambia lo stato del server: aggiunge una partita in
corso, elimina tutte le sfide che rigurdavano i due giocatori,
cambia gli stati degli utenti, se necessario elimina la partita
sospesa eventualmente sospesa e, infine, spedisce un messaggio ai due giocatori
con gli estremi della partita.

Si utilizza la funzione {\it CopiaPartitaInCorso} per trasformare una partita
sospesa in una in corso; inoltre {\it NuovoIndice} restituisce un indice non 
utilizzato per una partita in corso.

\begin{axdef}
	CopiaPartitaInCorso: Partita \pinj PartitaInCorso \\
	NuovoIndice: \finset INDICEPARTITA \surj INDICEPARTITA \\
\end{axdef}

\begin{schema}{AcceptOk}
	DeltaComando \\
	Receivers! : \finset ID ; Contenuto! : CONTENUTO
\where
	is(Comando?, Accept) = TRUE
\also
	\exists s:Sfida; nome:USERNAME; oldsf: \finset Sfida; p: PartitaInCorso | \\
	\t1 EstraiAccept(Comando?) = nome \land {} \\
	\t1 s \in Sfide \land s.Sfidante = nome \land s.Sfidato = User \land {} \\
	\t1 oldsf = \{x: Sfida | x \in Sfide \land \{x.Sfidante,x.Sfidato\} \cap \{User,nome\} \neq \emptyset \} \land {} \\
	\t1 p = \IF s.T1 = IndTempo \THEN CopiaPartitaInCorso(Sospese(\{User,nome\})) \\
		\t5 \ELSE NuovaPartita(User,nome,s.T1,s.T2) @ \\
\t2	Sfide' = Sfide \setminus oldsf \land {} \\
\t2	Sospese' = \IF p.Mosse = \langle \rangle \THEN Sospese \ELSE (\{\{User,nome\}\} \ndres Sospese) \land {} \\
\t2	InCorso' = InCorso \cup \{NuovoIndice(\dom InCorso) \mapsto p\} \land {} \\
\t2	StatoUtente' = StatoUtente \oplus
		\{User \mapsto StatoUtente(User) \setminus \{Open\} \cup \{Gioca\}, \\
\t3		nome \mapsto StatoUtente(nome) \setminus \{Open\} \cup \{Gioca\}\} \land {} \\
\t2	Receivers! = \{IdUtente(User),IdUtente(nome)\} \land {} \\
\t2	Contenuto! = MsgPartita(p)
\end{schema}

Lo schema seguente gestisce i casi di errore del comando accept.

\begin{schema}{AcceptKo}
	XiComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?, Accept) = TRUE \\
	\forall s:Sfida; nome:USERNAME | \\
	\t1 EstraiAccept(Comando?) = nome \land s \in Sfide @ \\
	\t2 s.Sfidante \neq nome \lor s.Sfidato \neq User \\
\also
	Receiver! = IdUtente(User) \\
	Contenuto! = MsgAcceptSbagliato
\end{schema}

Lo schema finale per il comando {\bf accept} \`e il seguente:

\begin{zed}
  ComandoAccept \defs (AcceptOk \pipe Broadcast) \lor (AcceptKo \pipe Spedisci)
\end{zed}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Comando DECLINE}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Il comando {\bf decline} elimina tutte le sfide rivolte ad un utente, e
invia un messaggio agli utenti che avevano proposto la sfida. Non ci sono
casi di errore siccome si ritiene corretto che l'insieme delle sfide da
declinare possa essere anche vuoto.

\begin{schema}{DeclineOk}
	DeltaComando \\
	Receivers! : \finset ID ; Contenuto! : CONTENUTO
\where
	is(Comando?, Decline) = TRUE
\also
	\exists oldsf: \finset Sfida | oldsf = \{x: Sfida | x.Sfidato = User \} @ \\
\t1	Sfide' = Sfide \setminus oldsf \land {} \\
\t1	Receivers! = \{x: Sfida | x \in oldsf @ IdUtente(x.Sfidante)\} \land {} \\
\t1	Contenuto! = MsgDecline(User)
\end{schema}

Lo schema finale per il comando {\bf decline} \`e il seguente:

\begin{zed}
  ComandoDecline \defs DeclineOk \pipe Broadcast
\end{zed}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Comando RESIGN}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Il comando {\bf resign} fa abbandonare una partita. E' definito uno
schema $Fine$ che serve per cambiare lo stato del server in caso che
la partita termini; in particolare lo schema di $Fine$ toglie la
partita in corso, cambia gli stati dei due giocatori, spedisce un messaggio
di fine partita, se necessario invia per posta le partite, e sempre
se necessario registra la partita nel data base.
Questo schema di fine verr\`a utilizzato ogni volta che un comando
fa terminare la partita.

\begin{schema}{FinePartita}
	\Delta Server
\also
	HaVinto? : COLORE\\
	Finita? : INDICEPARTITA\\
	Part! : Partita\\
	Receivers! : \finset ID\\
	Contenuto! : CONTENUTO
\where
	\exists U1,U2: USERNAME |
		\{U1,U2\} = \dom ((InCorso(Finita?)).Giocatori) @ \\
\t1	Part! = CopiaPartita(InCorso(Finita?)) \land {} \\
\t1	Part!.Risultato = \IF (HaVinto?=Bianco) \THEN VittoriaBianco \\
\t2		\ELSE \IF (HaVinto?=Nero) \THEN VittoriaNero \ELSE Patta \land {} \\
\t1	InCorso' = \{Finita?\} \ndres InCorso  \land {} \\
\t1	StatoUtente' = StatoUtente \oplus
	\{U1 \mapsto StatoUtente(U1)\setminus \{Gioca\} \cup \{Open\}, \\
\t2		U2 \mapsto StatoUtente(U2) \setminus \{Gioca\} \cup \{Open\} \} \land {} \\
\t1	Receivers! = \{IdUtente(U1),IdUtente(U2)\} \land {} \\
\t1	Contenuto! = MsgPartitaTerminata(Part!)
\end{schema}

Il prossimi due schemi servono per spedire e registrare una partita o meno.

\begin{schema}{SpedisciMatch}
	\Xi Server
\also
	Part?: Partita \\
	DestPosta!: \finset USERNAME \\
	Posta!: \finset Partita
\where
	\exists U1,U2: USERNAME | \{U1,U2\} = \dom(Part?.Giocatori) \land {} \\
	\t1 Regis \in StatoUtente(U1) \cap StatoUtente(U2) @ \\
	\t2 Posta! = \{Part?\} \land DestPosta! = \{U1,U2\}
\end{schema}

\begin{schema}{NonSpedireMatch}
	\Xi Server
\also
	Part?: Partita \\
\where
	\exists U1,U2: USERNAME | \{U1,U2\} = \dom(Part?.Giocatori) @ \\
	\t1 Regis \notin StatoUtente(U1) \cap StatoUtente(U2)
\end{schema}

\begin{schema}{ResignOk}
	XiComando \\
	HaVinto! : COLORE\\
	Finita! : INDICEPARTITA
\where
	is(Comando?,Resign) = TRUE
\also
	\exists i: INDICEPARTITA; U1: USERNAME | i \in \dom(InCorso) \land {} \\
	\t1 \{U1,User\} = \dom((InCorso(i)).Giocatori) @ \\
	\t2 Finita! = i \land HaVinto! = (InCorso(i)).Giocatori(U1)
\end{schema}

Lo schema seguente gestisce il caso di errore in cui un utente non sta
giocando. Questo schema verr\`a utilizzato anche in altri comandi.

\begin{schema}{NonStaGiocando}
	XiComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?,Resign) = TRUE \\
	Gioca \notin StatoUtente(User) \\
\also
	Receiver! = IdUtente(User) \\
	Contenuto! = MsgNonStaGiocando
\end{schema}

Gli schemi finali per la terminazione di una partita e per il comando
{\bf resign} sono i seguenti:

\begin{zed}
  Fine \defs FinePartita \pipe (Broadcast \land (SpedisciMatch \land \\
	\t1 InserisciPartita \land AggiornaElo \lor NonSpedireMatch))
\also
  ComandoResign \defs (ResignOk \pipe Fine) \lor (NonStaGiocando \pipe Spedisci)
\end{zed}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Comando FLAG}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Il comando {\bf flag} termina una partita dando la vittoria se l'avversario
ha finito il tempo a sua disposizione. Fa uso dello schema $Fine$ per
terminare la partita.

\begin{schema}{FlagOk}
	XiComando \\
	HaVinto! : COLORE\\
	Finita! : INDICEPARTITA
\where
	is(Comando?,Flag) = TRUE
\also
	\exists i: INDICEPARTITA; U1: USERNAME | i \in \dom(InCorso) \land {} \\
\t1	\{U1,User\} = \dom ((InCorso(i)).Giocatori) \land (InCorso(i)).Tempi(U1) <
0 @ \\
\t2 	Finita! = i \land HaVinto! = (InCorso(i)).Giocatori(User)
\end{schema}

Lo schema d'errore seguente gestisce il caso in cui un giocatore esegue
il comando flag pur non essendo scaduto il tempo a disposizione
dell'avversario.

\begin{schema}{FlagKo}
	XiComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?,Flag) = TRUE \\
	\exists i: INDICEPARTITA; U1: USERNAME | i \in \dom(InCorso) \land {} \\
\t1	\{U1,User\} = \dom ((InCorso(i)).Giocatori) @ (InCorso(i)).Tempi(U1) \geq 0
\\
\also
	Receiver! = IdUtente(User) \\
	Contenuto! = MsgFlagSbagliato
\end{schema}

Lo schema finale per il comando {\bf flag} \`e il seguente:

\begin{zed}
  ComandoFlag \defs (FlagOk \pipe Fine) \lor (FlagKo \pipe Spedisci)
\end{zed}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Comandi PROPOSEDRAW e ACCEPTDRAW}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

I Comando {\bf proposedraw} e {\bf acceptdraw} servono per proporre ed
accettare la patta. Il primo comando controlla che la partita
esista e quindi cambia lo stato della partita aggiungendo un legame
nella funzione $StatoPartita$ da $PropostaPatta$ al colore del giocatore
che l'ha proposta (questo viene fatto dalla funzione $Richiesta$).
Il comando {\bf acceptdraw}, invece, controlla che esista gi\`a un legame
nella funzione $StatoPartita$ che va da $PropostaPatta$ al colore
dell'avversario, quindi conclude la partita con il risultato di patta.

\begin{axdef}
	Richiesta: PartitaInCorso \cross USERNAME \cross STATOPARTITA \pinj PartitaInCorso \\
\where
	\forall P1: PartitaInCorso; User: USERNAME; s: STATOPARTITA @ (\exists P2: PartitaInCorso @\\
	\t1 P2.Giocatori = P1.Giocatori \land P2.Mosse = P1.Mosse \land {} \\
	\t1 P2.T1 = P1.T1 \land P2.T2 = P1.T2 \land P2.Tempi = P1.Tempi \land {} \\
	\t1 P2.Risultato = P1.Risultato \land P2.Osservatori = P1.Osservatori \land {} \\
	\t1 P2.DeveMuovere = P1.DeveMuovere \land P2.UltimaMossa = P1.UltimaMossa \land {} \\
	\t1 P2.Stato = P1.Stato \oplus \{s \mapsto P1.Giocatori(User)\} \land {} \\
		\t2 Richiesta(P1, User, s) = P2)
\end{axdef}

\begin{schema}{ProposeDrawOk}
	DeltaComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?,ProposeDraw) = TRUE
\also
	\exists i: INDICEPARTITA; U1: USERNAME | i \in \dom(InCorso) \land {} \\
\t1		\{U1,User\} = \dom((InCorso(i)).Giocatori) @ \\
\t2	InCorso' = InCorso \oplus \{i \mapsto Richiesta(InCorso(i),User, PropostaPatta)\} \land {} \\
\t2	Receiver! = IdUtente(U1) \land {} \\
\t2	Contenuto! = MsgPropostaPatta(User)
\end{schema}

Lo schema finale per il comando {\bf proposedraw} \`e il seguente:

\begin{zed}
 ComandoProposeDraw \defs (ProposeDrawOk \lor NonStaGiocando) \pipe Spedisci
\end{zed}

\begin{schema}{AcceptDrawOk}
	XiComando \\
	HaVinto! : COLORE\\
	Finita! : INDICEPARTITA
\where
	is(Comando?,AcceptDraw) = TRUE
\also
	\exists i: INDICEPARTITA | User \in \dom((InCorso(i)).Giocatori) \land {} \\
\t1	\{(InCorso(i)).Stato(PropostaPatta),(InCorso(i)).Giocatori(User)\}
		= \{Bianco,Nero\} @ \\
\t2		Finita! = i \land HaVinto! = IndColore
\end{schema}

Lo schema d'errore seguente gestisce il caso in cui un giocatore accetta la
patta pur non essendo stata offerta.

\begin{schema}{AcceptDrawKo}
	XiComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?,AcceptDraw) = TRUE \\
	\exists i: INDICEPARTITA | User \in \dom((InCorso(i)).Giocatori) @ \\
\t1	\{(InCorso(i)).Stato(PropostaPatta),(InCorso(i)).Giocatori(User)\}
		\neq \{Bianco,Nero\} \\
\also
	Receiver! = IdUtente(User) \\
	Contenuto! = MsgAcceptDrawSbagliato
\end{schema}

Lo schema finale per il comando {\bf acceptdraw} \`e il seguente:

\begin{zed}
  ComandoAcceptDraw \defs (AcceptDrawOk \pipe Fine) \lor (AcceptDrawKo \pipe Spedisci)
\end{zed}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Comandi ADJOURN e ACCEPTADJOURN}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

I comandi {\bf adjourn} e {\bf acceptajourn} servono per proporre ed
accettare la sospensione della partita. Il primo comando controlla che la
partita esista e che i giocatori siano registrati, quindi cambia lo stato
della partita aggiungendo un legame nella funzione $StatoPartita$ da
$PropostaSospens$ al colore del giocatore che l'ha proposta (questo viene
fatto dalla funzione $Richiesta$).
Il comando {\bf acceptadjourn}, invece, controlla che esista gi\`a un legame
nella funzione $StatoPartita$ che vada da $PropostaSosp$ al colore
dell'avversario, quindi sospende la partita togliendola dalle partite in
corso e mettendola in quelle sospese.

\begin{schema}{AdjournOk}
	DeltaComando \\
	Receiver!: ID ; Contenuto!: CONTENUTO
\where
	is(Comando?,Adjourn) = TRUE
\also
	\exists i: INDICEPARTITA; U1: USERNAME | i \in \dom(InCorso) \land {} \\
\t1	\{U1,User\} = \dom((InCorso(i)).Giocatori) \land {} \\
\t1	Regis \in StatoUtente(U1) \cap StatoUtente(User) @ \\
\t2	InCorso' = InCorso \oplus \{i \mapsto Richiesta(InCorso(i),User,PropostaSosp)\} \land {} \\
\t2	Receiver! = IdUtente(U1) \land {} \\
\t2	Contenuto! = MsgPropostaSospensione(User)
\end{schema}

Il seguente schema d'errore gestise il caso in cui un giocatore non
registrato chiede la sospensione.

\begin{schema}{NonRegistrato}
	NonConsentito
\where
	is(Comando?,Adjourn) = TRUE \\
	\exists i: INDICEPARTITA; U1: USERNAME | i \in \dom(InCorso) \land {} \\
\t1	\{U1,User\} = \dom((InCorso(i)).Giocatori) @ Regis \notin StatoUtente(U1) \cap StatoUtente(User)
\end{schema}

Lo schema finale per il comando {\bf adjourn} \`e il seguente:

\begin{zed}
  ComandoAdjourn \defs (AdjournOk \lor NonStaGiocando \lor NonRegistrato) \pipe Spedisci
\end{zed}

\begin{schema}{AcceptAdjournOk}
	DeltaComando \\
	Receivers!: \finset ID ; Contenuto!: CONTENUTO
\where
	is(Comando?,AcceptAdjourn) = TRUE
\also
	\exists i: INDICEPARTITA; U1: USERNAME | \\
\t1	\{U1,User\} = \dom((InCorso(i)).Giocatori) \land \\
\t1	\{(InCorso(i)).Stato(PropostaSosp),(InCorso(i)).Giocatori(User)\}
		= \{Bianco,Nero\} @ \\
\t2	Sospese' = Sospese \oplus \{\{U1,User\} \mapsto
			CopiaPartita(InCorso(i))\} \land {} \\
\t2	InCorso' = \{i\} \ndres InCorso \land {} \\
\t2	StatoUtente' = StatoUtente \oplus 
	\{U1 \mapsto StatoUtente(U1)\setminus \{Gioca\} \cup \{Open\}, \\
\t2		User \mapsto StatoUtente(User) \setminus \{Gioca\} \cup \{Open\} \} \land {} \\
\t2	Receivers! = \{IdUtente(U1),IdUtente(User)\} \land {} \\
\t2	Contenuto! = MsgPropostaSospensione(User)
\end{schema}

Il seguente schema di errore gestisce il caso in cui un gioctore accetta
la sospensione pur non essendo stata offerta.

\begin{schema}{AcceptAdjournKo}
	XiComando \\
	Receiver! : ID ; Contenuto! : CONTENUTO
\where
	is(Comando?,AcceptDraw) = TRUE \\
	\exists i: INDICEPARTITA | User \in \dom((InCorso(i)).Giocatori) @ \\
\t1	\{(InCorso(i)).Stato(PropostaSosp),(InCorso(i)).Giocatori(User)\}
		\neq \{Bianco,Nero\} \\
\also
	Receiver! = IdUtente(User) \\
	Contenuto! = MsgAcceptDrawSbagliato
\end{schema}

Lo schema finale per il comando {\bf acceptadjourn} \`e il seguente:

\begin{zed}
  ComandoAcceptAdjourn \defs (AcceptAdjournOk \pipe Broadcast) \lor 
	(AcceptAdjournKo \pipe Spedisci)
\end{zed}

% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
\subsubsection{Gestione delle mosse}
% +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

La gestione della mossa avviene con diversi schemi; il primo: $MossaOk$,
controlla la validit\`a della mossa e l'esistenza della partita, quindi
cambia le partite in corso, e infine invia un messaggio con la mossa sia
all'avversario che a tutti gli osservatori.

La funzione $Matto$ stabilisce se una sequenza di mosse porta allo scacco
matto.
\begin{axdef}
	Matto : MOSSE \surj BOOL
\end{axdef}

\begin{schema}{MossaOk}
	DeltaComando
\also
	Part!: INDICEPARTITA \\
	Receiver!: ID \\
	Contenuto!: CONTENUTO \\
	Receivers!: \finset ID \\
	Cont!: CONTENUTO
\where
	is(Comando?,Mossa) = TRUE \\
\also
	\exists m: SEMIMOSSA;i: INDICEPARTITA; U1: USERNAME | \\
	EstraiMossa(Comando?) = m \land {} \\
\t1	\{U1,User\} = \dom((InCorso(i)).Giocatori) \land {} \\
\t1	(InCorso(i)).Giocatori(User) = (InCorso(i)).DeveMuovere \land {} \\
\t1	MosseLegali((InCorso(i)).Mosse \cat \langle m \rangle) = TRUE @ \\
\t2	InCorso' = InCorso \oplus \{i \mapsto NuovaMossa(InCorso(i),m)\} \land \\
\t2	Receiver! = IdUtente(U1) \land {} \\
\t2	Contenuto! = MsgMossa(m,(InCorso(i)).Tempi(User),(InCorso(i)).Tempi(U1)) \land {} \\
\t2	Part! = i \\
	Receivers! = \{x: USERNAME | x \in (InCorso(Part!)).Osservatori @
		IdUtente(x)\} \\
	Cont!= MsgOsservatori(InCorso'(Part!),Part!)
\end{schema}

Il prossimi due schemi servono per stabilire se la mossa ha causato la fine
della partita oppure no.

\begin{schema}{ScaccoMatto}
	\Xi Server \\
	Part?: INDICEPARTITA\\
	HaVinto!: COLORE\\
	Finita!: INDICEPARTITA
\where
	Matto((InCorso(Part?)).Mosse) = TRUE \\
	HaVinto! = \IF (InCorso(Part?)).DeveMuovere = Bianco \THEN Nero \ELSE Bianco \\
	Finita! = Part?
\end{schema}

\begin{schema}{NoScaccoMatto}
	\Xi Server \\
	Part?: INDICEPARTITA
\where
	Matto((InCorso(Part?)).Mosse) = FALSE
\end{schema}

Lo schema finale inizia con gestire la mossa, mandare la mossa a tutti gli
osservatori, poi se c'\`e scacco matto si finisce la partita con $Fine$,
altrimenti si spedisce la mossa all'avversario. Per non rendere lo schema
troppo complicato non si \`e aggiunto lo schema di errore.

\begin{zed}
  ComandoMossa \defs MossaOk \pipe Broadcast[Cont!/Contenuto?] \pipe \\
  \t1 ((ScaccoMatto \pipe Fine) \lor (NoScaccoMatto \land Spedisci))
\end{zed}

% ***************************************************************************
\subsection{Gestione del Database Storico}
% ***************************************************************************

Il comando {\bf searchgames} utilizza lo schema omonimo definito nella sezione
relativa all'archivio storico. La funzione $EstraiSearch$ prende come
input il messaggio arrivato al server, e ritorna la coppia di giocatori
specificata nel comando; in caso sia presente un solo username la
funzione ritorna la coppia formata dall'username ripetuto due volte.
\begin{axdef}
	EstraiSearch: CONTENUTO \pfun USERNAME \cross USERNAME
\end{axdef}

\begin{schema}{EstraiCoppiaUsername}
  XiComando \\
  User1!, User2!: USERNAME \\
  Sender! : USERNAME
\where
  is(Comando?, Searchgames) = TRUE \\
  Sender! = User \\
  EstraiSearch(Comando?) = (User1!, User2!)
\end{schema}

\begin{zed}
  ComandoSearchGames \defs EstraiCoppiaUsername \pipe SearchGames
\end{zed}

% ***************************************************************************
\subsection{Gestione finale dei comandi}
% ***************************************************************************

Tutti i comandi vengono integrati in uno schema unico che utilizza lo schema
$Ricevi$ della comunicazione per l'acquisizione del comando e lo consuma
provando i possibili comandi.
\begin{zed}
	ConsumaComando \defs RichiestaCollegamento \lor RicezioneUsername \lor
	RicezionePassword \lor {} \\
\t1	ComandoExit \lor ComandoTopList \lor ComandoWho \lor ComandoPlayers \lor ComandoGames \lor {} \\
\t1	ComandoStat \lor ComandoFree \lor ComandoSet \lor ComandoObserve \lor ComandoShout \lor {} \\
\t1	ComandoTell \lor ComandoInChannel \lor ComandoOutChannel \lor ComandoChannels \lor {} \\
\t1	ComandoMatch \lor ComandoAccept \lor ComandoDecline \lor ComandoResign
\lor ComandoFlag \lor {} \\
\t1	ComandoProposeDraw \lor ComandoAcceptDraw \lor ComandoAdjourn \lor ComandoAcceptAdjourn \lor {} \\
\t1	ComandoSearchGames \lor ComandoMossa
\also
	Comando \defs Ricevi \pipe (ConsumaComando \lor NessunMessaggio)
\end{zed}
\end{document}




