quint
quint copied to clipboard
Simulator crashes with invalid `init` action
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: '=='
}
This seems to be also happening when calling setBy
with a non-existent key
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.
Changing the trace.result/outcome from Maybe to Either should help identify the problem(s) here.
A similar problem: the simulator crashes when running with an invariant that does not exist (ie, mistyping the name)