Stuttering steps are not inserted for unchanged steps

[riz0id]

The current algorithm for checking the "eventually" modality has unexpected failures for specifications with next actions that do not make progress. If a specification does not explicitly assign the new values for the specification state using the prime operation, the model checker will not insert a stutter-step. The failure to introduce a stutter-step can cause the eventually checker to refute valid specifications.

Minimal Example

Considering the following specification:

type AlphabetVars = '["letter" # Char]

type AlphabetSpec = Specification AlphabetVars '["next" # 'WeakFair] '["isLetterZ" # 'Eventually]

isLetterZ :: Temporal AlphabetVars Bool
isLetterZ = do
  clock <- plain #letter
  pure (clock == 'z')

bitClockSpec :: AlphabetSpec
bitClockSpec =
  Specification
    { specInit = ConF #letter (pure 'a') NilF
    , specNext = ConF #next (ActionWF next) NilF
    , specProp = ConF #isLetterZ (PropF isLetterZ) NilF
    }

If we define the next function to be:

next :: Action AlphabetVars Bool
next = do
  letter <- plain #letter
  #letter .= pure (succ letter)
  pure (letter < 'z')

The model checker is able to find evidence that satisfies the proposition "eventually, the unprimed value of letter will be equal to the character 'z'". This is due to the final stutter-step satisfying plain #letter == 'z', which can be seen in the trace:

$ cabal v2-repl integration-tests
ghci> import Specifications.Alphabet
ghci> :set args --trace --diagram
ghci> alphabetSpecInteract
* 0x5a7b1068
│   #letter = 'z'
│ 
* 0x5a7b1068
│   #letter = 'z'
│ 
* 0x6a7b1068
│   #letter = 'y'
│ 
... 
│ 
* 0xdb7b1068
│   #letter = 'b'
│ 
* 0xeb7b1068
    #letter = 'a'

check(pass)+trace

However, if next is reformulated such that #letter .= pure (succ letter) is only evaluated conditionally, then the resulting trace no longer contains the stutter-step satisfying plain #letter == 'z'. For example, the following definition of next:

next :: Action AlphabetVars Bool
next = do
  letter <- plain #letter
  when (letter < 'z') do
    #letter .= pure (succ letter)
  pure True

Should be equivalent to the former definition. However, wrapping(.=) with a when guard produces the following trace:

$ cabal v2-repl integration-tests
ghci> import Specifications.Alphabet
ghci> :set args --trace --diagram
ghci> alphabetSpecInteract
refuted property: eventually "isLetterZ"
  * from: 0x5a7b1068
      #letter = 'z'
  * to: 0x6a7b1068
      #letter = 'y'

* 0x5a7b1068
│   #letter = 'z'
│ 
* 0x6a7b1068
│   #letter = 'y'
│ 
...
│ 
* 0xdb7b1068
│   #letter = 'b'
│ 
* 0xeb7b1068
    #letter = 'a'

check(fail)+trace