modelator-py 0.1.1

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

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 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 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) (needs patch)
• Run Apalache model checker programmatically (reads and returns json data) (needs patch)
• Extract traces from TLC output in Informal Trace Format format (concise and machine readable counterexample representation)

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

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR