How fm4se/fm-playground works
FM Playground is a web platform for running formal-methods tools, viewing analyses, and collaborating on specifications. The main workflow is selecting a tool, editing or submitting a specification, running the corresponding executor, and viewing its output; some tools also provide comparison, witness/model iteration, and redundancy analysis. The repository also includes account and history services and real-time collaborative editing. The README documents the tool integrations; where source excerpts do not show their wiring, the graph avoids asserting specific frontend-to-service calls.
Main entry points: Playground.tsx Editor and output · OutputArea.tsx Analysis output · App.tsx Application shell · app.py Web backend
Components 33
Playground interface
- Application shell
frontend/src/App.tsx - Tool selection
frontend/src/ToolMaps.tsx - Editor and output
frontend/src/components/Playground/Playground.tsx - History drawer
frontend/src/components/HistoryDrawer/HistoryDrawer.tsx - Playground API client
frontend/src/api/playgroundApi.ts - Analysis output
frontend/src/components/Playground/OutputArea.tsx
Tool capabilities
- Alloy analysis
frontend/tools/alloy/alloyExecutor.ts - Alloy comparison
frontend/tools/alloy-diff/alloyDiffExecutor.ts - Limboole analysis
frontend/tools/limboole/limbooleExecutor.ts - Limboole comparison
frontend/tools/limboole-diff/limbooleDiffExecutor.ts - SMT analysis
frontend/tools/smt/z3Executor.ts - SMT comparison
frontend/tools/smt-diff/smtDiffExecutor.ts - Dafny verification
frontend/tools/dafny/dafnyExecutor.ts - nuXmv analysis
frontend/tools/nuxmv/nuxmvExecutor.ts - Spectra analysis
frontend/tools/spectra/spectraExecutor.ts
Execution services
- Dafny service
dafny-api/main.py - Dafny language proxy
dafny-lsp-proxy/main.py - Z3 service
z3-api/main.py - Limboole diff service
limboole-diff-api/main.py - SMT diff service
smt-diff-api/main.py - Alloy services
alloy-api/src/main/java/de/buw/fmp/alloy/api/AlloyInstanceController.java - Alloy diff service
alloy-diff-api/src/main/java/de/buw/fmp/alloy/api/DiffController.java - Limboole service
limboole-api/main.py - nuXmv service
nuxmv-api/main.py - Spectra service
spectra-api/main.py
Accounts and history
- Web backend
backend/app.py - Auth and playground
backend/routes/playground.py - Authentication routes
backend/routes/authentication.py - History queries
backend/db/db_query.py - Application database
backend/db/models.py
Collaboration
- Collaboration manager
frontend/src/collab/CollabManager.ts - Room WebSocket server
collab-server/server.js
Other components
- User
Connections 33
- User → Application shell: uses
- Application shell → Tool selection: offers tools
- Application shell → Editor and output: opens
- User → Editor and output: edits specification
- Editor and output → Alloy analysis: runs
- Editor and output → Alloy comparison: compares
- Editor and output → Limboole analysis: runs
- Editor and output → Limboole comparison: compares
- Editor and output → SMT analysis: runs
- Editor and output → SMT comparison: compares
- Editor and output → Dafny verification: verifies
- Editor and output → nuXmv analysis: runs
- Editor and output → Spectra analysis: runs
- Alloy analysis → Analysis output: shows results
- Alloy comparison → Analysis output: shows results
- Limboole analysis → Analysis output: shows results
- Limboole comparison → Analysis output: shows results
- SMT analysis → Analysis output: shows results
- SMT comparison → Analysis output: shows results
- Dafny verification → Analysis output: shows results
- nuXmv analysis → Analysis output: shows results
- Spectra analysis → Analysis output: shows results
- Editor and output → Playground API client: requests
- Playground API client → Web backend: calls
- Web backend → Auth and playground: dispatches
- Web backend → Authentication routes: dispatches
- Auth and playground → History queries: queries history
- Authentication routes → Application database: uses
- History queries → Application database: reads and writes
- Editor and output → History drawer: opens history
- History drawer → Playground API client: requests history
- Collaboration manager → Room WebSocket server: syncs room
- Editor and output → Collaboration manager: binds editor