`quint verify` fails when `--invariant` is not Boolean

konnov commented 2 months ago

Consider the following spec:

module t {                                                                                                                              
  var x: int
  val DEFAULT = 0
  action init = x' = DEFAULT
  action step = x' = x + 1
}

Execute the following command:

quint verify --invariant=DEFAULT t.qnt
error: internal error: while parsing in Apalache:
'key not found: 22'
Please report an issue: https://github.com/informalsystems/quint/issues/new

The reason for the failure is that DEFAULT is not a value of type bool. Unfortunately, it's impossible to figure that out from the error message. It would be great, if quint verify could print a readable error message.

bugarela commented 1 month ago

The error for quint run is not so bad, but it should also be a proper error (this one is throwing). Commenting here since the fix for both should be the same.

Error: Expected a Boolean value
    at RuntimeValueInt.toBool (/home/gabriela/projects/quint/quint/dist/src/runtime/impl/runtimeValue.js:366:19)
    at isTrue (/home/gabriela/projects/quint/quint/dist/src/runtime/impl/compilerImpl.js:1268:55)
    at /home/gabriela/projects/quint/quint/dist/src/runtime/impl/compilerImpl.js:1300:30
    at EitherConstructor.chain (/home/gabriela/projects/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:119:16)
    at doRun (/home/gabriela/projects/quint/quint/dist/src/runtime/impl/compilerImpl.js:1266:18)
    at Object.eval (/home/gabriela/projects/quint/quint/dist/src/runtime/impl/base.js:98:20)
    at compileAndRun (/home/gabriela/projects/quint/quint/dist/src/simulation.js:75:19)
    at runSimulator (/home/gabriela/projects/quint/quint/dist/src/cliCommands.js:422: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:60:39

konnov commented 1 month ago

The error for quint run is not so bad, but it should also be a proper error (this one is throwing). Commenting here since the fix for both should be the same.

Error: Expected a Boolean value

Yeah, I agree that this error would give the user a slight better hint about what is going on

informalsystems / quint

`quint verify` fails when `--invariant` is not Boolean #1460