FM Playground

---

A Formal Method playground for limboole, z3, nuXmv, Alloy, and Spectra. This project is a part of the Formal Methods course at the Bauhaus-Universität Weimar. It is a web application that allows users to run formal methods tools in the browser.

Overview and Examples

We started a small overview of the features of the FM Playground and how to use it. The video playlist is available on YouTube

For more updates, examples, and tutorials, please visit the formal-methods.net website.

Development

Requirements

• Python >= 3.10.0
• Node >= 20.0.0
• PostgreSQL >= 15.0 (optional) - use sqlite3 for development
• Docker >= 20.10.0 (optional)
• Docker Compose >= 1.27.0 (optional)

Installation

• [TODO]

Docker

• [TODO]

Docker Compose

• Copy the .env.example file to .env and update the environment variables as needed:

cp .env.example .env

• Run the following command:

docker compose up -d

Contributing

TODO: Create a contributing guide

Contributions are welcome! Please refer to the contributing guidelines for detailed instructions.

License

This project is licensed under the MIT License.

Third-Party Licenses

• Limboole - https://github.com/maximaximal/limboole/blob/master/LICENSE
• Z3 - https://github.com/Z3Prover/z3/blob/master/LICENSE.txt
• nuXmv - https://nuxmv.fbk.eu/downloads/LICENSE.txt
• Alloy - https://github.com/AlloyTools/org.alloytools.alloy/blob/master/LICENSE
• Spectra - https://github.com/SpectraSynthesizer/spectra-synt/blob/master/LICENSE