informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
607 stars 30 forks source link

Simulator crashes with invalid `init` action #1439

Open bugarela opened 1 month ago

bugarela commented 1 month ago

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 commented 1 month ago

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

bugarela commented 1 month ago

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 commented 2 weeks ago

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

ivan-gavran commented 23 hours ago

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