-------------------------- MODULE ButtonInterface --------------------------
VARIABLES r,g
TypeInv == r \in BOOLEAN /\ g \in BOOLEAN
ButtonInit == r=TRUE /\ g=FALSE
Idle == r=FALSE /\ g=FALSE
ButtonNext ==
(Idle /\ ((r'=TRUE /\ g'=FALSE) \/ (g'=TRUE /\ r'=FALSE)))
\/ (r=TRUE /\ r'=FALSE /\ UNCHANGED g)
\/ (g=TRUE /\ g'=FALSE /\ UNCHANGED r)
\/ UNCHANGED <<r,g>>
=============================================================================
Then an event generator that relies on signals r and g from the button interface:
------------------------------ MODULE Problem1 ------------------------------
VARIABLES r, g, e_r, e_g, e_clr
TypeInv == r \in BOOLEAN /\ g \in BOOLEAN /\ e_r \in BOOLEAN /\ e_g \in BOOLEAN /\ e_clr \in BOOLEAN
BI == INSTANCE ButtonInterface \* my g and r are substituting for ButtonIfce's g and r
\* can't just write r /\ ~g /\ etc
M_Init == e_r=FALSE /\ e_g=FALSE /\ e_clr=FALSE /\ TypeInv
all_vars == <<r,g, e_r, e_g, e_clr>>
M_Next == (r /\ ~g /\ e_r'=TRUE /\ UNCHANGED <<e_g, e_clr>>)
\/ (g /\ ~r /\ e_g'=TRUE /\ UNCHANGED <<e_r, e_clr>>)
\/ (e_r /\ e_r'=FALSE /\ UNCHANGED <<r, g, e_g, e_clr>>)
\/ (e_g /\ ~e_g'=TRUE /\ UNCHANGED <<r, g, e_r, e_clr>>)
CombinedInit == BI!ButtonInit /\ M_Init
CombinedNext == BI!ButtonNext /\ M_Next
Spec == CombinedInit /\ [][CombinedNext]_all_vars
The variable r was changed while it is specified as UNCHANGED at line 16, col 55 to line 16, col 55 of module Problem1
The variable g was changed while it is specified as UNCHANGED at line 16, col 57 to line 16, col 57 of module Problem1
Deadlock reached.
I've allowed ButtonInterface to stutter, so what's the problem?
Also, somewhat tangential, if I replace the expression (r'=TRUE /\ g'=FALSE) with Only_r' where I define
Only_r == r=TRUE /\ g=FALSE
I get an unexpected exception, I was under the impression that if e was an expression, e' was the same expression with all variables replaced by their primed forms?
thanks