[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLC error about a variable that was changed while it is specified as UNCHANGED

Hello, could someone let me know what I'm doing wrong here
I have a button interface that is responsible for 

-------------------------- MODULE ButtonInterface --------------------------
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

Now when I run this in TLC I get the error message 

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?


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f1e51aaf-e1e9-40f4-9823-b4894e1cf60c%40googlegroups.com.