Skip to content

Latest commit

 

History

History
149 lines (108 loc) · 4.37 KB

README.md

File metadata and controls

149 lines (108 loc) · 4.37 KB
Raw

TLC cmd tools

Welcome! Here you'll find scripts that automate TLC config file generation, batch model processing, simulation trace conversion to JSON, and Graphviz dot file conversion into traces.

Features:

  • Comprehensive support for nearly all options in the TLA+ toolbox model checking panel
  • Efficient batch processing of models
  • Convenient saving of batch result tables
  • Initialization of states from trace files
  • Script for reading trace files into Python objects or JSON dumps
  • Conversion of Graphviz dot state graph files into unique traces
  • Seamless execution in distributed mode for easy scalability

Dependencies

python3+, Java 11+

Optional modules:

pip3 install requests  # to download tla2tools.jar
pip3 install psutil    # for "memory ratio" option (see example.ini)
pip3 install networkx  # for conversion of Graphviz dot state graph file
git submodule update --init --recursive  # for distributed mode

How to run

tlcwrapper.py

usage: tlcwrapper.py [-h] [-j CLASSPATH] [-g] [-r] [-s] [-d] [-c] [-m] [-n] [config.ini]

Run TLC in CMD

positional arguments:
  config.ini    Configuration file (if not presented, stdin is used)

options:
  -h, --help    show this help message and exit
  -j CLASSPATH  Java classpath to use
  -g            Generate TLC config files and print Java CMD strings
  -r            Run without processing TLC output
  -s            Do not save summary file
  -d            Download tla2tools.jar and CommunityModules-deps.jar and exit
  -c            Separate constants and model options into two files
  -m            Require community modules
  -n            Not to print debug messages

An example: DieHard/run.sh

trace_reader.py

usage: trace_reader.py [-h] [-o JSON_FILE] [-i INDENT] [-p HANDLER] [-a] [-d] [-s] [-g] trace_file

Read TLA traces into Python objects

positional arguments:
  trace_file    TLA trace file

options:
  -h, --help    show this help message and exit
  -o JSON_FILE  output to json file
  -i INDENT     json file indent
  -p HANDLER    python user_dict and list/kv handers
  -a            save action name in '_action' key if available
  -d            make data structures hashable
  -s            sort dict by keys, true if -d is defined
  -g            get dot file graph

The trace file can be either the MC.out file or generated through the "simulation dump traces" option.

Python -p handler example:

# 'user_dict' replaces dict and list values (example: replace string 'None' to Python None obj)
user_dict = {'None': None}

# 'outside_kv_handler' replaces the outside dicts (i.e. keys are TLA+ variable names) keys and values
# 'inside_kv_handler' replaces the inside dicts/TLA+ records (nested in variables) keys and values
# Example: if key (TLA+ variable name) is "state", then return (k, v) without changing.
def outside_kv_handler(k, v):
    if k != "state":
        return k, v
    else:
        return k, "value is changed"

# 'list_handler' gets TLA+ set/sequence as list `l` with type annotation `k` (set/seq),
# and returns data after processing 
def list_handler(l, k):
    if k == "set":
        return l
    else:
        return [ "changed" ]

trace_counter.py

usage: trace_counter.py [-h] [-p NPROC] [-n NTRACE] [-l LOGFILE] [-f HASHFILE] [-r] trace_dir

Simulation unique traces and distinct states counter

positional arguments:
  trace_dir    Trace dir

options:
  -h, --help   show this help message and exit
  -p NPROC     Number of processes
  -n NTRACE    Print progress every n traces
  -l LOGFILE   Log output to file
  -f HASHFILE  Hash file
  -r           Reduce only

trace_generator.py

usage: trace_generator.py [-h] [-p NPROC] [-s SAVE_DIR] dot_file

Generate all simple paths of a dot file

positional arguments:
  dot_file     Dot file

options:
  -h, --help   show this help message and exit
  -p NPROC     Number of processes
  -s SAVE_DIR  Save all generated traces

How to write config.ini

See example.ini

An example: TPaxos/TPaxos-simulate.ini

An example of replacing Init: DieHard/DieHard-simulate-replace-init.ini

Misc

If you find bugs, welcome to submit issues and pull requests!

If you can speak Chinese, this video tutorial may help you get started.