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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 11 Jul 2023 08:21:47 +0200*References*: <bfacc5e7-ff53-4623-b03f-61f332fc9128n@googlegroups.com>

The action Next requires i to be 0, so it cannot be taken after the first transition. TLC signals a deadlock at a state when the next-state transition relation Next is disabled. Stuttering is always possible in TLA+, thus considering that a state isn't deadlocked because it has the default self loop wouldn't make sense. If you really want to consider TLC the state not to be deadlocked, you can write Next == \/ /\ i = 0 /\ i' = i+1 \/ i' = i This is essentially what the PlusCal translator does so that termination states (i.e., when all processes reached label "Done") are not flagged as deadlocks by TLC. Stephan
--
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/1FC8E031-8364-4DC3-B370-D4022F9BC804%40gmail.com. |

**References**:**[tlaplus] About stuttering steps and deadlock in TLC***From:*Jerry Clcanny

- Prev by Date:
**[tlaplus] About stuttering steps and deadlock in TLC** - Next by Date:
**Re: [tlaplus] About stuttering steps, deadlock and Implementation** - Previous by thread:
**[tlaplus] About stuttering steps and deadlock in TLC** - Next by thread:
**[tlaplus] About always and eventually.** - Index(es):