About stuttering steps, deadlock and Implementation

[Jerry Clcanny]

I have a spec named SimpleProgram, which disallow i stays unchanged (not stuttering step):

```tla

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

[Stephan Merz]

Not so fast: 

   [Next]_<<>> 

= Next \/ UNCHANGED << >> \* by definition of [A]_v

= Next \/ (<< >>' = << >>) \* by definition of UNCHANGED

= Next \/ (<< >> = << >>) \* since << >> is a constant expression

= Next \/ TRUE

Now, TRUE allows for any step, including stuttering transitions: there is no way you can write a TLA+ specification that disallows stuttering steps.

Moreover, TRUE covers any actions that your implementation takes, so refinement is trivial.

For the question about deadlock, see my answer to your other question.

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/19c210b4-5a03-4aa7-bba3-9d234d2c6bban%40googlegroups.com.