Appunti per il corso "Modellazione e analisi di sistemi", A.A 2018/2019, che presenta metodologie e tecniche per la specifica e l'analisi formale di sistemi complessi.
Argomenti affrontati:
• Cosa sono ed a cosa servono i Metodi Formali
• Applicazione dei Metodi Formali alla progettazione ed all'analisi di sistemi
• Modellazione ed analisi ad alto livello di astrazione. Le Abstract State Machines (ASM)
• Tecniche di raffinamento di modelli. Tecniche di astrazione
• Il tool-set ASMETA per modelli ASM
• Casi di studio di specifica di sistemi
• Modellazione ed analisi a basso livello di astrazione
• Automi di Kripke e Logica Temporale CTL: sintassi, semantica, pattern di specifica
• Algoritmi di model checking. Simbolic Model Checking con rappresentazione mediante OBDD
• Verifica di proprietà temporali: proprietà di raggiungibilità, di safety, di liveness, di fairness, assenza di deadlock.
• Astrazione di modelli: fusione degli stati; astrazione di variabili, riduzione di variabili, observer automata
• Raffinamenti di modelli: mappatura di modelli ad alto livello di astrazione verso modelli temporali
• Tool: NuSMV e AsmetaSMV
Modellazione e
analisi di sistemi
Appunti di Maurizio Fortunati
Università degli Studi di Milano
Facoltà di Scienze e Tecnologie
Corso di Laurea Magistrale in Sicurezza informatica (Classe LM-66)
Esame di Modellazione e analisi di sistemi
Docente: Elvinia Riccobene
Anno accademico - 2018/2019Modellazione e analisi dei
sistemi
Appunti a cura di Maurizio Fortunati
Università degli Studi di Milano – Corso Magistrale in Sicurezza Informatica LM-66
Corso tenuto da Elvinia Riccobene [mail]
AA 2018/ 19
Sito Docente
Link Ariel - Lucidi
Link Ariel - Video lezioni
Link SourceForge – Asm examples
V3.7 – 12 Febbraio 2020
Sommario
Sommario ..................................................................................................................................................................................... 2
Introduzione al corso ........................................................................................................................................................... 5
ASM I, Prima parte .................................................................................................................................................................. 6
Riassunto Automi a stati finiti ....................................................................................................................................................... 6
Da FSM a ASM ......................................................................................................................................................................................... 6
Esempi porta girevole e macchinetta caffè ...................................................................................................................... 8
ASM I, Seconda parte ......................................................................................................................................................... 11
Stato Asm ................................................................................................................................................................................................. 11
Domini ASM ............................................................................................................................................................................................. 13
ASM II, Prima parte .............................................................................................................................................................. 15
Regole di transizione ........................................................................................................................................................................ 15
Esempi Advanced Clock e Semaforo .................................................................................................................................. 15
ASM II, Seconda parte ....................................................................................................................................................... 19
Esempio SluiceGate( Chiusa) .................................................................................................................................................... 19
Esem pio fattoriale .............................................................................................................................................................................. 21
Esempio Swap sort vettore ......................................................................................................................................................... 21
AsmetaL - Linguaggio Strutturale ............................................................................................................................. 23
Name .......................................................................................................................................................................................................... 24
Header ....................................................................................................................................................................................................... 24
Body ............................................................................................................................................................................................................. 24
main rule ................................................................................................................................................................................................... 26
Inizializzazione ...................................................................................................................................................................................... 26
AsmetaL - Linguaggio delle definizioni .................................................................................................................. 26
Dichiarazione dei domini .............................................................................................................................................................. 26
Type Domain: .................................................................................................................................................................................................... 27
Structured Domain ...................................................................................................................................................................................... 28
Dichiarazione delle funzioni ........................................................................................................................................................ 31
Funzioni statiche ............................................................................................................................................................................................. 32
Funzioni dinamiche ...................................................................................................................................................................................... 32
Funzioni derivate ............................................................................................................................................................................................ 34
Invarianti.................................................................................................................................................................................................... 35
Locazioni e aggiornamenti ......................................................................................................................................................... 35
Convenzioni sugli ID ........................................................................................................................................................................ 36
AsmetaL - Linguaggio dei termini ............................................................................................................................. 37
AsmetaL - Linguaggio delle regole .......................................................................................................................... 38
Skip, Update, Par, Seq .................................................................................................................................................................... 38
Conditional rule (If, let, forall, choose, switch case) ................................................................................................. 40
Macro call rule ..................................................................................................................................................................................... 43
Extend Rule – Riserva di una ASM ........................................................................................................................................ 44
ASM multi agenti ................................................................................................................................................................. 46
Definizione .............................................................................................................................................................................................. 46
ASM Sincrone .................................................................................................................................................................................................... 47
ASM Asincrone ................................................................................................................................................................................................ 47
Multi Agent in AsmetaL ................................................................................................................................................................. 48
Case study – popolazione .................................................................................................................................................................... 48
AsmetaL - Protocollo Needham-Schroeder ........................................................................................................ 50
AsmetaL - Esempi ................................................................................................................................................................ 51
Esem pio ATM ........................................................................................................................................................................................ 51
Esame 2 luglio 2013 – sbarra cancello automobile .................................................................................................. 56
Multi Agent ASM - produttore consumatore ................................................................................................................ 57
Multi Agent ASM - Bambini e caramelle ......................................................................................................................... 60
Popolazione ........................................................................................................................................................................................... 62
FrameW ork ASM – Ground Model ............................................................................................................................. 66
Design ....................................................................................................................................................................................................... 66
Costruzione del ground model - GM ......................................................................................................................................... 67
Raffinamento del modello ................................................................................................................................................................... 68
Esempio chiusa .............................................................................................................................................................................................. 70
FrameW ork ASM – Analisi .............................................................................................................................................. 74
Logiche temporali ............................................................................................................................................................................. 74
Automi di Kripke ............................................................................................................................................................................................. 74
La CTL - Computational tree logic .............................................................................................................................................. 75
Equivalenze Canoniche .......................................................................................................................................................................... 80
Algoritmo di model Checking ........................................................................................................................................................... 80
Algoritmo di Labeling - Regole di etichettatura ............................................................................................................... 81
Esercizi CTL ....................................................................................................................................................................................................... 83
Algoritmo SAT ..................................................................................................................................................................................... 86
Algoritm i SAT (EX, EU, AF) ................................................................................................................................................................... 88
Esercizi SAT ....................................................................................................................................................................................................... 90
Verifica di proprietà temporali ................................................................................................................................................. 94
Proprietà ................................................................................................................................................................................................................ 94
Pattern Noti - Practical patterns of Specifications 2 ..................................................................................................... 97
Esercizi sulle proprietà temporali .................................................................................................................................................. 97
OBDD - Ordered Binary Decision Diagrams ............................................................................................................... 10 0
Teoria .................................................................................................................................................................................................................... 10 0
Regole di compattezza .......................................................................................................................................................................... 10 1
Esercizio di compattezza ..................................................................................................................................................................... 10 2
Alberi BDD ......................................................................................................................................................................................................... 10 4
Vantaggi di utilizzare ROBDD .......................................................................................................................................................... 10 5
Calcolo del ROBDD e del SAT ....................................................................................................................................................... 10 5
NuSMV ................................................................................................................................................................................................................ 10 6
Preparazione Esame Teorico ...................................................................................................................................... 110
Preparazione Esame di laboratorio ......................................................................................................................... 117
Note su Asmeta tools ...................................................................................................................................................... 121
Codici Sorgenti ................................................................................................................................................................... 122
Template ................................................................................................................................................................................................ 122
Advanced Clock ............................................................................................................................................................................... 123
Cena dei filosofi ................................................................................................................................................................................. 124
Adolfo ....................................................................................................................................................................................................... 126
ADOLFO V2 .......................................................................................................................................................................................... 134
Ex am 15 0 1 20 19 – prod consumatore ............................................................................................................................. 136
Morra cinese ........................................................................................................................................................................................ 139
ATM ............................................................................................................................................................................................................ 141
Tris – Tic Tac Toe ............................................................................................................................................................................. 145
Lotto .......................................................................................................................................................................................................... 147
Tombola con la seq .................................................................................................................................................................................. 149
Token ........................................................................................................................................................................................................ 151
Container ................................................................................................................................................................................................ 153
Popolazione ......................................................................................................................................................................................... 154
Indice delle figure ............................................................................................................................................................. 156
Introduzione al corso
Riferimenti
Lezione 201 8-02-28-11.0 0 .49
Introduzione
Obiettivo del corso, è quello di poter dimostrare che un sistema godi di certe proprietà.
Come faccio a provare queste proprietà?
Devo prima fare una rappresentazione astratta del sistema e per farla utilizzo i linguaggi di
specifica.
Un linguaggio di specifica permette di poter descrivere il sistema in modo univoco e non
ambiguo, con il quale si potrà descrivere i requisiti del sistema creando un modello che è la
rappresentazione astratta del sistema.
Con questo modello è possibile effettuare delle analisi, definite validazione e verifica, che
sono basate su simulazione, testing e model checking.
Validazione: processo di valutazione di un sistema o di una componente per l’intero ciclo di
sviluppo per determinare se esso soddisfa i requisiti specificati.
I requisiti, sono documenti scritti in linguaggio naturale che descrivano il sistema come lo
vuole il cliente.
Validare significa valutare se il sistema che ho realizzato alla fine o durante lo sviluppo sia
corretto rispetto ai requisiti. Validazione controlla i requisiti
Si effettua tramite la simulazione e il testing
Verifica: Processo di valutazione di un sistema o di una componente per determinare se i
prodotti di una data fase di sviluppo soddisfano le condizioni (proprietà) imposte allo stato di
quella fase.
Dimostrare che il sw che si sta sviluppando in qualsiasi punto soddisfi alcune proprietà.
Verifica correttezza di proprietà
Si procede attraverso tecniche di theorem prover e model checker.
Ovviamente non è possibile testare tutto a carta e penna, quindi utilizzeremo dei sistemi
automatici.
Quindi nel corso si studieranno 3 cose, linguaggimetodi tool.
Metodi formali.
Sono notazioni rigorose e dal significato preciso, dei simboli che non permettono ambiguità.
Formalismi operazionali: forniscono una descrizione del comportamento del sistema in
termini di operazioni di una macchina astratta, li utilizzeremo per effettuare la validazione.
Per fare simulazione del modello.
Esempi di formalismi operazionali sono: ASM, B & Z Method, SCR, Petri
Formalismi dichiarativi, descrive il sistema in termini di proprietà che devono soddisfare; li
utilizzeremo per la fase di verifica.
Esempi di formalismi dichiarativi sono: Logica temporale, trio, algebre dei processi.
ASM I, Prima parte
Riferimenti
Video lezione di riferimento 20 18 -02-28-13.0 5.27 lucidi 1 a 26
Riassunto Automi a stati finiti
Un automa, chiamato anche: macchina stati finiti, in inglese FSM (finite state macchine) è una
notazione formale che permette la rappresentazione astratta del comportamento di un
sistema.
La FSM è composta da una tupla di 3 elementi:
• S insieme finito di stati
• I insieme finito di eventi input
• δ che è la funzione di transizione che connette ogni stato S a S’ per via di un input,
Diagramma di stato è la rappresentazione grafica di una FSM.
Le FSM sono molto basilari e con esse non si riesce a modellare la memoria o l’output, per
questo motivo sono state introdotti:
Automi di Mealy e di Moore per modellare l’output.
Le FSM estese per modellare la memoria della macchina.
Le FSM di comunicazione per modellare la comunicazione, ad esempio nelle macchine nei
sistemi distribuiti.
FSM temporizzate per modellare il tempo, dove si può definire un tempo di durata della
transizione.
Infine si giunge alle macchine di stato di UML o FSM di Harel che permettono di modellare,
lo stato, input, output attività interne e trans interne e sotto macchine.
Vedremo altre estensioni:
ASM – Abstract state machine FSM con stati generalizzati
Automi di Kripke lo stato porta informazioni di una proprietà che è valida in esso.
Da FSM a ASM
Agganciandoci al concetto di modello delle FSM vediamo la ASM.
Per il momento non concentrarti sulla sintassi o sulla forma ma sull’idea di
funzionamento, perché alcuni dettagli o pezzi di codice non vengono inseriti o
spiegati per brevità.
Il linguaggio asm verrà spiegato in modo dettagliato più avanti
Le differenze che si possono notare riguardano la concezione degli stati, che risultano più
complessi nelle ASM e le condizioni di input e le azioni di output.
Nelle FSM si ha un alfabeto finito mentre nelle ASM, si può avere un input qualsiasi.
Introduciamo le asm con un modello di esempio; un orologio digitale che mostra l’ora che
viene aggiornata ad ogni delta di tempo, attraverso il DisplayTime.
Le macchine a stati sono costituite da due concetti, gli stati e le transizioni, andremo a
sviluppare il concetto di stato e poi quello di transizione delle ASM.
4 Funzioni:
CurrTime: Rappresenta il tempo corrente ed è di tipo reale
DisplayTime: variabile che rappresenta l’ora
Delta: un numero reale
+ : operazione di somma che dati due reali restituisce un reale, Real x Real
In questo caso utilizziamo solamente un insieme di funzioni matematiche, cioè l’insieme dei
reali.
CurrTime e DisplayTime le possiamo vedere come delle variabili, il delta come una costante
e il + come una funzione.
In ASM tutto viene considerato come una funzione con differenze in base all’arietà (ovvero il
numero di argomenti presenti).
In questo esempio le funzioni utilizzate hanno arietà zero tranne il + che ha arietà 2.
Quindi si possono distinguere funzioni con arietà zero e diverso da zero.
Successivamente si procede con la costruzione degli stati strutturati che modellano dati
complessi arbitrari e operazioni per la manipolazione dei dati, sostituendo uno stato non
strutturato con un’algebra.
Le transizioni nelle FSM vengono rappresentate con delle frecce, mentre in ASM
utilizzeremo una formula simile all’ if then else if condition then updates .
È possibile costruire delle regole con diversi costruttori:
• parallelismo (par) ed azioni sequenziali (seq)
• iterazioni (while) en invocazioni di sottomachine
• non determinismo (choose) e parallelismo sincrono non limitato (forall)
• multi-agenti sincroni e asincroni
Nella programmazione della ASM andremo a distinguere header, body,main rule,
initialization:
Figura 1 : Primo esempio di ASM
Per poter passare da una FSM ad una ASM si può utilizzare il seguente schema:
Figura 2: Da FSM a ASM
dove:
• ctl_state è una variabile che rappresenta lo stato corrente e può prendere come valore
uno stato di controllo (in un insieme finito)
• i, j1 , j2, … , jn sono stati interni di controllo (i valori di ctl_state)
• ck (k=1 , 2, … , n) rappresentano le condizioni di input
• Rk le azioni della macchina
Facendo un paragone tra fsm e asm si può notare che nelle Fsm esiste un unico stato di
controllo (ctl_state), che può assumere valori in un insieme finito di un certo tipo.
Mentre nelle ASM lo stato è più complesso
Le condizioni di input e le azioni di output, nelle fsm sono un alfabeto finito, mentre nelle
ASM l’input può avere qualsiasi input.
Esempi porta girevole e macchinetta caffè
Porta girevole
Figura 3: Esempio Porta girevole
Gli stati sono i 5 rettangoli (open, stayopen,..) e li inserisco nell’inizializzazione, mentre le
funzioni da simulare sono le 4 azioni che interconnettono gli stati (click, complete, click +
ctl_state che serve per verificare lo stato)
Si possono vedere le asm come dello pseudo codice con alcune differenze e caratteristiche.
Giusto per citarne qualcuna e anticipare alcuni concetti, si vedrà che alcuni stati possono
scattare contemporaneamente.
Il click e il time-out sono delle entità che rappresentano il flusso dell’ambiente sul sistema.
Queste funzioni si andranno a distinguerle tra monitorate e controllate.
Monitorate sono quelle che arrivano dall’ambiente, il valore viene dato ad ogni stato
dall’ambiente.
Il simulatore fornisce dei valori, mentre dal punto di vista semantico è l’ambiente che li
fornisce e non la macchina che ne effettua l’aggiornamento; la macchina sa che quando
avrà bisogno di certi dati li potrà ottenere dall’ambiente come una specie di oracolo.
Mentre quelle cambiate dalla macchina sono quelle controllate.
Sarà compito delle regole di transizione di aggiornare tali valori, la macchina aggiornerà la
funzione ctl_state mentre quelle controllate dall’ambiente sarà compito del simulatore
aggiornarle.
Esempio macchinetta caffè
Figura 4: Esempio macchinetta caffè
Versione tramite EFSM:
In questo caso è stata utilizzata una macchina estesa in quanto c’è bisogno della memoria
per contare le monete e le bevande scelte.
Si può notare che tutte le transazioni seguono una sequenza simile. In esempio quella rossa
Azione che attiva la transazione ins (50cent)
[possibile guardia che può bloccare la transazione][coin<25&…]
aggiornamento delle variabilicoin≔coin+1, …
/output /eroga(milk)
In ASM:
Segnatura/ definizione
Bisogna definire il tipo di monete e il tipo di prodotto erogato tramite il dominio
Monete half/ one e prodotto caffè e latte, quindi:
enum domain cointype = {HALF|ONE}
enum domain product ={MILK | COFFE}
Questi due elementi non sono infiniti, perché il latte e il caffè possono essere erogati al
massimo 1 0 volte e il contenitore delle monete ne contiene al massimo 25.
Si inseriscono altre due variabili che vengono chiamati domini, che appartengono all’insieme
degli interi.
signature:
domain QuantityDomain subsetof integer
domain CoinDomain subsetof integer
definitions:
domain QuantityDomain={0..10}
domain CoinDomain ={0..25}
Si definisce una funzione (available) che dato un prodotto (caffè o latte), ne restituisca la
quantità presente.
Questa funzione associa ad ogni prodotto la sua quantità
controlled available: productQuantityDomain
Si definisce l’insieme delle monete, che fanno parte del dominio delle monete.
controlled Coins: CoinDomain
e si definisce il dominio delle monete inserite
controlled insertedCoin: CoinType
inizializzazione:
default init s0:
function coins=0
function available($p in product)=10
regole:
main rule r_Main =
if(coins < 25) then
if(insertedCoin = HALF) then
if(available(MILK) > 0) then
r_serveProduct[MILK]
endif
else
if(available(COFFEE)>0) then
r_serveProduct[COFFE]
endif
endif
endif
endif
Volendo si può accorpare in un’unica regola per servire i prodotti, utilizzando una regola con
parametro.
Rule r_serveProduct($p in Product)=
par
Available($p):= available($p)-1
Coins:= coins+1
endpar
ASM I, Seconda parte
Riferimenti
Video lezione di riferimento 20 18 -03-07-10 .38 .44 lucidi da 27 a 42
Stato Asm
Nelle ASM gli stati sono associati a un insieme di valori di qualsiasi tipo, memorizzate in
apposite locazioni.
Matematicamente una locazione è definita come Il valore di una funzione f f(x1, … , xn) nello
stato S, cioè di funzioni con valore.
Es. availab le (LATTE) = 10
Potremmo pensare alle locazioni come a delle variabili, ma non sono spazi in memoria che
contengono un valore, sono invece occupati dal risultato di una certa funzione con un certo
parametro.
Per variabili si intende un valore, mentre per locazione la coppia la funzione + parametro.
Questo ci porta dire che le transizioni di stato delle FSM corrispondono alle transizioni di
stato delle ASM con aggiornamenti dei valori contenuti nelle locazioni.
Definizione formale dello stato di una ASM
Fissato un vocabolario, uno stato: è l’insieme non vuoto (super universo) delle interpretazioni
delle funzioni del vocabolario.
Iniziamo a definire cosa sia un vocabolario.
Vocabolario
Un vocabolario è una collezione finita di nomi e funzioni, un insieme di nomi che non hanno
significato fino a quando non glielo diamo noi.
Dare significato = dare un’interpretazione.
Si può pensar al vocabolario come alla dichiarazione di tutte le funzioni che verranno usate.
Le funzioni dichiarate possono essere dinamiche o statiche.
Dinamiche, se il significato può cambiare di stato in stato, mentre statiche se rimane lo
stesso per tutta l’esecuzione.
Nei linguaggi di programmazione classici, siamo abituati ad utilizzare le variabili, in asm le
variabili come le conosciamo noi, non esistono, perché tutto è funzione.
Per modellare una variabile bisogna creare una sono funzioni dinamica che abbia arietà zero.
Mentre per definire le costanti, utilizzo delle funzioni statiche con arietà 0.
Il concetto di funzione matematica racchiude il concetto di variabili, costanti, funzioni e
insieme.
Dal punto di vista matematico, se voglio modellare un sistema e rappresentare in astratto lo
stato attuale mi basta solo definire un insieme di funzioni e definire come queste funzioni
cambiano di interpretazione passando allo stato successivo.
Avendo un vocabolario, che contiene dei nomi, associo ai nomi delle funzioni alle quali
assegno delle interpretazioni e possono essere statiche o dinamiche a seconda del fatto che
la loro interpretazioni cambia o meno nel tempo.
Ogni vocabolario ASM contiene sempre 3 funzioni statiche di arietà zero (costanti statiche)
undef, true e false.
I numeri sono costanti numeriche che l’utente può definire a piacimento come ad esempio:
votomin=18
Il valore undef serve per poter dare la possibilità di far diventare le funzioni totali, perché non
sempre lo zero ha la stessa interpretazione, ad esempio nella moltiplicazione e nella
somma, lo zero ha due significati diversi.
Le funzioni statiche con arietà maggiore di zero sono definite tramite una legge fissa e di
solito sono le operazioni tra numeri, +, -, *… oppure tra booleani (op logici come and or… )
Le funzioni dinamiche con arietà zero sono le classiche variabili.
Esempio di vocabolario: Σ bool
Che è il vocabolario di tutte le funzioni booleane.
In questo vocabolario si inseriscono diversi elementi che sono:
Due simboli 0 e 1 che sono due costanti.
Una funzione con arietà 1 che è il NOT con il simbolo “-”.
Due funzioni binarie chiamate “+ ” “*” per OR e l’AND.
Per il momento abbiamo solamente definito il vocabolario senza darne un’interpretazione.
Prima di darla cerchiamo di definire il concetto di stato.
Fissato un vocabolario Σ (che è un insieme di nomi), uno stato A del vocabolario Σ è un insieme
non vuoto X, detto super universo di A, con le interpretazioni dei nomi delle funzioni di Σ.
Quindi fisso un vocabolario, definisco le interpretazioni dei simboli e definisco un insieme
non vuoto X che comprende i simboli con le loro interpretazioni, ecco definito il super
universo A
Se f è un nome di funzione n-aria di Σ, allora la sua interpretazione f A è una funzione da Xn a
X.
Se c è un nome di costante di Σ, allora la sua interpretazione A è un elemento di X
Adesso vedremo due esempi di stato su Σ
Ese m p i o 1:
Stiamo facendo discorsi a basso livello, quindi lo zero, l’uno, il meno, il più e l’asterisco devo
considerarli solo come dei simboli, come dei disegni che fanno parte del vocabolario Σ Bool
che per il momento non hanno significato.
Per dargli un significato creo lo stato A che è composto dai numeri chiamati anche costanti 0
e 1.
Quindi per questo motivo che ai simboli 0, 1 , -, +, * ho ad apice A per indicare che
attualmente stiamo considerando l’interpretazione nel contesto dello stato A.
I simboli a e b sono da interpretare come qualsiasi valore del dominio cioè che possono
essere solo 0 e 1 .
Con questa logica procedo ad analizzare le righe.
Lo zero, simbolo che ho messo all’interno del mio vocabolario Σ Bool
nella mia algebra che
ha come X come super universo gli associo la costante 0.
Stessa cosa per il simbolo 1.
Al simbolo – seguito da un valore arbitrario a gli conferisco l’interpretazione 1 -a.
E così via.
Domini ASM
Si possono dividere il super universo in domini o sotto universi in base alla loro funzione
caratteristica, cioè creo una funzione che risulti vera solamente per gli elementi presenti in
quel dominio.
Nella slide si fa l’esempio che il super universo è composto da i seguenti elementi {1,2,3, a, b,
mario, pippo} che si possono dividere nei domini interi char e string, questi domini sono
guidati da una funzione che risulterà vera solamente per gli elementi di quel dominio.
Parliamo sempre di funzioni, ma perché serve che tutto sia funzione?
Perché dobbiamo riportare il concetto delle ASM alle macchine a stato, composte da uno
stato più la transizione (la freccia).
Nelle ASM lo stato piuttosto che essere una cosa non strutturata a cui posso definire solo
nel nome diventa adesso uno stato che è una struttura algebrica, con nomi di funzioni e
d om ini.
Per il momento non abbiamo definito formalmente la transizione ma andando per intuizione
ipotizziamo di fotografare il sistema al momento t0 e t1 ; potremo avere due casi, il primo che
non sia successo niente e il secondo che sia successo qualcosa.
Il concetto matematico che può cambiare è l’interpretazione della funzione, perché le
funzioni non si possono creare o distruggere in quanto il vocabolario è fisso, quindi l’unica
cosa che si può cambiare è l’interpretazione della funzione.
Come abbiamo visto tutto è funzione, costanti variabili, domini, predicati.
Quello che dovrò fare nelle regole di transizione è definire come cambiano le regole di
interpretazione delle funzioni, questo mi darà il concetto di passo di computazio ne.
Durante le transizioni potranno cambiare solamente le interpretazioni delle funzioni
dinamiche.
Le transizioni hanno come mattone di base, l’aggiornamento della funzione.
Esempio di stato ASM – orologio:
Il vocabolario è composto da 4 elementi 2 funzioni dinamiche e 2 funzioni statiche, il super
universo è composto da elementi reali.