Re: [tlaplus] About stuttering steps and deadlock in TLC

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

On 11 Jul 2023, at 04:18, Jerry Clcanny <a837940593@xxxxxxxxx> wrote:

````tla
--------------------------- MODULE SimpleProgram ---------------------------
\* SimpleProgram.tla
EXTENDS Integers
VARIABLES i

Init == i = 0

Next ==
/\ i = 0
/\ i' = i + 1

SimpleProgramSpec ==
/\ Init
/\ [][Next]_<<i>>
============================================================================
```

```cfg
SPECIFICATION
SimpleProgramSpec
```

When I execute `tlc SimpleProgram`, why the tlc complains deadlock:

```text
Finished computing initial states: 1 distinct state generated at 2023-07-11 02:17:20.
Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
i = 0

State 2: <Next line 9, col 3 to line 10, col 15 of module SimpleProgram>
i = 1
```

--
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/bfacc5e7-ff53-4623-b03f-61f332fc9128n%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/1FC8E031-8364-4DC3-B370-D4022F9BC804%40gmail.com.