Modality Language Parser

This crate provides a parser for the Modality temporal logic language, specifically for parsing .modality files that contain LTS (Labeled Transition System) models.

Features

• Parse .modality files containing model definitions
• Support for multiple graphs per model
• Support for transitions with properties (signed properties with + or -)
• Handle comments and empty lines
• Robust error handling
• Two parser implementations:
  • Hand-written parser (robust and battle-tested)
  • LALRPOP-based parser (grammar-driven)
• Mermaid diagram generation for visualizing models

Language Specification

The formal syntax of the Modality language is defined by a BNF grammar. See BNF.md for the complete Backus-Naur Form specification.

Usage

Basic Usage

use modality_lang::{parse_file, parse_file_lalrpop};

// Parse from file using hand-written parser
let model = parse_file("path/to/model.modality")?;

// Parse from file using LALRPOP parser
let model = parse_file_lalrpop("path/to/model.modality")?;

// Parse from string content
let content = r#"
model MyModel:
  graph g1:
    n1 --> n2: +blue
    n2 --> n3: -red
"#;
let model = parse_content(content)?;

Multiple Models

use modality_lang::parse_all_models_lalrpop;

// Parse all models in a file using LALRPOP
let models = parse_all_models_lalrpop("path/to/models.modality")?;
for model in models {
    println!("Model: {}", model.name);
}

Mermaid Diagram Generation

use modality_lang::{parse_file_lalrpop, generate_mermaid_diagram, generate_mermaid_diagrams};

// Parse a model and generate a Mermaid diagram
let model = parse_file_lalrpop("path/to/model.modality")?;
let diagram = generate_mermaid_diagram(&model);
println!("{}", diagram);

// Generate diagrams for multiple models
let models = parse_all_models_lalrpop("path/to/models.modality")?;
let combined_diagrams = generate_mermaid_diagrams(&models);
println!("{}", combined_diagrams);

// Generate a styled diagram
let styled_diagram = generate_mermaid_diagram_with_styling(&model);
println!("{}", styled_diagram);

Example Models

The parser supports the following syntax:

// Simple model with one transition
model InitialModel:
  graph g1:
    n1 --> n1

// Model with properties
model Model3:
  graph g1:
    n1 --> n2: +blue
    n2 --> n3: +blue

// Model with multiple properties
model Model4:
  graph g1:
    n1 --> n2: +blue -red
    n2 --> n3: +blue -green
    n3 --> n1: -blue +red

// Model with multiple graphs
model Model4:
  graph g1:
    n1 --> n2: +blue -red
    n2 --> n3: +blue -green
    n3 --> n1: -blue +red
  graph g2:
    n1 --> n1: +yellow

Parser Implementations

Hand-written Parser

• File: src/parser.rs
• Functions: parse_file(), parse_content()
• Features: Robust, handles edge cases well
• Use case: Production parsing

LALRPOP Parser

• File: src/grammar.lalrpop, src/lalrpop_parser.rs
• Functions: parse_file_lalrpop(), parse_content_lalrpop(), parse_all_models_lalrpop()
• Features: Grammar-driven, supports multiple models
• Use case: Grammar-based parsing, multiple model support

Mermaid Diagram Generation

Basic Diagram Generation

• Function: generate_mermaid_diagram(model: &Model) -> String
• Features: Generates standard Mermaid state diagrams
• Output: Mermaid-compatible state diagram syntax

Multiple Model Diagrams

• Function: generate_mermaid_diagrams(models: &[Model]) -> String
• Features: Generates diagrams for multiple models with comments
• Output: Combined Mermaid syntax for all models

Styled Diagrams

• Function: generate_mermaid_diagram_with_styling(model: &Model) -> String
• Features: Includes CSS styling classes for visual enhancement
• Output: Mermaid syntax with custom styling

Diagram Features

• States: All states/nodes are represented as state boxes
• Transitions: Arrows show state transitions within each graph
• Properties: Edge labels show transition properties (e.g., : +blue -red)
• State Groups: Multiple graphs are grouped in isolated state containers
• Graph Isolation: Each graph is completely isolated - no transitions between graphs
• State Naming: Multiple graphs use prefixed state names (e.g., g1.n1, g2.n1) to prevent conflicts
• Styling: Optional CSS classes for visual customization

Example Mermaid Output

stateDiagram-v2
    state g1 {
        g1.n1 : n1
        g1.n2 : n2
        g1.n3 : n3
        g1.n1 --> g1.n2 : +blue -red
        g1.n2 --> g1.n3 : +blue -green
        g1.n3 --> g1.n1 : -blue +red
    }
    state g2 {
        g2.n1 : n1
        g2.n1 --> g2.n1 : +yellow
    }

Note: In the above example, g1 and g2 are completely isolated graphs. States in g1 (g1.n1, g1.n2, g1.n3) cannot transition to states in g2 (g2.n1), and vice versa. Each graph represents an independent LTS (Labeled Transition System). The prefixed naming (g1.n1, g2.n1) makes the graph isolation explicit and prevents naming conflicts. Properties are space-separated in transition labels.

Data Structures

Model

Represents a complete model containing multiple graphs.

pub struct Model {
    pub name: String,
    pub graphs: Vec<Graph>,
}

Graph

Represents a graph within a model containing transitions.

pub struct Graph {
    pub name: String,
    pub transitions: Vec<Transition>,
}

Transition

Represents a transition between nodes with optional properties.

pub struct Transition {
    pub from: String,
    pub to: String,
    pub properties: Vec<Property>,
}

Property

Represents a property with a sign (+ or -).

pub struct Property {
    pub sign: PropertySign,
    pub name: String,
}

pub enum PropertySign {
    Plus,
    Minus,
}

Examples

See the examples/ directory for working examples:

• parse_example.rs - Basic parsing example
• parse_all_models.rs - Parse all models in a file
• compare_parsers.rs - Compare hand-written vs LALRPOP parsers
• lalrpop_example.rs - LALRPOP parser with multiple models
• mermaid_example.rs - Mermaid diagram generation

Run examples with:

cargo run --example parse_example
cargo run --example parse_all_models
cargo run --example compare_parsers
cargo run --example lalrpop_example
cargo run --example mermaid_example

Grammar

The LALRPOP grammar (src/grammar.lalrpop) defines the syntax:

Model: Model = {
    <model:ModelDecl> => model
};

ModelDecl: Model = {
    "model" <name:Ident> ":" <graphs:Graph*> => { ... }
};

Graph: Graph = {
    "graph" <name:Ident> ":" <transitions:Transition*> => { ... }
};

Transition: Transition = {
    <from:Ident> "-->" <to:Ident> => { ... },
    <from:Ident> "-->" <to:Ident> ":" <properties:PropertyList> => { ... }
};

PropertyList: Vec<Property> = {
    <property:Property> => vec![property],
    <properties:PropertyList> <property:Property> => { ... }
};

Property: Property = {
    "+" <name:Ident> => Property::new(PropertySign::Plus, name),
    "-" <name:Ident> => Property::new(PropertySign::Minus, name)
};

Error Handling

The parser returns Result<Model, String> where errors are descriptive strings indicating what went wrong during parsing.

Common error cases:

• Invalid model declaration format
• Invalid graph declaration format
• Invalid transition format
• Missing or invalid property signs
• Empty property names

Building

The LALRPOP parser is automatically generated during the build process. The build script (build.rs) handles the grammar compilation.