Crate libpetri_verification 

libpetri-verification — Formal Verification

Verifies safety and liveness properties of Petri nets defined with libpetri-core.

Example: Mutual Exclusion

A classic mutual exclusion net where two processes compete for a shared mutex token. Verification proves that critical_a and critical_b can never both hold tokens simultaneously.

MutualExclusion

View DOT Source

digraph MutualExclusion {
    rankdir=TB;
    nodesep=0.5;
    ranksep=0.75;
    forcelabels="true";
    overlap="false";
    fontname="Helvetica,Arial,sans-serif";
    outputorder="edgesfirst";
    compound="true";
    node [fontname="Helvetica,Arial,sans-serif", fontsize=12];
    edge [fontname="Helvetica,Arial,sans-serif", fontsize=10];
    p_idle_a [label="", shape="circle", style="filled", fillcolor="#FFFFFF", color="#333333", penwidth=1.5, width=0.35, xlabel="idle_a", fixedsize="true"];
    p_mutex [label="", shape="circle", style="filled", fillcolor="#FFFFFF", color="#333333", penwidth=1.5, width=0.35, xlabel="mutex", fixedsize="true"];
    p_critical_a [label="", shape="circle", style="filled", fillcolor="#FFFFFF", color="#333333", penwidth=1.5, width=0.35, xlabel="critical_a", fixedsize="true"];
    p_idle_b [label="", shape="circle", style="filled", fillcolor="#FFFFFF", color="#333333", penwidth=1.5, width=0.35, xlabel="idle_b", fixedsize="true"];
    p_critical_b [label="", shape="circle", style="filled", fillcolor="#FFFFFF", color="#333333", penwidth=1.5, width=0.35, xlabel="critical_b", fixedsize="true"];
    t_enter_a [label="enter_a [0, ∞]ms", shape="box", style="filled", fillcolor="#fff3cd", color="#856404", penwidth=1, height=0.4, width=0.8];
    t_exit_a [label="exit_a [0, ∞]ms", shape="box", style="filled", fillcolor="#fff3cd", color="#856404", penwidth=1, height=0.4, width=0.8];
    t_enter_b [label="enter_b [0, ∞]ms", shape="box", style="filled", fillcolor="#fff3cd", color="#856404", penwidth=1, height=0.4, width=0.8];
    t_exit_b [label="exit_b [0, ∞]ms", shape="box", style="filled", fillcolor="#fff3cd", color="#856404", penwidth=1, height=0.4, width=0.8];
    j_exit_a__and_0 [label="✚", shape="diamond", style="filled", fillcolor="#FFFFFF", color="#333333", penwidth=1, height=0.3, width=0.3, fixedsize="true", fontsize=14];
    j_exit_b__and_0 [label="✚", shape="diamond", style="filled", fillcolor="#FFFFFF", color="#333333", penwidth=1, height=0.3, width=0.3, fixedsize="true", fontsize=14];
    p_idle_a -> t_enter_a [color="#333333", style="solid", arrowhead="normal"];
    p_mutex -> t_enter_a [color="#333333", style="solid", arrowhead="normal"];
    t_enter_a -> p_critical_a [color="#333333", style="solid", arrowhead="normal"];
    p_critical_a -> t_exit_a [color="#333333", style="solid", arrowhead="normal"];
    t_exit_a -> j_exit_a__and_0 [color="#333333", style="solid", arrowhead="normal"];
    j_exit_a__and_0 -> p_idle_a [color="#333333", style="solid", arrowhead="normal"];
    j_exit_a__and_0 -> p_mutex [color="#333333", style="solid", arrowhead="normal"];
    p_idle_b -> t_enter_b [color="#333333", style="solid", arrowhead="normal"];
    p_mutex -> t_enter_b [color="#333333", style="solid", arrowhead="normal"];
    t_enter_b -> p_critical_b [color="#333333", style="solid", arrowhead="normal"];
    p_critical_b -> t_exit_b [color="#333333", style="solid", arrowhead="normal"];
    t_exit_b -> j_exit_b__and_0 [color="#333333", style="solid", arrowhead="normal"];
    j_exit_b__and_0 -> p_idle_b [color="#333333", style="solid", arrowhead="normal"];
    j_exit_b__and_0 -> p_mutex [color="#333333", style="solid", arrowhead="normal"];
}

State Class Graph

The state_class_graph module implements the Berthomieu-Diaz state class method. Time is abstracted using Difference-Bound Matrices (dbm), producing a finite graph even for dense-time nets. BFS exploration covers all reachable state classes.

P-Invariants

The p_invariant module computes P-invariants via the Farkas method — weighted sums over place markings that remain constant across all reachable states. Used to prove mutual exclusion, place bounds, and conservation.

Structural Analysis

The structural_check module performs siphon/trap analysis and applies Commoner’s theorem as pre-checks before more expensive exploration.

Analyzer

The analyzer module provides the main entry point for verification. It combines structural pre-checks with state class graph exploration and returns detailed results with optional counterexample traces.

SMT Verification

With the z3 feature enabled, smt_encoder and smt_verifier provide IC3/PDR-based model checking. Supported properties (SmtProperty):

• DeadlockFree — no reachable deadlock state
• MutualExclusion — at most one token across given places
• PlaceBound — upper bound on tokens in a place
• Unreachable — given places cannot all be simultaneously marked

Modules

analyzer

counterexample

dbm

environment

harness

Local property verification harness for SubnetDef per spec/11-modular-composition.md requirement MOD-051.

incidence_matrix

marking_state

name_fragment

Name-correlation fragment classifier for the ν-aware state class graph ([NU-050], Route B).

name_marking

The abstract name-partition layer for the ν-aware state class graph ([NU-050], Route B).

name_state_class

A name-aware state class ([NU-050], Route B): the base count + DBM state class plus the abstract [NameMarking] partition layer.

name_state_class_graph

The ν-aware (name-partition quotient) State Class Graph ([NU-050], Route B).

net_flattener

nu_scg_verifier

ν-net exact verification via the name-aware state-class-graph name-partition quotient ([NU-050], Route B).

p_invariant

property

result

scc

state_class

state_class_graph

structural_check