
% chessMate.tex

\documentstyle[italian,a4wide,fuzz]{article}

\begin{document}

\title{Specifiche Z di ChessMate}
\author{Gianluca Busi
\and Stefano Liboni
\and Matteo Martinelli
\and Claudio Zani}

\date{Dicembre 1993}

\maketitle

\tableofcontents

\section{Introduzione}

Questo documento viene reso pubblico in modo che gli studenti del
corso di TPA 1994 abbiano un esempio di specifica Z in formato \LaTeX
tratto dai progetti dello scorso anno.

La presente specifica si riferisce ad un progetto di un editor grafico di 
partite di scacchi. L'editor si integrava con un modulo
giocatore (player), un modulo database di partite,
un modulo database di posizioni, un modulo di interfaccia modem.

La struttura del documento \`e stata giudicata ragionevole,
ma non necessariamente la migliore.
Siete liberi di cercare una struttura migliore.
In particolare, questo documento e' particolarmente
carente dal punto di vista dello sviluppo di 
propriet\`a formali della specifica (teoremi).

{\bf Note di scrittura:}
Si raccomanda di imparare a scrivere correttamente le parole
italiane accentate (in questo documento sono tutte sbagliate!).

\`a \`i \`o  \`u  hanno sempre tale accento 

\`e si usa per e aperta (cio\`e)
\'e si usa per e chiusa (perch\'e).

Si ricorda che i documenti in italiano andrebbero compilati
col comando {\tt ilatex}, che conosce la sillabazione italiana.


Le figure vengono fatte di solito con il programma xfig,
che \`e capace di salvare in formato \LaTeX.


\section{Tipi, variabili globali,funzioni e stati del sistema}
%*****************************************************
\subsection{Rappresentazione generale di una partita}

\begin{zed}
	[NOMIFILE, FILEASCII,SCACCHIERA, SEMIMOSSA, GIOCATORE, DATA, LUOGO,\\
\t1	SIMBOLISTAMPABILI, SIMBOLILATEX]
\end{zed}

\begin{itemize}
\item $NOMIFILE$ : insieme di tutti i possibili nomi di file 
\item $FILEASCII$ : insieme di tutti i possibili file ascii
\item $SCACCHIERA$: Insieme di tutte le possibili configurazioni di scacchiera.
\item $SEMIMOSSA$ : insieme di tutte le possibili mosse valide \\
\t2		Si possono pensare in notazione algebrica standard. 
\item $GIOCATORE$ : insieme di tutti i possibili giocatori 
\item $DATA$ : insieme di tutte le possibili date 
\item $LUOGO$ : insieme di tutti i possibili luoghi
\item $SIMBOLISTAMPABILI$ : insieme di tutti i caratteri della stampante 
\item $SIMBOLILATEX$ : insieme di tutti i simboli e caratteri latex

\end{itemize}


\begin{zed}
	COLORE ::= bianco | nero | indColore
\also
	BOOL ::= vero | falso 
\also
	RISULTATO ::= vinta | persa | pari | indRisultato
\end{zed}

\begin{itemize}
\item $indColore$ : e' il colore indeterminato
\item $indRisultato$ : e' il risultato indeterminato
\end{itemize}


Lo stato di una scacchiera e' rappresentato da una disposizione dei
pezzi e da chi deve muovere

\begin{schema}{STATOSCACCHIERA}
	scacchiera:SCACCHIERA \\
	deveMuovere:COLORE \\
\end{schema}


\begin{itemize}
\item $statoLegale$ determina se uno stato di scacchiera e' legale
\item $mossaLegale$ determina se una sequenza di semimosse puo' essere fatta \\ 
\t2	con una determinata cofigurazione della scacchiera.
\item $nuovoStato$ determina la configurazione che la scacchiera assumera' in
\t2	seguito ad una sequenza di semimosse.
\item $vecchioStato$ determina la configurazione che aveva la scacchiera prima  
\t2	di una sequenza di semimosse.
\end{itemize}

\begin{axdef}
	statoLegale:STATOSCACCHIERA \fun BOOL \\
	mossaLegale:STATOSCACCHIERA \cross \seq SEMIMOSSA \fun BOOL \\
	nuovoStato:STATOSCACCHIERA \cross \seq SEMIMOSSA \pfun STATOSCACCHIERA \\
	vecchioStato:STATOSCACCHIERA \cross \seq SEMIMOSSA \pfun STATOSCACCHIERA \\
\end{axdef}


Si definisce il tipo partita

\begin{schema}{PARTITA}
        mosseGiocate:\seq SEMIMOSSA \\
	posIniziale:STATOSCACCHIERA \\
        giocatoreB:GIOCATORE \\
        giocatoreN:GIOCATORE \\
        data:DATA \\
        luogo:LUOGO \\
\where
	\forall l,r : \seq SEMIMOSSA \mid l \cat r =mosseGiocate \spot \\
	mossaLegale(posIniziale,l) = vero
\end{schema}


Una partita in formato codificato contiene le stesse informazioni di una
partita in formato normale. Cambia solo il formato fisico di memorizzazione.
Un archivio di partite e' un insieme finito di partite in formato codificato.

\begin{zed}
	PARTITACOD == PARTITA 
\also
	ARCHPARTITE == \finset PARTITACOD 
\end{zed}


Disposizione dei pezzi iniziale. I pezzi sono disposti secondo la posizione iniziale standard.

\begin{axdef}
	scacchieraIniz : SCACCHIERA \\
\end{axdef}

Scacchiera iniziale. I pezzi sono disposti secondo la posizione iniziale standard e il
giocatore con diritto di mossa e' il bianco.

\begin{axdef}
	nuovaScacchiera:STATOSCACCHIERA\\
\where
	nuovaScacchiera.scacchiera = scacchieraIniz \\
	nuovaScacchiera.deveMuovere = bianco
\end{axdef}



Costanti per Giocatore, Data, Luogo, Nome, Scacchiera, StatoScacchiera e Partita indeterminati.

\begin{axdef}
	indGiocatore : GIOCATORE \\
	indData : DATA \\
	indLuogo : LUOGO \\
	indNome : NOMIFILE \\
	indScacchiera : SCACCHIERA \\
\end{axdef}

\begin{axdef}
	indStatoScacchiera : STATOSCACCHIERA
\where
	indStatoScacchiera.scacchiera = indScacchiera \\
	indStatoScacchiera.deveMuovere = indColore
\end{axdef}

\begin{axdef}
	indPartita : PARTITA \\
\where
	indPartita.mosseGiocate = \langle \rangle \\
	indPartita.posIniziale = indStatoScacchiera \\
	indPartita.giocatoreB = indGiocatore \\
	indPartita.giocatoreN = indGiocatore \\
	indPartita.data = indData \\
	indPartita.luogo = indLuogo \\
\end{axdef}

Showboard e' definita come una particolare semimossa.

\begin{axdef}
	showboard : SEMIMOSSA \\
\end{axdef}


\begin{itemize}
\item $compatta$ trasforma una partita in formato codificato
\item $scompatta$ trasforma una partita codificata in un formato normale
\item $partitaAscii$ trasforma un partita in formato ascii
\end{itemize}

\begin{axdef}	
	compatta :PARTITA \bij PARTITACOD \\
	scompatta :PARTITACOD \bij PARTITA \\
	partitaAscii : PARTITA \pfun FILEASCII

\end{axdef}

%*****************************************************
\subsection{File System}

Lo schema FileSystem viene utilizzato per associare oggetti ad un nome.\\
Rappresenta i supporti di memorizzazione permanenti.

\begin{schema}{FileSystem}
	fileArchivi : NOMIFILE \pfun ARCHPARTITE \\
	fileAscii :NOMIFILE \pfun FILEASCII \\
	fileLatex :NOMIFILE \pfun \seq SIMBOLILATEX \\
	fileStato :NOMIFILE \pfun STATOSCACCHIERA 
\where
	\dom fileArchivi \cap \dom fileAscii = \empty \\
	\dom fileArchivi \cap \dom fileLatex = \empty \\
	\dom fileArchivi \cap \dom fileStato = \empty \\
	\dom fileAscii \cap \dom fileLatex = \empty \\
	\dom fileAscii \cap \dom fileStato = \empty \\
	\dom fileLatex \cap \dom fileStato = \empty \\
\end{schema}
 
%*****************************************************
\subsection{Editor Testuale-Grafico}

$partita$ e' la partita da editare.\\
$posAttuale$ rappresenta la disposizione ultima della scacchiera.\\
$prima$ e $dopo$ servono per determinare la posizione del "cursore" nella lista delle
semimosse. Il cursore si trova sull'ultima semimossa di prima.\\
$clipboard$ e' la memoria di supporto utilizzata per le operazioni di editing.
 
\begin{schema}{StatoEditor}
    partita: PARTITA \\
    posAttuale: STATOSCACCHIERA \\
    prima: \seq SEMIMOSSA \\
    dopo: \seq SEMIMOSSA \\
    clipboard: \seq SEMIMOSSA
\where
    partita.mosseGiocate = prima \cat dopo \\
    posAttuale = nuovoStato(partita.posIniziale,partita.mosseGiocate) 
\end{schema}
 %***************************************************** 
\subsection{Stampa}
\begin{itemize}
\item $convertiInStampabili$  converte un sequenza di semimosse in simboli stampabili
\item $convertiInLatex$ converte un sequenza di semimosse in simboli latex
\end{itemize}

In entrambe le funzioni l'"incontro" della semimossa $showboard$ provoca la stampa della scacchiera in cui i simboli dei pezzi non sono caratteri ASCII ma figurine rappresentanti i pezzi stessi. Lo stato della scacchiera stampata e' determinato dalle mosse giocate fino a quel punto.
 
\begin{axdef}
        convertiInStampabili : \seq SEMIMOSSA \fun \seq SIMBOLISTAMPABILI \\
        convertiInLatex : \seq SEMIMOSSA \fun \seq SIMBOLILATEX
\end{axdef}
%*****************************************************
\subsection{Data Base di Partite}
Alcune funzioni di supporto vengono utilizzate dal modulo:

\begin{itemize}
\item $risultato$ determina se una partita e' stata vinta ,persa, o pareggiata da un certo giocatore 
\item $ordinaIntestazioni$ ordina le partite di un archivio partite in base all'intestazione
\item $ordinaMosse$ ordina le partite di un archivio partite in base alle mosse iniziali
\end{itemize}

\begin{axdef}
	risultato:(GIOCATORE \cross PARTITACOD) \fun RISULTATO \\
	ordinaIntestazioni : \power PARTITACOD \bij \\
	\power (GIOCATORE \cross GIOCATORE \cross DATA \cross LUOGO) \\
	ordinaMosse : \power (\seq SEMIMOSSA) \bij \power (\seq SEMIMOSSA) \\
\end{axdef}

Il database di partite comprende archivi su disco contenente partite in formato codificato e offre la possibilita' di caricare in memoria una partita e scorrerla.

Si definisce lo stato della memoria.\\
$partitaScelta$ e' la partita in memoria.\\
$prima$ e $dopo$ servono per determinare la posizione del "cursore" nella lista delle semimosse. Il cursore si trova sull'ultima semimossa di $prima$.\\
$nomeScelto$ e' l'archivio di partite a cui appartiene $partitaScelta$.\\

\begin{schema}{dbPartite}
	partitaScelta:PARTITA \\
	prima:\seq SEMIMOSSA \\
	dopo:\seq SEMIMOSSA \\
\where
	 risultato(partitaScelta.giocatoreB,partitaScelta) \neq indRisultato \\	
	 prima \cat dopo = partitaScelta.mosseGiocate \\
	
\end{schema}

%*****************************************************
\subsection{Analisi di una partita}

Data una partita memorizzata in un archivio in formato ASCII e' fornita la possibilita'
di richiedere una analisi della partita. \\
L'analisi indica per ogni mossa una valutazione e per ogni stato della scacchiera (ricavato dalla sequenza di mosse fino ad ora analizzate) la migliore variante di gioco.\\
In $MOSSAANALIZZATA$ $SEMIMOSSA$ e' la semimossa analizzata, $\nat$ e' la valutazione, $\seq SEMIMOSSA$ e' la variante.

\begin{zed}
        MOSSAANALIZZATA == SEMIMOSSA \cross \nat \cross \seq SEMIMOSSA
\end{zed}

\begin{axdef}
        analizzaPartita : FILEASCII \pfun \seq MOSSAANALIZZATA
\end{axdef}

%*****************************************************
\subsection{Data Base di Posizioni}


Alcune funzioni di supporto sono necessarie al modulo, esse sono:
\begin{itemize}
\item $mossePossibili$ fornisce le mosse che nel grafo seguono la posizione
corrente.
\item $calcolaNodi$ converte un archivio partite in un insieme di posizioni.
\item $calcolaArchi$ converte le mosse presenti in un archivio di partite in un
insieme di archi.  Qesta funzione e la precedente convertono solo le mosse che
mantengono la connessione del grafo.
\end{itemize}

\begin{axdef}
	ArcoLegale : STATOSCACCHIERA \cross STATOSCACCHIERA \surj BOOL \\
	mossePossibili : ((STATOSCACCHIERA \rel STATOSCACCHIERA) \\
\t1 \cross STATOSCACCHIERA) \pfun \power SEMIMOSSA \\
	calcolaNodi : (\power STATOSCACCHIERA \cross ARCHPARTITE) \\
\t1		\fun \power STATOSCACCHIERA \\
	calcolaArchi : (\power STATOSCACCHIERA \cross ARCHPARTITE) \\
\t1		\fun STATOSCACCHIERA \rel STATOSCACCHIERA \\ 
	convertiAscii : \seq STATOSCACCHIERA \pfun FILEASCII \\ 
\end{axdef}


Lo stato del data base di posizioni e' definito da:
\begin{itemize}
\item $nodi$ i nodi del grafo.
\item $archi$ gli archi del grafo.
\item $iniziale$ la configurazione iniziale della scacchiera. Rappresenta la
"partenza" della navigazione.
\item $corrente$ il nodo sul quale si e' attualmente posizionati.  Rappresenta
il punto che si e' raggiunto nella navigazione.
\item $storia$ e' la sequenza di nodi percorsi nella navigazione.
\end{itemize}
L'invariante definisce l'integrita' della storia, delle posizioni
iniziale e corrente e la raggiungibilita' di ogni nodo dalla posizione iniziale
(che implica anche la connessione del grafo).

\begin{schema}{DBposizioni}
	nodi : \power STATOSCACCHIERA \\
	archi : STATOSCACCHIERA \rel STATOSCACCHIERA \\
	iniziale : STATOSCACCHIERA \\
	corrente : STATOSCACCHIERA \\
	storia : \seq STATOSCACCHIERA 
\where
	iniziale \in nodi \land \\
	corrente \in nodi \land \\
	head(storia) = iniziale \land \\
	last(storia) = corrente \land \\
	(\forall a : STATOSCACCHIERA \cross STATOSCACCHIERA | a \in archi \spot ArcoLegale(a) = vero) \land \\
	(\forall n : STATOSCACCHIERA | \\
\t1		n \in nodi \spot \exists s : \seq STATOSCACCHIERA \spot \\
\t1		(head(s) = iniziale \land last(s) = n \land \\
\t1		(\forall i : 1 \upto \#s-1 \spot s(i) \mapsto s(i+1) \in archi))) \land \\
	(\forall i : 1 \upto \#storia-1 \spot \\
\t1		storia(i) \mapsto storia(i+1) \in archi)
\end{schema}
%*****************************************************
\subsection{Comunicazioni via Modem}

\begin{zed}
	STATOCOLLEGAMENTO ::= Inattivo | AttendiAperturaremoto | Muovi | \\
		AttendiMossa| RicevutaRichiestaApertura
\also
	[CHAR, IDENTIFICAZIONE]
\also
	STRINGA == \seq CHAR 
\end{zed} 

Ad ogni postazione di gioco e' associata una identificazione (per
esempio il numero di telefono).  Gli identificatori messaggio, posizione
e idRemoto rappresentano rispettivamente il messaggio correntemente
visualizzato, la configurazione corrente della scacchiera e
l'identificazione dell'avversario.

\begin{schema}{NODODIGIOCO}
	id : IDENTIFICAZIONE \\
	messaggio : STRINGA \\
	posizione : STATOSCACCHIERA \\
	statoCollegamento : STATOCOLLEGAMENTO \\
	idRemoto : IDENTIFICAZIONE
\end{schema}

La comunicazione avviene sempre tra due postazioni di gioco.

\begin{schema}{Comunicazione}
	locale : NODODIGIOCO \\
	remoto : NODODIGIOCO \\
\end{schema}




%*****************************************************
\subsection{Player}

\begin{itemize}
\item $TIPOPARTITA$ : rappresenta i possibili tipi di partita giocabili
\item $TIPOGIOCATORE$ : sono i possibili tipi di giocatore
\end{itemize}

\begin{zed}
	
	SCELTA::=si|no \\
\also
	TIPOPARTITA::=umanoUmano|umanoProgramma|programmaProgramma| \\
\t2		parIndef \\
\also
	TIPOGIOCATORE::=umano|programma|gioIndef \\
\also
	POSIZIONESCACCHIERA::=biancoInAlto|biancoInBasso|posIndef \\
\end{zed}


\begin{itemize}
\item $calcolaTipoGiocatore$ : determina il tipo del giocatore che deve muovere \\ \				 (umano o programma)
\item $calcolaVariante$ : trova la variante migliore da giocare nella situazione attuale.
\item $calcolaValoreVariante$ : da una valutazione alla variante proposta in base alla situazione attuale.
\item $scegliMossa$ : e' la funzione che sceglie quale mossa giocare nella situazione attuale.
\item $scegliMossaDaDb$ : scegli la mossa da giocare in base ad un database di posizioni.
\item $esisteMossaNelDb$ : controlla che nel database di posizioni selezionato vi sia una mossa per lo stato scacchiera attuale.
\end{itemize}

\begin{axdef}

	calcolaTipoGiocatore:(TIPOPARTITA \cross COLORE \cross COLORE) \\
		\t1 \fun TIPOGIOCATORE \\
	calcolaVariante:STATOSCACCHIERA \fun \seq SEMIMOSSA \\
	calcolaValoreVariante:(STATOSCACCHIERA \cross \seq SEMIMOSSA) \fun \nat \\ 
	scegliMossa:STATOSCACCHIERA \pfun SEMIMOSSA \\
	scegliMossaDaDb:(\power STATOSCACCHIERA \\
		\t1 \cross \power (STATOSCACCHIERA \cross STATOSCACCHIERA) \\
		\t1 \cross STATOSCACCHIERA \cross STATOSCACCHIERA) \pfun SEMIMOSSA \\ 
	esisteMossaNelDb:(\power STATOSCACCHIERA \\
		\t1 \cross \power (STATOSCACCHIERA \cross STATOSCACCHIERA) \\
		\t1 \cross STATOSCACCHIERA \cross STATOSCACCHIERA) \fun BOOL \\
\end{axdef}

$colore1$ indica il colore del primo giocatore in tipo Partita. 
Ad esempio se tipoPartita=umanoProgramma allora colore1 indica il colore del giocatore umano.\\
$livello$ e' il livello di difficolta' di gioco. \\
$tipoGiocatore$ e' il tipo del giocatore che deve muovere (umano o programma)
 
\begin{schema}{StatoPartita}
	tipoPartita:TIPOPARTITA \\
	livello:\nat \\
	colore1:COLORE \\
	posScac:POSIZIONESCACCHIERA \\
	tempoB:\nat \\
	tempoN:\nat \\
	statoScacchieraCorrente:STATOSCACCHIERA \\ 
	partita:PARTITA \\
	tipoGiocatore:TIPOGIOCATORE 
\where
	tempoB \geq 0 \\
	tempoN \geq 0 \\
	statoScacchieraCorrente = nuovoStato(partita.posIniziale,partita.mosseGiocate)
\end{schema}

%************************************************************
\newpage
\section{File system}


\subsection{Inizializzazione}

\begin{schema}{InitFileSystem}
	FileSystem
\where
	fileArchivi = \empty \\
	fileAscii = \empty \\
	fileLatex = \empty \\
	fileStato = \empty
\end{schema}


%***********************************************************

\newpage
\section{Editor Testuale}


\subsection{Inizializzazione}

\begin{schema}{InitStatoEditor}
	StatoEditor
\where
	partita = indPartita \\
	posAttuale = nuovaScacchiera\\
	prima = \langle \rangle \\
	dopo = \langle \rangle \\
	clipboard = \langle \rangle \\
\end{schema}

\subsection{Operazioni sul sistema}

Una mossa puo' essere aggiunta solo alla fine e solo se legale.

\begin{schema}{AggiungiMossa}
    \Delta StatoEditor \\
	mossa?:SEMIMOSSA 
\where
    dopo = \langle \rangle \\
	(mossaLegale(posAttuale,\langle mossa? \rangle) = vero \lor \\
\t1	mossa?=showboard) \\
	posAttuale' = nuovoStato(posAttuale, \langle mossa? \rangle) \\
	partita'.mosseGiocate = partita.mosseGiocate \cat \langle mossa?	\rangle \\
	 prima'=prima \cat \langle mossa? \rangle
\end{schema}


E' possibile rimuovere l'ultima mossa. Corrisponde all'undo.

\begin{schema}{RimuoviMossa}
    \Delta StatoEditor \\
\where
	dopo = \langle \rangle  \\
	prima'=front(prima) \\
	partita'.mosseGiocate = front(partita.mosseGiocate) \\
	posAttuale' = vecchioStato(posAttuale, \langle last(prima) \rangle) \\
	prima'=front(prima) 
\end{schema}

Avanza la posizione del cursore di una semimossa.

\begin{schema}{AvantiMossa}
    \Delta StatoEditor 
\where
    dopo \neq \langle \rangle  \\
    prima' = prima \cat \langle head(dopo) \rangle \\
    dopo' = tail(dopo)
\end{schema}

Arretra la posizione del cursore di una semimossa.

\begin{schema}{IndietroMossa}
    \Delta StatoEditor
\where
    prima \neq \langle \rangle  \\
    prima' = front(prima)  \\
    dopo' = \langle last(prima) \rangle \cat dopo
\end{schema}

Permette di inserire l'intestazione di una partita.

\begin{schema}{InserisciIntestazione}
    \Delta StatoEditor \\
    giocatoreB? : GIOCATORE  \\
    giocatoreN? : GIOCATORE  \\
    data? : DATA \\
    luogo? : LUOGO
\where
    partita'.giocatoreB = giocatoreB? \\
    partita'.giocatoreN = giocatoreN? \\
    partita'.data = data?  \\
    partita'.luogo = luogo? \\
\end{schema}

Permette di iniziare una nuova partita.\\
I pezzi sono disposti nella posizione iniziale standard e il bianco ha diritto di mossa.

\begin{schema}{NuovaPartita}
    \Delta StatoEditor \\
\where
    partita'.posIniziale = nuovaScacchiera \\
	partita'.mosseGiocate = \langle \rangle \\
	partita'.giocatoreB = indGiocatore \\
	partita'.giocatoreN = indGiocatore \\
	partita'.data = indData \\
	partita'.luogo = indLuogo \\
    posAttuale' = nuovaScacchiera \\
    prima' = \langle \rangle \\
    dopo' = \langle \rangle \\
\end{schema}


Le mosse da copiare sono numeroMosse a partire dalla posizione dopo il cursore.

\begin{schema}{CopiaMosse}
    \Delta StatoEditor \\
	numeroMosse?:\nat_1
\where
    dopo \neq \langle \rangle  \\
	numeroMosse? \leq \# dopo \\
    clipboard' = \{x : \nat_1 \mid x \in 1 \upto numeroMosse? \} \extract dopo 
\end{schema}


Le mosse che si possono eliminare  solo le ultime (a partire dalla posizione dopo il cursore).

\begin{schema}{RitagliaMosse}
    \Delta StatoEditor
\where
    dopo \neq \langle \rangle  \\
    clipboard' = dopo  \\
	posAttuale' = vecchioStato(posAttuale,dopo) \\
    	dopo' = \langle \rangle \\
	partita'.mosseGiocate =\{x : \nat_1 \mid x \in 1 \upto \#prima \} \extract partita.mosseGiocate 
\end{schema}


Le mosse possono essere incollate solo alla fine e solo se legali.

\begin{schema}{IncollaMosse}
    \Delta StatoEditor
\where
    dopo = \langle \rangle  \\
	mossaLegale(posAttuale,clipboard) = vero  \\
	posAttuale' = nuovoStato(posAttuale,clipboard) \\
    	dopo' = clipboard \\
	partita'.mosseGiocate = partita.mosseGiocate \cat clipboard  
\end{schema}


Salvataggio in un archivio di partite della partita corrente. \\
Una partita puo' essere salvata in un archivio partite solo se ha l'intestazione e il  risultato.
\begin{schema}{SalvaPartita}
	\Xi StatoEditor \\
	\Delta FileSystem \\
	nome?:NOMIFILE  
\where 
	partita.giocatoreB \neq indGiocatore \\
	partita.giocatoreN \neq indGiocatore \\
	partita.data \neq indData \\
	partita.luogo \neq indLuogo \\
	risultato(partita.giocatoreB, compatta(partita)) \neq indRisultato \\
	nome? \in \dom fileArchivi \\
	\forall x:PARTITACOD \mid x \in fileArchivi(nome?) \spot \\
\t1	x \neq partita \\

	fileArchivi' = fileArchivi \oplus \{ nome? \mapsto \\
\t1		fileArchivi(nome?) \cup \{ compatta(partita)\} \}
\end{schema}


Salvataggio in un archivio ASCII della partita corrente.
\begin{schema}{SalvaAscii}
	\Xi StatoEditor \\
	\Delta FileSystem \\
	nome?:NOMIFILE 
\where 
	nome? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \\
	fileAscii'= fileAscii \oplus \{nome? \mapsto partitaAscii(partita)\}
\end{schema}


Carica una partita da un archivio partite. 
\begin{schema}{CaricaPartita}
	\Delta StatoEditor \\
	\Xi FileSystem \\
	nome?:NOMIFILE  \\
	partitaInput?:PARTITACOD \\
\where
	nome? \in \dom fileArchivi \\
	partitaInput? \in fileArchivi(nome?) \\

	partita = scompatta(partitaInput?) \\
	posAttuale = nuovoStato(nuovaScacchiera,partitaInput?.mosseGiocate)\\
	prima'= partitaInput?.mosseGiocate \\
	dopo' =\langle \rangle \\
	clipboard = \langle \rangle
\end{schema}
%*********************************************

\newpage
\section{Editor Grafico}
Lo stato dell'editor grafico e' lo stesso di quello dell'editor testuale. \\
Cambia solo la modalita' di immissione.\\


\subsection{Operazioni sul sistema}

Immissione di una mossa grafica

\begin{schema}{AggiungiMossaGrafica}
    \Delta StatoEditor \\
	mossa?:SEMIMOSSA 
\where
	mossaLegale(posAttuale,\langle mossa? \rangle) = vero \\
	posAttuale' = nuovoStato(posAttuale, \langle mossa? \rangle) \\
	partita'.mosseGiocate = partita.mosseGiocate \cat \langle mossa?\rangle \\
	 prima'=partita'.mosseGiocate\\
	dopo' = \langle \rangle
\end{schema}


E' possibile rimuovere l'ultima mossa. 

\begin{schema}{RimuoviMossaGrafica}
    \Delta StatoEditor \\
\where
	partita'.mosseGiocate = front(partita.mosseGiocate) \\
	posAttuale' = vecchioStato(posAttuale, \langle last(partita.mosseGiocate) \rangle) \\
	prima'=partita'.mosseGiocate\\
	dopo' = \langle \rangle  \\
	 
\end{schema}


%*********************************************

\newpage
\section{Stampa}


Lo schema StampaAscii stampa una sequenza di mosse su una stampante 
convenzionale (a caratteri).
 
\begin{schema}{StampaAscii}
        \Xi StatoEditor \\
        stampa! : \seq SIMBOLISTAMPABILI
\where
        stampa! = convertiInStampabili(partita.mosseGiocate)
\end{schema}


StampaLatex esegue il salvataggio della sequenza di mosse  
dell' editor in un file LaTeX.

\begin{schema}{StampaLatex}
        \Xi StatoEditor \\
        \Delta FileSystem \\
        nome? : NOMIFILE
\where
        nome? \notin \dom fileArchivi \cup \dom fileAscii \cup \dom fileStato \\
\also
        fileLatex' = fileLatex \oplus \\
\t1             \{nome? \mapsto convertiInLatex(partita.mosseGiocate)\}
\end{schema}

%***********************************************
\newpage
\section{DataBase di Partite}


\subsection{Inizializzazione}
\begin{schema}{InitdbPartite}
	dbPartite \\
\where
	prima = \langle \rangle \\
	dopo = \langle \rangle \\
	partitaScelta = indPartita
\end{schema}

\subsection{Operazioni sul sistema}

Le operazioni di ricerca operano sull'archivio partite di nome $nomeS$. \\
Una interrogazione provoca la creazione di un nuovo archivio partite di nome $nomeD$ contenente le partite che soddisfano la condizione di ricerca. \\
E' richiesta la possibilita' di combinare logicamente le ricerche. Tale requisito e' soddisfatto combinando operazioni di ricerca e di merge.
\\
\\
\\
Ricerca le partite giocate da un certo giocatore. 

\begin{schema}{RicercaGiocatore} 
	\Xi dbPartite \\
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	giocatore?:GIOCATORE \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\
	nuovoArchivio = \{x:PARTITACOD \mid \\
\t1	(x.giocatoreB = giocatore? \lor x.giocatoreN=giocatore?) \\
\t1	\land x \in fileArchivi(nomeS?) \} \\

	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto nuovoArchivio\} \\

\end{schema}
\newpage
Ricerca le partite giocate in un certo anno.
\begin{schema}{RicercaAnno} 
	\Xi dbPartite \\
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	anno?:DATA \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\

	nuovoArchivio = \{x:PARTITACOD \mid \\
\t1	(x.data = anno?) \land x \in fileArchivi(nomeS?) \} \\
	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto nuovoArchivio\} \\

\end{schema}

Ricerca le partite giocate in un certo torneo.
\begin{schema}{RicercaTorneo} 
	\Xi dbPartite \\
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	luogo?:LUOGO \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\
	nuovoArchivio = \{x:PARTITACOD \mid \\
\t1	(x.luogo = luogo?) \land x \in fileArchivi(nomeS?) \} \\
	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto nuovoArchivio\} \\

\end{schema}
\newpage
Ricerca le partite vinte da un certo giocatore.
\begin{schema}{RicercaVinte} 
        \Xi dbPartite \\
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	giocatore?:GIOCATORE \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\
	nuovoArchivio = \{x:PARTITACOD \mid \\
\t1	(x.giocatoreB = giocatore? \lor x.giocatoreN=giocatore?) \\
\t1	\land risultato(giocatore?,x)= "vinta" \\
\t1	\land x \in fileArchivi(nomeS?) \} \\

	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto nuovoArchivio\} \\

\end{schema}

Ricerca le partite perse da un certo giocatore.
\begin{schema}{RicercaPerse} 
	\Xi dbPartite \\
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	giocatore?:GIOCATORE \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\
	nuovoArchivio = \{x:PARTITACOD \mid \\
\t1	(x.giocatoreB = giocatore? \lor x.giocatoreN=giocatore?) \\
\t1	\land risultato(giocatore?,x)= "persa" \\
\t1	\land x \in fileArchivi(nomeS?) \} \\

	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto nuovoArchivio\} \\

\end{schema}
\newpage
Ricerca le partite pareggiate da un certo giocatore.
\begin{schema}{RicercaPari} 
	\Xi dbPartite \\
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	giocatore?:GIOCATORE \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\
	nuovoArchivio = \{x:PARTITACOD \mid \\
\t1	(x.giocatoreB = giocatore? \lor x.giocatoreN=giocatore?) \\
\t1	\land risultato(giocatore?,x)= "pari" \\
\t1	\land x \in fileArchivi(nomeS?) \} \\

	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto nuovoArchivio\} \\

\end{schema}

Ricerca le partite che iniziano con una certa sequenza di mosse.
\begin{schema}{RicercaMossa} 
	\Xi dbPartite \\
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	mosse?:\seq SEMIMOSSA \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\
	nuovoArchivio = \{x:PARTITACOD \mid \\
\t1	(\forall n:1\upto \#mosse? \spot mosse?(n) = (x.mosseGiocate(n))) \\
\t1	\land x \in fileArchivi(nomeS?) \} \\

	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto nuovoArchivio\} \\

\end{schema}
\newpage
L'operazione di merge unisce i due archivi partite di nome $nomeS1$ $nomeS2$ in un unico archivio di nome $nomeD$.

\begin{schema}{Merge} 
	\Xi dbPartite \\
	\Delta FileSystem \\
	nomeS1?:NOMIFILE \\
	nomeS2?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	nuovoArchivio:ARCHPARTITE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS1? \in \dom fileArchivi \\
	nomeS2? \in \dom fileArchivi \\

	fileArchivi'=fileArchivi \oplus \{nomeD? \mapsto\\
\t1	 (fileArchivi(nomeS1?) \cup fileArchivi(nomeS2?))\} \\
\end{schema}



Visualizzazione delle intestazioni contenute nell'archivio partite $nomeS$.

\begin{schema}{VisuaIntestazione}
	\Xi dbPartite \\
	\Xi FileSystem \\
	nomeS?:NOMIFILE \\
	out!:\power(GIOCATORE \cross GIOCATORE \cross DATA \cross LUOGO) \\
\where
	nomeS? \in \dom fileArchivi \\
	
       out! =ordinaIntestazioni(\{x : PARTITACOD \mid \\
\t1     x \in fileArchivi(nomeS?) \}) \\
%(x.giocatoreB,x.giocatoreN,x.data,x.luogo) \}) \\
\end{schema}

Visualizzazione delle prime sette mosse delle partite contenute nell'archivio partite $nomeS$.

\begin{schema}{VisuaMosse}
	\Xi dbPartite \\
	\Xi FileSystem \\
	nomeS?:NOMIFILE \\
	out!:\power(\seq SEMIMOSSA) \\
\where
	nomeS? \in \dom fileArchivi \\
	
	out! =ordinaMosse(\{x:PARTITACOD \mid x \in fileArchivi(nomeS?)\\
\t1	\spot \{y : \nat_1 \mid y \in 1 \upto 7\} \extract x.mosseGiocate\}) \\
\end{schema}

Caricamento nella memoria del DbPartite di una partita dell'archivio $nomeS$.

\begin{schema}{SelezionaPartita}
	\Delta dbPartite \\
	\Xi FileSystem \\
	nomeS?:NOMIFILE \\
	partita?:PARTITACOD \\
\where
	nomeS? \in \dom fileArchivi \\
	partita? \in fileArchivi(nomeS?) \\ 
	\\
	partitaScelta' = partita? \\
	prima = partita?.mosseGiocate \\
	dopo = \langle \rangle \\
\end{schema}

Avanzamento del cursore di una semimossa (nella partita in memoria).

\begin{schema}{Avanti}
	\Delta dbPartite \\
\where
	dopo \neq \langle \rangle \\
	prima' = prima \cat \langle head(dopo) \rangle \\
	dopo' = tail(dopo) \\
\end{schema}

Arretramento del cursore di una semimossa (nella partita in memoria).

\begin{schema}{Indietro}
	\Delta dbPartite \\
\where
	prima \neq \langle \rangle \\
	prima' = front(prima) \\
	dopo' = \langle last(prima) \rangle \cat dopo \\
\end{schema}

Conversione di un archivio partite di nome $nomeS$ in un archivio equivalente in formato ASCII di nome $nomeD$.

\begin{schema}{ConvertiAscii} 
	\Delta FileSystem \\
	nomeS?:NOMIFILE \\
	nomeD?:NOMIFILE \\
	converti:ARCHPARTITE \fun FILEASCII \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \cup \dom fileAscii \\
	nomeS? \in \dom fileArchivi \\

	fileAscii'=fileAscii \cup \{nomeD? \mapsto (converti(fileArchivi(nomeS?)))\}
\end{schema}

Aggiunta di un archivio partite di nome $nomeD$ nel fileSystem.

\begin{schema}{CaricaArchivio}
	\Delta FileSystem \\
	archivio?:ARCHPARTITE \\
	nomeD?:NOMIFILE \\
\where
	nomeD? \notin \dom fileArchivi \cup \dom fileLatex \cup \dom fileStato \\

	fileArchivi' = fileArchivi \cup \{nomeD? \mapsto archivio? \}
\end{schema}


Utilizza lo stato del player.
Permette di iniziare a giocare una partita dalla posizione corrente.	
\begin{schema}{PassaAlPlayer}
	\Xi dbPartite \\
	\Delta StatoPartita \\
	tipoPartita?:TIPOPARTITA \\
	livello?:\nat \\
	posScac?:POSIZIONESCACCHIERA \\
	colore1?:COLORE
\where
	statoScacchieraCorrente' = \\
\t2 		nuovoStato(partitaScelta.posIniziale,partitaScelta.mosseGiocate) \\
	tempoB'=0 \\
	tempoN'=0 \\
	livello'=livello? \\
	posScac'=posScac? \\
	colore1'=colore1? \\
	partita'.posIniziale= \\
\t2 		nuovoStato(partitaScelta.posIniziale,partitaScelta.mosseGiocate) \\
	partita'.mosseGiocate= \langle \rangle \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita', \\
		\t1 colore1',partita.posIniziale.deveMuovere)
\end{schema}

%***************************************************************

\newpage
\section{Analisi di una partita}

Data una partita memorizzata in un archivio in formato ASCII e' fornita la possibilita'
di richiedere una analisi della partita. \\
L'analisi indica per ogni mossa una valutazione e per ogni stato della scacchiera (ricavato dalla sequenza di mosse fino ad ora analizzate) la migliore variante di gioco.

\begin{schema}{AnalisiPartita}
        \Xi FileSystem \\
        nome? : NOMIFILE \\
        analisi! : \seq MOSSAANALIZZATA
\where
        nome? \in \dom fileAscii
\also
        analisi! = analizzaPartita(fileAscii(nome?))
\end{schema}

%**********************************************************
\newpage
\section{Data base di posizioni}

Il modulo gestore di archivi permette di creare e manipolare archivi di 
posizioni.  Un archivio di posizioni rappresenta una parte di grafo di gioco.  
I nodi del grafo sono le posizioni e gli archi sono le mosse.  E' possibile
navigare sui nodi del grafo.



\subsection{Inizializzazione}

\begin{schema}{InitDBposizioni}
	DBposizioni
\where
	nodi = \{nuovaScacchiera\} \\
	archi = \empty \\
	iniziale = nuovaScacchiera \\
	corrente = nuovaScacchiera \\
	storia = \langle nuovaScacchiera\rangle
\end{schema}
	

\subsection{Operazioni sul sistema}

Sul grafo, a partire dalla posizione corrente, si puo' aggiungere una mossa.
La nuova posizione corrente diventa quella raggiunta in seguito alla mossa.

\begin{schema}{AggiungiPosizione}
	\Delta DBposizioni \\
	m? : SEMIMOSSA
\where
	m? \neq showboard \\
	mossaLegale(corrente, \langle m? \rangle) = vero  \\
	nuovoStato(corrente,\langle m? \rangle) \notin nodi
\also
	nodi' = nodi \cup \{nuovoStato(corrente,\langle m? \rangle)\} \\
	archi' = archi \cup \\
\t1		\{corrente \mapsto nuovoStato(corrente, \langle m? \rangle)\} \\
	iniziale' = iniziale \\
	corrente' = nuovoStato(corrente, \langle m? \rangle) \\
	storia' = storia \cat \langle corrente' \rangle
\end{schema}




La mossa da cancellare va scelta tra quelle che partono dalla configurazione
corrente della scacchiera.  Vengono eliminate anche tutte
le posizioni che non possono piu' essere raggiunte in seguto all'eliminazione 
della mossa.

\begin{schema}{CancellaMossa}
	\Delta DBposizioni \\
	m? : SEMIMOSSA
\where
	m? \in mossePossibili(archi, corrente)
\also
	archi' = archi \setminus \\
\t1		\{ a : STATOSCACCHIERA \cross STATOSCACCHIERA | \\
\t1		(\exists s : \seq STATOSCACCHIERA \spot \\
\t1		(\exists k : 1 \upto \#s-1 \spot \\
\t1		a = s(k) \mapsto s(k+1)) \land \\
\t1		head(s) = corrente \land \\
\t1		head(tail(s)) = nuovoStato(corrente,\langle m? \rangle) \land \\
\t1		(\forall i : 1 \upto \#s-1 \spot s(i) \mapsto s(i+1) \in archi) \land \\
\t1		(\forall j : 2 \upto \#s \spot archi \inv \limg \{s(j)\}\rimg \subseteq \ran(s))) \} \\ 
	nodi' = \ran(archi') \cup \dom(archi') \\
	iniziale' = iniziale \\
	corrente' = corrente \\
	storia' = storia 
\end{schema}




Salva su file la sequenza di mosse che dalla posizione iniziale portano alla
posizione corrente.

\begin{schema}{Salva}
	\Xi DBposizioni \\
	\Delta FileSystem \\
	nome? : NOMIFILE
\where
	nome? \notin \dom fileAscii \cup \dom fileLatex \cup \dom fileStato
\also
	fileAscii' = fileAscii \oplus \{nome? \mapsto convertiAscii(storia)\}
\end{schema}




L'avanzamento di una mossa viene fatto segliendo una delle mosse successive
alla posizione corrente.

\begin{schema}{AvantiPosizione}
	\Delta DBposizioni \\
	m? : SEMIMOSSA
\where
	mossaLegale(corrente,\langle m? \rangle) = vero \land \\
	corrente \mapsto nuovoStato(corrente,\langle m? \rangle) \in archi
\also
	nodi' = nodi \\
	archi' = archi \\
	iniziale' = iniziale \\
	corrente' = nuovoStato(corrente,\langle m? \rangle) \\
	storia' = storia \cat \langle nuovoStato(corrente,\langle m? \rangle) \rangle
\end{schema}

L' indietreggiamento invece avviene solo percorrendo a ritroso la storia di
1, 5, 10 mosse o tornando alla posizione iniziale.

\begin{schema}{Indietro1}
	\Delta DBposizioni \\
\where
	front(storia) \neq \empty 
\also
	nodi' = nodi \\
	archi' = archi \\
	iniziale' = iniziale \\
	corrente' = last(storia) \\
	storia' = front(storia)
\end{schema}

\begin{zed}
	Indietro5 \defs Indietro1 \semi Indietro1 \semi \\
\t1		Indietro1 \semi Indietro1 \semi Indietro1 
\also
	Indietro10 \defs Indietro5 \semi Indietro5
\end{zed}

\begin{schema}{Indietroinizio}
	\Delta DBposizioni \\
\where
	nodi' = nodi \\
	archi' = archi \\
	iniziale' = iniziale \\
	corrente' = iniziale \\
	storia' = \langle head(storia) \rangle
\end{schema}

Abbandona il gestore archivi e attiva il modulo player che prende come 
posizione iniziale quella corrente.

\begin{schema}{AttivaPlayer}
	\Xi DBposizioni \\
	\Delta StatoPartita \\
	tipoPartita?:TIPOPARTITA \\
	livello?:\nat \\
	posScac?:POSIZIONESCACCHIERA \\
	colore1?:COLORE
\where
	statoScacchieraCorrente' = corrente \\
	tempoB'=0 \\
	tempoN'=0 \\
	livello'=livello? \\
	posScac'=posScac? \\
	colore1'=colore1? \\
	partita'.posIniziale=corrente \\
	partita'.mosseGiocate= \langle \rangle \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita', \\
		\t1 colore1',partita.posIniziale.deveMuovere)
\end{schema}



E' possibile leggere un archivio di partite e convertirlo in un archivio di
posizioni. Il grafo viene quindi espanso con l'aggiunta delle mosse contenute
nell'archivio di partite.  La conversione viene specificata dalle funzioni 
$calcolaNodi$ e $calcolaArchi$; queste funzioni convertono solo le mosse che
mantengono la connessione del grafo.

\begin{schema}{CaricaArchivioPartite}
	\Delta DBposizioni \\
	\Xi FileSystem \\
	Nome? : NOMIFILE
\where
	Nome? \in \dom fileArchivi
\also
	nodi' = nodi \cup calcolaNodi(nodi, fileArchivi(Nome?)) \\
	archi' = archi \cup calcolaArchi(nodi, fileArchivi(Nome?)) \\
	iniziale' = iniziale \\
	corrente' = corrente \\
	storia' = storia
\end{schema}


%*******************************************************
\newpage
\section{Comunicazione via modem}
\subsection{Inizializzazione}
\begin{schema}{InitComunicazione}
	Comunicazione
\where
	locale.messaggio = \empty \land \\
	locale.posizione = nuovaScacchiera \land \\
	locale.statoCollegamento = Inattivo \land \\
	remoto.messaggio = \empty \land \\
	remoto.posizione = nuovaScacchiera \land \\
	remoto.statoCollegamento = Inattivo
\end{schema}

\subsection{Operazioni sul sistema}

Le transizioni comprendono i protocolli di apertura e chisura del
collegamento, l'esecuzuione di mosse e l'invio di messaggi
all'avversario.  Per $locale$ si intende sempre l'esecutore
dell'operazione e per $remoto$ il destinatario.\\
\\
Apertura della comunicazione

\begin{schema}{ApriComunicazione}
	\Delta Comunicazione \\
	Destinazione? : IDENTIFICAZIONE
\where
	locale.statoCollegamento = Inattivo \land \\
	remoto.statoCollegamento = Inattivo
\also
	locale'.statoCollegamento = AttendiAperturaremoto \\
	locale'.idRemoto = Destinazione? \\
	remoto'.id = Destinazione? \\
	remoto'.statoCollegamento = RicevutaRichiestaApertura \\
	remoto'.idRemoto = locale.id
\end{schema}

Risposta alla richiesta di apertura di comunicazione

\begin{schema}{RispondiApertura}
	\Delta Comunicazione
\where
	locale.statoCollegamento = RicevutaRichiestaApertura \\
	remoto.statoCollegamento = AttendiAperturaremoto
\also
	locale'.statoCollegamento = AttendiMossa \\
	locale'.idRemoto = remoto.id \\
	remoto'.id = remoto.id \\
	remoto'.posizione = locale'.posizione \\
	remoto'.statoCollegamento = Muovi \\
	remoto'.idRemoto = locale.id
\end{schema}

Chiusura della comunicazione

\begin{schema}{Chiudi}
	\Delta Comunicazione
\where
	locale'.statoCollegamento = Inattivo \\
	locale'.idRemoto = locale.idRemoto \\
	remoto'.statoCollegamento = Inattivo \\
	remoto'.idRemoto =remoto.idRemoto 
\end{schema}

Invio di una semimossa

\begin{schema}{EseguiMossa}
	\Delta Comunicazione \\
	m? : SEMIMOSSA
\where
	locale.statoCollegamento = Muovi \land \\
	remoto.statoCollegamento = AttendiMossa \land \\
	mossaLegale(locale.posizione, \langle m? \rangle) = vero
\also
	locale'.posizione = nuovoStato(locale.posizione,\langle m? \rangle) \\
	locale'.statoCollegamento = AttendiMossa \\
	locale'.idRemoto = locale.idRemoto \\
	remoto'.posizione = locale'.posizione \\
	remoto'.statoCollegamento = Muovi \\
\end{schema}

Invio di un messaggio generico

\begin{schema}{MandaMessaggio}
	\Delta Comunicazione \\
	Testo? : STRINGA
\where
	locale.statoCollegamento \neq Inattivo \land \\
	remoto.statoCollegamento \neq Inattivo 
\also
	remoto'.messaggio = Testo? \\
\end{schema}

%********************************************************
\newpage
\section{Player}

\subsection{Inizializzazione}

\begin{schema}{InitStatoPartita}
	StatoPartita
\where
	tipoPartita=parIndef \\
	livello=0 \\
	colore1=indColore \\
	posScac=posIndef \\
	tipoGiocatore=gioIndef \\
	tempoB=0 \\
	tempoN=0 \\
	statoScacchieraCorrente = indStatoScacchiera \\
	partita = indPartita
\end{schema}

\subsection{Operazioni sul sistema}

Lo schema NuovaPartita corrisponde all'inizio di una partita partendo da nuovaScacchiera.

\begin{schema}{NuovoGioco}
	\Delta StatoPartita \\
	tipoPartita?:TIPOPARTITA \\
	livello?:\nat \\
	colore1?:COLORE \\
	posScac?:POSIZIONESCACCHIERA
\where
	tempoB'=0 \\
	tempoN'=0
\also
	statoScacchieraCorrente' = nuovaScacchiera \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita?, \\
		\t1 colore1?,bianco) \\
	tipoPartita'=tipoPartita? \\
	livello'=livello? \\
	colore1'=colore1? \\
	posScac'=posScac? \\
	partita'.mosseGiocate=\langle \rangle \\
	partita'.posIniziale=nuovaScacchiera
\end{schema}


MossaUmano corrisponde ad una mossa effettuata da un giocatore umano.


\begin{schema}{MossaUmano}
	\Delta StatoPartita \\
	m?:SEMIMOSSA
\where
	tipoGiocatore=umano \\
	mossaLegale(statoScacchieraCorrente,\langle m? \rangle)=vero
\also
	partita'.mosseGiocate=partita.mosseGiocate \cat \langle m? \rangle \\
	statoScacchieraCorrente'=nuovoStato(statoScacchieraCorrente,\langle m? \rangle) \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita,colore1, \\
		\t1 statoScacchieraCorrente'.deveMuovere) 
\end{schema}


MossaProgrammaConDb corrisponde ad una mossa effettuata dal programma
nel caso in cui si scelga di utilizzare il Db di posizioni come libro di
aperture ed in esso esistono stati della scacchiera raggiungibili da
quello corrente.

\begin{schema}{MossaProgrammaConDb}
	\Delta StatoPartita \\
	\Xi DBposizioni \\
	libroAperture?:SCELTA \\
	m:SEMIMOSSA
\where
	tipoGiocatore=programma \\
	libroAperture?=si \\
	esisteMossaNelDb(nodi,archi,iniziale,statoScacchieraCorrente) \\
		\t1 =vero
\also
	m=scegliMossaDaDb(nodi,archi,iniziale,statoScacchieraCorrente) \\
	mossaLegale(statoScacchieraCorrente, \langle m \rangle)=vero \\
	partita'.mosseGiocate=partita.mosseGiocate \cat \langle m \rangle \\
	statoScacchieraCorrente'=nuovoStato(statoScacchieraCorrente,\langle m \rangle) \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita,colore1, \\
		\t1 statoScacchieraCorrente'.deveMuovere)
\end{schema}


MossaProgrammaSenzaDb corrisponde ad una mossa del programma nei
seguenti casi: \\

- se non si sceglie di utilizzare il Db di posizioni come libro di
aperture \\
- se si e' scelto di utilizzarlo ma non esistono mosse giocabili al suo
interno. \\


\begin{schema}{MossaProgrammaSenzaDb}
	\Delta StatoPartita \\
	\Xi DBposizioni \\
	libroAperture?:SCELTA \\
	m:SEMIMOSSA
\where
	tipoGiocatore=programma \\
	(libroAperture?=no) \lor ((libroAperture?=si) \land \\
		\t1 (esisteMossaNelDb(nodi,archi,iniziale, \\
		\t1 statoScacchieraCorrente)=falso))
\also
	m=scegliMossa(statoScacchieraCorrente) \\
	mossaLegale(statoScacchieraCorrente,\langle m \rangle)=vero \\
	partita'.mosseGiocate=partita.mosseGiocate \cat \langle m \rangle \\
	statoScacchieraCorrente'=nuovoStato(statoScacchieraCorrente,\langle m \rangle) \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita,colore1, \\
		\t1 statoScacchieraCorrente'.deveMuovere)
\end{schema}


\begin{zed}
	MossaProgramma \defs MossaProgrammaSenzaDb \lor MossaProgrammaConDb
\end{zed}


ImpostazioneInterattiva permette all'utente di giocare una partita da
uno stato della scacchiera da lui impostato.
 
\begin{schema}{ImpostazioneInterattiva}
	\Delta StatoPartita \\
	statoScacchieraInput?:STATOSCACCHIERA \\
	tipoPartita?:TIPOPARTITA \\
	livello?:\nat \\
	posScac?:POSIZIONESCACCHIERA \\
	colore1?:COLORE
\where
	statoLegale(statoScacchieraInput?)=vero
\also
	tempoB'=0 \\
	tempoN'=0 \\
	tipoPartita'=tipoPartita? \\
	livello'=livello? \\
	posScac'=posScac? \\
	colore1'=colore1? \\
	statoScacchieraCorrente'=statoScacchieraInput? \\
	partita'.posIniziale=statoScacchieraInput? \\
	partita'.mosseGiocate= \langle \rangle \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita', \\
		\t1 colore1',statoScacchieraCorrente'.deveMuovere)
\end{schema}

Visualizza le informazioni di gioco.

\begin{schema}{VisualizzaInfo}
	\Xi StatoPartita \\
	sceltaVisualizzaInfo?:SCELTA \\
	tempoB!:\nat \\
	tempoN!:\nat \\
	variante!:\seq SEMIMOSSA \\
	valoreVariante!:\nat
\where
	sceltaVisualizzaInfo?=si \\
	tempoB!=tempoB \\
	tempoN!=tempoN \\
	variante!=calcolaVariante(statoScacchieraCorrente) \\
	valoreVariante!=calcolaValoreVariante(statoScacchieraCorrente, \\ 
		\t1 variante!) \\
	\# variante!=5 \\
	valoreVariante! \geq -1000 \\
	valoreVariante! \leq 1000
\end{schema}

Visualizza la lista delle mosse giocate

\begin{schema}{VisualizzaListaMosse}
	\Xi StatoPartita \\
	sceltaVisualizzaMosse?:SCELTA \\
	mosse!:\seq SEMIMOSSA
\where
	sceltaVisualizzaMosse?=si \\
	mosse!=partita.mosseGiocate
\end{schema}


SalvaStatoCorrente corrisponde al salvataggio su file dello
statoScacchieraCorrente.

\begin{schema}{SalvaStatoCorrente}
	\Xi StatoPartita \\
	\Delta FileSystem \\
	nome?:NOMIFILE
\where
	fileStato'=fileStato \oplus \{nome? \mapsto statoScacchieraCorrente\} \\
\end{schema}


CaricaStatoCorrente permette di giocare una partita a partire da una
posizione precedentemente salvata su file. Gli altri parametri di
StatoPartita vengono impostati interattivamente.

\begin{schema}{CaricaStatoCorrente}
	\Delta StatoPartita \\
	\Xi FileSystem \\
	nome?:NOMIFILE \\
	tipoPartita?:TIPOPARTITA \\
	colore1?:COLORE \\
	livello?:\nat \\
	posScac?:POSIZIONESCACCHIERA
\where
	tempoB'=0 \\
	tempoN'=0 \\
	partita'.mosseGiocate=\langle \rangle \\
	partita'.posIniziale=fileStato(nome?) \\
	statoScacchieraCorrente'=fileStato(nome?) \\
	tipoPartita'=tipoPartita? \\
	livello'=livello? \\
	posScac'=posScac? \\
	colore1'=colore1? \\
	tipoGiocatore'=calcolaTipoGiocatore(tipoPartita',colore1', \\
		\t1 statoScacchieraCorrente'.deveMuovere)
\end{schema}


\end{document}



