[tlaplus] About stuttering steps and deadlock in TLC

[Jerry Clcanny <a837940593@xxxxxxxxx>]

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