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

CombinedNext == M_Next /\ BI!ButtonNext

the error about r and g being changed disappears. The deadlock is still reported, as it should be, given that the execution ends in a state where all variables are FALSE and therefore M_Next is not enabled. (TLC interprets deadlock as a state in which only stuttering is possible.)

You need to understand that TLC evaluates actions from left to right. I believe that what happened with your definition is that TLC chose the first disjunct of ButtonNext (since r and g are both FALSE) and set one of the variables to TRUE but then realized that this was in contradiction with the third disjunct of M_Next, which requires both variables to stutter. I also believe that the message that you are seeing is only a warning, given that TLC in fact constructed the successor state, but I'd like somebody (Markus?) to confirm this, and I agree that it is rather confusing.

–––

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?

TLC interprets the first occurrence of an _expression_ v' = e (where v is a variable and e an _expression_) as an assignment to the variable v. In contrast, the formula Only_r', which expands to

(r = TRUE /\ g = FALSE)'

does not have the syntactic form of an "assignment" and is interpreted as a predicate, but since r' and g' do not yet have assigned values in the successor state, the predicate cannot be evaluated and you see an error message. For similar reasons, you have to write

ButtonInit == r=TRUE /\ g=FALSE

instead of

ButtonInit == r /\ ~g

and you should change the fourth disjunct of M_Next to

\/ (e_g /\ e_g'=FALSE /\ UNCHANGED <<r, g, e_r, e_clr>>)

You can, however, replace the definition of Idle by

Idle == ~r /\ ~g

since it is only ever used as a test and never as an "assignment".

You might wish that TLC were clever enough to make these transformations transparently, but it seems to be too much programming complexity for a rare special case. If you are used to tools such as NuSMV whose modeling language doesn't have the same level of expressiveness as TLA+ and where expressions involving Boolean variables are treated as constraints, you'll have to adapt a bit to the operational interpretation of TLC.

Hope this helps,

Stephan

On 27 Nov 2019, at 02:53, ns <nedsri1988@xxxxxxxxx> wrote:

Let me just clarify my question a bit: I understand that its possible that ButtonInterface can change r even as e_r goes to FALSE. I think what I was (perhaps sloppily) hoping for was that TLC would somehow interpret my spec as requiring that ButtonInterface must stutter in order that r and g can remain unchanged

On Tuesday, November 26, 2019 at 4:53:36 PM UTC-8, ns wrote:
Hello, could someone let me know what I'm doing wrong here
I have a button interface that is responsible for

-------------------------- 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
=============================================================================

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?

thanks

--
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/9756a9c7-2f10-48cc-b6b6-be6ac548ea56%40googlegroups.com.