quint icon indicating copy to clipboard operation
quint copied to clipboard

Simulator crashes with invalid `init` action

Open bugarela opened this issue 9 months ago • 4 comments

If the init action refers to vars, the simulator breaks. Instead, we should properly report/explain the error.

MWE:

module test {
  var x: int

  action init = x' = x
  action step = x' = x
}

Results in:

$ quint run test.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
                 (suppresses all console output)                        [string]
  --max-samples  the maximum on the number of traces to try
                                                       [number] [default: 10000]
  --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]

AssertionError [ERR_ASSERTION]: invalid simulation failed to produce a result
    at compileAndRun (/home/gabriela/projects/quint/quint/dist/src/simulation.js:80:26)
    at runSimulator (/home/gabriela/projects/quint/quint/dist/src/cliCommands.js:407:51)
    at EitherConstructor.asyncChain (/home/gabriela/projects/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at /home/gabriela/projects/quint/quint/dist/src/cli.js:58:39 {
  generatedMessage: false,
  code: 'ERR_ASSERTION',
  actual: false,
  expected: true,
  operator: '=='
}

bugarela avatar May 15 '24 17:05 bugarela

This seems to be also happening when calling setBy with a non-existent key

bugarela avatar May 21 '24 23:05 bugarela

Also about setBy: sometimes it properly reports an error, but it seems like it finishes the entire simulation to only then report it. So you wait for nothing.

bugarela avatar May 24 '24 20:05 bugarela

Changing the trace.result/outcome from Maybe to Either should help identify the problem(s) here.

bugarela avatar Jun 10 '24 16:06 bugarela

A similar problem: the simulator crashes when running with an invariant that does not exist (ie, mistyping the name)

ivan-gavran avatar Jun 28 '24 09:06 ivan-gavran