Computability is an open-source desktop laboratory for defining, inspecting, and executing formal models of computation. It combines a Rust simulation core with a TypeScript and React interface delivered as a Tauri application.
The project is intended for coursework, self-study, and experimentation with formal languages and computability. Every model is validated before execution; the interface does not silently change a definition.
- A catalogue of supported computational models with a theory page for each model.
- Visual workspaces for state-based machines and Petri nets.
- Guided rule editors for grammars, L-systems, and regular expressions.
- Multiple open workspaces with local save, reopen, and portable JSON export/import.
- Execution traces, validation errors, and bounded simulation controls.
- A dedicated Algorithms laboratory with formal guidance, ordered derivation steps, result export, and direct links back into editable workspaces.
- Transformations including Thompson construction, NFA to DFA, DFA minimisation, FA to regular expression, epsilon and unreachable-state elimination, regular grammar to NFA, CFG to PDA, and Chomsky normal form.
- Analysis tools for DFA equivalence, CYK, FIRST/FOLLOW and LL(1), plus guided pumping-lemma decomposition for regular and context-free languages.
- English, Italian, French, German, Spanish, and Portuguese localization.
- Four built-in themes and an updater backed by signed Tauri release metadata.
| Area | Models |
|---|---|
| Finite automata | DFA; epsilon-NFA |
| Transducers | Mealy; Moore |
| Pushdown automata | Nondeterministic PDA |
| Turing machines | Nondeterministic single-tape TM; deterministic multi-tape TM |
| Grammars | Regular; context-free; unrestricted |
| Regular languages | Regular-expression recognition and Thompson conversion to epsilon-NFA |
| Formal systems | Deterministic, contextual, and stochastic L-systems |
| Concurrent systems | Place/transition Petri nets |
The feature matrix is the authoritative capability ledger. It distinguishes implemented operations from planned teaching tools. Recognition algorithms with potentially unbounded search use explicit bounds; the bound is part of the execution definition and is reported in the result.
The catalogue is the primary entry point for creating a project. It presents the available model families and links each model to its formal theory.
The workspace supports visual construction of state-based machines, labelled transitions, semantic state roles, and execution inspection. Transition properties are edited through separate guided fields: the UI inserts arrows, separators, and machine-specific operators automatically. Select an edge to adjust its bend, including self-loops; the bend is saved with the workspace.
Structured models use editors that match their notation. Grammar symbols are
entered as individual removable fields and productions update the model as
they are edited. Multi-tape values remain arrays, Turing movements use a fixed
choice list, and Petri arc weights accept only positive integers. JSON exports
also preserve semantic transition fields, while legacy definitions without a
kind field are detected from their structure when possible.
React and TypeScript UI
|
v
Tauri desktop shell and typed commands
|
v
computability-core (Rust)
- finite automata and transducers
- pushdown and Turing machines
- grammars, regular expressions, and L-systems
- Petri nets
The Rust crate owns model validation, simulation, conversions, and serializable domain types. The frontend owns presentation, editing, localization, and workspace state. Tauri is the narrow boundary between them, so the algorithms remain testable without rendering a desktop window. See docs/architecture.md for invariants and command boundaries.
End users only need a published package. Rust, Node.js, and build tools are not required.
- Open the latest GitHub release.
- Choose the package for your operating system:
- Windows: x64
.exeinstaller or.msipackage. - macOS:
.dmgfor Intel or Apple Silicon. - Debian and Ubuntu: x64
.debpackage. - Other Linux distributions: x64
.AppImage; it runs without a package manager and is the recommended portable option. - Arch Linux: download
PKGBUILD, then runmakepkg -siin its directory.
- Windows: x64
- Launch Computability from the application menu or installed shortcut.
The Windows installer is per-user. WebView2 is installed or reused by the
Tauri runtime, so a first install may require an internet connection. Linux
AppImage users may need their distribution's FUSE 2 compatibility package.
Release assets include detached updater signatures and latest.json; the
updater verifies these signatures before installing an update. macOS packages
may show the standard Gatekeeper confirmation when no Apple Developer signing
certificate is configured.
- Node.js 24 or newer
- Stable Rust toolchain
- The Tauri v2 system prerequisites
npm.cmd ci
npm.cmd run devnpm.cmd run build:appnpm.cmd test
npm.cmd run lint
npm.cmd run format:check
npm.cmd run build
npm.cmd run release:checkThe Quality GitHub Actions workflow runs the same gates on pull requests and
on pushes to master. Successful master builds receive an immutable tag in
the form v<version>-master.<run-number>; the desktop release workflow then
publishes Windows, macOS, Linux, Arch recipe, signatures, and the updater
manifest.
src/: React UI, editors, catalog, theory content, and localization.crates/computability-core/: Rust models and simulation algorithms.src-tauri/: Tauri commands, permissions, packaging, and application assets.docs/: architecture notes, feature matrix, and README screenshots.
Read CONTRIBUTING.md before opening a pull request. Changes should keep the Rust model boundary explicit, add tests for new behavior, and update the feature matrix or theory content when capabilities change.
Computability is distributed under the MIT License.