fsmc

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

Documentation • Quickstart • 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, MathWorks Stateflow, PlantUML, Mermaid, Graphviz DOT, JSON) with formal model checkers, middle-end pass optimizers (fsm-opt), 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 • MathWorks Stateflow"]
        Diagrams["<b>Visual & Interchange</b><br/>PlantUML • Mermaid<br/>Graphviz DOT • Canonical JSON"]
    end

    subgraph Compiler["2. Canonical IR & Middle-End Passes (fsm-opt)"]
        IR["<b>Canonical Metamodel (FsmIr)</b><br/>Partitioned Memory Model:<br/>InPorts • OutPorts • Registers • Services<br/>Unified Native JSON AST Engine"]
        Passes["<b>28 Analysis & Optimization Passes</b><br/>7-Stage Pipeline • Structural Lowering<br/>Temporal Model Checking • EFSM Intervals<br/>Unix Pipeline (--pipe-through) • C++ Plugins"]
    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<br/>Deterministic Timer • Flight Recorder"]
        SMV["<b>Formal Model Checking Export</b><br/>Pure SMV Symbolic Logic<br/>for nuXmv Solver Suite"]
        Safety["<b>Safety & Certification Tools</b><br/>MC/DC Test Harness Synthesis<br/>Requirement Traceability (RTM)"]
        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 9 formats: OMG SysML v2, Cameo / MagicDraw (OMG XMI), W3C SCXML, MathWorks Stateflow XML, nuXmv / SMV, PlantUML, Mermaid, Graphviz DOT, and Canonical 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
Canonical IR & Optimizer (fsm-opt)	Strongly typed FsmIr with 28 optimization, lowering, and analysis passes across a verified 7-stage pipeline, standalone optimizer driver (fsm-opt), Unix filter pipeline (--pipe-through), and dynamic C++ pass plugins.	Middle-End Passes
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
MC/DC Test Harness Synthesis	Automated synthesis of GoogleTest C++ test harnesses verifying Modified Condition / Decision Coverage (MC/DC) for safety standards (DO-178C / ISO 26262).	MC/DC Synthesis
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, deterministic real-time timer (tick(dt)), state residence permanence invariants, and thread-safe lock-free SPSC / MPSC wrappers.	Runtime C++ API

---

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

Or optimize and analyze the model using fsm-opt:

fsm-opt -i satellite.sysml --passes=dead-state-pruning,guard-simplification --emit-ir

---

Documentation Site Map

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

• Getting Started: Installation, Quickstart Tutorial, CLI Options (fsmc & fsm-opt), CMake Integration.
• Architecture & Concepts: HFSM Hierarchy, Transitions, Partitioned Memory Domains, Real-Time Guarantees.
• Formal Languages & Modeling: SysML v2, Cameo XMI, SCXML, MathWorks Stateflow, nuXmv / SMV, PlantUML, Mermaid, UML 2.5 Mapping.
• Verification & Safety: LTL/CTL Model Checking, Interval Analysis, MC/DC Test Harness Synthesis, Requirement Traceability (RTM).
• Runtime C++ API: Synchronous Dual-Paradigm Core, Lock-Free SPSC, Thread-Safe MPSC, Deterministic Real-Time Timer, Flight Recorder.
• Compiler Internals: Compiler Architecture, Middle-End Passes Catalog, Canonical AST Specification, Test Suite Catalog.

---

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®, MATLAB®, Simulink®, Stateflow®, 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.