Crate rumpsteak_aura_fsm 

Finite State Machine (FSM) support for session types.

This crate provides finite state machine representations for session types, enabling static analysis and verification of communication protocols. It includes support for DOT parsing, local type representations, subtyping verification, and Petrify output format.

Main Components

• Fsm - Core FSM representation with states and transitions
• Local - Local type representation (textual session types)
• Dot - DOT format export for visualization
• Petrify - Petrify format export for Petri net tools
• [subtype] - Asynchronous subtyping verification

Example

use rumpsteak_aura_fsm::{Fsm, Action, Message, Transition};

let mut fsm: Fsm<&str, &str, ()> = Fsm::new("Client");
let s0 = fsm.add_state();
let s1 = fsm.add_state();

let transition = Transition::new(
    "Server",
    Action::Output,
    Message::from_label("Hello")
);
fsm.add_transition(s0, s1, transition).unwrap();

Re-exports

pub use self::dot::Dot;

pub use self::local::Local;

pub use self::petrify::Petrify;

Modules

dot

DOT format support for FSMs.

local

Local session types represented as recursive types.

petrify

Petrify output format for FSMs.

Structs

Fsm

Finite state machine representing a local session type.

Message

Message with label, parameters, and assignments.

NamedParameter

Named parameter with optional refinement type.

Nil

Nil type representing the absence of a role in binary FSMs.

Normalizer

Normalizer for converting FSMs to canonical form.

StateIndex

Index of a state in the FSM graph.

Transition

FSM transition representing a communication action.

TransitionRef

Borrowed reference to a transition.

Enums

Action

Communication action performed by a role.

AddTransitionError

Errors that can occur when adding transitions to an FSM.

Associativity

Operator associativity for expression parsing.

BinaryOp

Binary operators for refinement expressions.

Expression

Refinement expression for message parameters.

Parameters

Message parameters, either unnamed or named with refinements.

UnaryOp

Unary operators for refinement expressions.

Traits

Operator

Trait for operators in expressions.