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

*From*: juliet kim <myjulietkim@xxxxxxxxx>*Date*: Wed, 24 Jul 2019 02:02:23 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] for all, the transition condition is true?***From:*Hillel Wayne

- Prev by Date:
**[tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm** - Next by Date:
**Re: [tlaplus] for all, the transition condition is true?** - Previous by thread:
**Re: [tlaplus] What's wrong with the following behaviors?** - Next by thread:
**Re: [tlaplus] for all, the transition condition is true?** - Index(es):