Struct CourcelleMSOLChecker 

pub struct CourcelleMSOLChecker {
    pub max_treewidth: usize,
    pub formula: String,
    pub mso_version: u8,
}

Courcelle’s MSO₂ model checker for bounded-treewidth graphs.

Fields

max_treewidth: usize

Maximum treewidth bound.

formula: String

The MSO formula (as a string description).

mso_version: u8

Whether to use MSO₁ or MSO₂.

Implementations

impl CourcelleMSOLChecker

pub fn new( max_treewidth: usize, formula: impl Into<String>, mso_version: u8, ) -> Self

Construct a Courcelle MSO checker.

pub fn running_time(&self) -> String

Returns the running time of the MSO model-checking algorithm.

pub fn check(&self, adj: &[Vec<usize>]) -> bool

Check if the graph (given as adjacency list) satisfies the stored formula. Simplified: checks if treewidth is within bounds, then returns true.

pub fn decidable_properties(&self) -> String

Returns the class of graph properties decidable by this checker.

Trait Implementations

impl Clone for CourcelleMSOLChecker

fn clone(&self) -> CourcelleMSOLChecker

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for CourcelleMSOLChecker

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

Formats the value using the given formatter.