Struct BisimulationChecker 

pub struct BisimulationChecker {
    pub lts: LabeledTransitionSystem,
}

Bisimulation checker for labeled transition systems.

Fields

lts: LabeledTransitionSystem

The LTS to analyze.

Implementations

impl BisimulationChecker

pub fn new(lts: LabeledTransitionSystem) -> Self

Create a new bisimulation checker for lts.

pub fn are_bisimilar(&self, s: usize, t: usize) -> bool

Check whether states s and t are bisimilar in the LTS.

Uses a partition-refinement approximation (up to max_rounds rounds).

pub fn compute_quotient(&self) -> HashMap<usize, usize>

Compute the bisimulation quotient using Paige-Tarjan partition refinement (simplified version).

Returns a map from state index to equivalence class index.

pub fn quotient_size(&self) -> usize

Return the number of equivalence classes in the quotient.

Trait Implementations

impl Debug for BisimulationChecker

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.