Suboptimal error reporting on out-of-bounds in the simulator

[konnov]

It looks like the new version of the simulator reports obvious out-of-bounds errors quite suboptimally.

Here is my spec:

module t {                                                                                                                         
    var myMap: int -> int

    action init = {
        myMap' = Map(1 -> 1)
    }

    action step = {
        nondet i = 0.to(10).oneOf()
        myMap' = myMap.put(i, i)
    }

    // this is my buggy invariant
    action inv = myMap.get(0) == 0
}

Here is how I run the simulator:

$ quint run --invariant=inv t.qnt

This is the message by quint run:

quint run --invariant=inv t.qnt
quint run <input>

Simulate a Quint specification and check invariants

Options:
  --help         Show help                                             [boolean]
  --version      Show version number                                   [boolean]
  --out          output file (suppresses all console output)            [string]
  --main         name of the main module (by default, computed from filename)
                                                                        [string]
  --out-itf      output the trace in the Informal Trace Format to file, e.g.,
                 out_{seq}.itf.json where {seq} is the trace sequence number
                 (suppresses all console output)                        [string]
  --max-samples  the maximum number of runs to attempt before giving up
                                                       [number] [default: 10000]
  --n-traces     how many traces to generate (only affects output to out-itf)
                                                           [number] [default: 1]
  --max-steps    the maximum on the number of steps in every trace
                                                          [number] [default: 20]
  --init         name of the initializer action       [string] [default: "init"]
  --step         name of the step action              [string] [default: "step"]
  --invariant    invariant to check: a definition name or an expression
                                                    [string] [default: ["true"]]
  --seed         random seed to use for non-deterministic choice        [string]
  --verbosity    control how much output is produced (0 to 5)
                                                           [number] [default: 2]
  --mbt          (experimental) whether to produce metadata to be used by
                 model-based testing                  [boolean] [default: false]

AssertionError [ERR_ASSERTION]: invalid simulation failed to produce a result
    at [REDACTED]/quint/quint/dist/src/simulation.js:81:30
    at Array.forEach (<anonymous>)
    at compileAndRun ([REDACTED]/quint/quint/dist/src/simulation.js:79:15)
    at runSimulator ([REDACTED]/quint/quint/dist/src/cliCommands.js:423:51)
    at EitherConstructor.asyncChain ([REDACTED]/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at [REDACTED]/quint/quint/dist/src/cli.js:60:39 {
  generatedMessage: false,
  code: 'ERR_ASSERTION',
  actual: false,
  expected: true,
  operator: '=='
}

I would rather expect a trace that explains the error.

[bugarela]

Hey! This is already fixed in the latest version (>= 0.22.0). This is what I get:

quint run ../local/test.qnt --invariant=inv
/home/gabriela/projects/quint/local/test.qnt:14:18 - error: [QNT507] Called 'get' with a non-existing key. Key is 0. Map has keys: 1
14:     action inv = myMap.get(0) == 0
                     ^^^^^^^^^^^^

error: Runtime error