Esercitazione I.S. II
a.a. 2001/2002
Un Nuovo Frame
Chiara Casanova
Massimo Ruffa
1
Descrizione del Frame
• Utile per la Automazione di un Business
• Idea intuitiva per una classe di problemi
parte del mondo fisico la cui automazione è controllata da operatori
che posso essere identificati in
• usufruitori del business ( Users )
• gestori del Business
Il problema è costruire un sistema software che accetti i comandi
degli operatori e li esegua in accordo con i requisiti e la business
logic
2
Descrizione del frame 1/7
Maggiori dettagli sui propositi del Frame
Il concetto di Automazione modella la necessità di eliminare dal
Domain delle entità reali e concettualizzarle all’ interno della
software application ( System ) presente nel design.
Per migliorare la comprensione sopraeleviamo il Design e
proiettiamo la sua ombra sul Domain evidenziando le entità
che vengono automatizzate.
L’ attenzione deve essere rivolta a due aspetti in particolare :
1. Nel normale Commanded Behaviour le entità presenti nel
dominio vengono considerate come preesistenti rispetto
all’inizio del funzionamento del sistema e comunicano con la
machine tramite eventi. Ora tutte quelle automatizzate sono
create dal system quindi presenti nella realtà digitale solo
dopo la messa in opera del system
2. Le comunicazioni tra le entità “automatized” ed il system
non avvengono più nel modo esterno-interno tipico del
Commanded Behaviour ma ( sempre che avvengano )
3
interno-interno
Descrizione del frame 2/7
Presentazione del Frame
Design
System
Domain ( Business Model )
User
…
Provider
…
Generic
…
boundaries
bound
Automatized
…
Requirement
Commanded
Behaviour
4
Descrizione del frame 3/7
Presentazione del Frame
Design
System
Domain ( Business Model )
S_Act
U_Req
S_Resp
User
P_Resp
*
S_Req.
Provider
boundaries
bound
Generic
…
Automatized
…
Requirement
Commanded
Behaviour
5
Descrizione del frame 4/7
Entità costituenti il Domain
• User
– utenti del sistema
• Provider
– fornitori di servizi al sistema
• Generic
– presenti concettualmente nel dominio ma non sono
direttamente coinvolte dal system
• Automatized
– “pezzi” di realtà simulati/sostituiti dal sistema
6
Descrizione del frame 5/7
Comunicazioni
• P_Resp
– Risposte che i provider forniscono al sistema
• U_Req
– Richieste che gli user rivolgono al sistema
• S_Resp
– Risposte che il sistema fornisce agli user
• S_Req
– Richieste che il sistema rivolge ai provider ( per soddisfare
richieste di user )
• S_Act
– Messaggi/comunicazioni che il sistema invia/instaura a seguito
di computazioni/eventi interni o di sua iniziativa.
– Possono essere conseguenza dell’ automazione di entità attive
del domain che non devono perdere del tutto la propria
autonomia decisionale una volta incorporate dall’ applicazione
( vicino al concetto di agente )
• NOTA
– la linea tratteggiata * evidenzia le comunicazioni fittizie tra
sistema e entità automatizzate ( racchiuse nel bound )
7
Descrizione del frame 6/7
Approfondimento : Business Logic
• Per rendere il frame più application-oriented si deve
descrivere la logica del business ovvero le
caratteristiche/vincoli che regolano la business application
• Include proprietà specifiche delle entità del Domain
Design
System
Domain ( Business Model )
S_Act
U_Req
S_Resp
User
P_Resp
*
S_Req.
Provider
boundaries
bound
Generic
…
Business
Logic
Automatized
…
8
Descrizione del frame 7/7
Applicazione del metodo
Formally Grounded Development
all’Automation Frame
Sistema Dinamico strutturato
Design
System
Domain ( Business Model )
S_Act
U_Req
S_Resp
P_Resp
S_Req.
*
Generic
…
User
Provider
boundaries
bound
Automatized
…
Requirement
Commanded
Behaviour
Business
Logic
Proprietà sul sistema dinamico strutturato
9
Domain : Specification
• Tecnicamente occorre lavorare sul Domain in due fasi che
producono due sitemi strutturati differenti
– nella prima si evidenziano le entità che concettualmente concorrono
alla creazione del sistema. Alcune entità ( User e Provider ) sono
fisicamente reali e tali rimarranno, altre ( Automatized ) sono
fisicamente reali ma verranno sostituite dalla loro copia virtuale
– la seconda fase esplicita la sostituzione mostrando il system
composto dalla sua parte naturale e da quella virtualizzata in
comunicazione con le restanti entità nel Domain
• A questo livello la seconda fase serve solo per identificare i
sottosistemi semplici che comporranno il sistema strutturato sul
quale si daranno i requisiti
10
Domain Specification 1/5
Torna a pag 19
Domain Specification : primo sistema strutturato
( prima fase )
• È un sistema dinamico strutturato (sds) chiuso (ovvero non vi
sono interazioni con il mondo esterno ) pertanto le etichette delle
sue transizioni saranno sempre l’insieme vuoto di interazioni
elementari e devono essere cancellate le parti riguardanti le
interazioni elementari nella specifica dell’sds
• Il sistema strutturato descritto è formato da sistemi semplici (user,
provider, automatized e generic)
• Le proprietà sull’ sds costituiscono la business logic
User
…
Provider
…
Generic
…
boundaries
bound
Automatized
…
11
Domain Specification 2/5
Torna a pag 19
Domain Specification : secondo sistema strutturato
( seconda fase )
• È un sistema dinamico strutturato (sds) chiuso
• Le proprietà addizionali sull’ sds costituiscono i requisiti,
quindi il commanded behaviour
System
S_Act
U_Req
S_Resp
User
P_Resp
S_Req.
Provider
INTERAZIONI ELEMENTARI LOCALI
12
Domain Specification 3/5
Le Ei dei sottosistemi sono suddivise in 5 categorie:
– S_Resp
• Interazioni elementari corrispondenti a una comunicazione
unidirezionale tra il sistema e gli User, a seguito di una richiesta di
quest’ultimi
– S_Req
• Interazioni elementari corrispondenti a una richiesta di servizio da
parte del sistema nei confronti dei Provider
– P_Resp
• Interazioni elementari corrispondenti a una comunicazione
unidirezionale tra i Provider e il sistema, a seguito di una richiesta
di quest’ultimo
– U_Req
• Interazioni elementari corrispondenti a una richiesta da parte degli
User nei confronti del sistema
– S_Act
• Interazioni elementari corrispondenti alle comunicazioni
unidirezionali che il sistema trasmette agli User
13
Domain Specification 4/5
I sottosistemi cooperano soltanto effettuando simultaneamente le
interazioni condivise. Quindi le proprietà di sincronizzazione tra le
diverse Ei locali sono standard e non dipendono dal caso particolare.
Lo stesso vale per le proprietà di Local Versus Global (nel nostro caso
non presenti).
Possono inoltre essere presenti osservatori di stato all’interno dei
sottosistemi. Nel caso ci siano sarà quindi necessario fornire le
proprietà su questi come specificato dal metodo FGD.
14
Domain Specification 5/5
Requirement : Specification
• I requisiti ( Desidered Behaviour) riguardano il sistema
strutturato sottostante
• Proprietà circa
– Entità automatizzate attive
– Interazioni elementari
System
S_Act
U_Req
S_Resp
User
P_Resp
S_Req.
Provider
15
Requirement Specification 1/2
• Le proprietà circa i tipi di EI individuati
– S_Resp
• Pre-condition / Vitality / Incompatibility
– S_Req
• Pre-condition / Post-condition / Vitality / Incompatibility
– P_Resp
• Pre-condition / Post-condition / Incompatibility / Vitality
– U_Req
• Pre-condition / Post-condition / Incompatibility / Vitality
– S_Act
• Pre-condition / Post-condition / Incompatibility / Vitality
• Notare
– Il system è Event Driven
• gli user effettuano richieste, alla sollecitazione il system
risponde
• Il system effettua rechieste ai provider, alla sollecitazione i
provider rispondono
• Eccezione fanno le S_Act
16
Requirement Specification 2/2
Istanziazione del frame:
Lotteria Algebrica
L-AL
1
2
3
4
Notaio
(**)
5
Utente
Gestore Accessi
Posta Elettronica
Gestore CC
Biglietto, Legge
Ordinamento
Direttore
(*)
Commanded
Behaviour
Business
Logic
17
Istanziazione 1/2
Elenco delle comunicazioni
1.
Registrami, Collegami, Scollegami, Cancellami,
AcquistaBil, BigliettiDisponibili
2.
Registrato, Collegato, Scollegato, Cancellato,,
BilAcquistato, SonoDisponibili
3.
ControllatoU, CancellatoU, ControllataC, Addebitato
4.
RegistraU, ControllaU, CancellaU, ControllaC, Addebita,
Manda
5.
IniziaNuovaLotteria, Estrai, Vincitori,
DistribuisciBilOmaggio
18
Istanziazione 2/2
FGM applicato all’ istanziazione del Frame
• L’ FGM viene utilizzato due volte corrispondenti ai due sistemi
strutturati individuati nella descrizione del Domain Specification
– Prima fase -> Primo sistema strutturato
– Seconda fase -> Secondo sistema strutturato
• Entità
– in entrambe ogni entità rappresenta un sistema semplice
• Interazioni Elementari
– Primo sistema : non sono esplicitate nel frame
– Secondo sistema : sono esattamente le comunicazioni che avvengono
tra le entità
19
FGM applicato alla prima fase
Sottosistemi individuati nel sistema strutturato della prima fase
D:Direttore
?
?
?
?
?
Vincitori : _ -> Sequence(Utenti)
Inizia_Lotteria: Ordinamento x Legge x Nat
Distribuisci_BilOmaggio: Nat
Estrai : Manda: String x String
L:Lotteria
Dim: Nat
Assegnati: Set(Int)
!
!
!
!
Vincitori:Sequence(Utenti)
Inizia_Lotteria: Ordinamento x Legge x Nat
Distribuisci_BilOmaggio: Nat
Estrai
Nota:
? Indica che e’ una richiesta (in Uscita)
! Una risposta (in Entrata)
U:Utente
Dati: DatiP
Carta: DatiC
BilOmaggio: Nat
? Cancellami: DatiP
? Registrami: DatiP x DatiC
? Collegami: DatiP
? Scollegami: DatiP
? Addebito: DatiP x DatiC x Int x Nat x Bool
! Collegato: DatiP x Bool
! Cancellato: DatiP x Bool
! Scollegato: DatiP x Bool
! Registrato: DatiP x DatiC x Bool
! AcquistaBil: DatiP x DatiC x Int
20
Applicazione FGM : prima fase 1/19
Gcc:Gestore CartaCredito
? Controllo_DatiC: DatiP x DatiC x Bool
? Addebito: DatiP x DatiC x Int x Nat x Bool
! RegistraC: DatiC x DatiP
! AcquistaBil: DatiP x DatiC x Int
Pt:Posta Elettronica
! Manda: String x String
Nota:
? Indica che e’ una richiesta (in Uscita)
! Una risposta (in Entrata)
Ga:Gestore Accessi
! Controllo_DatiC: DatiP x DatiC x Bool
! Cancellami: DatiP
! Registrami: DatiP x DatiC
! Collegami: DatiP
! Scollegami: DatiP
? RegistraC: DatiC x DatiP
? Collegato: DatiP x Bool
? Cancellato: DatiP x Bool
? Scollegato: DatiP x Bool
? Registrato: DatiP x DatiC x Bool
21
Applicazione FGM : prima fase 2/19
Strutture dati individuate nel sistema strutturato della prima fase
DatiP : Dati Personali
DatiC : Dati Carta di Credito
CdatiP
CdatiC
Ok : CdatiP -> Bool
Email : CdatiP -> String
Ok : CdatiC -> Bool
Ordinamento
Legge
Clegge
Cordinamento
NuovoNumero : Clegge x Set(Int) x Int -> Int
InOrdine : Cordinamento x Int x Int -> Bool
Nota
Usiamo altre strutture dati : Set e Sequence. Le diamo per native
22
Applicazione FGM : prima fase 3/19
Specifica Strutture Dati
Dati carta di credito
Dati Personali
Costruttore
Costruttore
 Definedness 1
 Definedness 1
• def( CdatiC )
• def( CdatiP )
Operazione
Operazione
 Definedness 3
 Definedness 3
• def( Ok )
• def( Email )
Op & Con
• def( Ok )
 Definedness 4
 Value 1
• If not def( CdatiC ) then not def( Ok )
• If Email = str1 then str1=“_@_”
 Applicazione
Op1 & Op2
• Ok( CdatiP ) = True
 Definedness 4
• if not def( Email ) then not def( Ok )
 Value 2
• If Email() = “” then Ok()=False
Op & Con
 Definedness 4
• If not def( CdatiP ) then not def( Ok ) And not def( Email )
 Applicazione
• Ok( CdatiP ) = True
• Email( CdatiP ) = “_@_”
23
Applicazione FGM : prima fase 4/19
Specifica Strutture Dati
Legge
Costruttore
 Definedness 1
• def( Clegge )
Operazione
 Definedness 3
• def( NuovoNumero( _,_,_ ) )
Op & Con
 Definedness 4
• If not def( Clegge ) then not def( NuovoNumero(_,_) )
Ordinamento
Costruttore
 Definedness 1
• def( Cordinamento )
Operazione
 Definedness 3
• def( InOrdine( _,_,_ ) )
Op & Con
 Definedness 4
• If not def( Clegge ) then not def( NuovoNumero(_,_) )
24
Applicazione FGM : prima fase 5/19
Specifica dei Sottosistemi
Spreedsheet contenente le matrici generate con il metodo fgm
Di seguito riportiamo le parti salienti unitamente ad una breve
spiegazione
•
A livello di Dominio discriminiamo gli utenti usando i loro dati personali. Per
questo motivo ogni utente deve necessariamente fornirli
– U.DatiP≠ NULL
•
Affinché ogni richiesta di un utente riceva risposta positiva è necessario che
i suoi dati personali siano sintatticamente corretti
–
–
–
–
–
if GA.Collegato(dp,TRUE) happen then dp.ok() = TRUE
if GA.Scollegato(dp,TRUE) happen then dp.ok() = TRUE
if GA.Cancellato(dp,TRUE) happen then dp.ok() = TRUE
if GA.Registrato(dp,-,TRUE) happen then dp.ok() = TRUE
if GCC.Addebito(dp,-,-,-,TRUE) happen then dp.ok() = TRUE
25
Applicazione FGM : prima fase 6/19
•
Un utente per poter partecipare alla lotteria deve fornire la sua carta di credito
– U.carta≠ NULL
•
Affinché ogni richiesta di un utente riceva risposta positiva è necessario che i dati
della sua carta di credito siano sintatticamente corretti
– if GA.Registrato(-,cc,TRUE) happen then cc.ok() = TRUE
– if GCC.Addebito(-,cc,-,-,TRUE) happen then cc.ok() = TRUE
– if GCC.Controllo_DatiC(-,cc,TRUE) happen then cc.ok() = TRUE
•
Il numero dei biglietti omaggio deve essere maggiore di 0, minore della metà dei
biglietti inizialmente disponibili, Null per utenti non ancora registrati
– NOT U.BilOmaggio < 0
– U.BilOmaggio <= L.Dim
– U.BilOmaggio < card(L.Assegnati)
•
Il valore del numero dei biglietti omaggio assegnabili ad un utente cambia in
conseguenza di
– if U.BilOmaggio = v1 and U.BilOmaggio' = v2 and v1≠v2 then U.Addebito(-,-,-,-,TRUE),
D.Distribuisci_BilOmaggio(-), Registrato(-,-,TRUE), Cancellato(-,TRUE) happen
26
Applicazione FGM : prima fase 7/19
•
Il valore del numero dei biglietti omaggio deve rispettare queste condizioni se un
utente ha il permesso di essere
– if GA.Collegato(-,TRUE) happen then U.BilOmaggio >= 0
– if GA.Scollegato(-,TRUE) happen then U.BilOmaggio >= 0
– if GA.Cancellato(-,TRUE) happen then U.BilOmaggio >= 0
if GA.Cancellato(-,TRUE) happen then U.BilOmaggio' = NULL
– if GA.Registrato(-,-,-) happen then U.BilOmaggio = NULL
if GA.Registrato(-,-,TRUE) happen then U.BilOmaggio’ = 0
– if GCC.Addebito(-,-,-,-,-) happen then U.BilOmaggio >= 0
if GCC.Addebito(-,-,-,-,-) happen then U.BilOmaggio' = U.BilOmaggio+1
– if GCC.Controllo_DatiC(-,-,-) happen then U.BilOmaggio = NULL
•
I cambiamenti sul valore del numero dei biglietti omaggio riguardanti tutti gli utenti
si hanno in conseguenza di
– if D.Inizia_Lotteria(-,-,-) happen then {  u  Utente if ( u.BilOmaggio != NULL ) then
u.BilOmaggio'=0 }
– if D.Distribuisci_BilOmaggio(-) happen then { u  Utente t.c. u=pickone(Utente) then
u.BilOmaggio'=u.BilOmaggio-1 }
Nota : la pickone è una funzione ausiliaria che dati un
insieme restituisce in modo casuale un suo elemento
27
Applicazione FGM : prima fase 8/19
•
Ad ogni richiesta dell’ utente un provider si attiva per valutare la possibilità di
soddisfarla
–
–
–
–
–
•
if U.Collegami(dp) happen then in any case eventually GA.Collegato(dp,-) happen
if U.Scollegami(dp) happen then in any case eventually GA.Scollegato(dp,-) happen
if U.Cancellami(dp) happen then in any case eventually GA.Cancellato(dp,-) happen
if U.Registrami(dp) happen then in any case eventually GA.Registrato(dp,-) happen
if U.AcquistaBil(dp,cc,-) happen then in any case eventually GCC.Addebito(dp,cc,-,-,-)
happen
Senza controllo è possibile che un utente richieda
–
–
–
–
–
in any case eventually U.Collegami(-) happen
in any case eventually U.Scollegami(-) happen
in any case eventually U.Cancellami(-) happen
in any case eventually U.Registrami(-) happen
in any case eventually U.AcquistaBil(-,-,-) happen
28
Applicazione FGM : prima fase 9/19
•
Un utente per potersi collegare deve essere registrato
– if GA.Collegato(dp,FALSE) happen then always in the past
U.Collegami(dp),GA.Registrato(dp,-,FALSE) happen
– if GA.Collegato(dp,TRUE) happen then always in the past
U.Collegami(dp),GA.Registrato(dp,-,TRUE) happen
•
Un Utente per potersi scollegare deve essere collegato
– if GA.Scollegato(dp,TRUE) happen then always in the past U.Scollegami(dp),
GA.Collegato(dp,TRUE) happen
– if GA.Scollegato(dp,FALSE) happen then always in the past U.Scollegami(dp),
GA.Collegato(dp,FALSE) happen
•
Un utente per potersi cancellare deve essere registrato
– if GA.Cancellato(dp,TRUE) happen then always in the past
U.Cancellami(dp),GA.Registrato(dp,cc,TRUE) happen
– if GA.Cancellato(dp,FALSE) happen then always in the past
U.Cancellami(dp),GA.Registrato(dp,cc,FALSE) happen
29
Applicazione FGM : prima fase 10/19
•
Lo stesso utente non può cancellarsi due volte
– GA.Cancellato(dp1,TRUE) incompatible with GA.Cancellato(dp2,TRUE) if dp1 = dp2
•
Un utente al fine di registrasi deve fornire i dati della sua carta di credito
– if GA.Registrato(dp,cc,TRUE) happen then always in the past U.Registrami(dp,cc) ,
GA.RegistraC(dp,cc) , GCC.Controlla_DatiC(dp,cc,TRUE) happen
– if GA.Registrato(dp,cc,FALSE) happen then always in the past U.Registrami(dp,cc) ,
GA.RegistraC(dp,cc) , GCC.Controlla_DatiC(dp,cc,FALSE) happen
•
Un utente per poter acquistare un biglietto deve essere collegato
– if GCC.Addebito(dp,cc,num,1000,TRUE) happen then always in the past
U.AcquistaBil(dp,cc,num), GA.Collegato(dp,TRUE)
•
Lo stesso biglietto non può essere comprato due volte
– GCC.Addebito(-,-,num,-,TRUE) incompatible with GCC.Addebito(-,-,num1,-,TRUE)
if num= num1
30
Applicazione FGM : prima fase 11/19
•
Lo stesso utente non può fare contemporaneamente due richieste ai provider né
ricevere risposte da un provider mentre effettua una richiesta
– U.Collegami(dp1) incompatible with
GA.Collegato(dp2,-), U.Scollegami(dp2), GA.Scollegato(dp2,-), U.Cancellami(dp2),
GA.Cancellato(dp2,-), U.Registrami(dp2,-), GA.Registrato(dp2,-,-), U.AcquistaBil(dp2,-,-),
GCC.Addebito(dp2,-,-,-,-), GA.RegistraC(dp2,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1 = dp2
– U.Scollegami(dp1) incompatible with
GA.Scollegato(dp2,-), U.Cancellami(dp2), GA.Cancellato(dp2,-), U.Registrami(dp2,-),
GA.Registrato(dp2,-,-), U.AcquistaBil(dp2,-,-), GCC.Addebito(dp2,-,-,-,-),
GA.RegistraC(dp2,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1 = dp2
– U.Cancellami(dp1) incompatible with
U.Registrami(dp2,-,-), U.Registrato(dp2,-,-), U.AcquistaBil(dp2,-,-), GCC.Addebito(dp2,-,-,-,-),
GA.RegistraC(dp2,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1 = dp2
– U.Registrami(dp1,-) incompatible with
GA.Registrato(d2,-,-), U.AcquistaBil(dp2,-,-), GCC.Addebito(dp2,-,-,-,-), GA.RegistraC(dp2,-),
GCC.Controllo_DatiC(dp2,-,-)
if dp1 = dp2
– U.AcqBiglietto(dp1,-,-) incompatible with
GCC.Addebito(dp2,-,-,-,-), GA.RegistraC(dp1,-), GCC.Controllo_DatiC(dp1,-,-)
if dp1 = dp2
31
Applicazione FGM : prima fase 12/19
•
Un provider non può rispondere a due richieste contemporaneamente né mentre
risponde ricevere una richiesta con interlocutore stesso utente
– GA.Collegato(dp1) incompatible with
U.Scollegami(dp2), GA.Scollegato(dp2,-), U.Cancellami(dp2), GA.Cancellato(dp2,-),
U.Registrami(dp2,-), GA.Registrato(dp2,-,-), U.AcquistaBil(dp2,-,-), GCC.Addebito(dp2,-,-,-,-),
GA.RegistraC(dp2,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1 = dp2
– GA.Scollegato(dp1,-) incompatible with
U.Cancellami(dp2), GA.Cancellato(dp1,-), U.Registrami(dp2,-), GA.Registrato(dp1,-),
U.AcquistaBil(dp2,-,-), GCC.Addebito(dp2,-,-,-,-), GA.RegistraC(dp2,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1 = dp2
– GA.Cancellato(dp1,-) incompatible with
U.Registrami(dp2,-), GA.Registrato(dp2,-,-), U.AcquistaBil(dp2,-,-), GCC.Addebito(dp2,-,-,-,-),
GA.RegistraC(dp2,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1= dp2
– GA.Registrato(dp1,-,-) incompatible with
U.AcquistaBil(dp2,-,-), GCC.Addebito(dp2,-,-,-,-), GA.RegistraC(dp2,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1 = dp2
– GCC.Addebito(dp2,-,-,-,-) incompatible with
GA.RegistraC(dp1,-), GCC.Controllo_DatiC(dp2,-,-)
if dp1=dp2
32
Applicazione FGM : prima fase 13/19
•
Il numero del biglietto scelto per l’acquisto deve appartenere all’ intervallo
determinato dal direttore al momento dell’inizio della lotteria
– if GCC.Addebito(-,-,bil,-,TRUE) happen then -L.Dim <= bil <= L.Dim
•
Una volta venduto un biglietto non sarà più disponibile
– if GCC.Addebito(-,-,bil,-,TRUE) happen then L.Assegnati' = L.Assegnati υ{bil}
•
Non è possibile acquistare un biglietto durante
– GCC.Addebito(-,-,-,-,TRUE) incompatible with
D.Inizia_Lotteria(-,-,-), D.Vincitori(), D.Estrai(), D.Manda(-,msg) if msg { "La lotteria è finita" , "Hai
vinto" , "La Lotteria è iniziata"}
•
La quantità di biglietti venduti deve rispettare i seguenti vincoli
– card(L.Assegnati) <= 2*L.Dim+1
– card(L.Assegnati) >= 0
•
Prima, subito dopo l’inizio della lotteria e dopo l’estrazione la dimensione della
lotteria varia
– L.Dim>0
– if D.Inizia_Lotteria(-,-,-) happen then L.Dim = 0
if D.Inizia_Lotteria(-,-,d) happen then L.Dim' = d
– if D.Estrai() happen then L.Dim' = 0
33
Applicazione FGM : prima fase 14/19
•
L’ insieme dei biglietti venduti viene aggiornato a seguito di
– if L.Assegnati = n and Assegnati' = n+1 then D.Distribuisci_BilOmaggio(-),
U.AcquistaBil(-,-,-) happen
– if D.Inizia_Lotteria(-,-,-) happen then L.Assegnati' = Ø
•
È possibile effettuare l’estrazione e decretare i vincitori solo se tutti i biglietti sono
stati venduti
– if D.Vincitori() happen then card(L.Assegnati) = 2*L.Dim+1
– if D.Estrai() happen then card(L.Assegnati) = 2*L.Dim+1
•
Dopo l’assegnazione dei biglietti omaggio l’insieme dei biglietti non più disponibili
viene aggiornato
– if D.Distribuisci_BilOmaggio(num) happen then
num'=min(num,Complementare(L.Assegnati)), card(L.Assegnati')=
card(L.Assegnati)+num‘
•
È possibile distribuire biglietti in omaggio solo quando sono stati venduti la metà
più uno dei biglietti totali
– if D.Distribuisci_BilOmaggio(-) happen then L.Assegnati = L.Dim + 1
34
Applicazione FGM : prima fase 15/19
•
La distribuzione dei biglietti omaggio può avvenire solo dopo l’inizio della lotteria
– if D.Distribuisci_BilOmaggio(-) happen then always in the past D.Inizia_Lotteria(-,-,-)
happen
•
Un utente scelto per ricevere un biglietto omaggio viene avvisato
– if D.Distribuisci_BilOmaggio(-) happen then {" u' = pickone({u  Utente t.c.
u.BilOmaggio> 0}) , D.Manda(u'.Dati.email,"Hai vinto un biglietto omaggio")
•
Non può avvenire la distribuzione dei biglietti omaggio contemporaneamente a
– D.Distribuisci_BilOmaggio(-) incompatible with D.Estrai(), D.Vincitori(), D.Manda(-,-)
•
Esiste sempre una lotteria in corso
– in any case eventually D.Inizia_Lotteria(-,-,-) happen
•
Non possono essere indette due lotterie contemporaneamente
– D.Inizia_Lotteria(-,-,-) incompatible with D.Inizia_Lotteria(-,-,-)
•
Tutti gli utenti sono avvisati dell’inizio della lotteria
– if D.Inizia_Lotteria(ord,lex,-) happen then in any case eventually {  u  Utente
D.Manda(u.Dati.email,"La lotteria è iniziata")}
35
Applicazione FGM : prima fase 16/19
•
Non può essere decretato l’inizio di una nuova lotteria contemporaneamente a
– D.Inizia_Lotteria (-,-,-) incompatible with
D.Estrai(), D.Vincitori(), D.Distribuisci_BilOmaggio(-), D.Manda(-,-)
•
Prima di decretare i vincitori occorre sia ordinata l’estrazione
– if D.Vincitori() happen then always in the past D.Estrai() happen
•
I vincitori sono avvisati
– if gs = D.Vincitori() happen then in any case eventually forall g in gs
D.Manda(g.Dati.email,"Hai Vinto") happen
•
Ogni lotteria ha vincitori
– in any case eventually D.Vincitori() happen
•
Non possono essere decretati i vincitori contemporaneamente a
– D.Vincitori() incompatible with D.Estrai(), D.Manda(-,-)
•
Avvisati tutti i vincitori si avvisano tutti gli utenti che la lotteria è finita
– if D.Vincitori() happen then in any case eventually {  u  Utente
D.Manda(u.Dati.email,"La Lotteria è finita") } happen
36
Applicazione FGM : prima fase 17/19
•
Per poter effettuare l’estrazione deve esistere una lotteria in corso
– if D.Estrai() happen then always in the past D.Inizia_Lotteria(-,-,-) happen
•
All’estrazione dei biglietti vincitori segue la nomina degli utenti vincitori
– if D.Estrai() happen then in any case eventually D.Vincitori() happen
•
L’estrazione avviene sempre
– in any case eventually D.Estrai() happen
•
Non può avvenire l’estrazione contemporaneamente a
– D.Estrai() incompatible with D.Manda(-,-)
•
Solo determinate comunicazioni agli utenti possono avvenire
contemporaneamente
– D.Manda(-,msg1) incompatible with D.Manda(-,msg2) if
( ms1="La lotteria è finita" and ms2  {"La lotteria è iniziata","Hai ricevuto biglietto omaggio"} )
OR ( ms1="Hai vinto" and ms2  {"La lotteria è iniziata","Hai ricevuto biglietto omaggio"} )
37
Applicazione FGM : prima fase 18/19
•
Le comunicazioni agli utenti avvengono nei seguenti casi
– if D.Manda(-,-) happen then at least in one case D.Inizia_Lotteria(-,-,-),
D.Distribuisci_BilOmaggio(-), Vincitori() happen
•
Finita una lotteria è possibile iniziarne una nuova
– If D.Manda(-,"La lotteria è finita") happen then in any case eventually
D.Inizia_Lotteria(-,-,-) happen
•
Gli utenti ricevono varie comunicazioni dalla lotteria
– in any case eventually D.Manda(-,-) happen
38
Applicazione FGM : prima fase 19/19
FGM applicato alla seconda fase
Sottosistemi individuati nel sistema strutturato della seconda fase
Gcc:Gestore Carta Credito
! ControllaC: DatiC
? ControllataC: DatiC x Bool
! Addebita: DatiC x Nat
? Addebitato : Bool
Pt:Posta Elettronica
! Manda: String x String
Ga:Gestore Accessi
! RegistraU : DatiP x DatiC -> Codice
! ControllaU : DatiP x Codice
? ControllatoU : DatiP x Codice x Chiave x Bool
! CancellaU : DatiP x Codice
? CancellatoU : DatiP x Codice x Bool
Nota:
? Indica che e’ una richiesta (in Uscita)
! Una risposta (in Entrata)
39
Applicazione FGM : seconda fase 1/29
Lal : L-AL
? RegistraU : DatiP x DatiC -> Codice
? ControllaU : DatiP x Codice
! ControllatoU : DatiP x Codice x Chiave x Bool
? CancellaU : DatiP x Codice
! CancellatoU : DatiP x Codice x Bool
? ControllaC: DatiC
! ControllataC: DatiC x Bool
? Addebita : DatiC x Nat
! Addebitato : Bool
? Manda : String x String
! Registrami : Identità x DatiP x DatiC
? Registrato : Identità x Codice x Bool
! Cancellami : Identità x DatiP x Codice
? Cancellato : Identità x DatiP x Bool
! Collegami : Identità x DatiP x Codice
? Collegato : Identità x Chiave x Codice x Bool
! Scollegami : Identità x Chiave
? Scollegato : Identità x Chiave x Bool
! BilDisponibili : Identità
? SonoDisponibili : Identità x Set(Int)
! AcquistaBil : Identità x Chiave x Int
? BilAcquistato : Chiave x Int x Bool
x IniziaNuovaLotteria : Ordinamento x Legge x Nat
x Vincitori : Sequence( DatiP )
x DistribuisciBilOmaggio : Nat
x Estrai : -
Dim: Nat
Disponibili : Set(Int)
Giocatori : Sequence( Codice x DatiP x Chiave x DatiC x Nat )
U:Utente
? Registrami : Identità x DatiP x DatiC
! Registrato : Identità x Codice x Bool
? Cancellami : Identità x DatiP x Codice
! Cancellato : Identità x DatiP x Bool
? Collegami : Identità x DatiP x Codice
! Collegato : Identità x Chiave x Codice x Bool
? Scollegami : Identità x Chiave
! Scollegato : Identità x Chiave x Bool
? BilDisponibili : Identità
! SonoDisponibili : Identità x Set(Int)
? AcquistaBil : Identità x Chiave x Int
! BilAcquistato : Identità x Chiave x Int x Bool
Nota:
? Indica che e’ una richiesta (in Uscita)
! Una risposta (in Entrata)
40
Applicazione FGM : seconda fase 2/29
Strutture dati individuate nel sistema strutturato della seconda fase
DatiP : Dati Personali
DatiC : Dati Carta di Credito
CdatiP
CdatiC
Ok : CdatiP -> Bool
Email : CdatiP -> String
Ok : CdatiC -> Bool
Legge
Identità
CIdentità
Codice
Ccodice
Ordinamento
Clegge
Cordinamento
NuovoNumero : Clegge x Set(Int) x Int -> Int
InOrdine : Cordinamento x Int x Int -> Bool
Chiave
Cchiave
Nota
Usiamo altre strutture dati : Set e Sequence. Le diamo per native
41
Applicazione FGM : seconda fase 3/29
Specifica Strutture Dati
Dati carta di credito
Dati Personali
Costruttore
Costruttore
 Definedness 1
 Definedness 1
• def( CdatiC )
• def( CdatiP )
Operazione
Operazione
 Definedness 3
 Definedness 3
• def( Ok )
• def( Email )
Op & Con
• def( Ok )
 Definedness 4
 Value 1
• If not def( CdatiC ) then not def( Ok )
• If Email = str1 then str1=“_@_”
 Applicazione
Op1 & Op2
• Ok( CdatiP ) = True
 Definedness 4
• if not def( Email ) then not def( Ok )
 Value 2
• If Email() = “” then Ok()=False
Op & Con
 Definedness 4
• If not def( CdatiP ) then not def( Ok ) And not def( Email )
 Applicazione
• Ok( CdatiP ) = True
• Email( CdatiP ) = “_@_”
42
Applicazione FGM : seconda fase 4/29
Legge
Costruttore
 Definedness 1
• def( Clegge )
Operazione
 Definedness 3
• def( NuovoNumero( _,_,_ ) )
Op & Con
 Definedness 4
• If not def( Clegge ) then not def( NuovoNumero(_,_,_) )
Ordinamento
Costruttore
 Definedness 1
• def( Cordinamento )
Operazione
 Definedness 3
• def( InOrdine( _,_,_ ) )
Op & Con
 Definedness 4
• If not def( Cordinamento ) then not def( InOrdine(_,_,_) )
43
Applicazione FGM : seconda fase 5/29
Chiave
Costruttore
 Definedness 1
• def( Cchiave )
Codice
Costruttore
 Definedness 1
• def( Ccodice )
Identità
Costruttore
 Definedness 1
• def( Cidentità )
44
Applicazione FGM : seconda fase 6/29
Specifica dei Sottosistemi
Spreedsheet contenente le matrici generate con il metodo fgm
Di seguito riportiamo le parti salienti unitamente ad una breve
spiegazione
•
A livello di Requisiti discriminiamo gli utenti usando la loro identità e
all’interno del sistema L-AL il codice attribuitogli in fase di registrazione.
•
Il sistema è sempre disponibile ad accettare e rispondere a richieste di
servizio da parte dell’utente
–
–
–
–
–
if Collegami(i,-,-) happen then in any case eventually Collegato(i,-,-) happen
if Scollegami(i,ch) happen then in any case eventually Scollegato(i,ch,-) happen
if Cancellami(i,-,-) happen then in any case eventually Cancellato(i,-,-) happen
if Registrami(i,-,-) happen then in any case eventually Registrato(i,-,-) happen
if AcquistaBil(i,-,-) happen then in any case eventually BilAcquistato(i,-,-,-)
happen
– if BilDisponibili(i) happen then in any case eventually SonoDisponibili(i,-) happen
45
Applicazione FGM : seconda fase 7/29
•
Senza controllo è possibile che un utente richieda
–
–
–
–
–
–
•
in any case eventually Collegami(-,-,-) happen
in any case eventually Scollegami(-,-) happen
in any case eventually Cancellami(-,-,-) happen
in any case eventually Registrami(-,-,-) happen
in any case eventually AcquistaBil(-,-,-) happen
in any case eventually BilDisponibili(-) happen
Un utente per potersi collegare deve essere registrato. Se l’ operazione termina
correttamente l’ utente riceva una chiave di sessione
– If Collegato(i,-,cod,FALSE) happen then always in the past Collegami(i,dp,cod) ,
ControllatoU(dp,cod,-,FALSE) , Registrato(i,cod,FALSE) happen
– if Collegato(i,ch,cod,TRUE) happen then always in the past Collegami(i,dp,cod) ,
ControllatoU(dp,cod,ch,TRUE) , Registrato(i,cod,TRUE) happen
•
Un Utente per potersi scollegare deve essere collegato
– if Scollegato(i,ch,TRUE) happen then always in the past Scollegami(i,ch) ,
Collegato(i,ch,TRUE) happen
– if Scollegato(i,ch,FALSE) happen then always in the past Scollegami(i,ch) ,
Collegato(i,ch,FALSE) happen
46
Applicazione FGM : seconda fase 8/29
•
Un utente per potersi cancellare deve essere registrato
– if Cancellato(i,dp,TRUE) happen then always in the past Cancellami(i,dp,cod) ,
CancellatoU(dp,cod,TRUE) , Registrato(i,cod,TRUE) happen
– if Cancellato(i,dp,FALSE) happen then always in the past Cancellami(i,dp,cod) ,
CancellatoU(dp,cod,FALSE) , Registrato(i,cod,FALSE) happen
•
Lo stesso utente non può cancellarsi due volte
– Cancellato(i1,dp1,TRUE) incompatible with Cancellato(i2,dp2,TRUE) if dp1 = dp2
•
Un utente al fine di registrasi deve fornire i dati della sua carta di credito. Se
l’operazione termina correttamente l’utente riceve il suo codice personale
– if Registrato(i,cod,TRUE) happen then always in the past Registrami(i,dp,cc),
ControllataC(cc,TRUE), cod = RegistraU(dp,cc) happen
– if Registrato(i,cod,FALSE) happen then always in the past Registrami(i,dp,cc),
ControllataC(cc,FALSE) happen
•
Un utente per poter acquistare un biglietto deve essere collegato
– if BilAcquistato(i,ch,bil,TRUE) happen then always in the past AcquistaBil(i,ch,bil) ,
Addebitato(cc,TRUE), Collegato(i,ch,TRUE), BilDisponibili(i) AND esiste g in Giocatori
t.c. g.carta = cc AND g.chiave = ch happen
47
Applicazione FGM : seconda fase 9/29
•
Lo stesso biglietto non può essere comprato due volte
– BilAcquistato(-,-,bil1,TRUE) incompatible with BilAcquistato(-,-,bil2,TRUE) if bil1 = bil2
•
L’ utente può sempre chiedere quali biglietti sono disponibili
– if SonoDisponibili(i,-) happen then always in the past BilDisponibili(i) happen
•
A seguito di richieste provenienti dall’utente il sistema richiede la collaborazione
dei provider
–
–
–
–
–
•
in any case eventually Addebita(-,1000)
in any case eventually ControllaC(-)
in any case eventually ControllaU(-,-) happen
in any case eventually RegistraU(-) happen
in any case eventually CancellaU(-,-) happen
Se viene effettuato una richiesta di addebito la carta di credito deve essere stata
riconosciuta valida
– if Addebita(cc,1000) happen then always in the past ControllataC(cc,TRUE) ,
AcquistaBil(i,ch,bil) AND esiste g in Giocatori t.c. g.carta = cc AND g.chiave = ch happen
48
Applicazione FGM : seconda fase 10/29
•
Una richiesta di controllo per la validità di una carta avviene solo in caso di
registrazione
– if ControllaC(cc) happen then always in the past Registrami(-,-,cc) happen
•
La restituzione di un codice ad un utente avviene solo se la sua carta di credito è
riconosciuta valida
– if cod = RegistraU(dp,cc) happen than always in the past Registrami(-,dp,cc),
ControllataC(cc,TRUE) happen
•
A seguito di una richiesta di collegamento al sistema quest’ ultimo richiede la
collaborazione del gestore degli accessi per la verifica del codice
– if ControllaU(dp,cod) happen then always in the past Collegami(-,dp,cod) happen
•
A seguito di una richiesta di cancellazione al sistema quest’ ultimo richiede la
collaborazione del gestore degli accessi per la verifica del codice
– if CancellaU(dp,cod) happen then always in the past Cancellami(-,dp,cod) happen
49
Applicazione FGM : seconda fase 11/29
•
Il sistema è sempre disponibile ad accettare e passare richieste di servizio ai
provider opportuni
– if Addebita(cc,1000) happen then in any case eventually Addebitato(cc,-) happen
– if ControllaC(cc) happen then in any case eventually ControllataC(cc,-) happen
– if cod = RegistraU(dp,cc) happen than in any case eventually Registrato(-,cod,TRUE)
happen
– if ControllaU(dp,cod) happen then in any case eventually ControllatoU(dp,cod,-,-)
happen
– if CancellaU(dp,cod) happen then in any case eventually CancellatoU(dp,cod,-) happen
•
Il sistema riceve una risposta dal gestore della carta di credito per ogni richiesta
di addebito inoltrata
– if Addebitato(cc,-) happen then always in the past Addebita(cc,1000) happen
•
Se all’utente viene addebitato il costo dei biglietti da lui acquistati allora la sua
carta è risultata valida
– if Addebitato(cc,TRUE) happen then always in the past ControllataC(cc,TRUE)
happen
– if Addebitato(cc,FALSE) happen then always in the past ControllataC(cc,FALSE)
happen
50
Applicazione FGM : seconda fase 12/29
•
Prima di permettere l’utilizzo della carta di credito il sistema richiede un controllo
sulla sua validità
– if ControllataC(cc,-) happen then always in the past ControllaC(cc) happen
•
Prima di permettere il collegamento di un utente il sistema richiede un controllo sul
codice al gestore degli accessi
– if ControllatoU(dp,cod,-,-) happen then always in the past ControllaU(dp,cod) happen
•
Prima di permettere la cancellazione di un utente il sistema richiede un controllo
sul codice al gestore degli accessi
– if CancellatoU(dp,cod,-) happen then always in the past CancellaU(dp,cod) happen
•
Se il sistema riceve conferma di addebito da parte del gestore della carta di
credito comunica all’utente l’avvenuto acquisto del biglietto
– if Addebitato(cc,TRUE) happen then in any case eventually BilAcquistato(i,ch,-,TRUE)
AND esiste g in Giocatori t.c. g.carta = cc AND g.chiave = ch happen
– if Addebitato(cc,FALSE) happen then in any case eventually BilAcquistato(i,ch,-,FALSE)
AND esiste g in Giocatori t.c. g.carta = cc AND g.chiave = ch happen
51
Applicazione FGM : seconda fase 13/29
•
Se il sistema riceve conferma circa la validità della carta di credito comunica all’
utente l’avvenuta registrazione comunicandogli il codice
– if ControllataC(cc,TRUE) happen then in any case evantually cod = RegistraU(-,cc),
Registrato(-,cod,TRUE) happen
– if ControllataC(cc,FALSE) happen then in any case evantually Registrato(-,-,FALSE)
happen
•
Se il sistema riceve conferma circa la validità del codice comunica all’ utente il
collegamento
– if ControllatoU(dp,-,ch,TRUE) happen then in any case eventually
Collegato(dp,ch,TRUE)
– if ControllatoU(dp,-,-,FALSE) happen then in any case eventually Collegato(dp,-,FALSE)
•
Se il sistema riceve conferma circa la validità del codice comunica all’ utente l’
avvenuta cancellazione
– if CancellatoU(dp,-,TRUE) happen then in any case eventually Cancellato(-,dp,TRUE)
happen
– if CancellatoU(dp,-,FALSE) happen then in any case eventually Cancellato(-,dp,FALSE)
happen
52
Applicazione FGM : seconda fase 14/29
•
L’ utente con la stessa identità non può fare contemporaneamente due richieste
al sistema né ricevere risposte dal sistema mentre effettua una richiesta.
Nel caso di richiesta rimane bloccato finché non gli viene risposto.
– Collegami(i1,-,cod1) incompatible with
Collegato(i2,-,cod2,-), Scollegami(i2,-), Scollegato(i2,-,-), Cancellami(i2,-,-), Cancellato(i2,-,-),
Registrami(i2,-,-), Registrato(i2,-,-), AcquistaBil(i2,-,-), BilAcquistato(i2,-,-), BilDisponibili(i2),
SonoDisponibili(i2,-)
if i1 = i2
– Scollegami(i1,-) incompatible with
Scollegato(i2,-,-), Cancellami(i2,-,-), Cancellato(i2,-,-), Registrami(i2,-,-), Registrato(i2,-,-),
AcquistaBil(i2,-,-), BilAcquistato(i2,-,-), BilDisponibili(i2), SonoDisponibili(i2,-)
if i1 = i2
– Cancellami(i1,-,-) incompatible with
Cancellato(i2,-,-), Registrami(i2,-,-), Registrato(i2,-,-), AcquistaBil(i2,-,-), BilAcquistato(i2,-,-),
BilDisponibili(i2), SonoDisponibili(i2,-)
if i1 = i2
– Registrami(i1,-,-) incompatible with
Registrato(i2,-,-), AcquistaBil(i2,-,-), BilAcquistato(i2,-,-), BilDisponibili(i2), SonoDisponibili(i2,-)
if i1 = i2
– AcqBiglietto(i1,-,-) incompatible with
BilAcquistato(i2,-,-,-), BilDisponibili(i2), SonoDisponibili(i2,-)
if i1 = i2
– BilDisponibili(i1) incompatible with SonoDisponibili(i2,-) if i1 = i2
53
Applicazione FGM : seconda fase 15/29
•
Non è possibile che per un utente con stessa identità avvengano
contemporaneamente una comunicazione con il sistema e una richiesta di
collaborazione dal sistema ai provider
– Collegami(-,-,cod) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if cod=cod1
– Scollegami(-,ch) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if esiste g in Giocatori t.c. g.codice = cod1 AND g.chiave = ch
– Cancellami(-,-,cod) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if cod=cod1
– Registrami(-,-,-) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if cod=cod1
– AcquistaBil(-,ch,-) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if esite g in Giocatori t.c. g.codice=cod1 AND g.chiave = ch
54
Applicazione FGM : seconda fase 16/29
•
Il sistema non può rispondere a due richieste contemporaneamente né mentre
risponde ricevere una richiesta da utente con stessa identità
– Collegato(i1,-,-,-) incompatible with
Scollegami(i2,-), Scollegato(i2,-,-), Cancellami(i2,-,-), Cancellato(i2,-,-), Registrami(i2,-,-),
Registrato(i2,-,-), AcquistaBil(i2,-,-), BilAcquistato(i2,-,-), BilDisponibili(i2), SonoDisponibili(i2,-))
if i1 = i2
– Scollegato(i1,-,-) incompatible with
Cancellami(i2,-,-), Cancellato(i2,-,-), Registrami(i2,-,-), Registrato(i2,-,-), AcquistaBil(i2,-,-),
BilAcquistato(i2,-,-), BilDisponibili(i2), SonoDisponibili(i2,-)
if i1 = i2
– Cancellato(i1,-,-) incompatible with
Registrami(i2,-,-), Registrato(i2,-,-), AcquistaBil(i2,-,-), BilAcquistato(i2,-,-), BilDisponibili(i2),
SonoDisponibili(i2,-)
if i1=i2
– Registrato(i1,-,-) incompatible with
AcquistaBil(i2,-,-,-), BilAcquistato(i2,-,-), BilDisponibili(i2), SonoDisponibili(i2,-)
if i1 = i2
– BilAcquistato(i1,-,-,-) incompatible with
BilDisponibili(i2), SonoDisponibili(i2,-)
if i1 = i2
55
Applicazione FGM : seconda fase 17/29
•
Il sistema non può rispondere e contemporaneamente richiedere servizi ai
provider per un utente con stessa identità
– Collegato(i1,-,-,-) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if cod=cod1
– Scollegato(-,ch,-) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if esiste g in Giocatori t.c. g.codice = cod1 AND g.chiave = ch
– Cancellato(-,dp,-) incompatible with
ControllaU(dp1,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if cod=cod1
– Registrato(-,cod,-) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if cod=cod1
– BilAcquistato(-,ch,-,-) incompatible with
ControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)
if esite g in Giocatori t.c. g.codice=cod1 AND g.chiave = ch
56
Applicazione FGM : seconda fase 18/29
•
Se la carta è stata accettata una volta allora è valida per ogni successivo
controllo
– Collegato(i1,-,cod,TRUE), Scollegato(i1,ch,TRUE), Registrato(i1,cod,TRUE),
BilAcquistato(-,ch,-,TRUE), ControllatoU(-,cod,-,TRUE), CancellatoU(-,cod,TRUE)
incompatible with
ControllataC(cc,FALSE)
if esiste g in Giocatori t.c. g.codice = cod AND g.datiC = cc
•
Non possono avvenire contemporaneamente richieste ai provider e risposte al
sistema per lo stesso utente
– ControllaU(-,cod1) incompatible with
ControllatoU(-,cod2,-,-), CancellaU(-,cod2), CancellatoU(-,cod2,-)
if cod1 = cod2
– ControllatoU(-,cod1,-,-) incompatible with
CancellaU(-,cod2), CancellatoU(-,cod2,-)
if cod1 = cod2
– CancellaU(-,cod1) incompatible with CancellatoU(-,cod2,-) if cod1 = cod2
57
Applicazione FGM : seconda fase 19/29
•
L’acquisto di un biglietto non può essere effettuato mentre viene iniziata una
una nuova lotteria, vengono estratti i biglietti vincenti o decretati i vincitori
– BilAcquistato(-,-,-,TRUE) incompatible with
IniziaNuovaLotteria(-,-,-), Vincitori(), Estrai(), Manda(-,msg) if msg  { "La lotteria è finita" ,
"Hai vinto" , "La Lotteria è iniziata"}
– Addebitato(-,-,-) incompatible with
IniziaNuovaLotteria(-,-,-), Vincitori(), Estrai(), Manda(-,msg) if msg  { "La lotteria è finita" ,
"Hai vinto" , "La Lotteria è iniziata"}
•
Le seguenti operazioni provocano cambiamenti all’ insieme delle immagini
degli utenti all’ interno del sistema. La dimensione della lista rimane sempre
maggiore o uguale di zero
– if n = length(Giocatori) AND n1 = length(Giocatori') then Registrato(-,-,TRUE) OR
Cancellato(-,-,TRUE) happen
– if n = Giocatori(n).BilOmaggio AND n1 = Giocatori(n).BilOmaggio' then
BilAcquistato(-,-,-,TRUE) OR DistribuisciBilOmaggio(-) happen
– length(Giocatori)>=0
58
Applicazione FGM : seconda fase 20/29
•
L’utente collegato ha una chiave di sessione. Essendo unica la chiave di
sessione lo stesso utente che si collega contemporaneamente da luoghi differenti
perde la prima chiave assegnatagli
– if Collegato(i1,ch,cod,TRUE) happen then esiste g in Giocatori t.c. ( g.codice = cod
AND g.chiave = NULL )
– if Collegato(i1,ch,cod,TRUE) happen then esiste g in Giocatori t.c. ( g.codice = cod
AND g.chiave = NULL AND esiste g' in Giocatori' t.c. ( g.codice = cod AND
g.chiave = ch )
•
È permesso scollegarsi solo se si collegati, lo scollegamento cancella la chiave di
sessione
– if Scollegato(-,ch1,TRUE) happen then esiste g in Giocatori t.c. ( g.chiave = ch1 )
– if Scollegato(-,ch1,TRUE) happen then esiste g in Giocatori t.c. ( g.chiave = ch1 ) AND
esiste g' in Giocatori' t.c. ( g.chiave = NULL )
•
È consentito cancellarsi solo se si possiede un codice valido, dopo la
cancellazione il sistema cancella la virtualizzazione dell’ utente in possesso del
codice fornito
– if Cancellato(i1,dp1,TRUE) happen then esiste g in Giocatori t.c. ( g.datiP = dp1 )
– if Cancellato(i1,dp1,TRUE) happen then esiste g in Giocatori t.c. ( g.datiP = dp1 ) AND
NOT esiste g' in Giocatori' t.c. ( g'.datiP = dp1 ) AND
lenght(Giocatori') = lenght(Giocatori)-1
59
Applicazione FGM : seconda fase 21/29
•
La registrazione crea una virtualizzazione dell’ utente all’ interno del sistema. Il
sistema identifica l’ utente attraverso il codice attribuitogli
– if Registrato(i1,cod,TRUE) happen then NOT esiste g in Giocatori t.c. ( g.codice = cod )
– if Registrato(i1,cod,TRUE) happen then NOT esiste g in Giocatori t.c. ( g.codice = cod )
AND esiste g' in Giocatori' t.c. ( g'.codice = cod ) AND lenght(Giocatori') =
lenght(Giocatori)+1
•
L’ acquisto di un biglietto aumenta il numero dei biglietti omaggio che l’ utente può
ricevere
– if BilAcquistato(i1,ch,bil,TRUE) happen then esiste g in Giocatori t.c. ( g.chiave = ch
AND g.bilOmaggio = n-1 )
– if BilAcquistato(i1,ch,bil,TRUE) happen then esiste g in Giocatori' t.c. ( g.chiave = ch
AND g.bilOmaggio = n )
•
All’ inizio di una nuova lotteria il sistema azzera il numero di biglietti omaggio che
ogni utente può ricevere
– if IniziaNuovaLotteria(-,-,-) happen then forall g in Giocatori g.bilOmaggio = 0
60
Applicazione FGM : seconda fase 22/29
•
Il numero del biglietto scelto per l’acquisto deve appartenere all’ intervallo
determinato al momento dell’inizio della lotteria
– if BilAcquistato(-,-,bil,TRUE) happen then -Dim <= bil <= Dim
•
La quantità di biglietti messi in vendita ottenuta usando Dim deve rispettare i
seguenti vincoli
– card( Disponibili ) <= 2*Dim+1
– card( Disponibili )>=0
•
Prima, subito dopo l’inizio della lotteria e dopo l’estrazione la quantità dei biglietti
messi in vendita è
–
–
–
–
•
if IniziaNuovaLotteria(-,-,-) happen then Disponibili = Ø
if IniziaNuovaLotteria(-,-,d) happen then Disponibili = { -d ...+d }
if Vincitori() happen then Disponibili = Ø
if Estrai() happen then Disponibili = Ø
Prima, subito dopo l’inizio della lotteria e dopo l’estrazione la dimensione della
lotteria varia
–
–
–
–
Dim>0
if IniziaNuovaLotteria(-,-,-) happen then Dim = 0
if IniziaNuovaLotteria(-,-,d) happen then Dim' = d
if Estrai() happen then Dim' = 0
61
Applicazione FGM : seconda fase 23/29
•
Una volta venduto un biglietto non sarà più disponibile
– if BilAcquistato(-,-,bil,TRUE) happen then bil  Disponibili
– if BilAcquistato(-,-,bil,TRUE) happen then Disponibili' = Disponibili - { bil }
•
L’ insieme dei biglietti disponibili viene aggiornato a seguito di
– if Disponibili = n AND Disponibili' = n+1 then DistribuisciBilOmaggio(-) OR
AcquistaBil(-,-,-) happen
•
È possibile distribuire biglietti in omaggio solo quando sono rimasti invenduti la
metà meno uno dei biglietti totali
– if DistribuisciBilOmaggio(-) happen then Disponibili = Dim
•
Dopo l’assegnazione dei biglietti omaggio l’insieme dei biglietti disponibili viene
aggiornato
– if DistribuisciBilOmaggio(num) happen then num'=min(num,Disponibili) ,
card(Disponibili') = card(Disponibili)-num‘
62
Applicazione FGM : seconda fase 24/29
•
La distribuzione dei biglietti omaggio avviene selezionando i giocatori aventi
diritto e attribuendogli un biglietto tra quelli disponibili scelto usando la legge, i
giocatori vengono poi avvertiti
– if DistribuisciBilOmaggio(num) happen then n = min(num,card(Disponibili)) ,
while ( n >= 0 ) { gs' = pickone({gs  Giocatori t.c. gs.BilOmaggio> 0 } ) ,
gs'.BilOmaggio-- , numero = legge.NuovoNumero(complementare(Disponibili,Dim)) ,
Manda(gs'.datiP.email,"Hai ricevuto un biglietto omaggio numero") }
•
Non possono essere indette due lotterie contemporaneamente
– IniziaNuovaLotteria(-,-,-) incompatible with IniziaNuovaLotteria(-,-,-)
•
Tutti gli utenti vengono avvisati dell’ inizio di una nuova lotteria
– if IniziaNuovaLotteria happen then in any case eventually for all gs in Giocatori
Manda(gs.datiP.email,"La lotteria è iniziata")
63
Applicazione FGM : seconda fase 25/29
•
Esiste sempre una lotteria in corso
– in any case eventually IniziaNuovaLotteria(-,-,-) happen
•
La distribuzione dei biglietti omaggio può avvenire solo dopo l’inizio della lotteria
– if DistribuisciBilOmaggio(-) happen then always in the past IniziaNuovaLotteria(-,-,-)
happen
•
Non può essere decretato l’inizio di una nuova lotteria contemporaneamente a
– D.Inizia_Lotteria (-,-,-) incompatible with
Estrai(), Vincitori(), Distribuisci_BilOmaggio(-), Manda(-,-)
•
Prima di decretare i vincitori occorre sia ordinata l’estrazione
– if Vincitori() happen then always in the past Estrai() happen
64
Applicazione FGM : seconda fase 26/29
•
I vincitori sono avvisati dell’ avvenuta vincita
– if gs = Vincitori() happen then in any case eventually forall g in gs
Manda(g.datiP.email,"Hai Vinto") happen
•
Avvisati tutti i vincitori si avvisano tutti gli utenti che la lotteria è finita
– if Vincitori() happen then in any case eventually forall g in Giocatori
Manda(g.datiP.email,"La Lotteria è finita") happen
•
Ogni lotteria ha vincitori
– in any case eventually Vincitori() happen
•
Non possono essere decretati i vincitori contemporaneamente a
– Vincitori() incompatible with Estrai(), Manda(-,-)
65
Applicazione FGM : seconda fase 27/29
•
Per poter effettuare l’estrazione deve esistere una lotteria in corso
– if Estrai() happen then always in the past IniziaNuovaLotteria(-,-,-) happen
•
All’estrazione dei biglietti vincitori segue la nomina degli utenti vincitori
– if Estrai() happen then in any case eventually Vincitori() happen
•
L’estrazione avviene sempre
– in any case eventually Estrai() happen
•
Non può avvenire l’estrazione contemporaneamente a
– Estrai() incompatible with Manda(-,-)
•
Solo determinate comunicazioni agli utenti possono avvenire
contemporaneamente
– Manda(-,msg1) incompatible with Manda(-,msg2) if (ms1="La lotteria è finita" and
ms2  {"La lotteria è iniziata","Hai ricevuto biglietto omaggio"}) OR (ms1="Hai vinto"
AND ms2  {"La lotteria è iniziata","Hai ricevuto biglietto omaggio"})
66
Applicazione FGM : seconda fase 28/29
•
Le comunicazioni agli utenti avvengono nei seguenti casi
– if Manda(-,-) happen then always in the past IniziaNuovaLotteria(-,-,-) , Vincitori() ,
DistribuisciBilomaggio(-) happen
•
Finita una lotteria è possibile iniziarne una nuova
– if Manda(-,"La lotteria è finita") happen then in any case eventually
IniziaNuovaLotteria(-,-,-) happen
•
Gli utenti ricevono varie comunicazioni dalla lotteria
– in any case eventually Manda(-,-) happen
67
Applicazione FGM : seconda fase 29/29