Modelator pre-0.3 code review

[andrey-kuprianov]

Let's review the code, and collect here improvement suggestions; first of all about the code structure and APIs, but also anything else.

Some will apply to the version 0.3, but most are for the post-0.3 work.

[andrey-kuprianov]

.modelator directory

Currently, whenever the tool is executed ,.modelator dir will be created in the the current directory. I don't think this is a good idea, especially because we download a lot of JARs; switching to another directory will mean we need to download them again and again.

The options I think are as follows:

• create .modelator in the user's home directory
• if the user in a git repo, create it in the root of the repo.

[andrey-kuprianov]

Rework Options

Options are carried over in multiple places throughout the codebase. For me this doesn't seem like a good idea:

• it is a lot of boilerplate code
• not all options are relevant in all contexts (e.g. what is the semantics of selecting the ModelChecker when we call a methods of a specific model checker, Apalache or TLC?)

Should we just store the options in some sort of a global map?

Also, we need to rethink in general what the options contain

[andrey-kuprianov]

Rework Apalache error extraction

Apalache error extraction will not work for multiline errors.

Probably better to orient not to the fixed list of error messages, but to the E@ marker.

[andrey-kuprianov]

Extract path handling

Currently filesystem paths are handled explicitely in multiple places, e.g. in Apalache and in TLC.

The path handling should be pulled into a global shared implementation, a central place, such that only it knows where everything is stored. All other code should work with abstract artifacts, and ask the path handling library to read or write files, when needed.

[andrey-kuprianov]

Generalize from model checkers

Extract common functionality from MCs into a shared implementation

[andrey-kuprianov]

Make dependencies explicit

Currently both via CLI and via Rust API, the user specifies a single TLA+ file; all other dependencies are pulled automatically by model checkers.

We need to make those dependencies explicit, and obvious to the user, such that the constituent files are not forgotten to be added to the repo, for example. There are a couple of options here:

• Always ask the user for a complete list of all files, and the tool will fail if any dependency is missing.
• Generate the list of dependencies automatically, e.g. via parsing EXTENDS lists from TLA+, but then make the user aware of those dependencies, or require their confirmation of those.