Uninformative error message when using .fail() in tests

[p-offtermatt]

Take this module:

module test {
    var x: int

    action init = x' = 1

    action inc = x' = x + 1

    action failAction =
        all {
            false,
            x' = 0
        }

    run FailTest = {
        init.then(
            failAction.fail()
        ).then(
            inc
        )
    }    
}

Consider in particular the FailTest. This might seem reasonable at first glance, but running it gives the following error message:

  test
    1) FailTest failed after 1 test(s)

  1 failed

  1) FailTest:
      /Users/offtermatt/projects/interchain-security/tests/mbt/model/test.qnt:2:5 - error: [QNT502] Variable x is not set
      2:     var x: int
    Use --seed=0x2f54eaed29061 --match=FailTest to repeat.

  Use --verbosity=3 to show executions.
  Further debug with: quint --verbosity=3 test.qnt
/Users/offtermatt/projects/interchain-security/tests/mbt/model/test.qnt:2:5 - error: [QNT502] Variable x is not set
2:     var x: int
       ^^^^^^^^^^

error: Tests failed

In particular, the error message is test.qnt:2:5 - error: [QNT502] Variable x is not set

The real error seems to be from line 16, e.g. if I replace that line simply with inc, everything works fine.

I personally think the original test is probably reasonable and should work, but I don't understand the semantics of fail and then closely enough to be sure. However, if it is expected that it does not work, the error message should for sure point not to line 5, but in the best case to line 16, and it should be detectable during typechecking (just like having actions with different updates gives an error during typechecking).

$ quint --version
0.18.3

[konnov]

As far as I remember, fail does not expect any extensions of an execution. It's meant to be a terminal action. However, I agree that it is not obvious from the error message.

[p-offtermatt]

I see. I think it would be useful to allow fail inside traces - it can be useful to e.g. check that a certain action is disabled, even when the run itself is useful and we want to keep it going (e.g. imagine that we want to check that at a certain point of a run, n different actions are disabled) Would be nice to have, but probably not super high priority.