CLI: model command

[hvanz]

Background/Motivation

A user has written a TLA+ model and wants to parse the TLA+ files, type check the spec, set the model constants.
Once a model is loaded, the user can call the trace command to generate traces from the model.

This command is also an interface to the Model class in Modelator.

Linked documents: CLI ADR

Description: CLI commands

The command atomkraft model is essentially a wrapper around Modelator's Model, where each of its sub-commands would map almost one-to-one to the methods of Model:

atomkraft model load <model-path> # in Model it's the parse_file method
atomkraft model typecheck
atomkraft model instantiate <constant-name> <constant-value>
atomkraft model check [<invariant-list>] [--constants=<name>:<value>,...] # for now, checker is Apalache, and checker params are the default values
atomkraft model sample [<sample-list>] [--constants=<name>:<value>,...] 
atomkraft model last-sample
atomkraft model all-samples
atomkraft model monitor add markdown <monitor-file.md>
atomkraft model monitor add html <monitor-file.html>

Additionally, model will have the following sub-commands that require some extra logic not provided by Modelator:

atomkraft model info # will display filename(s), init, next, constants, invariants, ... 
atomkraft model monitor remove-all # will remove all initialized monitors

Not included in the first prototype:

atomkraft model config load <model-config-file> # will call the `ModelConfig` class in Modelator

Apalache does not require a cfg file with the model.

Artifacts

This module can load a model in memory that can be used by other modules.

Programmatic interface

This module does not expect any connection to other components.

Dependencies

None

Tasks

• Implement the model command and the sub-commands that call Modelator directly.
• Implement the model sub-commands that do not call Modelator directly.
• Add unit tests for model.