verify: surprising temporal result

[lucab]

I was trying to verify a (state-machine plus math) model with some basic temporal props and I think I ran into a surprising false-negative result (likely a shortcoming in Apalache itself, I guess).

After deleting all the extra details, this is the minimal reproducer I have:

module buggyTemporals {
    var myState: int

    action init = myState' = 0

    action step = {
        myState' = myState + 1

        // This other logic instead gets a proper counterexample:
        // myState' = 1
    }

    temporal temporalProps = always(myState < 0)

    // Same result for:    
    // temporal temporalProps = eventually(myState < 0)
}

$ quint verify --temporal temporalProps buggyTemporals.qnt

[ok] No violation found (179ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.

Just for completeness, increasing the number of steps does not help finding a counterexample.

I tried tweaking slightly the example above in this way:

    action step = {
        if (myState > 5) {
            myState' = myState
        } else {
            myState' = myState + 1
        }
    }

In this other case, Apalache detects that it eventually enters a loop where temporalProps is not valid. However, the counterexample shows that it was already not valid in State 0:

[State 0]
{
  __InLoop: false,
  [...]
  myState: 0
}

[...]

[State 6]
{
  __InLoop: false,
  [...]
  myState: 6
}

[State 7]
{
  __InLoop: true,
  [...]
  myState: 6
}

While I can understand that eventually() may have some troubles without a cap on the counter, I'm more concerned about the verification result of the always() property which looks like a verifier bug.

[bugarela]

Thanks for reporting! I've actually come across some examples where temporal property verification is flaky in apalache. For example, it reports [ok] for this:

module test {
  var x: int

  action init = x' = 0
  action step = x' = x + 1

  temporal prop = always(next(x) < x)
}

I think the plan here is:

1. Check whether this problems also occur with TLA+ (using Apalache direcly)

• If not, then there should be a problem in the translation from Quint to TLA+ (unlikely), and we can fix the translation

2. If yes, then

• Open an issue in Apalache
• Integration with TLC #1424 so people can use TLC for temporal properties instead.

For now, I guess the workaround for anyone needing temporal properties is to quint compile the file into TLA+ and then use TLC manually. The compilation process is not 100% perfect yet (you might need to adjust the init definition and potentially convert empty records into empty tuples since TLA+ doesn't have empty records), but it is usually easy to get the file to valid TLA+ with the feedback from TLC error messages.

[lucab]

@bugarela thanks for the detailed instructions! I did the quint compile dance (with a minor manual fix) and checked the TLA+ spec directly with both TLC and Apalache. The former reports a proper counterexample while the latter reports a false negative NoError.
I've forwarded all the details to apalache-mc/apalache#2985.