# fm4se/fm-playground architecture

> Architecture diagram of the GitHub repository fm4se/fm-playground, generated by GitDiagram from its file tree, README and a sample of source files (last updated 2026-09-26). It is an AI-made overview: check details against the source.

- Interactive diagram: https://gitdiagram.com/fm4se/fm-playground
- Repository: https://github.com/fm4se/fm-playground

## Overview

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: [`frontend/src/components/Playground/Playground.tsx`](https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/Playground/Playground.tsx) (Editor and output), [`frontend/src/components/Playground/OutputArea.tsx`](https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/Playground/OutputArea.tsx) (Analysis output), [`frontend/src/App.tsx`](https://github.com/fm4se/fm-playground/blob/main/frontend/src/App.tsx) (Application shell), [`backend/app.py`](https://github.com/fm4se/fm-playground/blob/main/backend/app.py) (Web backend)

## Diagram (Mermaid)

```mermaid
flowchart TD

subgraph group_interface["Playground interface"]
  node_app["Application shell<br/>[App.tsx]"]
  node_toolmaps["Tool selection<br/>[ToolMaps.tsx]"]
  node_playground["Editor and output<br/>[Playground.tsx]"]
  node_history["History drawer<br/>[HistoryDrawer.tsx]"]
  node_playgroundapi["Playground API client<br/>[playgroundApi.ts]"]
  node_output["Analysis output<br/>[OutputArea.tsx]"]
end

subgraph group_tools["Tool capabilities"]
  node_alloy["Alloy analysis<br/>[alloyExecutor.ts]"]
  node_alloydiff["Alloy comparison"]
  node_limboole["Limboole analysis"]
  node_limboolediff["Limboole comparison"]
  node_smt["SMT analysis<br/>[z3Executor.ts]"]
  node_smtdiff["SMT comparison<br/>[smtDiffExecutor.ts]"]
  node_dafny["Dafny verification<br/>[dafnyExecutor.ts]"]
  node_nuxmv["nuXmv analysis<br/>[nuxmvExecutor.ts]"]
  node_spectra["Spectra analysis<br/>[spectraExecutor.ts]"]
end

subgraph group_services["Execution services"]
  node_dafnyservice["Dafny service<br/>[main.py]"]
  node_dafnyproxy["Dafny language proxy<br/>[main.py]"]
  node_z3service["Z3 service<br/>[main.py]"]
  node_limboolediffservice["Limboole diff service<br/>[main.py]"]
  node_smtdiffservice["SMT diff service<br/>[main.py]"]
  node_alloyservice["Alloy services"]
  node_alloydiffservice["Alloy diff service"]
  node_limbooleservice["Limboole service<br/>[main.py]"]
  node_nuxmvservice["nuXmv service<br/>[main.py]"]
  node_spectraservice["Spectra service<br/>[main.py]"]
end

subgraph group_accounts["Accounts and history"]
  node_backend["Web backend<br/>[app.py]"]
  node_routes["Auth and playground<br/>[playground.py]"]
  node_auth["Authentication routes<br/>[authentication.py]"]
  node_dbqueries["History queries<br/>[db_query.py]"]
  node_database[("Application database<br/>[models.py]")]
end

subgraph group_collaboration["Collaboration"]
  node_collabmanager["Collaboration manager<br/>[CollabManager.ts]"]
  node_collabserver["Room WebSocket server<br/>[server.js]"]
end

node_user(("User"))

node_user -->|"uses"| node_app
node_app -->|"offers tools"| node_toolmaps
node_app -->|"opens"| node_playground
node_user -->|"edits specification"| node_playground
node_playground -->|"runs"| node_alloy
node_playground -->|"compares"| node_alloydiff
node_playground -->|"runs"| node_limboole
node_playground -->|"compares"| node_limboolediff
node_playground -->|"runs"| node_smt
node_playground -->|"compares"| node_smtdiff
node_playground -->|"verifies"| node_dafny
node_playground -->|"runs"| node_nuxmv
node_playground -->|"runs"| node_spectra
node_alloy -->|"shows results"| node_output
node_alloydiff -->|"shows results"| node_output
node_limboole -->|"shows results"| node_output
node_limboolediff -->|"shows results"| node_output
node_smt -->|"shows results"| node_output
node_smtdiff -->|"shows results"| node_output
node_dafny -->|"shows results"| node_output
node_nuxmv -->|"shows results"| node_output
node_spectra -->|"shows results"| node_output
node_playground -->|"requests"| node_playgroundapi
node_playgroundapi -->|"calls"| node_backend
node_backend -->|"dispatches"| node_routes
node_backend -->|"dispatches"| node_auth
node_routes -->|"queries history"| node_dbqueries
node_auth -->|"uses"| node_database
node_dbqueries -->|"reads and writes"| node_database
node_playground -->|"opens history"| node_history
node_history -->|"requests history"| node_playgroundapi
node_collabmanager -->|"syncs room"| node_collabserver
node_playground -->|"binds editor"| node_collabmanager

click node_app "https://github.com/fm4se/fm-playground/blob/main/frontend/src/App.tsx"
click node_toolmaps "https://github.com/fm4se/fm-playground/blob/main/frontend/src/ToolMaps.tsx"
click node_playground "https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/Playground/Playground.tsx"
click node_history "https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/HistoryDrawer/HistoryDrawer.tsx"
click node_playgroundapi "https://github.com/fm4se/fm-playground/blob/main/frontend/src/api/playgroundApi.ts"
click node_alloy "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/alloy/alloyExecutor.ts"
click node_alloydiff "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/alloy-diff/alloyDiffExecutor.ts"
click node_limboole "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/limboole/limbooleExecutor.ts"
click node_limboolediff "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/limboole-diff/limbooleDiffExecutor.ts"
click node_smt "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/smt/z3Executor.ts"
click node_smtdiff "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/smt-diff/smtDiffExecutor.ts"
click node_dafny "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/dafny/dafnyExecutor.ts"
click node_nuxmv "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/nuxmv/nuxmvExecutor.ts"
click node_spectra "https://github.com/fm4se/fm-playground/blob/main/frontend/tools/spectra/spectraExecutor.ts"
click node_output "https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/Playground/OutputArea.tsx"
click node_backend "https://github.com/fm4se/fm-playground/blob/main/backend/app.py"
click node_routes "https://github.com/fm4se/fm-playground/blob/main/backend/routes/playground.py"
click node_auth "https://github.com/fm4se/fm-playground/blob/main/backend/routes/authentication.py"
click node_dbqueries "https://github.com/fm4se/fm-playground/blob/main/backend/db/db_query.py"
click node_database "https://github.com/fm4se/fm-playground/blob/main/backend/db/models.py"
click node_collabmanager "https://github.com/fm4se/fm-playground/blob/main/frontend/src/collab/CollabManager.ts"
click node_collabserver "https://github.com/fm4se/fm-playground/blob/main/collab-server/server.js"
click node_dafnyservice "https://github.com/fm4se/fm-playground/blob/main/dafny-api/main.py"
click node_dafnyproxy "https://github.com/fm4se/fm-playground/blob/main/dafny-lsp-proxy/main.py"
click node_z3service "https://github.com/fm4se/fm-playground/blob/main/z3-api/main.py"
click node_limboolediffservice "https://github.com/fm4se/fm-playground/blob/main/limboole-diff-api/main.py"
click node_smtdiffservice "https://github.com/fm4se/fm-playground/blob/main/smt-diff-api/main.py"
click node_alloyservice "https://github.com/fm4se/fm-playground/blob/main/alloy-api/src/main/java/de/buw/fmp/alloy/api/AlloyInstanceController.java"
click node_alloydiffservice "https://github.com/fm4se/fm-playground/blob/main/alloy-diff-api/src/main/java/de/buw/fmp/alloy/api/DiffController.java"
click node_limbooleservice "https://github.com/fm4se/fm-playground/blob/main/limboole-api/main.py"
click node_nuxmvservice "https://github.com/fm4se/fm-playground/blob/main/nuxmv-api/main.py"
click node_spectraservice "https://github.com/fm4se/fm-playground/blob/main/spectra-api/main.py"

classDef toneNeutral fill:#f8fafc,stroke:#334155,stroke-width:1.5px,color:#0f172a
classDef toneBlue fill:#dbeafe,stroke:#2563eb,stroke-width:1.5px,color:#172554
classDef toneAmber fill:#fef3c7,stroke:#d97706,stroke-width:1.5px,color:#78350f
classDef toneMint fill:#dcfce7,stroke:#16a34a,stroke-width:1.5px,color:#14532d
classDef toneRose fill:#ffe4e6,stroke:#e11d48,stroke-width:1.5px,color:#881337
classDef toneIndigo fill:#e0e7ff,stroke:#4f46e5,stroke-width:1.5px,color:#312e81
classDef toneTeal fill:#ccfbf1,stroke:#0f766e,stroke-width:1.5px,color:#134e4a
class node_app,node_toolmaps,node_playground,node_history,node_playgroundapi,node_output,node_user toneBlue
class node_alloy,node_alloydiff,node_limboole,node_limboolediff,node_smt,node_smtdiff,node_dafny,node_nuxmv,node_spectra toneAmber
class node_dafnyservice,node_dafnyproxy,node_z3service,node_limboolediffservice,node_smtdiffservice,node_alloyservice,node_alloydiffservice,node_limbooleservice,node_nuxmvservice,node_spectraservice toneMint
class node_backend,node_routes,node_auth,node_dbqueries,node_database toneRose
class node_collabmanager,node_collabserver toneIndigo
```

## Components

### Playground interface

- [Application shell](https://github.com/fm4se/fm-playground/blob/main/frontend/src/App.tsx): `frontend/src/App.tsx`
- [Tool selection](https://github.com/fm4se/fm-playground/blob/main/frontend/src/ToolMaps.tsx): `frontend/src/ToolMaps.tsx`
- [Editor and output](https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/Playground/Playground.tsx): `frontend/src/components/Playground/Playground.tsx`
- [History drawer](https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/HistoryDrawer/HistoryDrawer.tsx): `frontend/src/components/HistoryDrawer/HistoryDrawer.tsx`
- [Playground API client](https://github.com/fm4se/fm-playground/blob/main/frontend/src/api/playgroundApi.ts): `frontend/src/api/playgroundApi.ts`
- [Analysis output](https://github.com/fm4se/fm-playground/blob/main/frontend/src/components/Playground/OutputArea.tsx): `frontend/src/components/Playground/OutputArea.tsx`

### Tool capabilities

- [Alloy analysis](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/alloy/alloyExecutor.ts): `frontend/tools/alloy/alloyExecutor.ts`
- [Alloy comparison](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/alloy-diff/alloyDiffExecutor.ts): `frontend/tools/alloy-diff/alloyDiffExecutor.ts`
- [Limboole analysis](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/limboole/limbooleExecutor.ts): `frontend/tools/limboole/limbooleExecutor.ts`
- [Limboole comparison](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/limboole-diff/limbooleDiffExecutor.ts): `frontend/tools/limboole-diff/limbooleDiffExecutor.ts`
- [SMT analysis](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/smt/z3Executor.ts): `frontend/tools/smt/z3Executor.ts`
- [SMT comparison](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/smt-diff/smtDiffExecutor.ts): `frontend/tools/smt-diff/smtDiffExecutor.ts`
- [Dafny verification](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/dafny/dafnyExecutor.ts): `frontend/tools/dafny/dafnyExecutor.ts`
- [nuXmv analysis](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/nuxmv/nuxmvExecutor.ts): `frontend/tools/nuxmv/nuxmvExecutor.ts`
- [Spectra analysis](https://github.com/fm4se/fm-playground/blob/main/frontend/tools/spectra/spectraExecutor.ts): `frontend/tools/spectra/spectraExecutor.ts`

### Execution services

- [Dafny service](https://github.com/fm4se/fm-playground/blob/main/dafny-api/main.py): `dafny-api/main.py`
- [Dafny language proxy](https://github.com/fm4se/fm-playground/blob/main/dafny-lsp-proxy/main.py): `dafny-lsp-proxy/main.py`
- [Z3 service](https://github.com/fm4se/fm-playground/blob/main/z3-api/main.py): `z3-api/main.py`
- [Limboole diff service](https://github.com/fm4se/fm-playground/blob/main/limboole-diff-api/main.py): `limboole-diff-api/main.py`
- [SMT diff service](https://github.com/fm4se/fm-playground/blob/main/smt-diff-api/main.py): `smt-diff-api/main.py`
- [Alloy services](https://github.com/fm4se/fm-playground/blob/main/alloy-api/src/main/java/de/buw/fmp/alloy/api/AlloyInstanceController.java): `alloy-api/src/main/java/de/buw/fmp/alloy/api/AlloyInstanceController.java`
- [Alloy diff service](https://github.com/fm4se/fm-playground/blob/main/alloy-diff-api/src/main/java/de/buw/fmp/alloy/api/DiffController.java): `alloy-diff-api/src/main/java/de/buw/fmp/alloy/api/DiffController.java`
- [Limboole service](https://github.com/fm4se/fm-playground/blob/main/limboole-api/main.py): `limboole-api/main.py`
- [nuXmv service](https://github.com/fm4se/fm-playground/blob/main/nuxmv-api/main.py): `nuxmv-api/main.py`
- [Spectra service](https://github.com/fm4se/fm-playground/blob/main/spectra-api/main.py): `spectra-api/main.py`

### Accounts and history

- [Web backend](https://github.com/fm4se/fm-playground/blob/main/backend/app.py): `backend/app.py`
- [Auth and playground](https://github.com/fm4se/fm-playground/blob/main/backend/routes/playground.py): `backend/routes/playground.py`
- [Authentication routes](https://github.com/fm4se/fm-playground/blob/main/backend/routes/authentication.py): `backend/routes/authentication.py`
- [History queries](https://github.com/fm4se/fm-playground/blob/main/backend/db/db_query.py): `backend/db/db_query.py`
- [Application database](https://github.com/fm4se/fm-playground/blob/main/backend/db/models.py): `backend/db/models.py`

### Collaboration

- [Collaboration manager](https://github.com/fm4se/fm-playground/blob/main/frontend/src/collab/CollabManager.ts): `frontend/src/collab/CollabManager.ts`
- [Room WebSocket server](https://github.com/fm4se/fm-playground/blob/main/collab-server/server.js): `collab-server/server.js`

### Other components

- **User**

## Connections

- 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