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

Questo documento fornisce la specifica formale in Linguaggio {\bf Z} del
sistema di {\bf \it Asta Eletronica} a partire dal documento informale 
scritto in linguaggio naturale contenente le richieste del cliente.
Questo sistema \`e un servizio  distribuito che supporta la vendita di
oggetti, al meglio, mediante comunicazioni su rete Internet.
La specifica riguarda solamente il sistema d'asta vero e proprio, in
quanto si assume l'esistenza e l'utilizzo da parte degli utenti 
interessati all'asta di un servizio informativo, regolarmente
aggiornato, sulle aste indette che fornisce informazioni relativamente a 
data e ora di apertura di ogni asta, lista degli articoli banditi, loro 
descrizione, relativi prezzi base ed incrementi minimi richiesti per i 
rilanci. 
Previo accordo con i componenti degli altri gruppi, sono stati omessi 
volutamente gli invarianti negli schemi che modificano gli stati.

%  -------------------------------------------------------------------------
\section{Definizioni di base}
%  -------------------------------------------------------------------------
\label{band1}

I tipi $PERSONA$ e $STRINGA$ rappresentano rispettivamente l'insieme di 
tutte le possibili persone che hanno accesso alla rete Internet e 
l'insieme delle stringhe rappresentabili su video. 
Il tipo $PREZZO$ definisce l'insieme di tutti i possibili valori 
monetari, il tipo $RILANCIO$ indica le quantit\`a di denaro di cui \`e 
possibile rilanciare, $CODICE$ individua tutti i codici possibili utilizzati 
per identificare gli oggetti e i knowbot, mentre $BOOL$ rappresenta l'insieme
dei valori booleani.
 
\begin{zed}
[PERSONA,STRINGA]
\also
	PREZZO == \nat \\
	RILANCIO == \nat_1 \\
	CODICE == \nat_1 \\
	BOOL ::= TRUE | FALSE
\end{zed}


Lo schema {\it Oggetto } contiene le informazioni collegate ad un singolo 
oggetto dell'asta: codice identificativo, descrizione esauriente, prezzo 
di partenza ed incremento minimo di ogni rilancio.
Possono essere presenti codici uguali per oggetti diversi, infatti lo 
scopo di tale campo \`e quello di differenziare oggetti identici nei 
valori degli altri tre campi.

\index{Oggetto}
\begin{schema}{Oggetto}
	codice: CODICE \\
	descrizione: STRINGA \\
	prezzo\_base: PREZZO \\ 
	incremento\_min: RILANCIO 
\end{schema}


Il tipo $DATIRILANCIO$ contiene l'insieme dei dati, non ulteriormente 
specificati, che descrivono lo stato del singolo knowbot e che saranno 
utilizzati come parametri di ingresso della funzione che specifica la 
politica di rilancio. 
In particolare la politica di ogni oggetto \`e descritta nel seguente 
schema {\it PoliticaRilancio } contenente il prezzo massimo che il knowbot \`e 
abilitato a spendere per l'oggetto e la funzione rilancio di cui sopra.

\begin{zed}
[DATIRILANCIO]
\end{zed}

\index{PoliticaRilancio}
\begin{schema}{PoliticaRilancio}
	prezzo\_max: PREZZO \\
	rilancio: DATIRILANCIO \pfun RILANCIO
\end{schema}

Lo schema {\it knowbot } contiene le ulteriori informazioni associate al 
solo partecipante automatico, cio\`e il capitale complessivo spendibile,
la lista degli oggetti per i quali concorrere e relativa politica di rilancio.
L'informazione {\it codice } \`e stata introdotta allo scopo di 
differenziare knowbots identici in tutte le altre caratteristiche.

\index{Knowbot}
\begin{schema}{Knowbot}
	codice: CODICE \\
	capitale\_totale: PREZZO \\ 
	ogg\_di\_interesse: Oggetto \pfun PoliticaRilancio
\where
	\forall x: Oggetto | x \in \dom ogg\_di\_interesse \spot \\
\t1     (ogg\_di\_interesse(x)).prezzo\_max \leq capitale\_totale \land \\
\t1	(\forall y: DATIRILANCIO | y \in \dom 
(ogg\_di\_interesse(x)).rilancio \spot \\
\t2	(ogg\_di\_interesse(x)).rilancio(y) \geq x.incremento\_min) 
\end{schema}


Il tipo {\it COMUNICANTE } individua tutte le entit\`a che, all'interno del 
sistema, sono abilitate a comunicare tramite scambio di messaggi. 
Esso \`e formato dal {\it banditore } e dall'insieme dei possibili partecipanti,
sia automatici che non. Quest'ultimo insieme costituisce il tipo 
{\it PARTECIPANTE}.

\begin{syntax}
	PARTECIPANTE & ::= & fpersona \ldata PERSONA \rdata \\
		     & | & fknowbot \ldata Knowbot \rdata
\also
	COMUNICANTE & ::= & fpartecipante \ldata PARTECIPANTE \rdata \\
		    & | & banditore
\end{syntax}



%  -------------------------------------------------------------------------
\section{Stato dei partecipanti}
%  -------------------------------------------------------------------------
\label{statopart}

Il tipo $ACCREDITO$ individua l'insieme delle informazioni richieste dalla 
casa d'asta al partecipante al momento della sua richiesta di subscribe.
Tali dati di accredito sono contenuti nello schema $DatiPartecipante$ insieme
al valore del fido.

\begin{zed}
[ACCREDITO]
\end{zed}

\index{DatiPartecipante}
\begin{schema}{DatiPartecipante}
	dati\_accredito: ACCREDITO \\ 
	fido: PREZZO 
\end{schema}

Lo schema $StatoKnowbot$ rappresenta lo stato locale di ciascun knowbot e 
contiene le informazioni necessarie a quest'ultimo per effettuare la propria
politica di rilancio. In particolare: $vendita\_in\_corso$ indica se vi \'e 
un oggetto in fase di contrattazione, $oggetto\_attuale$ indica quale 
oggetto si sta trattando, $offerta\_attuale$ indica il valore monetario 
da incrementare per effettuare un rilancio, $capitale\_speso$ indica il 
totale del denaro speso dal knowbot fino ad un dato istante e infine  
$dati\_knowbot$ contiene i dati utilizzati dal knowbot per applicare la  
propria politica di rilancio. 

\index{StatoKnowbot}
\begin{schema}{StatoKnowbot}
	vendita\_in\_corso: BOOL \\
	oggetto\_attuale: Oggetto \\
	offerta\_attuale: PREZZO \\ 
	capitale\_speso: PREZZO \\
	dati\_knowbot: DATIRILANCIO
\end{schema}

Nel prossimo schema sono raccolte tutte le informazioni relative agli utenti,
inclusi i rappresentanti software, che operano nel sistema. In particolare
$collegati$ \`e l'insieme di tutti i partecipanti attivi e passivi e di tutti 
i knowbots attivi; la funzione $partecipanti\_attivi$ associa ad ogni 
persona che ha fatto subscribe o partecipa tramite knowbot i relativi dati di 
accredito (si noti che, anche nel seguito, per ``partecipante attivo'' si 
intende il partecipante umano che \`e attivo o perch\'e ha fatto subscribe o 
perch\'e \`e rappresentato da un knowbot ed una condizione esclude l'altra); la 
funzione $knowbots$ associa ad ogni persona che partecipa in modo automatico 
le informazioni aggiuntive relative al proprio knowbot; la funzione 
$stati\_knowbots$ associa ad ogni knowbot il proprio stato locale; 
l'insieme $pass$ contiene tutti i partecipanti attivi, umani o automatici, che 
non sono interessati all'acquisto dell'oggetto ora in vendita.

\index{Utenti}
\begin{schema}{Utenti}
	collegati: \finset PARTECIPANTE \\
	partecipanti\_attivi: PERSONA \pfun DatiPartecipante \\
	knowbots: PERSONA \pinj Knowbot \\
	stati\_knowbots: Knowbot \pfun StatoKnowbot \\
	pass: \finset PARTECIPANTE
\where
	\dom knowbots \subseteq \dom partecipanti\_attivi \\
	\dom partecipanti\_attivi \setminus \dom knowbots \subseteq 
	fpersona \inv \limg collegati \rimg \\
	\ran knowbots = fknowbot \inv \limg collegati \rimg \\
	\forall x:PERSONA | x \in \dom knowbots \spot \\
\t1     (knowbots(x)).capitale\_totale \leq (partecipanti\_attivi(x)).fido \\
	\ran knowbots = \dom stati\_knowbots \\
	fpersona \inv \limg pass \rimg \subseteq (\dom partecipanti\_attivi 
\setminus \dom knowbots) \\
	fknowbot \inv \limg pass \rimg \subseteq \ran knowbots 
\end{schema}

\begin{schema}{InitUtenti}
	Utenti'
\where
	collegati' = \emptyset \\
	partecipanti\_attivi' = \emptyset \\
	knowbots' = \emptyset \\
	stati\_knowbots' = \emptyset \\
	pass' = \emptyset                                   
\end{schema}


%  -------------------------------------------------------------------------
\section{Stato dell'Asta}
%  -------------------------------------------------------------------------


Il tipo $PARAMETRIDEC$ indica l'insieme dei parametri dai quali dipende la
decisione, di tipo $DECISIONE$, del banditore automatico di mandare o 
meno un messaggio di expiring time o di fine contrattazione ai partecipanti.
Il tipo $FASE$ \`e costituito dall'insieme dei valori che pu\`o assumere 
lo stato dell'asta, cio\`e $AstaInCorso$ durante la contrattazione vera 
e propria, $AstaFerma$ durante il passaggio dalla vendita di un oggetto al 
successivo e $AstaNonInCorso$ prima dell'inizio dell'asta. 

\begin{zed}
[PARAMETRIDEC]
\also
	LISTAOGGETTI == \iseq Oggetto \\
	FASE ::= AstaInCorso | AstaFerma | AstaNonInCorso \\
	DECISIONE ::= MessaggioExpiringTime | FineContrattazione      
\end{zed}


In questa sezione viene introdotto lo schema che rappresenta lo stato 
dell'asta. Esso contiene, nell'ordine, la lista, invariata nel corso 
dell'asta, degli oggetti messi in vendita; il numero 
di sequenza dell'oggetto attualmente in contrattazione con la 
relativa offerta valida e corrispondente detentore. Quest'ultimo assume 
inizialmente il valore della seguente costante:

\begin{axdef}
	DetentoreIniziale: PARTECIPANTE
\end{axdef}

Seguono i dati di accredito del detentore (necessari in caso di 
scollegamento del detentore prima della aggiudicazione del pezzo). Essi 
assumono inizialmente il valore della seguente costante:

\begin{axdef}
	DatiInizialiDet: ACCREDITO
\end{axdef}

Nello schema asta sono presenti inoltre le informazioni sulla natura del 
banditore, che pu\`o essere umano o automatico. In quest'ultimo caso viene 
anche specificata la funzione che ne descrive la politica di decisione.
Lo stato di svolgimento dell'asta viene individuato dal valore 
della variabile $fase$ ed infine la funzione $oggetti\_venduti$ tiene 
traccia delle vendite effettuate durante l`asta mantenendo i dati degli 
acquirenti. 

\index{Asta}
\begin{schema}{Asta}
	lista\_oggetti: LISTAOGGETTI \\
	oggetto\_in\_vendita: \nat \\
	current\_bid: PREZZO \\
	detentore\_CB: PARTECIPANTE \\
	dati\_detentore: ACCREDITO \\
	banditore\_umano: BOOL \\
	politica\_banditore: PARAMETRIDEC \pfun DECISIONE \\
	fase: FASE \\
	oggetti\_venduti: Oggetto \pfun (PERSONA \cross ACCREDITO \cross 
PREZZO) 
\where
	(politica\_banditore = \emptyset \land banditore\_umano = TRUE) 
\lor \\
\t1     (FineContrattazione \in \ran politica\_banditore \land 
banditore\_umano = FALSE) \\                     
	oggetto\_in\_vendita \leq \# lista\_oggetti \\
	\dom oggetti\_venduti \subseteq lista\_oggetti \limg 
1 \upto oggetto\_in\_vendita \rimg \end{schema}

\begin{schema}{InitAsta}
	Asta'
\where
	lista\_oggetti' = \langle \rangle \\
	oggetto\_in\_vendita' = 0 \\
	current\_bid' = 0 \\
	detentore\_CB' = DetentoreIniziale \\
	dati\_detentore' = DatiInizialiDet \\
	banditore\_umano' = TRUE \\
	politica\_banditore' = \emptyset \\
	fase' = AstaNonInCorso \\
	oggetti\_venduti' = \emptyset  
\end{schema}

%  -------------------------------------------------------------------------
\section{Stato della comunicazione}
%  -------------------------------------------------------------------------

La comunicazione \`e descritta mediante uno spazio condiviso nel quale ogni
mittente autorizzato pu\`o depositare messaggi ed ogni destinatario 
autorizzato pu\`o prelevarli.

Ogni messaggio \`e identificato da una tripla ordinata dove, la prima e 
la seconda componente rappresentano rispettivamente il mittente ed il 
destinatario del messaggio, e la terza rappresenta il contenuto dello stesso,
cio\`e la coppia formata dall'identificatore del messaggio (tipo $TIPOMES$) e 
dalle informazioni collegate (tipo $INFORMAZIONE$); questo elemento della 
coppia pu\`o essere in alcuni casi inutilizzato; per tale uso \`e definito 
InfoVuota.

Le funzioni ausiliarie $MsgMittente$, $MsgDestinatario$, $MsgContenuto$ 
estraggono da $MESSAGGIO$ le corrispondenti componenti; cos\`i come le 
funzioni $ContTipomes$, $ContInformazione$ estraggono da $CONTENUTO$ le 
corrispondenti componenti.  

\begin{zed}
[INFORMAZIONE]
\also
	TIPOMES ::= Vuoto | \\
\t1     ComRilancio | ComPass | ComSubscribe | \\
\t1     ComUnsubscribe | ComRichiestaPAttivi | \\
\t1     OggettoInvenduto | ModalitaConsegnaPagamento | AstaConclusa | \\
\t1     IlTempoStaPerScadere | SubscribeEffettuataConSuccesso | \\
\t1     UtenteGiaAttivo | CredenzialiInsufficienti | \\
\t1     UnsubscribeEffettuataConSuccesso | PassRifiutato | \\
\t1     UtenteConKnowbot | RilanciSospesiPerOggettoInVendita | \\
\t1     NoFaseAstaInCorso | CurrentBid | OggettoAggiudicato | \\
\t1     IllustraOggetto | ListaPAttivi | UtenteNonSubscribed
\also
	CONTENUTO == TIPOMES \cross INFORMAZIONE
\also
	MESSAGGIO == COMUNICANTE \cross COMUNICANTE \cross CONTENUTO
\end{zed}


\begin{axdef}
	MsgMittente: MESSAGGIO \fun COMUNICANTE \\
	MsgDestinatario: MESSAGGIO \fun COMUNICANTE \\
	MsgContenuto: MESSAGGIO \fun CONTENUTO 
\where
	\forall m: MESSAGGIO; s,r: COMUNICANTE; c: CONTENUTO | m = 
(s,r,c) \spot \\
\t1     MsgMittente(m) = s \land MsgDestinatario(m) = r \land 
MsgContenuto(m) = c
\end{axdef}

\begin{axdef}
	ContTipomes: CONTENUTO \fun TIPOMES  \\
	ContInformazione: CONTENUTO \fun INFORMAZIONE
\where
	\forall c:CONTENUTO; t:TIPOMES; i:INFORMAZIONE | c=(t,i) \spot \\
\t1	ContTipomes(c) = t \land ContInformazione(c) = i
\end{axdef}

\begin{axdef}
	InfoVuota: INFORMAZIONE
\end{axdef}

Lo spazio condiviso, chiamato $mailbox$, \`e una sequenza di 
lunghezza arbitraria di messaggi in cui viene mantenuto un ordinamento 
FIFO tra quelli che hanno lo stesso destinatario.
Lo scambio di messaggi pu\`o avvenire solo tra partecipanti collegati alla 
casa d'aste e banditore o viceversa. Quindi due partecipanti non 
possono comunicare tra loro, e nemmeno il banditore pu\`o spedirsi un
messaggio da solo (a questo proposito si veda~\ref{fixedbug})
	
\index{Comunicazione}
\begin{schema}{Comunicazione}
	mailbox: \seq MESSAGGIO
\where
	\forall x: MESSAGGIO | x \in \ran (mailbox) \spot \\
\t1     (MsgMittente(x) \in \ran fpartecipante MsgDestinatario(x) = 
banditore \land \\
\t2	ContTipomes(MsgContenuto(x)) \in \{ ComRilancio, ComPass, \\
\t3     ComSubscribe, ComUnsubscribe, ComRichiestaPAttivi \} ) \lor \\
\t1     (MsgMittente(x) = banditore \land MsgDestinatario(x) \in \ran
fpartecipante \land \\
\t2	ContTipomes(MsgContenuto(x)) \in TIPOMES \setminus \{ Vuoto, \\
\t3     ComRilancio, ComPass, ComSubscribe, \\
\t3	ComUnsubscribe, ComRichiestaPAttivi \} ) 
\end{schema} 

\begin{schema}{InitComunicazione}
	Comunicazione'
\where
	mailbox' = \langle \rangle
\end{schema}

%  -------------------------------------------------------------------------
\section{Stato globale del Sistema Asta}
%  -------------------------------------------------------------------------
\label{bug1}

Il seguente schema definisce lo stato globale del sistema asta attraverso 
l'inclusione degli schemi di stato che definiscono le tre componenti del 
sistema individuate inizialmente. La parte predicativa specifica che il 
mittente o il destinatario di un messaggio \`e il banditore o un 
partecipante che deve essere collegato.

\index{SistemaAsta}
\begin{schema}{SistemaAsta}
	Utenti \\
	Asta \\
	Comunicazione
\where
	\forall x: MESSAGGIO | x \in \ran mailbox \spot \\
\t1	( MsgMittente(x) = banditore \iff \\
\t2	fpartecipante \inv (MsgDestinatario(x) \in collegati )
\t1	( MsgDestinatario(x) = banditore \iff \\
\t2	fpartecipante \inv (MsgMittente(x)) \in collegati ) \land \\
\end{schema}

\begin{zed}  
	InitSistemaAsta \defs InitUtenti \land InitAsta \land 
InitComunicazione
\end{zed}

%  -------------------------------------------------------------------------
\section{Funzioni ausiliarie}
%  -------------------------------------------------------------------------
\label{whoami}

Si assume presente nel sistema un servizio identificativo indicato con
$WhoAmI$ che permette di individuare il comunicante che lo richiama.
Poich\'e la notazione {\bf Z } non permette di definire funzioni che non 
richiedono parametri in input, si \`e utilizzata una semplice variabile.

\begin{axdef}
	WhoAmI : COMUNICANTE
\end{axdef}

In questa sezione vengono specificate le funzioni ausiliarie utilizzate
in seguito negli schemi che costituiscono le operazioni.

La funzione $IndividuaPersona$ a partire da un elemento di tipo 
$PARTECIPANTE$ restituisce la persona corrispondente. In particolare
se in ingresso ha un partecipante umano restituisce la persona stessa, 
mentre, in caso di partecipante automatico, restituisce la persona che 
\`e rappresentata dal knowbot.

\begin{axdef}
	IndividuaPersona: (PARTECIPANTE \cross (PERSONA \pinj Knowbot)) 
\pfun PERSONA 
\where
	\forall x: PARTECIPANTE; y: (PERSONA \pinj Knowbot) \spot \\
\t1     (x \in \ran fpersona \land IndividuaPersona(x,y) = fpersona \inv 
(x)) \lor \\ 
\t1     (x \in \ran fknowbot \land fknowbot \inv (x) \in \ran y \land \\
\t2	IndividuaPersona(x,y) = y \inv (fknowbot \inv (x))) \lor \\
\t1     (x \in \ran fknowbot \land fknowbot \inv (x) \notin \ran y \land 
(x,y) \notin \dom IndividuaPersona) \\
\end{axdef}

La funzione $ConvertiComando$ esegue la conversione nel formato finale
del messaggio, della stringa contenente il comando scritto dall'utente.
Le successive quattro funzioni ausiliarie convertono gli elementi in input 
nel 
tipo $INFORMAZIONE$ al fine di consentirne l'inclusione nel formato finale 
del messaggio.

\begin{axdef}
	ConvertiComando: STRINGA \pfun CONTENUTO \\
\where
	ContTipomes \limg \ran ConvertiComando \rimg = \\
\t1     \{ ComRilancio, ComPass, ComSubscribe, ComUnsubscribe, \\ 
\t2     ComRichiestaPAttivi \} 
\end{axdef}

\begin{axdef}
	ConvertiRilancio: (Oggetto \cross PREZZO) \inj INFORMAZIONE  \\
	ConvertiOggetto: Oggetto \inj INFORMAZIONE \\
	ConvertiDetentore: (PERSONA \cross PREZZO) \inj 
INFORMAZIONE \\
	ConvertiListaPAttivi: (\finset PERSONA) \inj INFORMAZIONE 
\end{axdef}

La funzione $CreaModalita$ crea un messaggio contenente le modalit\`a di 
pagamento e consegna di un dato oggetto aggiudicato ad un dato prezzo.

\begin{axdef}
	CreaModalita: (Oggetto \cross PREZZO) \inj INFORMAZIONE  
\end{axdef}

La funzione $EstraiStringa$ viene applicata al messaggio ricevuto per 
ottenere la stringa da stampare sul video.
La funzione $EstraiDati$ viene applicata alla parte di informazioni del 
messaggio ricevuto per estrarne i dati relativi al partecipante che 
richiede una subscribe.
La funzione $VerificaCredenziali$ restituisce un booleano a seconda 
del giudizio sulla affidabilit\`a delle credenziali del cliente.

\begin{axdef}
	EstraiStringa: CONTENUTO \pinj STRINGA
\where
	ContTipomes \limg \dom EstraiStringa \rimg = TIPOMES \setminus {} \\
\t1     \{ Vuoto, ComRilancio, ComPass, ComSubscribe, ComUnsubscribe, \\
\t2	ComRichiestaPAttivi \} 
\end{axdef}

\begin{axdef}
	EstraiDati: INFORMAZIONE \surj DatiPartecipante \\
	VerificaCredenziali: DatiPartecipante \surj BOOL 
\end{axdef}

La funzione seguente, definita per necessit\`a come variabile, non ha 
parametri in input e restituisce il valore dei parametri utilizzati dal 
banditore automatico per decidere la sua politica di expiring time e di
fine contrattazione.

\begin{axdef}
	CalcoloParametri: PARAMETRIDEC
\end{axdef}

La funzione $ModificaDati$ modifica i dati locali di un knowbot 
utilizzati per sua la politica di rilancio. La modifica si basa sui 
messaggi ricevuti dal banditore. I dati vengono inoltre modificati in 
occasione di un rilancio del knowbot ($ComRilancio$) in modo da rilevare 
che tale evento \`e gi\`a avvenuto.     

\begin{axdef}
	ModificaDati: CONTENUTO \pfun DATIRILANCIO
\where
	ContTipomes \limg \dom ModificaDati \rimg = \{ ComRilancio, 
OggettoInvenduto, \\
\t1     IlTempoStaPerScadere, PassRifiutato, 
RilanciSospesiPerOggettoInVendita, \\
\t1	NoFaseAstaInCorso, CurrentBid, OggettoAggiudicato, IllustraOggetto 
\} 
\end{axdef}

%  -------------------------------------------------------------------------
\section{Schemi ausiliari}
%  -------------------------------------------------------------------------
\label{bug2}

In questa sezione vengono specificati gli schemi ausiliari utilizzati in 
seguito ed i $REPORT$, cio\`e i messaggi di errore restituiti all'entit\`a che
attiva lo schema, sia in caso di successo che non.

\begin{zed}
	REPORT ::= Ok | Partecipante\_gia\_collegato | 
Collegamento\_assente | \\
\t1     Non\_sono\_persona | Non\_sono\_persona\_collegata | \\
\t1     Non\_sono\_knowbot | Non\_sono\_banditore | \\
\t1     Fase\_non\_corretta | Nessun\_comando\_ricevuto | \\
\t1     Expiring\_time\_non\_inviato | Contrattazione\_non\_terminata | \\
\t1     Comando\_inesistente | Rilancio\_non\_inviato 
\end{zed}

Lo schema $Successo$ riporta incondizionatamente l'esito positivo di
qualsiasi operazione.

\index{Successo}
\begin{schema}{Successo}
	rep!: REPORT 
\where
	rep! =  Ok
\end{schema}

Gli schemi definiti nel seguente gruppo sono utilizzati ogni volta che si 
vuole controllare che le operazioni siano attivate solamente dall'entit\`a
abilitata.
	
\index{SonoPersona}
\begin{schema}{SonoPersona}
	rep!: REPORT            
\where
	WhoAmI \neq banditore \\
	fpartecipante \inv (WhoAmI) \in \ran fpersona \\
\end{schema}

\index{NonSonoPersona}
\begin{schema}{NonSonoPersona}
	rep!: REPORT
\where
	(WhoAmI = banditore) \lor \\
\t1     (fpartecipante \inv (WhoAmI) \in \ran fknowbot) \\
\also
	rep! = Non\_sono\_persona
\end{schema}
	
\index{SonoPersonaCol}
\begin{schema}{SonoPersonaCol}
	\Xi Utenti \\   
	rep!: REPORT         
\where
	WhoAmI \neq banditore \\
	fpartecipante \inv (WhoAmI) \in \ran fpersona \\
	fpartecipante \inv (WhoAmI) \in collegati
\end{schema}

\index{NonSonoPersonaCol}
\begin{schema}{NonSonoPersonaCol}
	\Xi Utenti \\
	rep!: REPORT
\where
	(WhoAmI = banditore) \lor \\
\t1     (fpartecipante \inv (WhoAmI) \in \ran fknowbot) \lor \\
\t1     (fpartecipante \inv (WhoAmI) \notin collegati) \\
\also
	rep! = Non\_sono\_persona\_collegata
\end{schema}

\index{SonoKnowbot}
\begin{schema}{SonoKnowbot}
	\Xi Utenti \\
	rep!: REPORT      
\where
	WhoAmI \neq banditore \\
	fpartecipante \inv (WhoAmI) \in \ran fknowbot \\
	fpartecipante \inv (WhoAmI) \in collegati
\end{schema}

\index{NonSonoKnowbot}
\begin{schema}{NonSonoKnowbot}
	\Xi Utenti \\
	rep!: REPORT
\where
	(WhoAmI = banditore) \lor \\
\t1     (fpartecipante \inv (WhoAmI) \in \ran fpersona) \lor \\
\t1     (fpartecipante \inv (WhoAmI) \notin collegati) \\
\also
	rep! = Non\_sono\_knowbot
\end{schema}

\index{SonoBanditore}
\begin{schema}{SonoBanditore}
	rep!: REPORT    
\where
	WhoAmI = banditore \\
\end{schema}

\index{NonSonoBanditore}
\begin{schema}{NonSonoBanditore}
	rep!: REPORT
\where
	WhoAmI \neq banditore \\
\also
	rep! = Non\_sono\_banditore
\end{schema}


%  -------------------------------------------------------------------------
\section{Gestione comunicazione}
%  -------------------------------------------------------------------------

Lo schema $Spedisci$ rappresenta l'operazione di invio di un singolo 
messaggio ad un unico destinatario, cio\`e tratta il caso della 
comunicazione uno a uno. 

\index{Spedisci}
\begin{schema}{Spedisci}
	\Delta Comunicazione \\
	destinatario?: COMUNICANTE \\
	contenuto?: CONTENUTO
\where
	mailbox' = mailbox \cat \langle (WhoAmI,destinatario?,contenuto?) 
\rangle
\end{schema}

Lo schema $Broadcast$ rappresenta l'operazione di invio di un singolo 
messaggio all'insieme di tutti i partecipanti collegati, attivi e non. 
Questa operazione ha l'effetto di inserire nel $mailbox$ tante copie 
del messaggio (con egual mittente e contenuto) quanti sono i destinatari.  

\index{Broadcast}
\begin{schema}{Broadcast}
	\Delta Comunicazione \\
	\Xi Utenti \\
	contenuto?: CONTENUTO
\where
	\exists messaggi: \iseq MESSAGGIO | \\
\t2     \# messaggi = \# collegati \land \\
\t2	(\forall x,y : COMUNICANTE; z : CONTENUTO | (x,y,z) \in \ran 
messaggi \spot \\
\t3  	x = WhoAmI \land \\
\t3	y \in \ran fpartecipante \land fpartecipante \inv (y) \in 
collegati \land \\
\t3	z = contenuto? ) \spot \\
\t1	mailbox' = mailbox \cat messaggi
\end{schema}

L'operazione di ricezione ($Ricevi$) restituisce il primo messaggio nel 
$mailbox$ che ha come destinatario colui che attiva l'operazione.
Nel caso in cui non ci siano messaggi per il destinatario viene 
restituito un messaggio vuoto ($ZeroMessaggi$).

\begin{schema}{RiceviOK}
	\Delta Comunicazione \\
	mittente!: COMUNICANTE\\
	contenuto!: CONTENUTO
\where
	(\LET Messaggi == mailbox \filter \{ s:COMUNICANTE; c:CONTENUTO 
\spot \\
\t2	(s,WhoAmI,c) \} \spot \\
\t1     Messaggi \neq \langle\rangle \land \\
\also
\t1     mittente! = MsgMittente(head(Messaggi)) \land \\
\t1     contenuto! = MsgContenuto(head(Messaggi)) \land \\
\t1     (\exists l: \seq MESSAGGIO; r: \seq_1 MESSAGGIO | l \cat r = mailbox 
\land \\
\t3	head(Messaggi) \notin \ran l \land head(r) = head(Messaggi) \spot \\ 
\t2	mailbox' = l \cat tail(r)))
\end{schema}

\begin{schema}{ZeroMessaggi}
	\Xi Comunicazione \\
	mittente!: COMUNICANTE \\
	contenuto!: CONTENUTO
\where
	mailbox \filter \{ s: COMUNICANTE; c: CONTENUTO \spot (s,WhoAmI,c) \} 
= \langle \rangle \\      
\also
	mittente! = WhoAmI \\
	contenuto! = (Vuoto,InfoVuota)
\end{schema}

\index{Ricevi}
\begin{zed}
	Ricevi \defs RiceviOK \lor ZeroMessaggi
\end{zed}

Lo schema seguente ($NessunComando$) prevede il caso di errore 
in cui un comunicante tenta di ricevere il comando vuoto.

\index{NessunComando}
\begin{schema}{NessunComando}
	mittente?: COMUNICANTE \\
	contenuto?: CONTENUTO \\
	rep!: REPORT
\where
	ContTipomes(contenuto?) = Vuoto \\
\also
	rep! = Nessun\_comando\_ricevuto
\end{schema}

%  -------------------------------------------------------------------------
\section{Operazioni dei partecipanti umani}
%  -------------------------------------------------------------------------

In questa sezione sono trattate le operazioni che pu\`o effettuare un 
partecipante umano.

%  -------------------------------------------------------------------------
\subsection{Invio di un comando}
%  -------------------------------------------------------------------------
\label{inviocom}

L'operazione $DOInviaComando$ permette al partecipante umano di richiedere 
al banditore l'esecuzione di uno dei seguenti comandi: Rilancio, Pass, 
Subscribe, Unsubscribe, RichiestaPAttivi. L'effetto di questa operazione \`e 
quello di inviare un messaggio al banditore specificando nel contenuto il 
comando richiesto ed i relativi parametri.
Sono gestiti i casi di errore in cui \`e richiesto un comando 
inesistente oppure in cui l'operazione \`e attivata da un comunicante 
non abilitato.
      
\begin{schema}{InserisciComandoOK}
	comando?: STRINGA \\
	destinatario!: COMUNICANTE \\
	contenuto!: CONTENUTO
\where
	comando? \in \dom ConvertiComando \\
\also
	destinatario! = banditore \\
	contenuto! = ConvertiComando(comando?)
\end{schema}

\begin{schema}{ComandoInesistente}
	comando?: STRINGA \\
	rep!: REPORT
\where
	comando? \notin \dom ConvertiComando \\
\also
	rep!= Comando\_inesistente
\end{schema}

\index{DOInviaComando}
\begin{zed}
	InviaComando \defs ((InserisciComandoOK \pipe Spedisci) \land 
Successo) \lor \\
\t1	ComandoInesistente 
\also
	DOInviaComando \defs (InviaComando \land SonoPersonaCol) \lor 
NonSonoPersonaCol
\end{zed}

%  -------------------------------------------------------------------------
\subsection{Ricezione di un messaggio}
%  -------------------------------------------------------------------------

La ricezione di un messaggio del banditore da parte di un partecipante 
umano collegato \`e gestita con la semplice stampa a video della stringa 
estratta dal messaggio. 

\begin{schema}{StampaMessaggio}
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	stampa!: STRINGA
\where
	stampa! = EstraiStringa(contenuto?)
\end{schema}

\index{DORiceviMessaggio}
\begin{zed}
	RiceviMessaggio \defs Ricevi \pipe ((StampaMessaggio \land 
Successo) \lor NessunComando)
\also
	DORiceviMessaggio \defs (RiceviMessaggio \land SonoPersonaCol) \lor 
NonSonoPersonaCol 
\end{zed}

%  -------------------------------------------------------------------------
\subsection{Apertura del collegamento}
%  -------------------------------------------------------------------------

L'operazione $DOCollegamento$ permette ad un utente di collegarsi alla 
casa d'aste come partecipante passivo, al fine di seguire lo svolgimento 
dell'asta o di effettuare una subscribe.

\begin{schema}{CollegamentoOK}
	\Delta Utenti 
\where
	fpartecipante \inv(WhoAmI) \notin collegati \\
\also
	collegati' = collegati \cup \{ fpartecipante \inv (WhoAmI) \}
\end{schema}

\begin{schema}{CollegamentoPresente}
	\Xi Utenti \\
	rep! : REPORT
\where
	fpartecipante \inv(WhoAmI) \in collegati \\     
\also
	rep! = Partecipante\_gia\_collegato
\end{schema}

\index{DOCollegamento}
\begin{zed}
	Collegamento \defs (CollegamentoOK \land Successo) \lor 
CollegamentoPresente 
\also
	DOCollegamento \defs (Collegamento \land SonoPersona) \lor 
NonSonoPersona
\end{zed}

%  -------------------------------------------------------------------------
\subsection{Chiusura del collegamento}
%  -------------------------------------------------------------------------
\label{domres}

L'operazione $DOChiudiCollegamento$, simmetrica alla precedente, 
permette ad un partecipante di scollegarsi dal sistema. Se richiesto da un 
partecipante attivo, il comando ha anche l'effetto di unsubscribe.
Se sono presenti nel $mailbox$ messaggi che hanno come mittente o 
destinatario tale partecipante questi vengono rimossi.

\begin{schema}{ChiudiCollegamentoOK}
	\Delta Comunicazione \\
	\Delta Utenti 
\where
	fpartecipante \inv(WhoAmI) \in collegati \\
\also
	( \LET PersonaAmI == fpersona \inv (fpartecipante \inv(WhoAmI)) \spot \\
\t1     partecipanti\_attivi'= \\ 
\t2	\IF PersonaAmI \in \dom partecipanti\_attivi 
\setminus \dom knowbots \\
\t2     \THEN \{ PersonaAmI \} \ndres partecipanti\_attivi \ELSE 
partecipanti\_attivi ) \\
	mailbox' = mailbox \filter \{ mittente,destinatario: COMUNICANTE; \\
\t1     c: CONTENUTO | mittente \neq WhoAmI \land destinatario \neq WhoAmI 
\spot \\
\t1     (mittente,destinatario,c) \} \\
	collegati' = collegati \setminus \{ fpartecipante \inv (WhoAmI) \}
\end{schema}

\begin{schema}{CollegamentoAssente}
	\Xi Utenti \\
	rep!: REPORT
\where
	fpartecipante \inv (WhoAmI) \notin collegati \\
\also
	rep! = Collegamento\_assente
\end{schema}

\index{DOChiudiCollegamento}
\begin{zed}
	ChiudiCollegamento \defs (ChiudiCollegamentoOK \land Successo) \lor 
CollegamentoAssente 
\also   
	DOChiudiCollegamento \defs (ChiudiCollegamento \land SonoPersona) 
\lor NonSonoPersona
\end{zed} 

%  -------------------------------------------------------------------------
\section{Operazioni dei knowbot partecipanti}
%  -------------------------------------------------------------------------

In questa sezione sono trattate le operazioni che pu\`o effettuare un 
partecipante knowbot.

%  -------------------------------------------------------------------------
\subsection{Spedizione di un Comando}
%  -------------------------------------------------------------------------

Il partecipante Knowbot pu\`o spedire al banditore o un comando di 
rilancio, o un comando di pass. 
Applicando la funzione che descrive la politica di rilancio del Knowbot,
relativa all'oggetto in contrattazione, si decide se effettuare il rilancio
e con quale valore. Se il rilancio avviene, tale evento si riflette in 
una modifica dei dati locali del knowbot. 
Controllando se l'oggetto in contrattazione appartiene all'insieme di 
oggetti di interesse del knowbot, si decide se effettuare il pass. 

\zedtab 1em
\begin{schema}{RilancioKnowbotOK}
	\Delta Utenti \\
	destinatario!: COMUNICANTE \\
	contenuto!: CONTENUTO
\where
	( \LET KnowbotAmI == fknowbot \inv(fpartecipante \inv(WhoAmI)) \spot \\
\t1     (stati\_knowbots(KnowbotAmI)).vendita\_in\_corso = TRUE \land \\
\t1     ( \LET StatoK == stati\_knowbots(KnowbotAmI) \spot \\
\t2     StatoK.oggetto\_attuale \in \dom KnowbotAmI.ogg\_di\_interesse 
\land \\ 
\t2     ( \LET PoliticaK == 
KnowbotAmI.ogg\_di\_interesse(StatoK.oggetto\_attuale) \spot \\
\t3     StatoK.dati\_knowbot \in \dom PoliticaK.rilancio \land \\
\t3	( \LET RilancioK == PoliticaK.rilancio(StatoK.dati\_knowbot) \spot \\
\t4	RilancioK + StatoK.offerta\_attuale \leq PoliticaK.prezzo\_max 
\land \\
\t4	RilancioK + StatoK.offerta\_attuale + StatoK.capitale\_speso \leq \\
\t5	KnowbotAmI.capitale\_totale \land 
\also
\t4     destinatario! = banditore \land \\
\t4	contenuto! = (ComRilancio, ConvertiRilancio(StatoK.oggetto\_attuale, \\
\t5	RilancioK + StatoK.offerta\_attuale)))) \land \\
\t2     stati\_knowbots' = stati\_knowbots \oplus \{ x: StatoKnowbot | \\
\t3     x.vendita\_in\_corso = StatoK.vendita\_in\_corso \land \\
\t3     x.oggetto\_attuale = StatoK.oggetto\_attuale \land \\  
\t3	x.offerta\_attuale = StatoK.offerta\_attuale \land \\
\t3	x.capitale\_speso = StatoK.capitale\_speso \land \\  
\t3     x.dati\_knowbot = ModificaDati(contenuto!) \\
\t3	\spot KnowbotAmI \mapsto x \}  ) )
\end{schema}

\begin{schema}{NoRilancioKnowbot}
	\Xi Utenti \\
	rep!: REPORT
\where
	( \LET KnowbotAmI == fknowbot \inv(fpartecipante \inv(WhoAmI)) \spot \\
\t1     (stati\_knowbots(KnowbotAmI)).vendita\_in\_corso = FALSE \lor \\
\t1     ( \LET StatoK == stati\_knowbots(KnowbotAmI) \spot \\
\t2     StatoK.oggetto\_attuale \notin \dom KnowbotAmI.ogg\_di\_interesse 
\lor \\ 
\t2     ( \LET PoliticaK == 
KnowbotAmI.ogg\_di\_interesse(StatoK.oggetto\_attuale) \spot \\
\t3     StatoK.dati\_knowbot \notin \dom PoliticaK.rilancio \lor \\
\t3	( \LET RilancioK == PoliticaK.rilancio(StatoK.dati\_knowbot) \spot \\
\t4	RilancioK + StatoK.offerta\_attuale > PoliticaK.prezzo\_max 
\lor \\
\t4	RilancioK + StatoK.offerta\_attuale + StatoK.capitale\_speso > \\
\t5	KnowbotAmI.capitale\_totale )))) 
\also
	rep! = Rilancio\_non\_inviato
\end{schema}
\zedtab 2em

\index{DORilancioKnowbot}
\begin{zed}
	RilancioKnowbot \defs ((RilancioKnowbotOK \pipe Spedisci) \land 
Successo) \lor \\ 
\t1	NoRilancioKnowbot 
\also
	DORilancioKnowbot \defs (RilancioKnowbot \land SonoKnowbot) \lor 
NonSonoKnowbot \\
\end{zed}

\begin{schema}{PassKnowbot}
	\Xi Utenti \\
	mittente?: COMUNICANTE \\
	contenuto?: CONTENUTO \\
	destinatario!: COMUNICANTE \\
	contenuto!: CONTENUTO 
\where
	( \LET KnowbotAmI == fknowbot \inv(fpartecipante \inv(WhoAmI)) \spot \\
\t1     ConvertiOggetto \inv (ContInformazione(contenuto?)) \notin \\
\t2     \dom KnowbotAmI.ogg\_di\_interesse ) \\
\also
	contenuto! = (ComPass,ContInformazione(contenuto?)) \\
	destinatario! = mittente?
\end{schema}

\begin{schema}{NoPassKnowbot}
	\Xi Utenti \\
	mittente?: COMUNICANTE \\
	contenuto?: CONTENUTO 
\where
	( \LET KnowbotAmI == fknowbot \inv(fpartecipante \inv(WhoAmI)) \spot \\
\t1     ConvertiOggetto \inv (ContInformazione(contenuto?)) \in \\
\t2     \dom KnowbotAmI.ogg\_di\_interesse ) \\
\end{schema}

\index{GestionePass}
\begin{zed}
	GestionePass \defs (PassKnowbot \pipe Spedisci) \lor NoPassKnowbot \\ 
\end{zed}

%  -------------------------------------------------------------------------
\subsection{Ricezione di un messaggio}
%  -------------------------------------------------------------------------

In questa sezione viene gestita la ricezione di un messaggio da parte 
di un knowbot. Il messaggio ricevuto viene utilizzato per modificare lo 
stato locale del knowbot, che in questo modo viene mantenuto 
costantemente aggiornato.

\begin{schema}{MesIllustraOggetto}
	\Delta Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE
\where
	ContTipomes(contenuto?) = IllustraOggetto \\
\also
	( \LET KnowbotAmI == fknowbot \inv(fpartecipante \inv(WhoAmI)) \spot \\
\t1     stati\_knowbots' = stati\_knowbots \oplus \{ x: StatoKnowbot | \\
\t2     x.vendita\_in\_corso = TRUE \land \\
\t2     x.oggetto\_attuale = ConvertiOggetto \inv  
(ContInformazione(contenuto?)) \land \\
\t2	x.offerta\_attuale = (x.oggetto\_attuale).prezzo\_base \land \\
\t2	x.capitale\_speso = (stati\_knowbots(KnowbotAmI)).capitale\_speso 
\land \\  
\t2     x.dati\_knowbot = ModificaDati(contenuto?) \\
\t2	\spot KnowbotAmI \mapsto x \} )
\end{schema}

\begin{schema}{MesFineVenditaOggetto}
	\Delta Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE
\where
	ContTipomes(contenuto?) \in \{ OggettoInvenduto, OggettoAggiudicato \} 
\\
\also
	( \LET KnowbotAmI == fknowbot \inv(fpartecipante \inv(WhoAmI)) \spot \\
\t1     stati\_knowbots' = stati\_knowbots \oplus \{ x: StatoKnowbot | \\
\t2     x.vendita\_in\_corso = FALSE \land \\
\t2     x.oggetto\_attuale = (stati\_knowbots(KnowbotAmI)).oggetto\_attuale 
\land \\  
\t2	x.offerta\_attuale = (stati\_knowbots(KnowbotAmI)).offerta\_attuale 
\land \\  
\t2	x.capitale\_speso = (\IF (ContTipomes(contenuto?) = 
OggettoAggiudicato \land \\
\t4	(\exists p: PREZZO \spot (knowbots \inv (KnowbotAmI),p) = \\
\t5	ConvertiDetentore \inv (ContInformazione(contenuto?)))) \\
\t3	\THEN (stati\_knowbots(KnowbotAmI)).capitale\_speso + {} \\ 
\t4	x.offerta\_attuale \\ 
\t3	\ELSE (stati\_knowbots(KnowbotAmI)).capitale\_speso) \land \\  
\t2     x.dati\_knowbot = ModificaDati(contenuto?) \\
\t2	\spot KnowbotAmI \mapsto x \} )
\end{schema}

\begin{schema}{AltriMessaggi}
	\Delta Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE
\where
	ContTipomes(contenuto?) \notin \\
\t3	\{ IllustraOggetto, OggettoInvenduto, OggettoAggiudicato \} \\
\also
	( \LET KnowbotAmI == fknowbot \inv(fpartecipante \inv(WhoAmI)) \spot \\
\t1     stati\_knowbots' = stati\_knowbots \oplus \{ x: StatoKnowbot | \\
\t2     x.vendita\_in\_corso = 
(stati\_knowbots(KnowbotAmI)).vendita\_in\_corso \land \\
\t2     x.oggetto\_attuale = (stati\_knowbots(KnowbotAmI)).oggetto\_attuale 
\land \\  
\t2	x.offerta\_attuale = (\IF ContTipomes(contenuto?) = CurrentBid \\
\t3	\THEN ( \lambda pers: PERSONA; val: PREZZO \spot \\
\t4	val ) (ConvertiDetentore \inv (ContInformazione(contenuto?))) \\
\t3	\ELSE (stati\_knowbots(KnowbotAmI)).offerta\_attuale) \land \\  
\t2	x.capitale\_speso = (stati\_knowbots(KnowbotAmI)).capitale\_speso 
\land \\  
\t2     x.dati\_knowbot = ModificaDati(contenuto?) \\
\t2	\spot KnowbotAmI \mapsto x \} )
\end{schema}

\index{DORiceviMesKnowbot}
\begin{zed}
	GestioneMessaggio \defs (MesIllustraOggetto \land GestionePass) \lor \\
\t1     MesFineVenditaOggetto \lor AltriMessaggi
\also
	RiceviMesKnowbot \defs Ricevi \pipe ((GestioneMessaggio \land 
Successo) \lor \\
\t1     NessunComando)
\also
	DORiceviMesKnowbot \defs (RiceviMesKnowbot \land SonoKnowbot) 
\lor NonSonoKnowbot
\end{zed}

%  -------------------------------------------------------------------------
\section{Operazioni del banditore}
%  -------------------------------------------------------------------------

In questa sezione sono trattate le operazioni che pu\`o effettuare il 
banditore.

%  -------------------------------------------------------------------------
\subsection{Ricezione di un comando (in qualsiasi fase)}
%  -------------------------------------------------------------------------

La ricezione di un messaggio da parte del banditore implica la gestione 
del comando richiesto dal partecipante.

%  -------------------------------------------------------------------------
\subsubsection{Subscribe}
%  -------------------------------------------------------------------------

Subscribe viene richiesto da un partecipante passivo che vuole 
partecipare attivamente all'asta. Prevede che l'utente fornisca alla 
casa d'aste le credenziali necessarie per la verifica della sua 
affidabilit\`a. 
I possibili casi di errore gestiti sono quello in cui l'utente sia gi\`a 
un partecipante attivo, e quello in cui le credenziali siano ritenute 
insufficienti. In entrambi i casi l'effetto dell'operazione \`e nullo.

\begin{schema}{SubscribeOK}
	\Delta Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE \\
\where
	ContTipomes(contenuto?) = ComSubscribe \\
	fpersona \inv (fpartecipante \inv (mittente?)) \notin 
\dom partecipanti\_attivi \\
	VerificaCredenziali(EstraiDati(ContInformazione(contenuto?))) = TRUE \\
\also
	partecipanti\_attivi' = partecipanti\_attivi \cup {} \\
\t1     \{ fpersona \inv (fpartecipante \inv(mittente?)) \mapsto {} \\
\t2     EstraiDati(ContInformazione(contenuto?)) \} \\
	destinatario! = mittente? \\
	contenuto! = (SubscribeEffettuataConSuccesso,InfoVuota)
\end{schema}

\begin{schema}{UtenteAttivo}
	\Xi Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE \\
\where
	ContTipomes (contenuto?) = ComSubscribe \\
	fpersona \inv (fpartecipante \inv (mittente?)) \in \dom 
partecipanti\_attivi \\
\also
	destinatario! = mittente? \\
	contenuto! = (UtenteGiaAttivo,InfoVuota)
\end{schema}

\begin{schema}{CredenzialiInsuff}
	\Xi Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE \\
\where
	ContTipomes(contenuto?) = ComSubscribe \\
	fpersona \inv (fpartecipante \inv (mittente?)) \notin 
\dom partecipanti\_attivi \\
	VerificaCredenziali(EstraiDati(ContInformazione(contenuto?))) = FALSE 
\\    
\also
	destinatario! = mittente? \\
	contenuto! = (CredenzialiInsufficienti,InfoVuota)
\end{schema}

\index{Subscribe}
\begin{zed}
	Subscribe \defs (SubscribeOK \lor UtenteAttivo \lor 
CredenzialiInsuff) \pipe Spedisci
\end{zed}

%  -------------------------------------------------------------------------
\subsubsection{Unsubscribe}
%  -------------------------------------------------------------------------

Unsubscribe viene richiesta da un partecipante attivo che non ha pi\`u 
intenzione di  partecipare attivamente alle contrattazioni. Questa 
operazione permette comunque di rimanere collegati al sistema come 
osservatore.
I casi di errore previsti sono quello in cui il partecipante sia gi\`a 
passivo e quello in cui il partecipante sia rappresentato da un knowbot.

\begin{schema}{UnsubscribeOK}
	\Delta Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE \\
\where
	ContTipomes(contenuto?) = ComUnsubscribe \\
	(\LET PersonaMit == fpersona \inv(fpartecipante \inv(mittente?)) \spot \\
\t1     (PersonaMit \in \dom partecipanti\_attivi) \land \\
\t1     (PersonaMit \notin \dom knowbots) \land \\
\also
\t1     (partecipanti\_attivi' = \{ PersonaMit \} \ndres 
partecipanti\_attivi) ) \\
	destinatario! = mittente? \\
	contenuto! = (UnsubscribeEffettuataConSuccesso,InfoVuota)
\end{schema}


\begin{schema}{UtenteUnsubscribed}
	\Xi Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE
\where
	ContTipomes(contenuto?) = ComUnsubscribe \\
	fpersona \inv (fpartecipante \inv(mittente?)) \notin \dom 
partecipanti\_attivi \\
\also
	destinatario! = mittente? \\
	contenuto! = (UtenteNonSubscribed,InfoVuota)
\end{schema}

\begin{schema}{UtenteKnowbot}
	\Xi Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE \\
\where
	ContTipomes(contenuto?) = ComUnsubscribe \\
	fpersona \inv (fpartecipante \inv(mittente?)) \in \dom knowbots \\
\also
	destinatario! = mittente? \\
	contenuto! = (UtenteConKnowbot,InfoVuota)
\end{schema}    

\index{UnSubscribe}
\begin{zed}
	Unsubscribe \defs (UnsubscribeOK \lor UtenteUnsubscribed \lor 
UtenteKnowbot) \pipe \\
\t1	Spedisci
\end{zed} 

%  -------------------------------------------------------------------------
\subsubsection{RichiestaPAttivi}
%  -------------------------------------------------------------------------

Qualsiasi partecipante umano collegato, in ogni momento pu\`o richiedere una 
lista dei partecipanti attivi. Il banditore, ricevuta la richiesta del 
partecipante, invia un messaggio contenente l'insieme delle persone che 
partecipano attivamente (anche tramite knowbot). Se siamo durante la fase 
AstaInCorso da tale lista vengono eliminati i partecipanti attivi che 
hanno fatto pass per l'oggetto corrente.

\begin{schema}{RichiestaPAttiviOK}
	\Xi Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE \\
\where
	ContTipomes(contenuto?) = ComRichiestaPAttivi \\
\also
	destinatario! = mittente? \\
	contenuto! = (ListaPAttivi,ConvertiListaPAttivi(\dom  
partecipanti\_attivi \setminus {} \\ 
\t1	IndividuaPersona \limg \{ x:PARTECIPANTE | x \in pass \spot 
(x,knowbots) \} \rimg)) 
\end{schema}    

\index{RichiestaPAttivi}
\begin{zed}
	RichiestaPAttivi \defs RichiestaPAttiviOK \pipe Spedisci
\end{zed}

%  -------------------------------------------------------------------------
\subsubsection{Pass}
%  -------------------------------------------------------------------------

Quando il banditore riceve il comando $Pass$ da parte di un 
partecipante attivo, lo inserisce nell'insieme degli utenti non 
interessati all'acquisto  dell'oggetto corrente. L'effetto di questo 
comando \`e di bloccare la possibilit\`a di rilancio agli utenti che lo 
hanno attivato.
Tale effetto decade quando terminano le contrattazioni per l'oggetto 
corrente. 
Il $Pass$ viene respinto quando a richiederlo \`e un partecipante 
passivo, oppure quando si riferisce ad un oggetto diverso da quello 
corrente. \`E previsto, inoltre, un messaggio di errore apposito qualora 
venga richiesto in una fase dell'asta diversa da AstaInCorso.

\begin{schema}{PassOK}
	\Xi Asta \\
	\Delta Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE \\
\where
	ContTipomes(contenuto?) = ComPass \\
	fase = AstaInCorso \\
	(fpartecipante \inv(mittente?) \in \ran fknowbot) \lor \\
\t1     (fpersona \inv (fpartecipante \inv (mittente?)) \in \\
\t2	(\dom partecipanti\_attivi \setminus \dom knowbots)) \\
	ConvertiOggetto \inv (ContInformazione(contenuto?)) = \\
\t1	lista\_oggetti(oggetto\_in\_vendita) 
\also
	pass' = pass \cup \{ fpartecipante \inv(mittente?) \} \\
	destinatario! = mittente? \\
	contenuto! = (RilanciSospesiPerOggettoInVendita,InfoVuota)
\end{schema}

\begin{schema}{PassRespinto}
	\Xi Asta \\
	\Xi Utenti \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE 
\where
	ContTipomes(contenuto?) = ComPass \\
	fase = AstaInCorso \\
	(fpartecipante \inv(mittente?) \in \ran fpersona) \land \\
\t2     (fpersona \inv (fpartecipante \inv (mittente?)) \notin \\
\t3	(\dom partecipanti\_attivi \setminus \dom knowbots)) \lor \\
\t1	ConvertiOggetto \inv (ContInformazione(contenuto?)) \neq \\
\t2	lista\_oggetti(oggetto\_in\_vendita) 
\also
	destinatario! = mittente? \\
	contenuto! = (PassRifiutato,InfoVuota)
\end{schema}

\begin{schema}{FaseErrata}
	\Xi Asta \\
	contenuto?: CONTENUTO \\
	mittente?: COMUNICANTE \\
	contenuto!: CONTENUTO \\
	destinatario!: COMUNICANTE 
\where
	ContTipomes(contenuto?) = ComPass \\
	fase \neq AstaInCorso \\
\also
	destinatario! = mittente? \\
	contenuto! = (NoFaseAstaInCorso,InfoVuota)
\end{schema}

\index{Pass}
\begin{zed}
	Pass \defs (PassOK \lor PassRespinto \lor FaseErrata) \pipe Spedisci
\end{zed}


%  -------------------------------------------------------------------------
\subsubsection{Rilancio}
%  -------------------------------------------------------------------------
	
Quando il banditore riceve un comando di rilancio controlla la 
validit\`a dell'offerta. L'offerente non pu\`o essere un partecipante 
passivo e non pu\`o fare parte degli utenti che hanno fatto pass 
sull'oggetto attualmente in vendita. Si controlla, inoltre, che il 
rilancio non si riferisca ad un oggetto diverso da quello corrente. 
Si ha poi che: il rilancio deve essere inferiore al limite imposto dal fido 
dell'offerente e maggiore o uguale alla current bid pi\`u il rilancio minimo 
per l'oggetto. I rilanci che non rispettano queste caratteristiche vengono 
semplicemente ignorati. 

\begin{schema}{RilancioOK}
	\Delta Asta \\
	\Xi Utenti \\
	mittente?: COMUNICANTE \\
	contenuto?: CONTENUTO \\
	contenuto!: CONTENUTO 
\where
	ContTipomes(contenuto?) = ComRilancio \\
	fase = AstaInCorso \\
	(fpartecipante \inv(mittente?) \in \ran fknowbot) \lor \\
\t1     (fpersona \inv (fpartecipante \inv (mittente?)) \in \\
\t2	(\dom partecipanti\_attivi \setminus \dom knowbots)) \\
	fpartecipante \inv(mittente?) \notin pass \\
	lista\_oggetti(oggetto\_in\_vendita) = (\lambda ogg: Oggetto; val: PREZZO 
\spot \\
\t1	ogg)(ConvertiRilancio \inv(ContInformazione(contenuto?))) \\
	( \LET Offerta == (\lambda ogg: Oggetto; val: PREZZO \spot \\
\t2	val)(ConvertiRilancio \inv(ContInformazione(contenuto?))) \spot \\
\t1	Offerta \geq current\_bid + (lista\_oggetti(oggetto\_in\_vendita)).
incremento\_min \land \\
\t1	( \LET Titolare == IndividuaPersona (fpartecipante \inv (mittente?),
knowbots) \spot \\
\t2	(partecipanti\_attivi(Titolare)).fido \geq Offerta \land \\
\also
\t2	current\_bid' = Offerta \land \\ 
\t2	detentore\_CB' = fpartecipante \inv (mittente?) \land \\
\t2	dati\_detentore' = (partecipanti\_attivi(Titolare)).dati\_accredito 
\land \\
\t2	contenuto! = (CurrentBid,ConvertiDetentore(Titolare,current\_bid')) ) )
\end{schema}

\begin{schema}{IgnoraRilancio}
	\Xi Asta \\
	\Xi Utenti \\
	mittente?: COMUNICANTE \\
	contenuto?: CONTENUTO 
\where
	ContTipomes(contenuto?) = ComRilancio \\
	fase \neq AstaInCorso \lor \\
\t1	((fpartecipante \inv(mittente?) \in \ran fpersona) \land \\
\t2     (fpersona \inv (fpartecipante \inv (mittente?)) \notin \\
\t3	(\dom partecipanti\_attivi \setminus \dom knowbots))) \lor \\
\t1     fpartecipante \inv(mittente?) \in pass \lor \\
\t1	lista\_oggetti(oggetto\_in\_vendita) \neq (\lambda ogg: Oggetto; val: 
PREZZO \spot \\
\t2	ogg)(ConvertiRilancio \inv(ContInformazione(contenuto?))) \lor \\
\t1	( \LET Offerta == (\lambda ogg: Oggetto; val: PREZZO \spot \\
\t3	val)(ConvertiRilancio \inv(ContInformazione(contenuto?))) \spot \\
\t2     Offerta < current\_bid + {} \\
\t3	(lista\_oggetti(oggetto\_in\_vendita)).incremento\_min \lor \\
\t2	( \LET Titolare == \\
\t4	IndividuaPersona (fpartecipante \inv (mittente?),knowbots) \spot \\
\t3     (partecipanti\_attivi(Titolare)).fido < Offerta ) )
\end{schema}

\index{Rilancio}
\begin{zed}
	Rilancio \defs (RilancioOK \pipe Broadcast) \lor IgnoraRilancio
\end{zed}

%  -------------------------------------------------------------------------
\subsubsection{Ricezione comando}
%  -------------------------------------------------------------------------

\index{DORiceviComando}
\begin{zed}
	RiceviComando \defs Ricevi \pipe (((Subscribe \lor Unsubscribe 
\lor RichiestaPAttivi \lor \\
\t1     Pass \lor Rilancio) \land Successo) \lor NessunComando)
\also
	DORiceviComando \defs (RiceviComando \land SonoBanditore) \lor 
NonSonoBanditore
\end{zed} 

%  -------------------------------------------------------------------------
\subsection{Operazioni eseguibili in fase AstaNonInCorso}
%  -------------------------------------------------------------------------

$NoAstaNonInCorso$ \`e uno schema di controllo che verifica il caso di 
errore in cui le operazioni vengano eseguite in una fase diversa da 
$AstaNonInCorso$.

\begin{schema}{NoAstaNonInCorso}
	\Xi Asta \\
	rep! : REPORT 
\where
	fase \neq AstaNonInCorso \\
\also
	rep! = Fase\_non\_corretta
\end{schema}

%  -------------------------------------------------------------------------
\subsubsection{Inizio Asta}
%  -------------------------------------------------------------------------

Di seguito vengono definiti gli schemi corrispondenti alle operazioni 
preliminari all'inizio dell'asta. Esse prevedono l'inserimento della 
lista di oggetti messi in vendita, l'istruzione e l'attivazione di 
eventuali rappresentanti software sia per i partecipanti che per il 
banditore. Lo schema InfoKnowbots descrive il tipo dei dati 
utilizziati per l'istruzione dei knowbot, e la costante StatoInizialeKnowbot
rappresenta il valore a cui sono inizializzati gli stati dei knowbot.
Al momento dell'attivazione dei knowbot, vengono esclusi quelli che
rappresentano un utente che ha gia fatto $Subscribe$. Lo schema 
InfoBanditore descrive il tipo dei dati utilizzati per l'inserimento 
delle informazioni riguardanti il banditore. Lo schema $CambioFase$ 
rappresenta l'inizio effettivo dell'asta.

\begin{schema}{InserimentoOggetti}
	\Delta Asta \\
	lista?: LISTAOGGETTI
\where
	lista\_oggetti' = lista? \\
	oggetto\_in\_vendita' = 0 \\
	oggetti\_venduti' = \emptyset 
\end{schema}

\begin{axdef}
	DatiIniziali: DATIRILANCIO
\end{axdef}

\begin{axdef}
	StatoInizialeKnowbot: StatoKnowbot
\where
	StatoInizialeKnowbot.vendita\_in\_corso = FALSE \\
	StatoInizialeKnowbot.capitale\_speso = 0 \\
	StatoInizialeKnowbot.dati\_knowbot = DatiIniziali
\end{axdef}

\begin{schema}{InfoKnowbots}
	proprietario: PERSONA \pinj Knowbot \\
	dati\_persona: PERSONA \pfun DatiPartecipante
\where
	\dom proprietario = \dom dati\_persona \\
	\forall x:PERSONA | x \in \dom proprietario \spot \\
\t1     (proprietario(x)).capitale\_totale \leq 
(dati\_persona(x)).fido \\
\end{schema}

\begin{schema}{IstruzioneKnowbots}
	\Delta Utenti \\
	dati\_knowbots?: InfoKnowbots
\where
	knowbots' = \dom partecipanti\_attivi \ndres
dati\_knowbots?.proprietario \\
	collegati' = collegati \cup fknowbot \limg \ran knowbots' \rimg \\
	partecipanti\_attivi' = partecipanti\_attivi \cup {} \\
\t1	( \dom partecipanti\_attivi \ndres dati\_knowbots?.dati\_persona ) \\
	stati\_knowbots' = \{ x: Knowbot | x \in \ran knowbots' \spot x \mapsto 
StatoInizialeKnowbot \} 
\end{schema}

\begin{schema}{InfoBanditore}
	band\_umano: BOOL \\
	funz\_banditore: PARAMETRIDEC \pfun DECISIONE
\where
	(funz\_banditore = \emptyset \land band\_umano = TRUE) \lor \\
\t1	(FineContrattazione \in \ran funz\_banditore \land band\_umano 
= FALSE) 
\end{schema}

\begin{schema}{IstruzioneBanditore}
	\Delta Asta \\
	dati\_banditore?: InfoBanditore 
\where
	banditore\_umano' = dati\_banditore?.band\_umano \\
	politica\_banditore' = dati\_banditore?.funz\_banditore
\end{schema}

\begin{schema}{CambioFase}
	\Delta Asta
\where
	fase = AstaNonInCorso \\
\also
	fase' = AstaFerma
\end{schema}

\index{DOInizioAsta}
\begin{zed}
	InizioAsta \defs ((InserimentoOggetti \land IstruzioneKnowbots 
\land IstruzioneBanditore \land \\
\t1	CambioFase) \land Successo) \lor NoAstaNonInCorso
\also
	DOInizioAsta \defs (InizioAsta \land SonoBanditore) \lor 
NonSonoBanditore
\end{zed}

%  -------------------------------------------------------------------------
\subsection{Operazioni eseguibili in fase AstaFerma}
%  -------------------------------------------------------------------------

$NoAstaFerma$ \`e uno schema di controllo che verifica il caso di 
errore in cui le operazioni vengono eseguite in una fase diversa da 
$AstaFerma$.

\begin{schema}{NoAstaFerma}
	\Xi Asta \\
	rep! : REPORT 
\where
	fase \neq AstaFerma \\
\also
	rep! = Fase\_non\_corretta
\end{schema}

%  -------------------------------------------------------------------------
\subsubsection{Contrattazione dell'oggetto successivo}
%  -------------------------------------------------------------------------

Terminata la contrattazione di un oggetto, il banditore passa alla 
messa all'asta dell'oggetto successivo ($NuovoOggetto$), se ve n'\`e 
uno, o dichiara conclusa l'asta ($FineAsta$). In quest'ultimo caso 
vengono disattivati tutti i knowbots e viene fatto un unsubscribe 
implicito per tutte le persone attive.
Il banditore, in entrambi i casi, comunica la decisione a tutti i 
partecipanti, inviando le informazioni sul nuovo oggetto nel primo caso 
e il messaggio di $AstaConclusa$ nel secondo. La informazione da inviare 
viene decisa nello schema $CreaMessaggio$.


\begin{schema}{NuovoOggetto}
	\Delta Asta \\
	\Delta Utenti \\
\where
	fase = AstaFerma \\
	oggetto\_in\_vendita < \# lista\_oggetti \\
\also
	fase' = AstaInCorso \\
	oggetto\_in\_vendita' = oggetto\_in\_vendita + 1 \\
	current\_bid' = (lista\_oggetti(oggetto\_in\_vendita')).prezzo\_base
\end{schema}

\begin{schema}{FineAsta}
	\Delta Asta \\
	\Delta Utenti \\
	\Delta Comunicazione \\
\where
	fase = AstaFerma \\
	oggetto\_in\_vendita = \# lista\_oggetti \\
\also
	fase' = AstaNonInCorso \\
	partecipanti\_attivi' = \emptyset \\
	knowbots' = \emptyset \\
	collegati' = collegati \setminus fknowbot \limg \ran knowbots 
\rimg \\
	mailbox' = mailbox \filter \{ mit, des: COMUNICANTE; c: CONTENUTO | \\
\t1	mit \in fpartecipante \limg collegati' \rimg \land des \in 
fpartecipante \limg collegati' \rimg \spot (mit, des, c) \} \\
	stati\_knowbots'= \emptyset \\
\end{schema}

\begin{schema}{CreaMessaggio}
	\Xi Asta \\
	contenuto! : CONTENUTO
\where
	contenuto! = \IF (oggetto\_in\_vendita < \# lista\_oggetti) \\
\t1	\THEN (IllustraOggetto, 
ConvertiOggetto(lista\_oggetti(oggetto\_in\_vendita))) \\
\t1	\ELSE (AstaConclusa,InfoVuota)
\end{schema}

\index{DOContrattazioneSuccessiva}
\begin{zed}
	ContrattazioneSuccessiva \defs (((NuovoOggetto \lor FineAsta) \semi 
(CreaMessaggio \\
\t1	\pipe Broadcast)) \land Successo) \lor NoAstaFerma 
\also
	DOContrattazioneSuccessiva \defs (ContrattazioneSuccessiva \land 
SonoBanditore) \lor \\
\t1	NonSonoBanditore 
\end{zed}

%  -------------------------------------------------------------------------
\subsection{Operazioni eseguibili in fase AstaInCorso}
%  -------------------------------------------------------------------------

$NoAstaInCorso$ \`e uno schema di controllo che verifica il caso di 
errore in cui le operazioni vengano eseguite in una fase diversa da 
$AstaInCorso$.

\begin{schema}{NoAstaInCorso}
	\Xi Asta \\
	rep! : REPORT 
\where
	fase \neq AstaInCorso \\
\also
	rep! = Fase\_non\_corretta
\end{schema}

%  -------------------------------------------------------------------------
\subsubsection{Fine contrattazione di un oggetto}
%  -------------------------------------------------------------------------

La terminazione della contrattazione di un oggetto \`e arbitrariamente 
decisa dal banditore umano. Nel caso in cui quest'ultimo sia automatico,
tale decisione \`e la conseguenza dell'applicazione della funzione che ne
descrive la politica.
Il banditore comunica a tutti i partecipanti il risultato della 
vendita e l'acquirente con il relativo prezzo 
di vendita, se l'oggetto \`e venduto.
All'eventuale acquirente (nel caso di Knowbot, alla persona che esso 
rappresenta) vengono anche comunicate le modalit\`a di pagamento e consegna 
dell'oggetto acquistato se egli risulta collegato. In caso contrario 
viene attivata una procedura di invio fuori linea (posta elettronica).

\begin{schema}{FineContrattOggettoOK}
	\Delta Utenti \\
	\Delta Asta \\
	contenuto!: CONTENUTO 
\where
	fase = AstaInCorso \\
	banditore\_umano = TRUE \lor \\
\t1	(CalcoloParametri \in \dom politica\_banditore \land \\
\t2     politica\_banditore(CalcoloParametri) = FineContrattazione) \\
\also
	fase' = AstaFerma \\
	pass' = \emptyset \\
	(current\_bid \neq (lista\_oggetti(oggetto\_in\_vendita)).
prezzo\_base \implies \\
\t1	(\LET DetCB == IndividuaPersona(detentore\_CB,knowbots) \spot \\
\t2	partecipanti\_attivi' = (\IF (DetCB \in \dom partecipanti\_attivi) \\
\t3	\THEN partecipanti\_attivi \oplus \{ x: DatiPartecipante | \\
\t4	x.fido = (partecipanti\_attivi(DetCB)).fido - current\_bid \land \\
\t4	x.dati\_accredito = (partecipanti\_attivi(DetCB)).dati\_accredito \\
\t4	\spot DetCB \mapsto x \} \\
\t3	\ELSE partecipanti\_attivi) \land\\
\t2	oggetti\_venduti' = oggetti\_venduti \cup {} \\ 
\t3	\{ lista\_oggetti(oggetto\_in\_vendita) \mapsto 
(DetCB,dati\_detentore,current\_bid) \} \land \\ 
\t2     contenuto! = \\
\t3	(OggettoAggiudicato, ConvertiDetentore (DetCB,current\_bid)) ) ) \land \\
	(current\_bid = (lista\_oggetti(oggetto\_in\_vendita)).
prezzo\_base \implies \\
\t1	partecipanti\_attivi' = partecipanti\_attivi \land \\
\t1     oggetti\_venduti' =oggetti\_venduti \land \\
\t1     contenuto! = (OggettoInvenduto,InfoVuota) ) 
\end{schema}

\begin{schema}{NoFineContrattazione}
	\Xi Asta \\
	rep!: REPORT
\where
	fase = AstaInCorso \\
	banditore\_umano = FALSE \\
	(CalcoloParametri \notin \dom politica\_banditore \lor \\
\t1	politica\_banditore(CalcoloParametri) \neq FineContrattazione) \\
\also
	rep! = Contrattazione\_non\_terminata
\end{schema}

\begin{schema}{ModalitaOK}
	\Xi Utenti \\
	\Xi Asta \\
	destinatario!: COMUNICANTE \\
	contenuto!: CONTENUTO
\where
	current\_bid \neq (lista\_oggetti(oggetto\_in\_vendita)).prezzo\_base \\
	fpersona (IndividuaPersona(detentore\_CB,knowbots)) \in collegati
\\
\also
	destinatario! = \\
\t1	fpartecipante(fpersona(IndividuaPersona(detentore\_CB,knowbots))) \\
	contenuto! = (ModalitaConsegnaPagamento, \\
\t1	CreaModalita(lista\_oggetti(oggetto\_in\_vendita),current\_bid))
\end{schema}

\begin{axdef}
	mail: (CONTENUTO \cross PERSONA) \fun BOOL
\where
	\forall x: (CONTENUTO \cross PERSONA) \spot mail(x) = TRUE
\end{axdef}

\begin{schema}{MailModalita}
	\Xi Utenti \\
	\Xi Asta 
\where
	current\_bid \neq (lista\_oggetti(oggetto\_in\_vendita)).prezzo\_base \\
	fpersona (IndividuaPersona(detentore\_CB,knowbots)) \notin 
collegati \\
\also
	mail((ModalitaConsegnaPagamento, \\
\t2	CreaModalita(lista\_oggetti(oggetto\_in\_vendita),current\_bid)), \\
\t1	IndividuaPersona(detentore\_CB,knowbots)) = TRUE 
\end{schema}
    
\begin{schema}{AstaDeserta}
	\Xi Asta \\
\where
	current\_bid = (lista\_oggetti(oggetto\_in\_vendita)).prezzo\_base \\
\end{schema}

\begin{zed}
	InvioModalita \defs (ModalitaOK \pipe Spedisci) \lor MailModalita 
\lor AstaDeserta 
\end{zed}

\index{DOFineContrattOggetto}
\begin{zed}
	FineContrattOggetto \defs (((FineContrattOggettoOK \pipe Broadcast) 
\semi \\
\t1     InvioModalita) \land Successo) \lor NoFineContrattazione \lor 
NoAstaInCorso 
\also
	DOFineContrattOggetto \defs (FineContrattOggetto \land SonoBanditore)
\lor \\
\t1     NonSonoBanditore
\end{zed}

%  -------------------------------------------------------------------------
\subsubsection{Invio Expiring Time}
%  -------------------------------------------------------------------------

Il banditore al fine di stimolare il rilancio da parte dei partecipanti , 
pu\`o inviare dei messaggi di expiring time (anche pi\`u di uno per uno 
stesso oggetto). Nel caso in cui il banditore sia umano tale decisione 
viene presa in modo arbitrario dallo stesso, mentre se il banditore \`e 
automatico la decisione \`e restituita dalla funzione che definisce la 
politica del banditore

\begin{schema}{ExpiringTimeOK}
	\Xi Asta \\
	contenuto!: CONTENUTO
\where       
	fase = AstaInCorso \\
	(banditore\_umano = TRUE) \lor \\
\t1	(CalcoloParametri \in \dom politica\_banditore \land \\
\t2     (politica\_banditore(CalcoloParametri) = MessaggioExpiringTime)) \\
\also
	contenuto! = (IlTempoStaPerScadere,InfoVuota)
\end{schema}

\begin{schema}{NoExpiringTime}
	\Xi Asta \\
	rep! : REPORT
\where       
	fase = AstaInCorso \\
	banditore\_umano = FALSE \\
	(CalcoloParametri \notin \dom politica\_banditore \lor \\
\t1	politica\_banditore(CalcoloParametri) \neq MessaggioExpiringTime) \\
\also
	rep! = Expiring\_time\_non\_inviato
\end{schema}

\index{DOInviaExpiringTime}
\begin{zed}
	InviaExpiringTime \defs ((ExpiringTimeOK \pipe Broadcast) \land 
Successo) \lor \\ 
\t1 NoExpiringTime \lor NoAstaInCorso
\also
	DOInviaExpiringTime \defs (InviaExpiringTime \land SonoBanditore) 
\lor \\
\t1     NonSonoBanditore
\end{zed}

%  -------------------------------------------------------------------------
\section{Dimostrazioni}
%  -------------------------------------------------------------------------

Dimostriamo il seguente invariante dello stato $Utenti$ 
(Sezione~\ref{statopart}) che afferma
che tutti i partecipanti attivi che interagiscono personalmente (non 
tramite knowbot) devono essere collegati :

\begin{argue}
        \dom partecipanti\_attivi \setminus \dom knowbots \subseteq
        fpersona \inv \limg collegati \rimg \\
\end{argue}

Lo schema di inizializzazione dello stato pone sia i collegati
che i partecipanti attivi al vuoto quindi la propriet\`a risulta 
banalmente vera.

Gli schemi che modificano il $\dom partecipanti\_attivi$ per la parte 
che riguarda i partecipanti che non interagiscono tramite knowbot sono
lo schema $Subscribe$, lo schema $Unsubscribe$ e l'operazione di
$ChiudiCollegamento$ nel caso in cui il partecipante sia attivo
(Unsubscribe implicito)

\bigskip
Per quanto riguarda $Subscribe$ si considera solo il caso in cui tale
comando ha successo (altrimenti lo stato rimane invariato). Si noti che
tale comando pu\`o essere inviato solamente da una persona collegata;
infatti tale invio pu\`o essere effettuato solamente con l'operazione 
$DOInviaComando$ (Sezione~\ref{inviocom}) 
che controlla che la persona che lo esegue sia 
collegata.

\begin{argue}
	fpartecipante \inv (mittente?) \in collegati \\
\also
	collegati'=collegati \\
\also
	(\dom partecipanti\_attivi' \setminus \dom knowbots') = ((\dom 
partecipanti\_attivi \setminus \dom knowbots) \cup {} \\
\t1 \{ fpersona \inv ( fpartecipante \inv (mittente?)) \} )
\end{argue}

Per ipotesi induttiva l'invariante risulta valido.

\bigskip
Per quanto riguarda $Unsubscribe$, anche in questo caso si considera solo il 
caso in cui tale comando ha successo (altrimenti lo stato rimane invariato).

\begin{argue}
	collegati'=collegati \\
\also
	(\dom partecipanti\_attivi' \setminus \dom knowbots') \subset (\dom 
partecipanti\_attivi \setminus \dom knowbots) \\
\end{argue}

Per ipotesi induttiva l'invariante risulta valido.

\bigskip
La operazione $ChiudiCollegamento$ (considerata solo nel caso di 
successo) attua una Unsubscribe implicita se la persona e un partecipante 
attivo (non tramite knowbot).
Consideriamo quindi questo caso:

\begin{argue}
	collegati'=collegati \setminus fpartecipante \inv (WhoAmI) \\
\also
	(\dom partecipanti\_attivi' \setminus \dom knowbots') = ((\dom 
partecipanti\_attivi \setminus \dom knowbots) \setminus {} \\
\t1	\{ fpersona \inv ( fpartecipante \inv (WhoAmI)) \} )  
\end{argue}

Per ipotesi induttiva l'invariante risulta valido.

%\end{document}


