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.
- Python >= 3.9.0
- Node >= 18.0.0
- PostgreSQL >= 15.0
- Docker >= 20.10.0 (optional)
- Docker Compose >= 1.27.0 (optional)
- Copy the
.env.examplefile to.envand update the environment variables as needed:
cp .env.example .env- Run the following command:
docker-compose up -dversion: '3'
services:
frontend:
build:
context: ./frontend
args:
VITE_FMP_API_URL: http://localhost:8000/api
container_name: fmp-frontend
env_file:
- .env
ports:
- "5173:5173"
networks:
- my_network
restart: unless-stopped
backend:
build:
context: ./backend
container_name: fmp-backend
env_file:
- .env
ports:
- "8000:8000"
depends_on:
postgres:
condition: service_healthy
networks:
- my_network
restart: unless-stopped
postgres:
image: postgres:15.4
container_name: fmp-db
environment:
POSTGRES_USER: ${DB_USERNAME}
POSTGRES_PASSWORD: ${DB_PASSWORD}
POSTGRES_DB: ${DB_NAME}
volumes:
- postgres_data:/var/lib/postgresql/data
healthcheck:
test: ["CMD-SHELL", "pg_isready -U postgres"]
interval: 5s
timeout: 5s
retries: 5
env_file:
- .env
networks:
- my_network
restart: unless-stopped
alloy-api:
build:
context: ./alloy-api
container_name: fmp-alloy-api
ports:
- "8080:8080"
networks:
- my_network
restart: unless-stopped
volumes:
postgres_data:
networks:
my_network:
driver: bridgeContributions are welcome! Please refer to the contributing guidelines for detailed instructions.
This project is licensed under the MIT License.
- 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
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent