modelator-py

⚠️ The tools in this repo are unstable and may be subject to major changes ⚠️

Lightweight utilities to assist model writing and model-based testing activities using the TLA+ ecosystem.

What is this project?

A collection of cli utilities and library functions to reduce leg-work when developing TLA+ models, running model checkers, and doing model-based testing. The utilities are also intended to act as building blocks for tool development in the TLA+ ecosystem.

What can it do right now?

Currently there is a cli and library functions implementing utilities:

• Run TLC model checker without side effects (runs in temporary directory and is cleaned up)
• Run TLC model checker programmatically (reads and returns json data)
• Run Apalache model checker without side effects (runs in temporary directory and is cleaned up)
• Run Apalache model checker programmatically (reads and returns json data)
• Extract traces from TLC output in Informal Trace Format format (concise and machine readable counterexample representation)

Allowing clean programmatic access to model checkers and other utility.

What will it do in the future?

The model-based testing capabilities developed at Informal are currently in the modelator tool and are being migrated to a multi language architecture. Please expect more utilities and more tooling soon.

Usage

Please see usage.

Running the code in this repository

Please see contributing.

Contributing

Please see contributing.

License

Copyright © 2021 Informal Systems Inc. and modelator authors.

Licensed under the Apache License, Version 2.0 (the "License"); you may not use the files in this repository except in compliance with the License. You may obtain a copy of the License at

https://www.apache.org/licenses/LICENSE-2.0