Skip to content

Latest commit

 

History

History
234 lines (175 loc) · 7.54 KB

usage.md

File metadata and controls

234 lines (175 loc) · 7.54 KB

Usage examples

This document is a work in progress and not all features are documented yet.

This document focuses on usage overview and using the cli executable tool. The functionality is all also useable via library functions. Please see library_usage.py for library function examples.

Getting the cli tool

To install the cli tool

pip install modelator-py;

To call the cli program

modelator <args>

Feature: Extract traces from TLC output in Informal Trace Format format

The TLC model checker will generate counterexamples written in TLA+ and embed them in stdout, interleaved with ASCII text. This output can contain 0, 1 or more traces, and will extract traces generated by TLCs model checking or simulator modes. Run the modelator util tlc itf tool to extract a list of traces in the Informal Trace Format.

There is more than one way to run the tool. The tool always writes output as Json to stdout.

Option 1: provide TLC's stdout data on stdin and flags as cli args

modelator util tlc itf --help
modelator util tlc itf < <TLC_STDOUT_STRING> # Run without flags
modelator util tlc itf --lists=<bool> --records=<bool> < <TLC_STDOUT_STRING> # Run with flags

Option 2: provide TLC's stdout data and flags inside a json object

modelator util tlc itf --json < <JSON_OBJECT>

Flag explanation

# In TLA+ there is no distinction between some functions and sequences. This means
# that a sequence may be represented by function with domain 1..n for some n,
# and vice versa. It is likely convenient to handle such functions as lists.
# Default: True
--lists
# In TLA+ there is no distinction between some functions and records. This means
# that a record may be represented by functions with domain all strings, and vice
# versa. It is likely convenient to handle such functions as records.
# Default: True
--records

Examples

# Provide TLC's stdout data and other flags inside a json object
modelator util tlc itf --json < cli_input_tlc_itf.json > traces.json
# Provide TLC's stdout data on stdin and flags as cli args
modelator util tlc itf --lists=True records=False < TlcTraces.out > traces.json

Nuance

The tool should be able to handle partial TLC outputs (if you hit ctrl+c while it was running, for example). The tool cannot handle lasso shaped traces yet (for temporal property violations). The tool can handle multiple traces (generated when using TLC's continue feature, for example).

FAQ

  1. You can dump various formats using TLC's -dumpTrace flag. Why does this exist?
    This was written before that flag existed. This tool also supports multiple traces
  2. Is this fast?
    Not really: it will take a while to extract traces with hundreds of thousands of states. If you're doing that you're likely doing model-based testing. For regular users, the speed is fine.
  3. Why don't you parse the TTrace files that TLC outputs instead of parsing stdout?
    It probably should be done that way!

Feature: run Apalache model checker

Run the Apalache model checker in a basic 'raw' mode or run it in a 'pure' mode. The pure mode encapsulates file system operations, removing side effects. The raw mode does not, but can be useful for debugging.

Option 1: Run Apalache pure with all input data piped from json

# See cli_input_apalache_pure.json
modelator apalache pure < <JSON_OBJECT>

Option 2: Run Apalache raw with all input data piped from json

# See cli_input_apalache_raw.json
modelator apalache raw --json < <JSON_OBJECT>

Option 3: Run Apalache raw with all input data given in args

modelator apalache raw\
 --jar=<apalache.jar>\ # absolute paths!
 --cwd=<working_dir>\ # absolute paths!
 --cmd=<apalache_command_name>\ # apalache check, typecheck ect
 --file=<.tla file>\ # target
 # other Apalache arguments ...

Argument explanation

apalache pure has no arguments but apalache raw takes modelator and Apalache arguments. Only some are shown here.

# Read arguments from json piped to stdin instead of from sys.argv?
--json
# Full path to directory to run Apalache from.
--cwd=
# Full path to Apalache jar.
--jar=
# Apalache command: check, typecheck ect
--cmd=
# Apalache target tla file name
--file=

Examples

Please run python3 cli_input_gen.py to generate working example input data.

# Provide the inputs to Apalache pure mode with a json object
modelator apalache pure < cli_input_apalache_pure.json > apalache_pure_result.json
# Provide the inputs to Apalache raw mode with a json object
modelator apalache raw --json < cli_input_apalache_raw.json > apalache_raw_result.json
# Provide the inputs to Apalache raw mode with explicit values
modelator apalache raw\
 --jar=<apalache.jar>\ # absolute paths!
 --cwd=<this_directory>\ # absolute paths!
 --cmd=check\ # apalache check
 --file=Hello.tla\
 > apalache_raw_result.json

Nuance

Pure mode does write to the filesystem, but inside a temporary directory.

Feature: run TLC model checker

Run the TLC model checker in a basic 'raw' mode or run it in a 'pure' mode. The pure mode encapsulates file system operations, removing side effects. The raw mode does not, but can be useful for debugging.

Option 1: Run TLC pure with all input data piped from json

# See cli_input_tlc_pure.json
modelator tlc pure < <JSON_OBJECT>

Option 2: Run TLC raw with all input data piped from json

# See cli_input_tlc_raw.json
modelator tlc raw --json < <JSON_OBJECT>

Option 3: Run TLC raw with all input data given in args

modelator tlc raw\
 --jar=<tlc.jar>\ # absolute paths!
 --cwd=<working_dir>\ # absolute paths!
 --file=<.tla file>\ # tla target
 --config=<.cfg file>\ # TLC config file
 # other TLC arguments ...

Argument explanation

tlc pure has no arguments but tlc raw takes modelator and TLC arguments. Only some are shown here.

# Read arguments from json piped to stdin instead of from sys.argv?
--json
# Full path to directory to run TLC from.
--cwd=
# Full path to TLC jar.
--jar=
# TLC target tla file name
--file=
# TLC target cfg file name
--config=

Examples

Please run python3 cli_input_gen.py to generate working example input data.

# Provide the inputs to TLC pure mode with a json object
modelator tlc pure < cli_input_tlc_pure.json > tlc_pure_result.json
# Provide the inputs to TLC raw mode with a json object
modelator tlc raw --json < cli_input_tlc_raw.json > tlc_raw_result.json
# Provide the inputs to TLC raw mode with explicit values
modelator tlc raw\
 --jar=<tlc.jar>\ # absolute paths!
 --cwd=<this_directory>\ # absolute paths!
 --file=Hello.tla\
 --config=Hello.cfg\
 > tlc_raw_result.json

Nuance

Pure mode does write to the filesystem, but inside a temporary directory.

How to get help

Please try

modelator tlc --help
modelator tlc pure --help
modelator tlc raw --help
modelator apalache --help
modelator apalache pure --help
modelator apalache raw --help
modelator util --help
modelator util tlc --help
modelator util tlc itf --help

ect.

This CLI documentation will grow as the APIs stabilize.