fsmc

The Universal Finite State Machine Compiler, Optimization & Formal Verification Infrastructure.
Transpile, optimize, formally verify, and compile statecharts across 8 industry modeling formats and hard real-time C++ target architectures.

📖 Documentation • 🚀 Quickstart • 💻 Interactive Playground • ⚙️ CLI Reference • 📚 Runtime API

---

🏛️ Welcome to fsmc

fsmc (Finite State Machine Compiler) is a modern, modular compiler infrastructure and formal verification engine designed for deterministic, safety-critical embedded systems.

It bridges the gap between high-level Model-Based Systems Engineering (MBSE) specifications—such as OMG SysML v2, Cameo Systems Modeler (XMI), and W3C SCXML—and hard real-time C++ implementations (C++17 and C++20), guaranteeing that behavioral models are formally verified before execution and deployed with zero dynamic heap allocations.

flowchart LR
    subgraph Ingestion["1. Frontend Ingestion"]
        SysML["OMG SysML v2\nCameo XMI 2.1\nW3C SCXML"]
        Diagrams["PlantUML\nMermaid\nGraphviz DOT\nXState JSON"]
    end

    subgraph Compiler["2. Verification & Pass Pipeline"]
        IR["Canonical FsmIr AST"]
        Verify["Temporal Model Checking\nEFSM Interval Analysis\nDead Code & Determinism"]
        RTM["Traceability Matrix (RTM)"]
    end

    subgraph Targets["3. Target Code & Diagnostics"]
        CPP["C++17 / C++20 Engine\n(Zero-Alloc, O(1), ISR-Safe)"]
        Exports["Universal Transpilation\n(SysML, SCXML, SMV, PUML)"]
    end

    Ingestion --> Compiler
    Compiler --> Targets

Loading

---

🌟 Key Capabilities

Capability	Technical Details	Documentation
Universal Modeling	Ingest and transpile across 8 formats: OMG SysML v2, Cameo / MagicDraw (OMG XMI), W3C SCXML, nuXmv / SMV, PlantUML, Mermaid, Graphviz DOT, and XState JSON.	Modeling Languages
Formal Model Checking	Integrated LTL/CTL temporal model checker verifying safety invariants, livelocks, deadlock freedom, and choice completeness before code emission.	Model Checking
EFSM Interval Analysis	Abstract interpretation of numerical guard bounds (<, >, <=, >=) detecting dead transitions and runtime unreachable branches.	Interval Analysis
Safety Traceability (RTM)	Automated Requirement Traceability Matrix export in Markdown and JSON linking @fsm:req tags to transitions and states.	RTM Specification
Hard Real-Time C++ Runtime	Zero-heap, $O(1)$ dispatching, ISR-safe lock-free SPSC queue (fsm::spsc_fsm), MPSC worker (fsm::thread_safe_fsm), and deterministic hardware tick timers.	Runtime C++ API
Live Web Playground	Client-side WebAssembly compiler with live C++ generation, diagram visualization, and Monaco code editing directly in the browser.	Try Playground

---

⚡ Quickstart

1. Installation

fsmc is available via Conan, CMake FetchContent, or manual source compilation:

# Build and install locally using CMake
cmake -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build -j$(nproc)
sudo cmake --install build

For complete instructions (including Conan and vcpkg), see the Installation Guide.

2. Compile a Model

Given a formal SysML v2 state machine specification (satellite.sysml):

state def SatelliteControl {
    entry; then Booting;

    state Booting;
    state Operational;
    state SafeMode;

    transition boot_ok
        first Booting
        accept EvSysInit
        do action { log("Satellite online"); }
        then Operational;

    transition fault_detected
        first Operational
        accept EvAnomaly
        then SafeMode;
}

Run fsmc to formally verify and compile into a standalone C++20 header:

fsmc -i satellite.sysml -o satellite_fsm.hpp --standard 20 --standalone

---

📚 Documentation Site Map

The complete, official documentation is hosted at simoneCavalleri.github.io/fsmc:

• Getting Started: Installation, Quickstart Tutorial, CLI Options, CMake Integration.
• Architecture & Concepts: HFSM Hierarchy, Transitions, Guards, Actions, Memory Real-Time Guarantees.
• Formal Languages & Modeling: SysML v2, Cameo XMI, SCXML, nuXmv / SMV, PlantUML, Mermaid, UML 2.5 Mapping.
• Verification & Safety: LTL/CTL Model Checking, Interval Analysis, Requirement Traceability (RTM).
• Runtime C++ API: Synchronous Core, Lock-Free SPSC, Thread-Safe MPSC, Transition Trace Telemetry.
• Compiler Internals: Compiler Architecture, Canonical AST Specification, Test Suite Catalog.
• Interactive Playground: Live WebAssembly transpile & compilation playground.

---

📄 License & Trademarks

• License: fsmc is released under the permissive MIT License.
• Trademarks: All product names, logos, brands, and registered trademarks (such as SysML®, Cameo®, MagicDraw®, ARM®, FreeRTOS™, STM32®) mentioned in this repository and documentation are property of their respective owners. Their mention is strictly for technical interoperability, compatibility identification, and reference purposes, and does not imply any affiliation, sponsorship, or endorsement.