11
IntroduzioneIntroduzione
Il presente progetto ha come scopo la Il presente progetto ha come scopo la sperimentazione della composizione sperimentazione della composizione automatica di web services (WS) per automatica di web services (WS) per mezzo della tecnica di mezzo della tecnica di Simulazione, Simulazione, tramite l’uso del tool TLVtramite l’uso del tool TLV. .
22
Scenario applicativoScenario applicativo
Il lavoro si concentra sul particolare Il lavoro si concentra sul particolare scenario applicativo dell’scenario applicativo dell’e-learninge-learning nell’ambito di corsi di laurea della facoltà nell’ambito di corsi di laurea della facoltà di ingegneria di una data università. In di ingegneria di una data università. In particolare si ipotizza l’esistenza di un particolare si ipotizza l’esistenza di un WS per ogni corso di laurea (gestionale, WS per ogni corso di laurea (gestionale, informatica ...), i quali rappresentano la informatica ...), i quali rappresentano la nostra nostra comunitàcomunità dei WS sorgenti. dei WS sorgenti.
33
Focus sulle conversazioni Focus sulle conversazioni
Ogni WS sorgente in un dato momento Ogni WS sorgente in un dato momento dell’interazione col client offre un set dell’interazione col client offre un set limitato di azioni invocabili, nel rispetto dei limitato di azioni invocabili, nel rispetto dei particolari paradigmi di interazione previsti particolari paradigmi di interazione previsti ((conversazioniconversazioni) .) .
44
Transistion system: Un Transistion system: Un modello formale di modello formale di rappresentazione(1/3)rappresentazione(1/3)
Formalmente, le conversazioni con il client Formalmente, le conversazioni con il client supportate da un ws, vengono rappresentati supportate da un ws, vengono rappresentati tramite tramite Transition System (TS),Transition System (TS), diagrammi con diagrammi con un maggiore potere espressivo degli ASF: un maggiore potere espressivo degli ASF:
i TS sono riconoscitori di linguaggi, in grado di i TS sono riconoscitori di linguaggi, in grado di esprimere anche differenze al livello di esprimere anche differenze al livello di comportamento dell’ interazionecomportamento dell’ interazione
55
Transistion system: Un Transistion system: Un modello formale di modello formale di rappresentazione(2/3)rappresentazione(2/3)
66
Transistion system: Un Transistion system: Un modello formale di modello formale di rappresentazione(3/3)rappresentazione(3/3)
Definizione formale di TS:Definizione formale di TS:
77
Composizione via Composizione via Simulazione:il ProblemaSimulazione:il Problema
nn TS sorgenti non deterministici TS sorgenti non deterministici costituenti la comunità. costituenti la comunità.
Avere una composizione dei servizi di comunità, per Avere una composizione dei servizi di comunità, per un TS target t deterministicoun TS target t deterministico, significa disporre di un , significa disporre di un programma che ne “realizzi” il comportamento programma che ne “realizzi” il comportamento coordinando i servizi di comunità in modo opportuno:coordinando i servizi di comunità in modo opportuno:
ogni azione computata sul target t sarà ogni azione computata sul target t sarà automaticamente “delegata” ad uno dei TS di automaticamente “delegata” ad uno dei TS di
comunità.comunità.
88
Composizione via Composizione via Simulazione:Simulazione:il il Community TSCommunity TS• A partire dagli n TS sorgenti possiamo definire il TS A partire dagli n TS sorgenti possiamo definire il TS prodotto asincrono prodotto asincrono (detto (detto community TScommunity TS),), a sua volta a sua volta non deterministico.non deterministico.
99
Composizione via Composizione via Simulazione: Simulazione: definizione di Simulazionedefinizione di Simulazione
Fondamentale nel problema della Composizione Fondamentale nel problema della Composizione automatica di servizi via automatica di servizi via SimulazioneSimulazione è la è la definizione co-induttiva di relazione binaria di definizione co-induttiva di relazione binaria di Simulazione R tra il TS target e il Simulazione R tra il TS target e il community TScommunity TS :
• s è il generico stato del target T;• (q1,..,qn) è il generico stato del community TScommunity TS .
1010
Composizione via Composizione via Simulazione: Simulazione: Esistenza di una composizioneEsistenza di una composizione
Detta Detta RRRR la più grande relazione binaria di la più grande relazione binaria di Simulazione tra il TS target e il Simulazione tra il TS target e il community TScommunity TS ::
TEO1TEO1:: Una composizione dei servizi per Una composizione dei servizi per il il target esiste target esiste se e solo sese e solo se la coppia la coppia
(s°,(q(s°,(q11°,...,q°,...,qnn°)) °)) RRRR.. TEO2TEO2:: Se esiste una composizione dei servizi Se esiste una composizione dei servizi
per il target, ne esiste sempre una di per il target, ne esiste sempre una di dimensione finitadimensione finita..
1111
Composizione via Composizione via Simulazione: Simulazione: Orchestrator Generator OG Orchestrator Generator OG (1/2)(1/2) Se esiste una composizione, da Se esiste una composizione, da RRRR è possibile è possibile
costruire l’costruire l’orchestrator generator orchestrator generator (OG) così (OG) così
definito:definito:
1212
Composizione via Composizione via Simulazione: Simulazione: Orchestrator Generator OG Orchestrator Generator OG (2/2)(2/2)
L’O.G. quando esiste ha sempre L’O.G. quando esiste ha sempre dimensione finita.dimensione finita.
Se l’O.G. esiste, è possibile realizzare il Se l’O.G. esiste, è possibile realizzare il comportamento del target coordinando i comportamento del target coordinando i servizi di comunità.servizi di comunità.
1313
Composizione via Composizione via Simulazione: Simulazione: Orchestratore (1/2)Orchestratore (1/2)
Definiamo orchestratore un programma Definiamo orchestratore un programma P(h,a) = i che prende in input la history P(h,a) = i che prende in input la history “h”, ovvero la sequenza di azioni “h”, ovvero la sequenza di azioni eseguite sul target fino a un dato eseguite sul target fino a un dato momento, e l’azione “a” da eseguire al momento, e l’azione “a” da eseguire al passo successivo sceglie un particolare passo successivo sceglie un particolare sorgente “i” tra quelli che possono sorgente “i” tra quelli che possono computarla dal loro stato attualecomputarla dal loro stato attuale
1414
Composizione via Composizione via Simulazione: Simulazione: Orchestratore (2/2)Orchestratore (2/2)
Conoscendo la history “h” è possibile risalire Conoscendo la history “h” è possibile risalire allo stato attuale del TS target per via del suo allo stato attuale del TS target per via del suo determinismo;determinismo;
Conoscendo l’orchestratore P è possibile Conoscendo l’orchestratore P è possibile sapere il sorgente scelto in ogni istante della sapere il sorgente scelto in ogni istante della history;history;
Tramite P è quindi possibile risalire allo stato Tramite P è quindi possibile risalire allo stato assunto da tutti i TS sorgenti nell’evoluzione assunto da tutti i TS sorgenti nell’evoluzione della history.della history.
Il problema però è che qui l’input h di P non è Il problema però è che qui l’input h di P non è limitato, ma può crescere indefinitamente…limitato, ma può crescere indefinitamente…
1515
L’uso di TLV ci permette di computare L’uso di TLV ci permette di computare l’OG, qualora esista, a partire dalle sole l’OG, qualora esista, a partire dalle sole codifiche codifiche smv smv dei TS sorgenti e target dei TS sorgenti e target
Composizione via Composizione via Simulazione:Simulazione:Tool TLVTool TLV
1616
Tipi di nonTipi di non determinismo determinismo
Il non determinismo riguarda azioni il cui effetto sulle sorgenti non è Il non determinismo riguarda azioni il cui effetto sulle sorgenti non è sotto il controllo del client del target;sotto il controllo del client del target;
A livello delle sorgenti il non determinismo può avere A livello delle sorgenti il non determinismo può avere diversa natura:diversa natura:
DevilishDevilish quando esso si osserva su un particolare sorgente (archi del quando esso si osserva su un particolare sorgente (archi del OG non detOG non det Osservabilità totale) Osservabilità totale)
AngelishAngelish quando esso si osserva solo sul Community TS e non sulle quando esso si osserva solo sul Community TS e non sulle singole sorgentisingole sorgenti
In ogni caso l’OG ha il controllo su tutto ciò che accade a livello della In ogni caso l’OG ha il controllo su tutto ciò che accade a livello della comunità di sorgenti(osservabilità totale) comunità di sorgenti(osservabilità totale)
1717
Scenario ApplicativoScenario Applicativo
Nell’ambito di una università, vengono Nell’ambito di una università, vengono esposti WS per servizi di e-learning per esposti WS per servizi di e-learning per ogni Corso di Laurea limitatamente alla ogni Corso di Laurea limitatamente alla facoltà di Ingegneria facoltà di Ingegneria
Dal punto di vista didattico, il contesto e-Dal punto di vista didattico, il contesto e-learning prevede un’informativa suddivisa learning prevede un’informativa suddivisa in due settori: le video-lezioni e il classico in due settori: le video-lezioni e il classico materiale didattico (dispense).materiale didattico (dispense).
1818
A scopo esemplificativo, mostriamo di A scopo esemplificativo, mostriamo di seguito un possibile activity diagram per seguito un possibile activity diagram per il generico sorgente, limitato,per il generico sorgente, limitato,per semplicità, alle sole funzionalità di login e semplicità, alle sole funzionalità di login e consultazione di video e dispense:consultazione di video e dispense:
Activity DiagramActivity Diagram
1919
LEGENDA
2020
2121
FunzionalitàFunzionalità aggiuntiveaggiuntive
In un tale scenario ogni WS potrebbe esporre In un tale scenario ogni WS potrebbe esporre funzionalità di ricerca e fruizione di video e funzionalità di ricerca e fruizione di video e dispense particolari per il singolo corso di dispense particolari per il singolo corso di laurea, oltre che ricerca di informazioni di laurea, oltre che ricerca di informazioni di carattere generale sull’intera facoltà, quali carattere generale sull’intera facoltà, quali prenotazioni di esami, prenotazioni di esami, prenotazioni in prenotazioni in biblioteca e laboratorio, ricerca di stage, login, biblioteca e laboratorio, ricerca di stage, login, prenotazioni ricevimento professori, prenotazioni ricevimento professori, informazioni sulla segreteria amministrativainformazioni sulla segreteria amministrativa etc.etc.
2222
Sottosistemi comuni a Sottosistemi comuni a tutte le sorgenti (1/2)tutte le sorgenti (1/2)
Sottosistema prenotazione esami / ricevimento Professori
listDegreeCourses
listCourseslistExams
reserveAppointment
reserveExam
listTeacher NX_7_5
NX_7_4NX_7_2
NX_7_3
NX_1
2323
Sottosistemi comuni a Sottosistemi comuni a tutte le sorgenti (2/2)tutte le sorgenti (2/2)
Sottosistemi richiesta informazioni segreteria amministrativa, gestione profilo utente e richiesta informazioni biblioteche:
infoAdmSecr
infoLoginoverwriteData
listLibrariesinfoLibrary
2424
Available ServicesAvailable Services
I TS sorgenti previsti sono – nel nostro I TS sorgenti previsti sono – nel nostro caso – i seguenti sette:caso – i seguenti sette:
1.1. Informatica , “S1”Informatica , “S1”
2.2. Elettronica, “S2” Elettronica, “S2”
3.3. Gestionale, “S3”Gestionale, “S3”
4.4. Log-in, “S4”Log-in, “S4”
5.5. Edile, “S5”Edile, “S5”
6.6. Chimica, “S6”Chimica, “S6”
7.7. Elettrica, “S8”Elettrica, “S8”
2525
TS Informatica – S1TS Informatica – S1
N1_2
searchVideoByProgram_1
searchVideoByProgram_1
searchVideoByAuthor_1
searchVideoByAuthor_1
N1_3
searchPaperByProgram_1
N1_1
searchPaperByAuthor_1
searchPaperByAuthor_1
S7
searchPaperByProgram_1
readPaper_1
N1_7 N1_8 searchVideoByAuthor_1 watchLesson_1
searchPaperByAuthor_1
readPaper_1
N1_6
watchLesson_1
Output T5_a
2626
Pattern per la simulabilità del Target Pattern per la simulabilità del Target (1/2)(1/2)
searchVideo
ByAuthor_1 watchLesson_1searchPaper
ByAuthor_1readPaper_1
…
il primo, il terzo e il quinto stato sono opzionalmente finaliil primo, il terzo e il quinto stato sono opzionalmente finali
il secondo e il quarto stato sono obbligatoriamente non finaliil secondo e il quarto stato sono obbligatoriamente non finali
una volta eseguita l’azione “searchVideoByAuthor_1”, il target, una volta eseguita l’azione “searchVideoByAuthor_1”, il target, limitatamente alle azioni di esclusiva competenza di S1limitatamente alle azioni di esclusiva competenza di S1,, deve invocare le azioni mostrate rispettandone l’ordine, deve invocare le azioni mostrate rispettandone l’ordine, fermandosi eventualmente al terzo stato se finalefermandosi eventualmente al terzo stato se finale
2727
Pattern per la simulabilità del Target Pattern per la simulabilità del Target (2/2)(2/2)
searchVideo
ByAuthor_1 watchLesson_1searchPaper
ByAuthor_1readPaper_1
…
Non è quindi accettabile nessuna aggiunta o sostituzioneNon è quindi accettabile nessuna aggiunta o sostituzionedi azioni, infatti:di azioni, infatti:
sostituendo l’azione del pattern “searchPaperByAuthor_1” con sostituendo l’azione del pattern “searchPaperByAuthor_1” con “searchPaperByProgram_1”,“searchPaperByProgram_1”,
aggiungendo l’azione “searchPaperByProgram_1” in parallelo a aggiungendo l’azione “searchPaperByProgram_1” in parallelo a “searchPaperByAuthor_1”,“searchPaperByAuthor_1”,
inserendo un cappio con una azione di esclusiva competenza di S1 inserendo un cappio con una azione di esclusiva competenza di S1 in uno qualsiasi dei nodi costituenti il pattern,in uno qualsiasi dei nodi costituenti il pattern,
etc etc,etc etc,
si otterrebbe 1 target non simulabile.si otterrebbe 1 target non simulabile.
2828
TS Elettronica – S2TS Elettronica – S2
searchVideoByProgram_2
watchLesson_2
N2_3
searchVideoByProgram_2
searchPaperByProgram_2
searchPaperByProgram_2
readPaper_2
S7
N2_1
watchLesson_2
searchPaperByProgram_2
N2_2
Output T1_3Output T2_a
2929
Pattern per la simulabilità del Target Pattern per la simulabilità del Target (1/2)(1/2)
il primo, il secondo e lo stato che segue l’azione il primo, il secondo e lo stato che segue l’azione “searchVideoByProgram_2” sono opzionalmente finali“searchVideoByProgram_2” sono opzionalmente finali
lo stato che segue l’azione “searchPaperByProgram_2” è lo stato che segue l’azione “searchPaperByProgram_2” è obbligatoriamente non finaleobbligatoriamente non finale
una volta eseguita l’azione “watchLesson_2”, una volta eseguita l’azione “watchLesson_2”, limitatamente limitatamente alle azioni di esclusiva competenza di S2alle azioni di esclusiva competenza di S2,, il target può il target può invocare esclusivamente quelle mostrate rispettandone l’ordine, invocare esclusivamente quelle mostrate rispettandone l’ordine, o in alternativa fermarsi in uno stato opzionalmente finale. o in alternativa fermarsi in uno stato opzionalmente finale.
watchLesson_2 searchPaperByProgram_2
…
searchVideo
ByProgram_2
…
…
3030
Pattern per la simulabilità del Target Pattern per la simulabilità del Target (2/2)(2/2)
Non è quindi accettabile nessuna aggiunta o sostituzione Non è quindi accettabile nessuna aggiunta o sostituzione di azioni,di azioni,
infatti:infatti: eseguendo l’azione “watchLesson_2” due volte di seguito,eseguendo l’azione “watchLesson_2” due volte di seguito, inserendo un cappio con una azione di competenza di S2 in inserendo un cappio con una azione di competenza di S2 in
uno qualsiasi dei nodi costituenti il pattern,uno qualsiasi dei nodi costituenti il pattern, etc etc,etc etc,
si otterrebbe 1 target non simulabile.si otterrebbe 1 target non simulabile.
watchLesson_2 searchPaperByProgram_2
…
searchVideo
ByProgram_2
…
…
3131
TS Gestionale – S3TS Gestionale – S3
N3_2
readPaper_3
searchPapersByCourseYear_3
searchPapersByAuthor_3
searchPapersByProgram_3
searchPapersByCourseYear_3
searchPapersByAuthor_3
searchPapersByProgram_3
S7N3_1
N3_6N3_5
listAllUsers
listPC
listLaboratories
reservePC
Output T1_6
3232
TS Login – S4TS Login – S4
N4_3
N4_2
Reg-KO
reg
Login-KO
login
login
Login-KO
N4_1
logout
3333
TS Edile – S5TS Edile – S5
readPaper_5
searchVideoByLesson_5
watchLesson_5
searchVideoByLesson_5
searchPaperByLesson_5
searchCourse_5
searchCourse_5
searchCourse_5
infoCourse_5
searchCourse_5
searchPaperByLesson_5S7
N5_1
N5_3N5_2
N5_4
searchStage
N5_5
infoStage
searchStage
Output T1_2
3434
TS Chimica – S6TS Chimica – S6
N6_4searchCourse_6
infoProgr_6
searchCourse_6
infoCourse_6
searchPapersByLesson_6
searchPapersByLesson_6
readPap_6
searchCourse_6
searchVideoByLesson_6
searchVideoByLesson_6
watchLes_6
searchCourse_6
searchTeacher_6
infoTeacher_6 S7
sear
chTe
acher
_6
N6_2 info
Teac
her
_6
sear
chSta
ge_6
info
Stage_6
N6_5
N6_6
N6_7
N6_8
N6_1
N6_3
searchStage
infoStage
InfoStage
Output T1_2
3535
Note sul non determinismo di infoStageNote sul non determinismo di infoStage
Il non determinismo dell’azione “infoStage” qui è molto pericoloso, perché se fossimo in un contesto in cui “searchStage” ed “infoStage” comparissero solo in S6 (come “searchStage_6” ed “infoStage_6”) questo comporterebbe che mai in un target risulterebbe realizzabile il comportamento naturale :
Tale interazione invece è sempre simulabile grazie al sorgente S5, nel quale l’azione “infoStage” è deterministica.
L’ OrchestratorGenerator quando a run-time riceve l’azione “searchStage”(e successivamente l’azione “infoStage”), sceglierà sempre di mapparla su S5.
3636
TS Elettrica – S8TS Elettrica – S8
readPaper_8
searchVideoByLesson_8
watchLesson_8
searchVideoByLesson_8
searchPaperByLesson_8
searchCourse_8
searchCourse_8
searchCourse_8
infoCourse_8
searchPaperByLesson_8S7
N8_1
N8_5
N8_2
N8_3
N8_4
listAllUsers
listAllUsers
listLaboratories
listPC
reservePC
N8_8
N8_9N8_10
Output T1_6
3737
CONSIDERAZIONI SULLA SIMULABILITA’ CONSIDERAZIONI SULLA SIMULABILITA’ DEL TARGET:DEL TARGET:
Le azioni “listAllUsers”, “listLaboratories”, “listPC” e “reservePC” sono Le azioni “listAllUsers”, “listLaboratories”, “listPC” e “reservePC” sono offerte sia da S8 che da S3. Nel caso di un target che preveda il ramo di offerte sia da S8 che da S3. Nel caso di un target che preveda il ramo di seguito riportatoseguito riportato
l’Orchestrator Generator effettua le sue scelte a run-time : inizialmente si l’Orchestrator Generator effettua le sue scelte a run-time : inizialmente si troverà a dover scegliere se computare l’azione listAllUsers su S3 o su troverà a dover scegliere se computare l’azione listAllUsers su S3 o su S8; se sceglie S3 è obbligato a continuare a scegliere S3 per le prossime S8; se sceglie S3 è obbligato a continuare a scegliere S3 per le prossime 3 azioni previste; se sceglie S8 è interessante evidenziare che l’OG 3 azioni previste; se sceglie S8 è interessante evidenziare che l’OG necessità di necessità di osservarne osservarne lo stato raggiunto: se esso è lo stato N8_1, l’OG lo stato raggiunto: se esso è lo stato N8_1, l’OG è obbligato a scegliere S3 per le prossime tre azioni previste; se invece è obbligato a scegliere S3 per le prossime tre azioni previste; se invece S8 raggiunge lo stato N8_8 l’OG continuerà a mappare le prossime azioni S8 raggiunge lo stato N8_8 l’OG continuerà a mappare le prossime azioni su S8 poichè, per quanto espresso dalla definizione di Simulabilità, se il su S8 poichè, per quanto espresso dalla definizione di Simulabilità, se il target si trova in uno stato finale anche tutte le sorgenti devono stare in target si trova in uno stato finale anche tutte le sorgenti devono stare in uno stato finale. uno stato finale.
listAllUsers listLaboratories listPC
reservePC
3838
TRANSITION SYSTEM TRANSITION SYSTEM TARGETTARGET
3939
TS TARGET “T1” (1/10)TS TARGET “T1” (1/10)
Consente di ottenere informazioni trasversali Consente di ottenere informazioni trasversali su tutti i corsi di laurea offerti dalla facoltà, su tutti i corsi di laurea offerti dalla facoltà, attraverso percorsi che flessibilmente attraverso percorsi che flessibilmente possono essere intrapresi dal client a possono essere intrapresi dal client a seconda delle proprie esigenze. seconda delle proprie esigenze.
Per leggibilità seguono rappresentazioni Per leggibilità seguono rappresentazioni grafiche (T1.1, T1.2, T1.3, T1.4, T1.5, T1.6) grafiche (T1.1, T1.2, T1.3, T1.4, T1.5, T1.6) di di T1 T1 raffiguranti sottoparti dell’intero TS raffiguranti sottoparti dell’intero TS target tutte aventi in comune lo stato finale target tutte aventi in comune lo stato finale NT1_1.NT1_1.
4040
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_1 - Sottosistema T1_1 - (2/10) (2/10)
watchLes_5
NT1_8
watchLes_1
searchCourse_5
infoCourse_5
searchPapByLes_5
readPap_5
searchVideoByLes_5
searchPapByProgr_1
readPap_1
searchVideoByProgr_1
searchCourse_5
NT1_1
NT1_4
NT1_2 NT1_3
NT1_7
NT1_6
NT1_5
Reg-KO
reg
Login-KO
login
login Login-KO
NT1_L_1 NT1_L_2
NT1_24
searchCourse_5
logout
4141
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_2 - Sottosistema T1_2 - (3/10) (3/10)
searchPapersByCourseYear_3
searchCourse_6
watchLesson_6
readPaper_3
searchPapersByProgram_3
searchPapersByAuthor_3
searchPapersByProgram_3
searchPapersByCourseYear_3
searchVideoByLesson_6
readPap_6
searchPapersByLesson_6
searchCourse_6
infoCourse_6
NT1_1
NT1_9
NT1_10
NT1_12
NT1_13
NT1_11
searchStage
infoStage
NT1_23
NT1_25
searchCourse_6
Output T1_2
4242
Relativamente al non-determinismo dei Relativamente al non-determinismo dei
sorgenti:sorgenti:
T1.2 cattura il non determinismo dell’azione T1.2 cattura il non determinismo dell’azione infoStage in S6, ed è simulabile grazie alla infoStage in S6, ed è simulabile grazie alla presenza della stessa azione nel sorgente S5.presenza della stessa azione nel sorgente S5.
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_2 - Sottosistema T1_2 - (4/10)(4/10)
4343
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_3 - Sottosistema T1_3 - (5/10) (5/10)
watchLes_2
searchPapByProgr_2
readPap_2
searchVideoByProgr_2
searchPapByProgr_2
NT1_1
NT1_14
NT1_15
NT1_16
Output T1_3
4444
Relativamente al non-determinismo dei Relativamente al non-determinismo dei
sorgenti:sorgenti:
T1.3 cattura il non determinismo dell’azione T1.3 cattura il non determinismo dell’azione watchLesson_2 in S2,ed è simulabile perchè watchLesson_2 in S2,ed è simulabile perchè rispetta il pattern di S2.rispetta il pattern di S2.
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_3 - Sottosistema T1_3 - (6/10)(6/10)
4545
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_4 - Sottosistema T1_4 - (7/10)(7/10)
listDegreeCourses
listCourses
listExams
reserveExam
NT1_1
NT1_17 NT1_18
NT1_19
Output T1_4
4646
TS TARGET “T1” STS TARGET “T1” Sottosistema T1_5 - ottosistema T1_5 - (8/10)(8/10)
infoLibraries
listLibraries
overwriteData
infoAdmSecr
infoLoginNT1_1
NT1_21
NT1_22
Output T1_5
4747
TS TARGET “T1” STS TARGET “T1” Sottosistema T1_6 -ottosistema T1_6 -(9/10)(9/10)
NT1_1
searchCourse_8
searchPaperByLesson_8 readPaper_8
searchVideoByLesson_8
watchLesson_8
listAllUsers
listLaboratories listPC
reservePC
NT1_26NT1_27
NT1_28
NT1_29
NT1_30NT1_31 NT1_32
Output T1_6
4848
Relativamente al non-determinismo dei Relativamente al non-determinismo dei
sorgenti:sorgenti:
T1.6 cattura il non determinismo dell’azione T1.6 cattura il non determinismo dell’azione listAllUsers in S8 e usufruisce di azioni in listAllUsers in S8 e usufruisce di azioni in comune tra S3 e S8 forzando l’OG ad comune tra S3 e S8 forzando l’OG ad osservare lo stato corrente dei TS sorgenti.osservare lo stato corrente dei TS sorgenti.
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_6 - Sottosistema T1_6 - (10/10)(10/10)
4949
TS TARGET “T2a” (1/3)TS TARGET “T2a” (1/3)
Progettato per la consultazione a Progettato per la consultazione a cascata di tutte le informazioni di cascata di tutte le informazioni di interesse relative ai soli corsi di laurea interesse relative ai soli corsi di laurea di informatica ed elettronica. di informatica ed elettronica.
Non si lascia totale flessibilità di Non si lascia totale flessibilità di consultazione all’utente in quanto lo consultazione all’utente in quanto lo scopo di T2a è quello di guidarlo in una scopo di T2a è quello di guidarlo in una analisi comparativa delle offerte analisi comparativa delle offerte formative secondo un ordine prefissato formative secondo un ordine prefissato di esplorazione di corsi di laurea .di esplorazione di corsi di laurea .
5050
TS TARGET “T2a” (2/3)TS TARGET “T2a” (2/3)
searchPapers
ByProgram_1readPapers_1
searchVideo
ByProgram_1watchLesson_1
searchVideo
ByProgram_1
searchVideo
ByProgram_1
searchPapers
ByProgram_1
searchPapers
ByProgram_1
searchPaperByProgram_2
searchPaperByProgram_2
readPaper_2
searchVideoByProgram_2
searchVideoByProgram_2
watchLesson_2
NT2a_6
NT2a_7
NT2a_8
NT2a_1
NT2a_2NT2a_3
NT2a_4
NT2a_5
searchVideoByProgram_2
searchPaperByProgram_2
Reg-KO
reg
Login-KO
login
loginLogin-KO
NT2a_L_1NT2a_L_2
logout
logout
NT2a_9
Output T2_a
5151
TS TARGET “T2a” (3/3)TS TARGET “T2a” (3/3)
Riguardo al non determinismo dei sorgenti:Riguardo al non determinismo dei sorgenti:
Esercita il non determinismo dell’azione Esercita il non determinismo dell’azione watchLesson_2 di S2 ed è simulabile watchLesson_2 di S2 ed è simulabile grazie alla sua aderenza al pattern grazie alla sua aderenza al pattern previsto per tale sorgente.previsto per tale sorgente.
5252
TS TARGET “T2b” (1/2)TS TARGET “T2b” (1/2)
searchPapers
ByProgram_1readPapers_1
searchVideo
ByProgram_1watchLesson_1
searchVideo
ByProgram_1
searchVideo
ByProgram_1
searchPapers
ByProgram_1
searchPapers
ByProgram_1
searchPaperByProgram_2
searchPaperByProgram_2
readPaper_2
searchVideoByProgram_2
searchVideoByProgram_2
watchLesson_2
NT2b_6
NT2b_7
NT2b_8
NT2b_9
NT2b_1
NT2b_2NT2b_3
NT2b_4
NT2b_5
searchVideoByProgram_2
searchPaperByProgram_2
login
Login-KO
NT2b_L_1 NT2b_L_2
watchLesson_2
Non prevista dal pattern!
Reg-KO
Login-KO login
logout
logout
reg
5353
TS TARGET “T2b” (2/2)TS TARGET “T2b” (2/2)
Riguardo al non determinismo dei sorgenti:Riguardo al non determinismo dei sorgenti:
Esercita il non determinismo dell’azione Esercita il non determinismo dell’azione watchLesson_2 di S2 e non è watchLesson_2 di S2 e non è simulabile poichè non aderente al simulabile poichè non aderente al pattern previsto per tale sorgente (TLV pattern previsto per tale sorgente (TLV restituisce “restituisce “specification isspecification is unrealizable”unrealizable”).).
5454
TS TARGET “T5a” (1/3)TS TARGET “T5a” (1/3)
Progettato per la consultazione a Progettato per la consultazione a cascata di tutte le informazioni di cascata di tutte le informazioni di interesse relative ai soli corsi di laurea interesse relative ai soli corsi di laurea di informatica e elettronica. di informatica e elettronica.
Non si lascia totale flessibilità di Non si lascia totale flessibilità di consultazione all’utente in quanto lo consultazione all’utente in quanto lo scopo di T5a è quello di guidarlo in una scopo di T5a è quello di guidarlo in una analisi comparativa delle offerte analisi comparativa delle offerte formative secondo un ordine prefissato formative secondo un ordine prefissato di esplorazione di corsi di laurea .di esplorazione di corsi di laurea .
5555
TS TARGET “T5a” (2/3)TS TARGET “T5a” (2/3)
searchVideo
ByAuthor_1
watchLesson_1searchPaper
ByAuthor_1readPaper_1
searchPaperByProgram_2
searchPaperByProgram_2
readPaper_2
NT5a_6
NT5a_7
NT5a_1
NT5a_2NT5a_3
NT5a_4
NT5a_5
searchPaperByProgram_2
Reg-KO
reg
Login-KO
loginlogin
Login-KO
NT5a_L_1NT5a_L_2
logout
logout
Output T5_a
5656
TS TARGET “T5a” (3/3)TS TARGET “T5a” (3/3)
Riguardo al non determinismo dei sorgenti:Riguardo al non determinismo dei sorgenti:
Esercita il non determinismo dell’azione Esercita il non determinismo dell’azione “searchVideoByAuthor_1” di S1 ed è “searchVideoByAuthor_1” di S1 ed è simulabile grazie alla sua aderenza al simulabile grazie alla sua aderenza al pattern previsto per tale sorgente.pattern previsto per tale sorgente.
5757
TS TARGET “T5b” (1/2)TS TARGET “T5b” (1/2)
searchVideo
ByAuthor_1watchLesson_1
searchPaper
ByProgram_1readPaper_1
searchPaperByProgram_2
searchPaperByProgram_2
readPaper_2
NT5b_6
NT5b_7
NT5b_1
NT5b_2NT5b_3
NT5b_4
NT5b_5
searchPaperByProgram_2
Reg-KO
reg
Login-KO
loginlogin
Login-KO
NT5b_L_1 NT5b_L_2
Non prevista dal pattern!
logout
logout
5858
TS TARGET “T5b” (2/2)TS TARGET “T5b” (2/2)
Riguardo al non determinismo dei sorgenti:Riguardo al non determinismo dei sorgenti:
Esercita il non determinismo dell’azione Esercita il non determinismo dell’azione “searchVideoByAuthor_1” di S1 e non è “searchVideoByAuthor_1” di S1 e non è simulabile in quanto non aderente al simulabile in quanto non aderente al pattern previsto per tale sorgente (TLV pattern previsto per tale sorgente (TLV restituisce “restituisce “Specification is Specification is unrealizable”unrealizable”).).
5959
ANALISI DELL’OUTPUT ANALISI DELL’OUTPUT TLVTLV
6060
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_1 Sottosistema T1_1
NOME FILE:
T1_1.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 20
NUM. TRANSIZIONI OG: 46
TEMPO CPU: 0.11 sec
6161
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_2 Sottosistema T1_2 - (1/2) - (1/2)
NOME FILE:
T1_2.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 18
NUM. TRANSIZIONI OG: 58
TEMPO CPU: 0.11 sec
6262
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_2 Sottosistema T1_2 - (2/2) - (2/2)
L’OG, per l’esecuzione dell’azione L’OG, per l’esecuzione dell’azione “searchStage”, seleziona esclusivamente il “searchStage”, seleziona esclusivamente il sorgente S5. Difatti, graficando le transizioni sorgente S5. Difatti, graficando le transizioni dell’OG, si ottiene quanto segue:dell’OG, si ottiene quanto segue:
Action = SSIndex=5
T1_2.loc = 0S5.loc = 0
Action = ISIndex=5
T1_2.loc = 22S5.loc = 4
3 18
S5 S6T1_2
6363
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_3 Sottosistema T1_3 – (1/3)– (1/3)
NOME FILE:
T1_3.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 7
NUM. TRANSIZIONI OG: 11
TEMPO CPU: 0.1 sec
6464
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_3 - Sottosistema T1_3 - (2/3)(2/3)
Il target T1_3 esercita il non determinismo dell’azione Il target T1_3 esercita il non determinismo dell’azione “watchLesson_2” di S2. L’O.G. ottenuto dalla “watchLesson_2” di S2. L’O.G. ottenuto dalla computazione di TLV tratta questa caratteristica negli computazione di TLV tratta questa caratteristica negli stati corrispondenti, restituendo il seguente output:stati corrispondenti, restituendo il seguente output:
T1_3 S2
Action = WL_2T2_a.loc = 15
S2.loc = 1
Action = SPP_2T2_a.loc = 0S2.loc = 0
Action = RP_2T2_a.loc = 13
S2.loc = 2
Action = SPP_2T2_a.loc = 0S2.loc = 1
Action = SPP_2T2_a.loc = 13
S2.loc = 2
6
2
7
4
3
6565
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_3 - Sottosistema T1_3 - (3/3)(3/3)
Rappresentando l’OG in quest’ultima forma, è Rappresentando l’OG in quest’ultima forma, è evidente come le uniche transizioni non evidente come le uniche transizioni non deterministiche siano quelle relative all’azione deterministiche siano quelle relative all’azione “watchLesson_2” (evidenziata in rosso).“watchLesson_2” (evidenziata in rosso).
Per meglio evidenziare l’invocazione dell’azione non Per meglio evidenziare l’invocazione dell’azione non deterministica, possiamo intervenire nella sintassi deterministica, possiamo intervenire nella sintassi grafica sopra utilizzata ottenendo le seguenti grafica sopra utilizzata ottenendo le seguenti transizioni: transizioni:
T2_a.loc = 15S2.loc = 1
T2_a.loc = 0S2.loc = 0
T2_a.loc = 13S2.loc = 2
T2_a.loc = 0S2.loc = 1
Action = WL_2
Action = WL_2
Action = SPP_2
Action = SPP_2
6666
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_4 Sottosistema T1_4 – (1/2)– (1/2)
NOME FILE:
T1_4.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 25
NUM. TRANSIZIONI OG: 60
TEMPO CPU: 0.1 sec
6767
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_4 Sottosistema T1_4 – (2/2)– (2/2)
L’alto numero di transizioni in uscita dagli stati L’alto numero di transizioni in uscita dagli stati mostrati è dovuto all’alto grado di non determinismo mostrati è dovuto all’alto grado di non determinismo angelico dell’azione listDegreeCourses angelico dell’azione listDegreeCourses
T1_4
6868
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_5 Sottosistema T1_5 – (1/2)– (1/2)
NOME FILE:
T1_5.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 31
NUM. TRANSIZIONI OG: 354
TEMPO CPU: 0.1 sec
6969
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_5 Sottosistema T1_5 – (2/2)– (2/2)
L’alto numero di transizioni in uscita dagli stati mostrati è dovuto L’alto numero di transizioni in uscita dagli stati mostrati è dovuto all’alto grado di non determinismo angelico delle azioni all’alto grado di non determinismo angelico delle azioni infoLogin, listLibraries, infoAdmSecrinfoLogin, listLibraries, infoAdmSecr
T1_5
7070
TS TARGET “T1” Sottosistema T1_6 TS TARGET “T1” Sottosistema T1_6 – (1/3)– (1/3)
NOME FILE:
T1_6.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 14
NUM. TRANSIZIONI OG: 23
TEMPO CPU: 0.11 sec
7171
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_6 - Sottosistema T1_6 - (2/3)(2/3)
Il target T1_6 esercita il non determinismo dell’azione Il target T1_6 esercita il non determinismo dell’azione “listAllUsers” di S8 ed S3. Utilizza inoltre le azioni “listAllUsers” di S8 ed S3. Utilizza inoltre le azioni “listLaboratories”, “listPC”, “reservePC” comuni a S3 e S8 “listLaboratories”, “listPC”, “reservePC” comuni a S3 e S8 stesso. L’O.G. ottenuto dalla computazione di TLV tratta questa stesso. L’O.G. ottenuto dalla computazione di TLV tratta questa caratteristica negli stati corrispondenti, restituendo il seguente caratteristica negli stati corrispondenti, restituendo il seguente output:output:
T1_6 S3
Action = LAUT1_6.loc = 0S3.loc = 0S8.loc = 0Index = 3
Action = LLT1_6.loc = 29
S3.loc = 0S8.loc = 0Index = 3
Action = LAUT1_6.loc = 0S3.loc = 0S8.loc = 0Index = 8
4
5
38
Action = LLT1_6.loc = 29
S3.loc = 0S8.loc = 7Index = 8
6
9
S8
7272
TS TARGET “T1” TS TARGET “T1” Sottosistema T1_6 - Sottosistema T1_6 - (3/3)(3/3)
Come evidenziato dalla rappresentazione Come evidenziato dalla rappresentazione sottostante, l’OG – qualora mappi l’azione sottostante, l’OG – qualora mappi l’azione listAllUsers (L.A.U.) su S8 - è forzato ad listAllUsers (L.A.U.) su S8 - è forzato ad osservarneosservarne lo stato di arrivo per poter scegliere su chi mappare lo stato di arrivo per poter scegliere su chi mappare la successiva azione “listLaboratories”.la successiva azione “listLaboratories”.
T1_6.loc = 29S3.loc = 0S8.loc = 0
T1_6.loc = 0S3.loc = 0S8.loc = 0
Action = LAU / 3 {3,8}
T1_6.loc = 29S3.loc = 0S8.loc = 7
Action = LAU / 8 {3,8}
Action = LAU / 8 {3,8}
Action = listLaboratories / 3 {3}
Action = listLaboratories / 8 {8}
7373
TS TARGET “T2_a” TS TARGET “T2_a” – (1/3)– (1/3)
NOME FILE:
T2_a.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 43
NUM. TRANSIZIONI OG: 106
TEMPO CPU: 0.12 sec
7474
TS TARGET “T2_a” TS TARGET “T2_a” - (2/3)- (2/3)
Il target T2_a esercita il non determinismo dell’azione Il target T2_a esercita il non determinismo dell’azione “watchLesson_2” di S2. L’O.G. ottenuto dalla “watchLesson_2” di S2. L’O.G. ottenuto dalla computazione di TLV tratta questa caratteristica negli computazione di TLV tratta questa caratteristica negli stati corrispondenti, restituendo il seguente output:stati corrispondenti, restituendo il seguente output:
Action = SVP_2T2_a.loc = 8S2.loc = 0S4.loc = 1
Action = WL_2T2_a.loc = 7S2.loc = 1S4.loc = 1
Action = SVP_2T2_a.loc = 8S2.loc = 1S4.loc = 1
21
22
23
Action = logoutT2_a.loc = 8S2.loc = 0S4.loc = 0
Action = logoutT2_a.loc = 8S2.loc = 1S4.loc = 0
24
25
7575
TS TARGET “T2_a” TS TARGET “T2_a” - (3/3)- (3/3)
Per meglio evidenziare l’invocazione dell’azione non Per meglio evidenziare l’invocazione dell’azione non deterministica, possiamo intervenire nella sintassi deterministica, possiamo intervenire nella sintassi grafica sopra utilizzata ottenendo le seguenti grafica sopra utilizzata ottenendo le seguenti transizioni: transizioni:
T2_a S2
T2_a.loc = 7S2.loc = 1S4.loc = 1
T2_a.loc = 8S2.loc = 0S4.loc = 1
T2_a.loc = 8S2.loc = 1S4.loc = 1
Action = WL_2
Action = WL_2
Action = SVP_2
Action = SVP_2
7676
TS TARGET “T2_b”TS TARGET “T2_b”
NOME FILE:
T2_b.smv
RISULTATO ATTESO: Composizione non esistente
RISULTATO OTTENUTO: Composizione non esistente
NUM. STATI OG: -
NUM. TRANSIZIONI OG: -
TEMPO CPU: 0.12 sec
La rottura del La rottura del pattern pattern previsto per S2 fa si previsto per S2 fa si che TLV restituisca che TLV restituisca Specification is Specification is unrealizableunrealizable . .
7777
TS TARGET “T5_a” TS TARGET “T5_a” – (1/3)– (1/3)
NOME FILE:
T5a.smv
RISULTATO ATTESO: composizione esistente
RISULTATO OTTENUTO: composizione esistente
NUM. STATI OG: 20
NUM. TRANSIZIONI OG: 44
TEMPO CPU: 0.11 sec
7878
TS TARGET “T5_a” TS TARGET “T5_a” - (2/3)- (2/3)
Il target T5_a esercita il non determinismo dell’azione Il target T5_a esercita il non determinismo dell’azione “searchVideoByAuthor_1” di S1. L’O.G. ottenuto “searchVideoByAuthor_1” di S1. L’O.G. ottenuto dalla computazione di TLV tratta questa caratteristica dalla computazione di TLV tratta questa caratteristica negli stati corrispondenti, restituendo il seguente negli stati corrispondenti, restituendo il seguente output:output:
Action = SVA_1T5_a.loc = 0S1.loc = 0
Action = WL_1T5_a.loc = 1S1.loc = 1
Action = WL_1T5_a.loc = 1S2.loc = 5
6
8
9
10
17
7979
TS TARGET “T5_a” TS TARGET “T5_a” - (3/3)- (3/3)
Per meglio evidenziare l’invocazione dell’azione non Per meglio evidenziare l’invocazione dell’azione non deterministica, possiamo intervenire nella sintassi deterministica, possiamo intervenire nella sintassi grafica sopra utilizzata ottenendo le seguenti grafica sopra utilizzata ottenendo le seguenti transizioni: transizioni:
T5_a S1
T5_a.loc = 0S1.loc = 0
T5_a.loc = 1S1.loc = 1
T5_a.loc = 1S2.loc = 5
6
8
9
10
17
Action = SVA_1
Action = SVA_1Action = WL_1
Action = WL_1
8080
TS TARGET “T5_b”TS TARGET “T5_b”
NOME FILE:
T5b.smv
RISULTATO ATTESO: Composizione non esistente
RISULTATO OTTENUTO: Composizione non esistente
NUM. STATI OG: -
NUM. TRANSIZIONI OG: -
TEMPO CPU: 0.1 sec
La rottura del La rottura del pattern pattern previsto per S1 fa si previsto per S1 fa si che TLV restituisca che TLV restituisca Specification is Specification is unrealizableunrealizable . .
Top Related