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

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Sat, 28 Jan 2023 11:00:24 -0800 (PST)

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)

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 get

for a total of *3 states but 2 distinct* ones.

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.

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

- Prev by Date:
**[tlaplus] Re: In TLC, what does the num parameter do given the -simulate flag?** - Next by Date:
**Re: [tlaplus] A simple (distinct) states question** - Previous by thread:
**Re: [tlaplus] checking that a pluscal spec implements another pluscal spec** - Next by thread:
**Re: [tlaplus] A simple (distinct) states question** - Index(es):