libpetri_verification/lib.rs
1//! # libpetri-verification — Formal Verification
2//!
3//! Verifies safety and liveness properties of Petri nets defined with
4//! [`libpetri-core`](https://docs.rs/libpetri-core).
5//!
6//! ## Example: Mutual Exclusion
7//!
8//! A classic mutual exclusion net where two processes compete for a shared
9//! mutex token. Verification proves that `critical_a` and `critical_b` can
10//! never both hold tokens simultaneously.
11//!
12#![doc = include_str!(concat!(env!("OUT_DIR"), "/mutex_example.svg"))]
13//!
14//! ## State Class Graph
15//!
16//! The [`state_class_graph`] module implements the Berthomieu-Diaz state class
17//! method. Time is abstracted using Difference-Bound Matrices ([`dbm`]),
18//! producing a finite graph even for dense-time nets. BFS exploration covers
19//! all reachable state classes.
20//!
21//! ## P-Invariants
22//!
23//! The [`p_invariant`] module computes P-invariants via the Farkas method —
24//! weighted sums over place markings that remain constant across all reachable
25//! states. Used to prove mutual exclusion, place bounds, and conservation.
26//!
27//! ## Structural Analysis
28//!
29//! The [`structural_check`] module performs siphon/trap analysis and applies
30//! Commoner's theorem as pre-checks before more expensive exploration.
31//!
32//! ## Analyzer
33//!
34//! The [`analyzer`] module provides the main entry point for verification.
35//! It combines structural pre-checks with state class graph exploration and
36//! returns detailed [`result`]s with optional counterexample traces.
37//!
38//! ## SMT Verification
39//!
40//! With the `z3` feature enabled, `smt_encoder` and `smt_verifier` provide
41//! IC3/PDR-based model checking. Supported properties
42//! ([`SmtProperty`](property::SmtProperty)):
43//!
44//! - **DeadlockFree** — no reachable deadlock state
45//! - **MutualExclusion** — at most one token across given places
46//! - **PlaceBound** — upper bound on tokens in a place
47//! - **Unreachable** — given places cannot all be simultaneously marked
48
49pub mod analyzer;
50pub mod counterexample;
51pub mod dbm;
52pub mod environment;
53pub mod incidence_matrix;
54pub mod marking_state;
55pub mod net_flattener;
56pub mod p_invariant;
57pub mod property;
58pub mod result;
59pub mod scc;
60#[cfg(feature = "z3")]
61pub mod smt_encoder;
62pub mod state_class;
63pub mod state_class_graph;
64pub mod structural_check;
65
66#[cfg(feature = "z3")]
67pub mod smt_verifier;