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
3 maintainers
Metadata
3 maintainers
Release files for modelator-py 0.2.6
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | Provenance | Actions |
|---|---|---|---|---|
| modelator_py-0.2.6.tar.gz | 94.9 kB | Without provenance | Details for modelator_py-0.2.6.tar.gz |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Actions Reset |
|---|---|---|---|---|
| modelator_py-0.2.6-py3-none-any.whl | Python 3 | none | any | Details for modelator_py-0.2.6-py3-none-any.whl |
Total release size: 206.1 kB
Release files / modelator_py-0.2.6.tar.gz
| Download URL | modelator_py-0.2.6.tar.gz |
|---|---|
| Size | 94.9 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
db1d45d7e92d3dfed4c04c836ce019b78f88ceb331db2a787c781c367d55443e
|
|
BLAKE2b-256 checksum How to use checksums |
bc10167bd6a8474118c7d3a2a0afa4d01645d4257f20d8427175d989b442b154
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
poetry/1.2.2 CPython/3.10.8 Linux/5.15.78-1-lts
|
Release files / modelator_py-0.2.6-py3-none-any.whl
| Download URL | modelator_py-0.2.6-py3-none-any.whl |
|---|---|
| Size | 111.1 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
d43f9a9c396f3836d5f1896228ed051f6c2ad6cb476a5528c8f13e92abb2add1
|
|
BLAKE2b-256 checksum How to use checksums |
db41ec0deb4fc4f5a87ea5e3000013f11ffa0b36721e212f1aac5d979e2730f3
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
poetry/1.2.2 CPython/3.10.8 Linux/5.15.78-1-lts
|
Security for modelator-py 0.2.6
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
No provenance found
None of the files in this release were uploaded with provenance metadata.
A note on package security
PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.
To learn more about protecting yourself from malicious actors, visit our package security documentation.
