fsmc

The Universal Finite State Machine Compiler, Optimization & Formal Verification Infrastructure.
Ingest, verify, optimize, transpile, and compile statecharts across 8 industry modeling formats with extensible target backends.

Documentation • Quickstart • Interactive Playground • CLI Reference • Runtime API • Changelog

---

Welcome to fsmc

fsmc (Finite State Machine Compiler) is a modular, format-agnostic compiler infrastructure and verification toolchain for Finite State Machines and Hierarchical Statecharts.

Built with a decoupled, three-stage compiler architecture (Frontends $\to$ Canonical IR & Middle-End $\to$ Pluggable Backends), fsmc bridges high-level Model-Based Systems Engineering (MBSE) specifications (OMG SysML v2, Cameo XMI, W3C SCXML, PlantUML, Mermaid, Graphviz DOT) with formal model checkers and deterministic target runtimes:

flowchart TD
    subgraph Ingestion["1. Frontend Ingestion"]
        SysML["<b>MBSE & Formal Specs</b><br/>OMG SysML v2 • Cameo XMI 2.1<br/>W3C SCXML"]
        Diagrams["<b>Visual & Web Diagrams</b><br/>PlantUML • Mermaid<br/>Graphviz DOT • XState JSON"]
    end

    subgraph Compiler["2. Canonical IR & Middle-End Passes"]
        IR["<b>Canonical Metamodel (FsmIr)</b><br/>Partitioned Memory Model:<br/>InPorts • OutPorts • Registers • Services"]
        Passes["<b>Analysis & Optimization Passes</b><br/>Temporal Model Checking • EFSM Intervals<br/>Dead Code Elimination • RTM Traceability"]
    end

    subgraph Targets["3. Extensible Target Backends"]
        CPP["<b>Deterministic C++ Engine</b><br/>C++17 / C++20 • Zero Allocations<br/>Lock-Free SPSC • Thread-Safe MPSC"]
        SMV["<b>Formal Model Checking Export</b><br/>Pure SMV Symbolic Logic<br/>for nuXmv Solver Suite"]
        Transpile["<b>Universal Transpiler</b><br/>Lossless Roundtrip Conversion<br/>Across All Supported Formats"]
    end

    Ingestion --> Compiler
    Compiler --> Targets

Loading

---

Key Capabilities

Capability	Technical Details	Documentation
Universal Ingestion	Ingest and parse statecharts from 8 formats: OMG SysML v2, Cameo / MagicDraw (OMG XMI), W3C SCXML, nuXmv / SMV, PlantUML, Mermaid, Graphviz DOT, and XState JSON.	Modeling Languages
Pluggable Backends	Decoupled architecture supporting code generation for modern C++ (C++17/20), formal SMV logic for external provers, visual diagram transpilation, and future target languages.	Architecture
Partitioned Domains	Clean separation of InPorts (read-only), OutPorts (write-only), Registers ($z^{-1}$ internal state), and Services (injected dependencies/side-effects).	Architecture
Dual-Paradigm Execution	Synchronous continuous sampled loop (step(in, out)) and asynchronous event-driven dispatch (dispatch(ev, in, out)).	Runtime C++ API
Formal Model Checking	Integrated LTL/CTL temporal model checker verifying safety invariants, livelocks, deadlock freedom, and choice completeness before emission.	Model Checking
EFSM Interval Analysis	Abstract interpretation of numerical guard bounds (<, >, <=, >=) detecting dead transitions and contract violations.	Interval Analysis
Requirement Traceability (RTM)	Automated Requirement Traceability Matrix export in Markdown, CSV, and JSON linking @fsm:req annotations to model elements.	RTM Specification
Zero-Overhead C++ Backend	Reference implementation with zero heap allocation, zero virtual tables, $O(1)$ dispatching, and thread-safe lock-free SPSC / MPSC wrappers.	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 can be installed directly via CMake, integrated with CMake FetchContent, or packaged locally with Conan 2.0:

# 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 CMake FetchContent), see the Installation Guide.

2. Compile a Model

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

state def SatelliteControl {
    in port sensor_temp : Real { assert constraint { self >= -50.0 and self <= 150.0; } }
    out port heater_power : Real { assert constraint { self >= 0.0 and self <= 100.0; } }
    attribute cycle_count : Integer = 0;

    entry; then Booting;

    state Booting;
    state Operational;
    state SafeMode;

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

    transition overheat_fault
        first Operational
        if in.sensor_temp > 90.0
        then SafeMode;
}

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

fsmc -i satellite.sysml -o satellite_fsm.hpp --std 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, Partitioned Memory Domains, 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 Dual-Paradigm 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.