--------------------------- MODULE SimpleProgram ---------------------------
\* SimpleProgram.tla
EXTENDS Integers
VARIABLES i
Init == i = 0
Next ==
/\ i = 0
/\ i' = i + 1
SimpleProgramSpec ==
/\ Init
/\ [][Next]_<<>>
============================================================================
```
I have another spec named SimpleProgramImpl tried to implement SimpleProgram:
```tla
--------------------------- MODULE SimpleProgramImpl -----------------------
\* SimpleProgramImpl.tla
EXTENDS Integers
VARIABLES i, j
Init ==
/\ i = 0
/\ j = 0
Next ==
\/ /\ i = 0
/\ j = 0
/\ j' = j + 1
/\ UNCHANGED <<i>>
\/ /\ i = 0
/\ j = 1
/\ i' = i + 1
/\ UNCHANGED <<j>>
SimpleProgramImplSpec ==
/\ Init
/\ [][Next]_<<i, j>>
SP == INSTANCE SimpleProgram
SimpleProgramSpec == SP!SimpleProgramSpec
\* https://lamport.azurewebsites.net/video/video8b-script.pdf
\* 1. Asserts that for every behavior:
\* if it satisfies SimpleProgramImplSpec, then it satisfies SimpleProgramSpec.
\* 2. Every behavior satisfying SimpleProgramImplSpec satisfies SimpleProgramSpec.
\* 3. SimpleProgramImplSpec implements SimpleProgramSpec.
THEOREM SimpleProgramImplSpec => SimpleProgramSpec
============================================================================
```
```cfg
\* SimpleProgramImpl.cfg
SPECIFICATION
SimpleProgramImplSpec
PROPERTY
\* THEOREM SimpleProgramImplSpec => SimpleProgramSpec
\* Let TLC check this theorem by adding SimpleProgramSpec
\* as a property to check
\* in a model you constructed for module SimpleProgramImpl.
SimpleProgramSpec
```
I have two questions:
1. When I run `tlc SimpleProgramImpl.tla -config SimpleProgramImpl.cfg`, tlc complains "Deadlock reached", but `SimpleProgramImplSpec` allow stuttering steps.
2. When I run `tlc SimpleProgramImpl.tla -config SimpleProgramImpl.cfg -deadlock`, tlc says "Model checking completed. No error has been found.", but I think `SimpleProgramImplSpec` does not implement `SimpleProgramSpec` because `SimpleProgramSpec` does not allow stuttering steps.
Thanks for reading this!