1 Esercitazione I.S. II a.a. 2001/2002 Un Nuovo Frame Chiara Casanova Massimo Ruffa.

1

Esercitazione I.S. IIa.a. 2001/2002

Un Nuovo Frame

Chiara CasanovaMassimo Ruffa

2

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

Descrizione del frame 1/7

3

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 ) interno-interno


4

Presentazione del Frame

DesignDomain ( Business Model )

Requirement

CommandedBehaviour

Provider…

User…

System

Automatized…Generic

…

bound

boundaries


5

Presentazione del Frame


Requirement

CommandedBehaviour

Provider

UserU_Req

S_Resp

P_Resp

S_Req.bound


…

boundaries

System S_Act


6

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


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 )


8BusinessLogic

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


Provider

UserU_Req

S_Resp

P_Resp

S_Req.bound

*


…

boundaries

System S_Act


9

Applicazione del metodo Formally Grounded Development

all’Automation Frame


Provider

UserU_Req

S_RespP_Resp

S_Req.bound

*


…

boundaries

System S_Act

Requirement

CommandedBehaviour

Sistema Dinamico strutturato

Proprietà sul sistema dinamico strutturato

BusinessLogic

10

• 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

Domain : Specification

Domain Specification 1/5

11

Provider…

User…


…

bound

boundaries

• È 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


Domain Specification : primo sistema strutturato( prima fase )

Torna a pag 19

12

Provider

UserU_Req

S_Resp

P_Resp

S_Req.

System S_Act

• È un sistema dinamico strutturato (sds) chiuso• Le proprietà addizionali sull’ sds costituiscono i requisiti,

quindi il commanded behaviour

INTERAZIONI ELEMENTARI LOCALIDomain Specification 3/5

Domain Specification : secondo sistema strutturato( seconda fase )

Torna a pag 19

13

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


14

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.


15

Requirement : Specification

Provider

UserU_Req

S_Resp

P_Resp

S_Req.

System S_Act

• I requisiti ( Desidered Behaviour) riguardano il sistema strutturato sottostante

• Proprietà circa– Entità automatizzate attive– Interazioni elementari

Requirement Specification 1/2

16

• 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

Requirement Specification 2/2

17

BusinessLogic

Istanziazione del frame:Lotteria Algebrica

L-AL

CommandedBehaviour

Gestore AccessiPosta Elettronica

Gestore CC

Utente1

2

3

4

(**)

(*)

Biglietto, LeggeOrdinamento

DirettoreNotaio

5

Istanziazione 1/2

18

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

Istanziazione 2/2

19

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à

20

D:Direttore? Vincitori : _ -> Sequence(Utenti)? Inizia_Lotteria: Ordinamento x Legge x Nat? Distribuisci_BilOmaggio: Nat? Estrai : -? Manda: String x String

L:LotteriaDim: NatAssegnati: Set(Int)

! Vincitori:Sequence(Utenti)! Inizia_Lotteria: Ordinamento x Legge x Nat! Distribuisci_BilOmaggio: Nat! Estrai

U:UtenteDati: DatiPCarta: DatiCBilOmaggio: 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

Nota: ? Indica che e’ una richiesta (in Uscita)! Una risposta (in Entrata)

FGM applicato alla prima fase

Applicazione FGM : prima fase 1/19

Sottosistemi individuati nel sistema strutturato della prima fase

21

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

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



22

DatiP : Dati Personali DatiC : Dati Carta di Credito

Legge Ordinamento

CdatiP

Ok : CdatiP -> BoolEmail : CdatiP -> String

CdatiC

Ok : CdatiC -> Bool

NuovoNumero : Clegge x Set(Int) x Int -> Int

Clegge

InOrdine : Cordinamento x Int x Int -> Bool

Cordinamento

NotaUsiamo altre strutture dati : Set e Sequence. Le diamo per native


Strutture dati individuate nel sistema strutturato della prima fase

23

Specifica Strutture Dati

Dati PersonaliCostruttore

Definedness 1• def( CdatiP )

Operazione Definedness 3

• def( Email )• def( Ok )

Value 1• If Email = str1 then str1=“_@_”

Op1 & Op2 Definedness 4

• if not def( Email ) then not def( Ok ) Value 2

• If Email() = “” then Ok()=FalseOp & Con

Definedness 4• If not def( CdatiP ) then not def( Ok ) And not def( Email )

Applicazione• Ok( CdatiP ) = True• Email( CdatiP ) = “_@_”

Dati carta di creditoCostruttore

Definedness 1• def( CdatiC )


• def( Ok )Op & Con

Definedness 4• If not def( CdatiC ) then not def( Ok )

Applicazione• Ok( CdatiP ) = True


24


LeggeCostruttore

Definedness 1• def( Clegge )


• def( NuovoNumero( _,_,_ ) )Op & Con

Definedness 4• If not def( Clegge ) then not def( NuovoNumero(_,_) )

OrdinamentoCostruttore

Definedness 1• def( Cordinamento )


• def( InOrdine( _,_,_ ) )Op & Con

Definedness 4• If not def( Clegge ) then not def( NuovoNumero(_,_) )


25

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


26

• 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


27

• 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


28

• 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


29

• 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


30

• 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


31

• 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


32

• 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


33

• 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


34

• 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


35

• 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")}


36

• 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


37

• 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"} )


38

• 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


39

FGM applicato alla seconda fase

Sottosistemi individuati nel sistema strutturato della seconda fase

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

Pt:Posta Elettronica

! Manda: String x String

Gcc:Gestore Carta Credito

! ControllaC: DatiC? ControllataC: DatiC x Bool! Addebita: DatiC x Nat? Addebitato : Bool


Applicazione FGM : seconda fase 1/29

40

Lal : L-AL

Dim: NatDisponibili : Set(Int)Giocatori : Sequence( Codice x DatiP x Chiave x DatiC x Nat )

? 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 Boolx IniziaNuovaLotteria : Ordinamento x Legge x Natx Vincitori : Sequence( DatiP )x DistribuisciBilOmaggio : Natx Estrai : -

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)


41

DatiP : Dati Personali DatiC : Dati Carta di Credito

Legge Ordinamento

CdatiP

Ok : CdatiP -> BoolEmail : CdatiP -> String

CdatiC

Ok : CdatiC -> Bool

NuovoNumero : Clegge x Set(Int) x Int -> Int

Clegge

InOrdine : Cordinamento x Int x Int -> Bool

Cordinamento

NotaUsiamo altre strutture dati : Set e Sequence. Le diamo per native

Identità

CIdentità

Codice

Ccodice

Chiave

Cchiave

Strutture dati individuate nel sistema strutturato della seconda fase


42

Dati PersonaliCostruttore

Definedness 1• def( CdatiP )


• def( Email )• def( Ok )

Value 1• If Email = str1 then str1=“_@_”

Op1 & Op2 Definedness 4

• if not def( Email ) then not def( Ok ) Value 2

• If Email() = “” then Ok()=FalseOp & Con

Definedness 4• If not def( CdatiP ) then not def( Ok ) And not def( Email )

Applicazione• Ok( CdatiP ) = True• Email( CdatiP ) = “_@_”

Dati carta di creditoCostruttore

Definedness 1• def( CdatiC )


• def( Ok )Op & Con

Definedness 4• If not def( CdatiC ) then not def( Ok )

Applicazione• Ok( CdatiP ) = True



43

LeggeCostruttore

Definedness 1• def( Clegge )


• def( NuovoNumero( _,_,_ ) )Op & Con

Definedness 4• If not def( Clegge ) then not def( NuovoNumero(_,_,_) )

OrdinamentoCostruttore

Definedness 1• def( Cordinamento )


• def( InOrdine( _,_,_ ) )Op & Con

Definedness 4• If not def( Cordinamento ) then not def( InOrdine(_,_,_) )


44

ChiaveCostruttore

Definedness 1• def( Cchiave )

CodiceCostruttore

Definedness 1• def( Ccodice )

IdentitàCostruttore

Definedness 1• def( Cidentità )


45

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


46

• 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


47

• 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


48

• 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


49

• 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


50

• 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


51

• 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


52

• 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


53

• 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


54

• 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


if cod=cod1– Registrami(-,-,-) incompatible with


if cod=cod1– AcquistaBil(-,ch,-) incompatible with


if esite g in Giocatori t.c. g.codice=cod1 AND g.chiave = ch


55

• Il sistema non può rispondere a due richieste contemporaneamente né mentre risponde ricevere una richiesta da utente con stessa identità

– Collegato(i1,-,-,-) incompatible withScollegami(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


56

• Il sistema non può rispondere e contemporaneamente richiedere servizi ai provider per un utente con stessa identità

– Collegato(i1,-,-,-) incompatible withControllaU(-,cod1), ControllatoU(-,cod1,-,-), CancellaU(-,cod1), CancellatoU(-,cod1,-)

if cod=cod1– Scollegato(-,ch,-) incompatible with


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


if cod=cod1– BilAcquistato(-,ch,-,-) incompatible with


if esite g in Giocatori t.c. g.codice=cod1 AND g.chiave = ch


57

• 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 withControllatoU(-,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


58

• 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 withIniziaNuovaLotteria(-,-,-), Vincitori(), Estrai(), Manda(-,msg) if msg { "La lotteria è finita" , "Hai vinto" , "La Lotteria è iniziata"}

– Addebitato(-,-,-) incompatible withIniziaNuovaLotteria(-,-,-), 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


59

• 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


60

• 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


61

• 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


62

• 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‘


63

• 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")


64

• 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


65

• 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(-,-)


66

• 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"})


67

• 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


1 Esercitazione I.S. II a.a. 2001/2002 Un Nuovo Frame Chiara Casanova Massimo Ruffa.

Documents

Transcript of 1 Esercitazione I.S. II a.a. 2001/2002 Un Nuovo Frame Chiara Casanova Massimo Ruffa.