Re: [tlaplus] for all, the transition condition is true?

[Hillel Wayne <hwayne@xxxxxxxxx>]

Hi Juliet,

We can rewrite Next as:

Next == \A x \in {1, 2}:
  IF x = 1 THEN q' = [q EXCEPT  !["a1"] = Append(@, x)]
  ELSE IF x = 2 THEN q' = [q EXCEPT  !["a2"] = Append(@, x)]
  ELSE UNCHANGED q

In practice that will be

Next ==
  /\ q' = [q EXCEPT  !["a1"] = Append(@, 1)]
  /\ q' = [q EXCEPT  !["a2"] = Append(@, 2)]

From Init, that will be equivalent to

Next ==
  /\ q' = [a1 |-> <<1>>, a2 |-> <<>>, a3 |-> <<>>]  
  /\ q' = [a1 |-> <<>>, a2 |-> <<2>>, a3 |-> <<>>]

So we have two different values for q', which is impossible, so Next is never enabled.

There are a few different ways you can get what you want, but the simplest is to probably make it explicit:

\* Sequences are functions with domain 1..Len(seq)
Map == <<"a1", "a2", "a3">>
Next ==
  /\ q' = [x \in DOMAIN q |->
     IF Map(x) \in {1, 2}
     THEN Append(q[x], Map(x))
     ELSE q[x]]

H

On 7/24/19 4:02 AM, juliet kim wrote:

Hello, 

Here is a simple specification.

I wonder whether the Next is enabled.

--------------------------------

Variable q

SetA == {"a1", "a2", s3}

Init == q = [a \in  SetA |-> <<>>]

Next = \A x \ {1,2} : 

                         LET m = IF x = 1 THEN "a1"

                                        ELSE 

                                                 IF x = 2 THEN "a2"

                                                 ELSE "a3"

                         IN

                                q' = [q EXCEPT  ![m] = Append(@, x)]

Spec = Init /\ [][Next]_q

For all x, Next can be true?

When I use TLC, it doesn't seem to be true. For example, for 1, it's true at first but next 2 is not true.

Ideally, I expected that q's state is like [a1 |-> <<1>>, a2 |-> <<2>>, a3 |-> <<>>], but Next action is not enabled.

I want q's field value to be changed for all x values.

I need your advice.

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/fd9c65b6-68c6-418e-9436-ab4e5cacf99a%40googlegroups.com.

--
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/b5d3149e-0c47-e6a2-cc83-3cf5acd237ee%40gmail.com.