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

*From*: Calvin Loncaric <c.a.loncaric@xxxxxxxxx>*Date*: Sat, 28 Jan 2023 22:42:38 -0800*References*: <61933610-d4ee-46a2-aa35-ebd0f3ed1eb0n@googlegroups.com> <CABf5HMhx8oz3rRDgRPLD=TGKuj=Lxu_DANBOe1z7nVZ9bJoLRQ@mail.gmail.com> <f4b85f25-268e-02d3-d25d-38504bc1a6e4@gmail.com>

My mistake! I thought the total number of states could be affected by thread interleaving in parallel TLC, but it seems that's not the case. :)

--

Calvin

On Sat, Jan 28, 2023 at 10:05 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:

--AFAICT the number of total states should be stable for the same spec and the same model, unless model checking ends early due to a broken invariant. I've used (total states / distinct states) as a spec fingerprint in my teaching materials and nobody's ever reported a divergence. Do you know an example spec where this doesn't hold?

H

On 1/28/2023 3:51 PM, Calvin Loncaric wrote:

You should almost always ignore the total number of states (3). It is affected by lots of factors and can change from run to run on the same input spec. Only the number of distinct states (2) really matters.

The more interesting question is why you saw two "B"s!

The model checker does not just visit every reachablestate; it also visits every reachableaction.Your spec has two reachable states:

v="A"v="B"

...and two reachable actions:

v="A" ---[SetV]---> v="B"

v="B" ---[SetV]---> v="B"Yes, the second one is indeed a legal action, even though it doesn't change any of the variables! I suspect the second "B" is the result of the second possible action, where v does not change.

To see this in action, add "/\ v' /= v" to the definition of SetV before the PrintT call, thus requiring it to change the value of v. The second "B" should go away.

One final warning: the PrintT calls happen while the model checker is exploring. The model checker promises to explore everything, but it doesn't really promise anything about what order it explores things or how many times it visits them. If you use multiple threads, two different threads might visit the same action in parallel, and you will get duplicated outputs. So while there is a good explanation for the two "B"s in this simple case, you shouldn't necessarily rely on PrintT to behave how you expect it does in a real programming language.

--Calvin

--On Sat, Jan 28, 2023 at 11:00 AM jack malkovick <sillymouse333@xxxxxxxxx> wrote:

I have this very simple spec

EXTENDS TLC

VARIABLES v

vars == << v >>

Init == v = "A" /\ PrintT("A")

SetV ==

/\ v' = "B"

/\ IF v' = "B" THEN PrintT("B") ELSE TRUE

Spec == Init /\ [][SetV]_vars /\ WF_vars(SetV)

If I model check it in TLA Toolbox, I get1 state found for action Init and 2 states found for action SetVfor a total of3 states but 2 distinctones.

The output is also "A", "B", "B". Why two "B"s? Why 2 identical states?--

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/61933610-d4ee-46a2-aa35-ebd0f3ed1eb0n%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/CABf5HMhx8oz3rRDgRPLD%3DTGKuj%3DLxu_DANBOe1z7nVZ9bJoLRQ%40mail.gmail.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/f4b85f25-268e-02d3-d25d-38504bc1a6e4%40gmail.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/CABf5HMhSH2C58fRuTLbcpsTV9VK4j4BP0kfgFsV6g0LvXYg46A%40mail.gmail.com.

**References**:**[tlaplus] A simple (distinct) states question***From:*jack malkovick

**Re: [tlaplus] A simple (distinct) states question***From:*Calvin Loncaric

**Re: [tlaplus] A simple (distinct) states question***From:*Hillel Wayne

- Prev by Date:
**Re: [tlaplus] A simple (distinct) states question** - Next by Date:
**Re: [tlaplus] checking that a pluscal spec implements another pluscal spec** - Previous by thread:
**Re: [tlaplus] A simple (distinct) states question** - Next by thread:
**[tlaplus] Specifying initial state of a spec while running TLC** - Index(es):