About stuttering steps and deadlock in TLC

[Jerry Clcanny]

````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
```

[Stephan Merz]

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bfacc5e7-ff53-4623-b03f-61f332fc9128n%40googlegroups.com.