Statecharts
Riferimenti (1)
D. Harel, Statecharts: A visual formalism for complex systems,
Science of Computer Programming 8 (1987), pp. 231-274.
D. Harel, On visual formalisms,Communications of the ACM 31
(1988), pp. 514-530.
D. Harel, A. Pnueli, J. Schmidt, R. Sherman, On the formal
semantics of Statecharts, Proc. 1st LICS, IEEE Press, pp. 5464, 1986.
C. Huizing, G. Gerth, W. De Roever, Modeling statecharts
behavior in a fully abstract way, Proc. 13th CAAP, LNCS
299, Springer, pp. 271-294, 1988.
C. Huizing, W. De Roever, Introduction to design choices in the
semantics of Statecharts, Information Processing letters 37
(1991), pp. 205-213.
Riferimenti (2)
A. Maggiolo-Schettini, A. Peron, S. Tini, A comparison of
Statecharts step semantics, Theoretical Computer Science 290
(2003), pp. 465-498.
A. Pnueli, M. Shalev, What is a step: on the semantics of
Statecharts, Proc. TACS ‘91, LNCS 526, Springer, pp.244264, 1991.
A. Peron, A., Maggiolo-Schettini, Transitions as Interrupts: A New
Semantics for Timed Statecharts, in: Proc. TACS’94, LNCS
789, Springer, 1994, pp. 806-821.
A. Maggiolo-Schettini, A., Peron, A., Retiming Techniques for
Statecharts, Proc. FTRTFT’96, LNCS 1135, Springer, 1996,
pp. 55-71.
A. Maggiolo-Schettini, M. Merro, Priorities in Statecharts, Proc.
Workshop on Analysis and Verification of Multiple-Agent
Languages, Stockholm, June 1996, LNCS 1192, Springer,
1996, pp. 404-429.
Motivazioni
La descrizione di sistemi complessi con macchine a stati
finiti (FSM) e della loro controparte visuale con diagrammi a
transizione di stato pone le seguenti difficoltà:
1. i diagrammi sono piatti e quindi non supportano sviluppo
a passi, top-down o bottom-up
2. i diagrammi non sono economici; un evento che causa la
stessa transizione da un gran numero di stati, come un
interrupt ad alto livello, deve essere rappresentato da una
transizione con lo stesso evento da tutti gli stati
3. alla crescita lineare del sistema da descrivere corrisponde
una crescita esponenziale del numero degli stati
4. i diagrammi sono sequenziali e non esprimono la
concorrenza in modo naturale.
Statecharts (1)
Gli Statecharts sono stati proposti per ovviare agli
inconvenienti detti dei diagrammi di stato:
Statecharts = diagrammi di stato + profondità
+ ortogonalità + broadcast
D
e
A
f
g
C
f
diventa
A
e
f
g
B
B
C
h
h
Statecharts (2)
k
B,E
B,G
g
e
C,E
e
mp
k
k
C,G
f
diventa
h e
C,F
p
e
f
mp
H
p
h
B,F
I
A
D
B
e
E
g
f[in(G)]
C
k
k
h
F
e
G
m
k
H
e
e
p
I
Statecharts (3)
Un’altra caratteristica degli statecharts è la possibilità di
ricordare la visita precedente a uno stato e di entrare in
uno stato composito A non nello stato di default, ma
nello stato in cui il sistema si trovava quando ha lasciato
A l’ultima volta.
Esempio
Entrando in A facendo la
trasizione etichettata e, il
sistema entrerà in quello
degli stati B, C, D in cui
si trovava l’ultima volta
che ha lasciato A.
A
e
f
H
B
C
D
Statecharts (4)
Le transizioni dello possono avere un comportamento di
output che non è mandato al mondo esterno (come nelle
macchine di Mealy), ma può influire sul comportamento
dello statechart stesso nelle sue componenti ortogonali
dando luogo a reazioni a catena.
A
Esempio
Se l’ambiente dà m si ha
un passo J  I, B  C,
D  G.
Se poi l’ambiente dà n si
ha un passo I  J, C  B,
G  E.
k
B
e
E
f/g
n
C
g
D
G
e
H
A
J
m/e
n/f
I
Statecharts (5)
Data una configurazione C la reazione dello statechart
all’input che viene dall’ambiente è descritto come un
passo. Si tratta di trovare l’insieme T di transizioni che
sono rilevanti in C, ossia originano in qualche antenato
di una sottoconfigurazione di C, che sono abilitati
dall’evento e sono consistenti (di qui può venire non
determinismo). A un micropasso determinato da un
evento proveniente dall’ambiente possono seguire
micropassi determinati sia dall’ambiente sia da segnali
emessi come output da transizioni del micropasso
precedente sia dall’aggiornamento di condizioni. Una
sequenza di micropassi termina quando non restano più
scelte consistenti da effettuare. A questo punto il passo,
che è una sequenza massimale di micropassi, è
osservabile dall’estermo nei suoi effetti.
Statecharts (6)
Esempio
A
Se il sistema è in B
e occorre e, allora può
andare in C o in D
nondeterministicamente
Esempio
Il sistema può passare
dalla configurazione
(A,B,C) alla
configurazione (D,B,F)
B
e
e
D
C
A
B
e/f
D
C
ef
e[ny f]
E
F
se le transizioni sono considerate nell’ordine A  D, B  E, C  F
e alla configurazione (D,E,F) se le transizioni sono considerate
nell’ordine B  E, A  D, C  F.
Statecharts (7)
Esempio
A
B
C
Se i valori iniziali di x e y
sono 0 all’occorrere di e
e/x:=1
e/y:=1
x=y
il sistema effettuerà le
E
F
D
due transizioni che
assegnano 1 a x e a y. Se
le due transizioni A  D,
B  E sono avvenute in due micropassi differenti allora in un
micropasso successivo sarà x = y e potrà avvenire la transizione
C  F.
Esempio
Come descrivere l’esclusività di
un evento. Le configurazioni finali
sono (C,B) con x=1 oppure (A,D)
con x=2.
A
C
e[cur(in B)]/x:=1
B
e[cur(in A)]/x:=2
D
Statecharts (8)
Esempio
A
Quando il sistema è in
(A,C) la componente a
sinistra può andare in F o in
B nondeterministicamente
ma la componente a destra
può andare in D solo se è
stata fatta la prima scelta.
Esempio
Come descrivere priorità. Se e
ed f occorrono simultaneamente
la e-transizione ha priorità.
C
E
e/f
e/f
f[cur(in(F))]
B
G
F
e
A
f[ny(e)]
B
D
Semantica HPSS86 (1)
Consideriamo un sottoinsieme ristretto di Statecharts. La reazione del
sistema agli stimoli esterni (eventi) è fatta dalle transizioni. Le
transizioni sono etichettate con un’etichetta della forma e/a
(evento/azione).
Si assume l’ipotesi di sincronia: il sistema è infinitamente più veloce
dell’ambiente e la risposta a uno stimolo esterno è sempre generata
nel medesimo passo in cui si ha lo stimolo.
Esempio
Si abbiano le transizioni parallele t0: a/e1, t1: e1/e2, … , tn: en/b .
In presenza di a gli eventi e1, …, en, b sono tutti generati nel medesimo
passo.
Semantica HPSS86 (2)
Si vuole però mantenere la relazione di causalità ed escludere
situazioni in cui ci sono due transizioni che si causano l’una l’altra.
Esempio
t1: a/b
t2: b/a
Possiamo voler assegnare priorità alle risposte agli stimoli. Si può
fare usando eventi negati ed espressioni trigger.
Esempio
Nel caso di due transizioni in conflitto t1: a, t2: b tra cui la scelta
sarebbe nondeterministica possiamo dare priorità alla transizione
stimolata da b:
t1: a.b--
t2: b
Semantica HPSS86 (3)
Il comportamento di uno statechart è una sequenza di passi
ciascuno dei quali porta da una configurazione stabile alla successiva.
L’ambiente può introdurre nuovi eventi esterni all’inizio di ciascun
passo. La risposta del sistema è una sequenza di micropassi. Il primo
micropasso consiste di tutte le transizioni stimolate dall’insieme degli
eventi di input. I micropassi successivi consistono di tutte le
transizioni stimolate dall’insieme di eventi contenenti gli eventi di
input e gli eventi generati dai micropassi precedenti. Poiché il numero
di transizioni che possono essere fatte in un passo è finito la sequenza
di micropassi termina quando non ci sono più transizioni abilitate da
aggiungere. Questo conclude un passo e l’insieme degli eventi
generati dal passo è l’insieme degli eventi generati nei micropassi.
Tale semantica soddisfa sincronia, causalità ed espressione della
priorità mediante eventi negati.
Semantica HPSS86 (4)
La semantica data è localmente consistente, ma non globalmente
consistente.
Esempio
Consideriamo due transizioni parallele
t1: a--/b
t2: b/a
Supponiamo inizialmente E = . Poiché a  E allora t1 è abilitata e il
primo micropasso fa t1 generando b, nel micropasso successivo b  E
e si può fare t2 generando a. Il passo {{t1}, {t2}} è localmente
consistente ma non globalmente consistente.
Semantica HPSS86 (5)
La semantica data è operazionale in quanto definisce il
comportamento del sistema in termini di operazioni atomiche.
E` utile per una realizzazione del linguaggio.
Una semantica dichiarativa definisce il comportamento mediante
equazioni ignorando dettagli operazionali (e.g.ordine delle
operazioni). Se la semantica dichiarativa è composizionale si chiama
denotazionale. Si vuole consistenza delle due semantiche.
La mancanza di consistenza globale della semantica a micropassi di
HPSS86 impedisce di dare una semantica dichiarativa e una
operazionale consistenti l’una con l’altra.
Semantica PS91 (1)
Vediamo per un insieme ristretto di Statecharts una semantica
dichiarativa e una semantica operazionale consistenti.
Sia uno statechart una 5-tupla <P, S, T, r, V>, dove
P è un insieme di eventi primitivi
S è un insieme di stati
T è un insieme di transizioni
r  S è lo stato radice
V è un insieme di variabili assunto inizialmente vuoto.
Per ogni stato la funzione children: S  2S dà l’insieme dei suoi
sottostati immediati. Uno stato s è basilare se children(s) = ,
altrimento è composto. L’insieme degli stati basilari è chiamato
Basic. Se s2  children(s1) diciamo s1 padre di s2 e s2 figlio di s1.
Esiste un unico stato che non ha padre, è r lo stato radice.
Semantica PS91 (2)
Chiamiamo children* e children+ le chiusure riflessiva-transitiva e
transitiva, rispettivamente, di children. La funzione children* può
essere estesa a un insieme di stati
children*(X) =  x  X children*(s)
Se s2  children*(s1) diciamo s1 antenato di s2 e s2 discendente di s1.
Uno stato s1 è antenato e discendente di se stesso. Se uno stato s1
è antenato o discendente di uno stato s2 diciamo che s1 e s2 sono
ancestralmente relati. La radice è un antenato di tutti gli stati.
Si richiede che ogni stato abbia un solo padre. Cosí la relazione di
figliolanza organizza gli stati di uno statechart in un albero con radice
r le cui foglie sono stati basilari e i nodi intermedi sono stati
composti.
Semantica PS91 (3)
La funzione type: S  {and, or} è una funzione parziale che assegna a
ciascuno stato composto il suo tipo. Se children(s)   e type(s) = or,
allora children(s) è una or-decomposizione di s, ossia quando il sistema
è in s è in uno e uno solo dei suoi sottostati. Se children(s)   e
type(s) = and, allora children(s) è una and-decomposizione di s, ossia
quando il sistema è in s è simultaneamente in tutti i suoi sottostati.
La funzione type è indefinita sugli stati basilari e la radice deve essere
uno stato or.
La funzione default: S  S identifica per ciascuno stato or s uno dei
suoi immediati discendenti come stato di default, ossia come stato in cui
il sistema entra entrando in s.
Per un insieme di stati X  S lca(X), il minimo antenato comune di X, è
lo stato x tale che X  children*(x) e per ogni altro s  S tale che
X  children*(s) vale x  children*(s).
Per un insieme di stati X esiste un minimo antenato comune unico.
Semantica PS91 (4)
Un insieme di stati X  S è consistente se per ogni due stati s1, s2  X
o s1 , s2 sono ancestralmente relati oppure s1 _|_ s2 . Un insieme X è
massimalmente consistente se per ogni stato s  S -X, X {x} non è
consistente. Un insieme massimalmente consistente è una
configurazione dello statechart.
Se X è un insieme consistente il completamento per default di X,
completion(X), è la configurazione Y contenente X tale che per ogni
stato s  Y se X oppure children(s) =  allora default(s)  Y. Tale
richiesta identifica un’unica configurazione Y. La configurazione
iniziale X0 è il completamento per default della radice.
Per ogni transizione t  T source(t) denota l’insieme di stati da cui la
transizione esce, target(t) denota l’insieme di stati bersaglio della
transizione.
Semantica PS91 (5)
A
B1
Esempio
B2
c1
c2
g1
g2
h1
h2
t1
N
d1
d2
e1
e2
t2
f1
f2
i1
j1
i2
j2
t3
source(t1) ={c2,d2} target(t1) ={g1,h1,i1}
Semantica PS91 (6)
L’arena di una transizione t, denotata arena(t), è il minimo contesto
che contiene tutti i cambiamenti causati dalla transizione.
Usualmente è il più piccolo stato or contenente source(t)  target(t),
ma ci possono essere altri casi. Nell’esempio l’arena di t3 non è lo
stato N che contiene source(t3)  target(t3), bensí lo stato A.
L’abilitazione di una transizione t, denotato trigger(t), consiste di
letterali l1,…, lk, k ≥ 0, ciascuno dei quali è o un evento primitivo
eP o la negazione e di un tale evento e--.
Dato un insieme di eventi E  P la transizione t è abilitata da E se
eE per ogni e  trigger(t) ed e  E per ogni e--  trigger(t).
Denotiamo con triggered(E) l’insieme di transizioni abilitate da E.
Denotiamo con actions(t) l’insieme di eventi g1,…, gn, giP, 1i0,
generati dalla transizione t. Per un insieme di transizioni T, si ha
generated(T) =  t  T actions(t).
Semantica PS91 (7)
Due transizioni t1, t2 sono consistenti se t1= t2 oppure
arena(t1)_|_arena(t2). In caso contrario le transizioni sono in
conflitto. Ogni transizione è consistente con se stessa.
Un insieme di transizioni T è un insieme consistente se t1, t2 sono
consistenti per ogni t1, t2  T. Denotiamo con consistent(T)
l’insieme di tutte le transizioni che sono consistenti con ogni t  T.
Running example (1)
Esempio
Binary_stopwatch
ShowTime
a
a
Stopwatch
Off
b
On
High
Medium
H0
cm/
cl
b
cm cl/
H1
cm
M0
M1
Low
cl
L0
Time
/cl
L1
Time
Running example (2)
L’attività dell’orologio ha due modi, Stopwatch e ShowTime. Il
sistema passa da uno stato all’altro all’occorrenza dell’evento a che
può rappresentare il premere il bottone dell’orologio. Quando il
sistema è nel modo Stopwatch è nello stato Off e va nello stato On
all’occorrenza di b che può rappresentare il premere un altro
bottone dell’orologio. Lo stato On rappresenta il conteggio del
tempo. Lo stato On consiste di tre sottostati Low, Medium e High
che rappresentano tre bit di un contatore binario. Ciascun contatore
può essere a zero oppure a uno. Inizialmente i contatori sono tutti a
zero. Il conteggio è stimolato dal segnale esterno Time. Quando un
contatore passa da uno a zero emette un segnale che fa passare di
stato il contatore della cifra di ordine più alto. Tutte le reazioni
hannoluogo nello stesso passo stimolato da Time. Ad ogni punto
dell’attività la pressione del bottone b ferma il sistema e la
pressione di a mostra il tempo conteggiato.
Semantica PS91 (8)
Si abbia una configurazione C e un insieme di eventi primitivi I  P. Si
vuole definire un insieme di transizioni T che è fatto in un solo passo in
risposta a I. Questo passo sarà costruito incrementalmente prendendo
dapprima l’insieme delle transizioni che sono abilitate da I che
generano altri eventi e abilitano altre transizioni, e cosí via.
La funzione abilitante En(T) assume che si sia già deciso di effettuare
l’insieme di transizioni T e identifica tutte le transizioni che sono
abilitate come conseguenza della decisione
En(T) = relevant(C)  consistent (T)  triggered (I  generated(T))
dove relevant(C) è l’insieme di tutte le transizioni i cui insiemi sorgente
sono contenuti nella configurazione C. L’insieme consistent(T) sceglie
dall’insieme relevant(C) quelle transizioni che sono consistenti con ogni
t  T. Si considerano solo quelle transizioni che sono abilitate dagli
eventi in I e quelle che sono abilitate da queste.
Running example (3)
Sia C = {Binary-Stopwatch, Stopwatch, On, H0, M1, L1}.
Le transizioni rilevanti a C sono
relevant( C) = Stopwatch  ShowTime, On  Off, H0  H1,
 M0, L1  L0.
M1
Consideriamo l’insieme di eventi di input I = {a, time} e prendiamo
T = {L1  L0}. Allora si ha
consistent(T) = {L1  L0, M0  M1, M1  M0, H0  H1, H1H0}
I  generated(T) = {a, Time, cl}
triggered (I  generated(T)) = {L0  L1, L1  L0, M0  M1,
M1  M0, Stopwatch  ShowTime, ShowTime  Stopwatch}
Abbiamo infine
En({L1  L0})= {L1  L0, M1  M0}.
Semantica PS91 (9)
Una proprietà importante della funzione En è che sia concava. Siano X e
Y due domini. Una funzione f : 2X  2Y è concava se per ogni X1, X2,
X3  X con X1  X2  X3 si ha f(X1)  f(X3)  f(X2). Se f,g sono
funzioni concave lo è anche la loro intersezione f  g. Infatti (f(X1) 
g(X1))  (f(X3)  g(X3)) = (f(X1)  f(X3))  (g(X1)  g(X3))  f(X2) 
g(X2).
Una funzione è monotonicamente decrescente se per ogni X1  X2 
X3 si ha f(X3)  f(X2)  f(X1) e quindi f(X1)  f(X3) = f(X3)  f(X2).
Ora relevant (C) essendo indipendente da T, è concava. Mostriamo che
triggered (E) è una funzione concava da 2P a 2 T . Basta dimostrare che se
E1  E2  E3 sono tre insiemi di eventi e una transizione t è abilitata sia
da E1 che da E3 è abilitata anche da E2 . Consideriamo un evento e 
trigger(t). Poiché t  triggered(E1) ne segue e  E1 e quindi anche e  E2
poiché E1  E2. D’altra parte se e--  trigger(t) e t  triggered(E3) allora
non e  E3 e quindi anche non e  E2  E3 . Poiché la concavità è chiusa
per intersezione, En(T) è una funzione concava di T.
Semantica PS91 (10)
Consideriamo ora due definizioni degli insiemi di transizioni che sono
considerati passi ammissibili da una configurazione C in risposta a un
insieme di eventi esterni T. La prima è una definizione operazionale, la
seconda è una definizione dichiarativa. Mostreremo che, grazie alla
concavità, le due definizioni coincidono.
La definizione operazionale è basata su una procedura non
deterministica che costruisce un passo T aggiungendo una transizione
alla volta.
Semantica PS91 (11)
Procedura Step construction
1. Poni T = 
2. Confronta En(T) con T
2.1 Se T = En(T) riporta successo
2.2 Se T  En(T) prendi una transizione t  En(T)-T, aggiungila a
T e ripeti il passo 2
2.3 altrimenti, ossia se non T  En(T) riporta fallimento.
Un insieme T che può essere ottenuto con una successione di scelte
di transizioni t  En(T)-T è chiamato costruibile.
Running example (4)
Sia T =  , I = {time}.
En() = {L1 L0} quindi T  En(T).
Poniamo allora T = {L1 L0}. Abbiamo En ({L1 L0}) = {L1 L0,
M1 M0} e quindi ancora T  En(T).
Poniamo allora T = {L1 L0, M1 M0}.
Abbiamo En {L1 L0, M1 M0} = {L1 L0, M1 M0, H0  H1} e
quindi ancora T  En(T).
Poniamo T = {L1 L0, M1 M0, H0  H1} e abbiamo infine
En(T) = T.
Semantica PS91 (12)
Un insieme di transizioni T è separabile se esiste un sottoinsieme
T’T tale che En(T’)  (T-T’) = , altrimenti è detto inseparabile.
Un insieme di transizioni T inseparabile che soddisfa T = En(T)
è detto passo ammissibile del sistema.
Proposizione. Un insieme di transizioni T è una soluzione
inseparabile dell’equazione T = En(T) se e solo se è costruibile.
Prova. Assumiamo che t0 sia una soluzione inseparabile
dell’equazione T0 = En(T0). Mostriamo che T0 è costruibile.
Applichiamo la procedura Step construction aggiungendo nel passo
2.2 solo transizioni nell’insieme (En(T)-T)  T0 .
Semantica PS91 (13)
a) La procedura non può fallire.
Inizialmente si ha T =  che implica T  En(T). Assumiamo che la
procedura fallisca dopo aver aggiunto una transizione t a un T  T0.
Questo implica che sia T  En(T), ma esista un t’  T  {t} tale che
t’  En(T {t}). Se t’ = t poiché t  (En(T)-T)  T0 segue t’  En(T).
Altrimenti t’  T  En(T) e quindi ancora t’  En(T). Inoltre poiché
t’  T  {t}  T0 e T0 = En(T0) segue t’  En(T0).
Cosí abbiamo identificato tre insiemi di transizioni T  T  {t}  T0.
Con t’ appartenente a En(T) e a EN(T0) ma non a En(T {t}). Ma
questo contraddice che la funzione En sia concava. Quindi la
procedura non può fallire.
Semantica PS91 (14)
b) La procedura non può fermarsi a T  T0.
La procedura può fermarsi a T  T0 solo se (En(T)-T)  T0 = , ma
(En(T)-T)  T0 = En(T)  (T0 -T) =  contraddice il fatto che T sia
inseparabile.
Viceversa, sia stato ottenuto T con la procedura Step-construction.
Mostriamo che T è una soluzione inseparabile. Siano le transizioni
ordinate in una sequenza t1, t2 , …, tn secondo l’ordine della loro
aggiunta a T. Poiché la costruzione si è fermata T abbiamo che T
soddisfa T = En(T).
Rimane da mostrare che T è inseparabile.
Consideriamo un T’  T . Sia tk la prima transizione nell’ordinamento
che appartiene a T-T’. Asseriamo che tk  En(T’), che conduce al fatto
che En(T’)  (T -T’)   (poiché tk appartiene a entrambi gli insiemi).
Semantica PS91 (15)
Assumiamo, al contrario, che tk  En(T’). Allora abbiamo tre insiemi:
T1 = {t1, t2 , …, tk-1} , T2 = T’, T3 = T = {t1, t2 , …, tn } tali che T1  T2
 T3 e tuttavia
1. tk  En({t1, t2 , …, tk-1})
2. tk  En(T’)
3. tk  En(T)
1 segue dal fatto che la procedura Step-construction prende le
transizioni da aggiungere solo se sono abilitate sotto
l’approssimazione corrente, 2 è il nostro assunto, 3 segue dal fatto che
tk  T = En(T).
Ma questo contraddice la proprietà di concavità. Dobbiamo allora
concludere che En(T’)  (T -T’)   per un T’ T, e quindi T è
inseparabile.
Semantica PS91 (16)
Vediamo ora l’effetto del passo T. Come reazione all’input I vengono
generati gli eventi generated(T). La configurazione successiva è
Nextconfig(C,T) = completion ((C- children*(arena (T)))tT target(t))
Ossia l’effetto di ogni transizione t  T sulla configurazione C è di
rimuovere da C tutti gli stati che sono tra i discendenti di arena(T) e di
aggiungere a C tutti gli stati che sono in target di T. Questo dà una
configurazione parziale il cui completamento per default dà la nuova
configurazione risultante dal passo T.
Running example (5)
Asssumiamo che C sia il completamento per default dell’insieme di
stati consistente {H0, M1, L1}. Supponiamo che sia I = { Time}.
Il solo passo possibile consiste dell’insieme di transizioni
T = {L1  L0, M1  M0, H0  H1} che genera gli eventi
addizionali cl, cm. Per calcolare la nuova configurazione prima
sottraiamo da C le arene delle tre transizioni e i loro figli, ossia
rimuoviamo da C gli stati High, H0, Medium, M1, Low, L1, quindi
aggiungiamo a C i bersagli delle tre transizioni e completiamo,
ossia aggiungiamo High, H1, Medium, M0, Low, L0.