|
Wiki
UniCrema
Materie per semestre
Materie per anno
Materie per laurea
Help
|
|
Uni.ASM History
Hide minor edits - Show changes to output
Changed lines 167-171 from:
''Figura presa dalle slide del corso''
Questo è l'albero delle funzioni ASM, si può osservare che le funzioni Dynamic possiedono più tipi di sotto-funzioni, diamone una breve descrizione: to:
''Figura presa dalle slide del corso''\\\
Questo è l'albero delle funzioni ASM, si può osservare che le funzioni '''Dynamic''' possiedono più tipi di sotto-funzioni, diamone una breve descrizione:
Changed lines 124-125 from:
Ci sono diversi costruttori i quali consentono di far aggiornare lo stato attuale della macchina e sono: \\ to:
Ci sono diversi costruttori i quali consentono di far aggiornare lo stato attuale della macchina e sono: \\\ Added line 168:
Added line 42:
Added line 50:
Added line 190:
Added line 192:
Added line 2:
Changed line 8 from:
Ove non meglio specificato, tutti i testi tra virgolette vanno intesi come citazioni letterali dalle slide della prof [[RiccobeneElviniaMaria]], 2010. to:
Ove non meglio specificato, tutti i testi tra virgolette vanno intesi come citazioni letterali dalle slide della prof [[Riccobene Elvinia Maria]], 2010. Added line 193:
[[#su|[-'''Torna su'''-]]]
Changed lines 56-59 from:
Per concludere si può dire che un' ASM è una macchina a stati finiti con memoria, le cui transizioni possono far cambiare valore alla cella utilizzata per memorizzare gli stati. \\ to:
Per concludere si può dire che un' ASM è una macchina a stati finiti con memoria, le cui transizioni possono far cambiare valore alla cella utilizzata per memorizzare gli stati. \\\ Changed lines 83-85 from:
''“Fissato un vocabolario '''Σ''', uno stato '''A''' del vocabolario è un insieme non vuoto X, detto '''super-universo di A''', con le interpretazioni dei nomi delle funzioni di Σ”.'' to:
''“Fissato un vocabolario '''Σ''', uno stato '''A''' del vocabolario è un insieme non vuoto X, detto '''super-universo di A''', con le interpretazioni dei nomi delle funzioni di Σ”.''\\\ Changed lines 103-105 from:
Grazie a questa proprietà è possibile operare su domini eterogenei, dove l'utente può definirne altri di base (domini enumerativi, astratti, ecc) oppure a partire da altri domini esistenti, formando domini strutturati.\\ to:
Grazie a questa proprietà è possibile operare su domini eterogenei, dove l'utente può definirne altri di base (domini enumerativi, astratti, ecc) oppure a partire da altri domini esistenti, formando domini strutturati.\\\ Changed lines 115-118 from:
* ''Se f è una funzione n-aria di Σ e t1, t2, … tn sono termini, allora f(t1, t2, … tn) è un termine.”'' to:
* ''Se f è una funzione n-aria di Σ e t1, t2, … tn sono termini, allora f(t1, t2, … tn) è un termine.”''\\\ Added line 160:
Changed lines 163-165 from:
Attach:AlberoFunzioniASM.png\\
''Figura presa dalle slide del corso''
to:
Attach:AlberoFunzioniASM.png\\
''Figura presa dalle slide del corso'' Added lines 168-190:
* '''in''': sono le cosiddette funzioni monitorate ovvero quelle funzioni il cui valore proviene dall'esterno delle macchina, quindi dall'ambiente (lette dalla macchina e scritte dall'ambiente);\\
* '''out''': sono quelle funzioni fornite dalla macchina ASM (scritte dalla macchina e lette dall'ambiente);\\
* '''controlled''': sono quelle funzioni che sono aggiornate dalla macchina ASM secondo le sue regole (lette e scritte dalla macchina);\\
* '''shared''': sono quelle funzioni che sono condivide tra l'ambiente e la macchina (lette e scritte da ambiente e macchina);
Osservando l'albero è possibile osservare che ci sono anche una classe di funzioni chiamate '''Derived''' e sono quelle funzioni che non sono nuove ma derivate da altre funzioni. Più precisamente i valori di questa tipologia di funzioni sono ''“computati da funzioni monitorate e funzioni statiche per mezzo di una legge o schema fissati a priori”''.\\\
!!!Aggiornamenti Consistenti
Si è detto in precedenza cosa vuol dire aggiornare lo stato di una ASM e come tale aggiornamento può essere fatto. Formalmente un aggiornamento può essere definito come una tripla ''(f, (a1,...,an), b)'' dove ''f'' è la funzione n-aria in considerazione, ''(a1,...,an)'' sono gli argomenti di tale funzione e ''b'' sono elementi del super-universo.\\
Dati gli elementi formali di un aggiornamento la definizione formale di aggiornamento è la seguente: ''“Aggiornare un ASM per uno stato A vuol dire che l'interpretazione della funzione f in A viene modificata per gli argomenti a1,...,an con il valore di b”''.\\
Il problema degli aggiornamenti consistenti può essere provocato da una serie di aggiornamenti, effettuati in parallelo, su una funzione per gli stessi argomenti. Di conseguenza ogni qual volta si utilizzi il costruttore par nel quale sia richiesto aggiornare più volte gli stessi argomenti di una data funzione, bisogna assicurarsi che tutti gli aggiornamenti siano consistenti. Per far rispettare questa proprietà possiamo verificare la seguente proprietà:
''' (f, (a1,...,an),b) ∈ U & (f, (a1,...,an),c) ∈ U, con b=c'''
così facendo saremo sicuri che di non avere nessun aggiornamento inconsistente.
Changed lines 164-167 from:
Attach:AlberoFunzioniASM.png to:
Attach:AlberoFunzioniASM.png\\
''Figura presa dalle slide del corso''
Questo è l'albero delle funzioni ASM, si può osservare che le funzioni Dynamic possiedono più tipi di sotto-funzioni, diamone una breve descrizione:
Changed lines 156-164 from:
Si può dire che questa è la base del costruttore '''par''', essendo la regola eseguita in parallelo prima dello stato S'_1_' il valore della funzione g(3) assumerà il valore di f(5) posseduto allo stato precedente. to:
Si può dire che questa è la base del costruttore '''par''', essendo la regola eseguita in parallelo prima dello stato S'_1_' il valore della funzione g(3) assumerà il valore di f(5) posseduto allo stato precedente. \\\
Il costruttore seq esegue due regole in sequenza, quindi a differenza del par nell'esempio precedente si avrà che, per effetto della regola g(3) := f(5), il valore di g(3) questa volta sarà 2. Tale evento è spiegabile da fatto che, per effetto delle operazioni fatte in sequenza, prima verrà aggiornato lo stato di f(5) e successivamente ci sarà l'assegnamento a g(3).\\\
Le MacroCall Rule invece corrispondono a delle chiamate di funzione, quindi la seguente notazione r[t1,...,tn] possiede il seguente significato: “Chiama r (regola con parametri) con argomenti t1,...,tn”. \\\
!!!Classificazione delle funzioni ASM
Attach:AlberoFunzioniASM.png
Changed lines 151-153 from:
to:
Attach:EsempioASM1.png
Nell'immagine si è supposto che allo stato S'_0_' il valore di f(5) sia pari ad 1. Dopo la regola R allo stato S1 la stessa funzione f(5) è aggiornata al valore 2, mentre l'effetto della regola su g(3) vede come conseguenza l'assegnazione a tale funzione del valore 1.
Si può dire che questa è la base del costruttore '''par''', essendo la regola eseguita in parallelo prima dello stato S'_1_' il valore della funzione g(3) assumerà il valore di f(5) posseduto allo stato precedente.
Changed line 151 from:
to:
Changed lines 149-151 from:
Il ''Block Rule'', come detto in precedenza esegue in parallelo due regole. Per capire il suo funzionamento osserviamo l'esempio seguente:
to:
Il ''Block Rule'', come detto in precedenza esegue in parallelo due regole. Per capire il suo funzionamento osserviamo l'esempio seguente:\\
Attach:Esempio1.png
Added lines 88-154:
Modellando un sistema con le ASM è possibile considerare un ''super-universo'' all'interno del quale vi sono tanti piccoli universi, anziché vedere ogni componente del sistema separata. Ogni universo è un '''dominio''', il quale contiene le sue funzioni e le sue operazioni.\\
Ad esempio se ho un super-universo che fa riferimento ai Processi all'interno di esso potrò identificare due universi:
* Processo ''Sender'';\\
* Processo ''Receiver''.
Come identifico uno dei due domini all'interno del mio super-universo? Supponiamo di voler identificare il processo dei Receiver:\\
'''RECEIVER: X → Bool t.c. RECEIVER(t) = TRUE, ∀ t ∈ X'''
Grazie a questa proprietà è possibile operare su domini eterogenei, dove l'utente può definirne altri di base (domini enumerativi, astratti, ecc) oppure a partire da altri domini esistenti, formando domini strutturati.\\
!!!Termini ASM
''“I termini di Σ sono espressioni sintattiche così costruite:''\\
* ''Le variabili v0, v1, v2, … sono termini;''\\
* ''Costanti c di Σ sono termini;''\\
* ''Se f è una funzione n-aria di Σ e t1, t2, … tn sono termini, allora f(t1, t2, … tn) è un termine.”''
!!!Regole di transizione ASM
Modellare un sistema mediante le ASM vuol dire costruire un modello il quale possiede diversi stati, attraverso i quali la macchina può passare a seconda della computazione fatta. Di conseguenza, nella fase di modellazione, dovremo scrivere delle regole che faranno aggiornare il sistema a seconda del verificarsi o meno di alcune regole. Si è parlato prima di domini astratti, ''“aggiornare stati astratti vuol dire cambiare l'interpretazione delle funzioni di segnatura della macchina”''.
Ci sono diversi costruttori i quali consentono di far aggiornare lo stato attuale della macchina e sono: \\
* '''Update Rule''': costruttore base il quale possiede la seguente forma: ''“f(t1,t2,...,tn) := s”'' ovvero allo stato successivo della macchina il valore della ''f'' sarà aggiornato ad ''s''. Nel qual caso la funzione ''f'' sia una funzione di arietà 0 (quindi una costante) il costruttore acquisirà la seguente forma ''“c := s”'';\\
* '''Conditional Rule''': sarebbe il costruttore ''if-then-else'' il quale prima di aggiornare lo stato della macchina controlla se è verificata o meno una determinata regola.\\
Oltre a questi due costruttori di regole ce ne sono altri e sono (il contenuto delle parentesi graffe denota la sintassi):\\
* '''Skip Rule''': non fa nulla ''[skip]'';\\
* '''Block Rule''': esecuzione in parallelo di più regole ''[par P Q endpar]'';\\
* '''Sequence Rule''': esegue in sequenza più regole ''[seq P Q endseq]'';\\
* '''Let Rule''': assegna il valore di t ad x ed esegue successivamente P ''[let x = t in P]'';\\
*''' Forall Rule''': esegue una regola P in parallelo per ogni x che soddisfa una determinata condizione φ ''[forall x with φ do P]'';\\
* '''Choose Rule''': Sceglie una x (in modo non deterministico) che soddisfa la condizione φ e quindi esegui P ''[choose x with φ do P''];\\
* '''MacroCall Rule''': Esegui la regola di transizione r con parametri t1,...tn (equivalente ad una chiamata di funzione).
Analizziamo alcuni dei costruttori di regole:
Il ''Block Rule'', come detto in precedenza esegue in parallelo due regole. Per capire il suo funzionamento osserviamo l'esempio seguente:
Added line 11:
Changed lines 56-57 from:
Per concludere si può dire che un' ASM è una macchina a stati finiti con memoria, le cui transizioni possono far cambiare valore alla cella utilizzata per memorizzare gli stati.\\ to:
Per concludere si può dire che un' ASM è una macchina a stati finiti con memoria, le cui transizioni possono far cambiare valore alla cella utilizzata per memorizzare gli stati. \\
!!!Vocabolario
Nelle ASM in un vocabolario Σ definisco tutti i simboli e i nomi di funzione che si possono utilizzare. Si possono distinguere due tipi di funzioni, Statiche o Dinamiche.\\
Le funzioni Statiche sono quelle funzioni (che posseggono arietà > 0) definite mediante una legge fissa. In particolare sono funzioni che non variano durante l'esecuzione della macchina. Esempi di funzioni statiche sono le classiche operazioni sui numeri (+,-,*, …) e sui booleani. Si possono definire anche funzioni nuove, il vincolo che si deve rispettare è che tali operazioni siano ammesse nel dominio definito. Esistono anche funzioni statiche di arietà pari a 0, tali funzioni prendono il nome di costanti.\\
La funzioni Dinamiche sono quelle funzioni che variano la legge durante l'esecuzione della macchina.\\
Esempio di vocabolario: Σ'_bool_' → vocabolario dell'algebra boolena. Tale vocabolario possiede:\\
* due costanti: 0 e 1;\\
* funzione unaria per la negazione;\\
* due funzioni binarie per i nomi: “+” per l'OR e “*” per l'AND;\\
* tutte funzioni statiche.\\
Se fisso un insieme di simboli e ne do la loro interpretazione quello che ottengo è una struttura algebrica o algebra. Dall'esempio precedente si ottiene:\\
'''Σ'_bool_' = { 0, 1, -, +, *}'''
Possedendo questi elementi possiamo dare una definizione di Stato ASM:\\
''“Fissato un vocabolario '''Σ''', uno stato '''A''' del vocabolario è un insieme non vuoto X, detto '''super-universo di A''', con le interpretazioni dei nomi delle funzioni di Σ”.''
!!!Domini ASM
Added lines 3-4:
[[Torna alla pagina di Modellazione ed Analisi di Sistemi-> Modellazione ed Analisi di Sistemi]] Added lines 57-60:
----
[[Torna alla pagina di Modellazione ed Analisi di Sistemi-> Modellazione ed Analisi di Sistemi]]
Added lines 1-54:
(:title Modellazione ed Analisi di Sistemi - ASM:)
%titolo%''':: Modellazione ed Analisi di Sistemi - Abstract State Machines ::'''
>>frame<<
Ove non meglio specificato, tutti i testi tra virgolette vanno intesi come citazioni letterali dalle slide della prof [[RiccobeneElviniaMaria]], 2010.
>><<
!!!Introduzione alle ASM
A causa delle innumerevoli limitazioni presentate dalle FMS sono state introdotte le ASM – Abstract State Machines. Le ASM sono l'estensione degli automi a stati finiti, la differenza con quest'ultimi sta proprio nello stato, di fatti si passa ad uno stato di controllo strutturato, dove è possibile effettuare una modellazione anche su dati complessi.\\
Le transizioni nelle ASM sono regole che governano il cambiamento di funzioni da uno stato attuale allo stato successivo. Esistono diversi costruttori di regole, i quali sono descritti brevemente di seguito:
* '''par''' (parallelismo): esecuzione in parallelo di più regole;\\
* '''seq''' (sequenziale): esecuzione in sequenza di più regola;\\
* '''choose''': scelta non deterministica;\\
* '''forall''': parallelismo sincrono non limitato;\\
* Multi agenti sincroni/asincroni.
Per poter modellare un sistema le AMS posseggono un tool per l'Editing, la Simulazione, la Validazione, la Verifica e Generazione di casi di Test. Tutti questi ingredienti rendono le ASM uno strumento molto vicino al linguaggio di programmazione. \\
Le ASM si compongono di un:\\
* '''Header''': dove c'è una fase di inizializzazione e dove si importano le librerie necessarie; \\
* '''Body''': dove vengono definite le regole del modello; \\
* '''Main rule''': è la regola principale (punto di partenza), mediante il quale si mandano in esecuzione le altre regole a seconda della modalità scelta (se in parallelo o in sequenza); \\
* '''Inizialization''': dove si inizializzano le regole ad uno stato iniziale prescelto.
Nelle macchine a stati finiti una particolare situazione può essere modellata con un automa, il quale possiede uno stato iniziale e delle funzioni di transizione che fanno cambiare lo stato a seconda del verificarsi di determinate regole. Questo in ASM può essere definito da programmi:\\
[@ if ctl_state = i then
if c1 then
R1
ctl_state := j1
[…] @]
''ASM vs FSM quali sono le differenze?''\\
*Le ASM sono la diretta estensione delle FSM, la differenza è nello stato, il quale, nelle FSM, può assumere solo un determinato valore di un insieme finito, mentre nelle ASM lo stato è più complesso. \\
*Una seconda differenza la si trova nelle condizioni di input e di output. Nelle FSM si ha a disposizione un alfabeto finito, mentre nelle ASM si può avere un input di qualsiasi genere.\\
Inoltre nelle ASM gli stati, oltre ad essere associati ad un insieme di qualsiasi tipo, possono essere memorizzati in variabili e funzioni. Dunque quando si avrà un cambiamento di stato all'interno della locazione si avrà un cambiamento di valore.\\
Per concludere si può dire che un' ASM è una macchina a stati finiti con memoria, le cui transizioni possono far cambiare valore alla cella utilizzata per memorizzare gli stati.\\
|
|
