search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
442 stars 40 forks source link

Refactor option configurations #2999

Open konnov opened 2 months ago

konnov commented 2 months ago

The current version relies on pureconfig. As a result, when passing parameters from quint verify, we have a configuration file like this:

{
    "common": {
      "write-intermediate": true,
      "debug": true
    },
    "checker": {
        "discard-disabled": false,
        "no-deadlocks": true,
        "algo": "incremental",
        "tuning": {
            "search.invariant.mode": "after",
            "search.invariantFilter": "(1->.*)"
        }
    }
}

On the other hand, the option processing code is processing options like this:

https://github.com/apalache-mc/apalache/blob/9d89eb39ba9fffc29c7119ac548fc995ca82d048/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala#L683-L692

What is worse, if I pass discardDisabled: true instead of discard-disabled: true in the configuration file, the configuration parser does not complain.

We have to streamline configuration parsing and get rid of unnecessary complexity. Currently, it is very hard to understand what parameters have to be passed, even by reading the code.