Struct ModelChecker 

pub struct ModelChecker {
    pub states: Vec<Vec<f64>>,
    pub transitions: Vec<(StateIdx, StateIdx)>,
}

A simple explicit-state model checker.

States are represented as Vecf64(e.g., phase-space coordinates). Transitions are labeled pairs(from, to)`.

Fields

states: Vec<Vec<f64>>

All states in the model.

transitions: Vec<(StateIdx, StateIdx)>

Transitions as (from_idx, to_idx) pairs.

Implementations

impl ModelChecker

pub fn new( states: Vec<Vec<f64>>, transitions: Vec<(StateIdx, StateIdx)>, ) -> Self

Create a new model checker from a set of states and transitions.

pub fn reachable_states(&self, start_idx: StateIdx) -> HashSet<StateIdx>

Return all states reachable from start_idx via BFS.

pub fn satisfies_invariant<F>(&self, start_idx: StateIdx, invariant: F) -> bool

where F: Fn(&[f64]) -> bool,

Check whether all reachable states from start_idx satisfy invariant.

pub fn find_counterexample<F>( &self, start_idx: StateIdx, invariant: F, ) -> Option<StateIdx>

where F: Fn(&[f64]) -> bool,

Find a counterexample state (as index) that violates invariant.

Returns None if all reachable states satisfy the invariant.

pub fn shortest_path( &self, start_idx: StateIdx, target_idx: StateIdx, ) -> Option<Vec<StateIdx>>

Return the shortest path (as a sequence of state indices) from start_idx to target_idx, or None if unreachable.

pub fn reachable_count(&self, start_idx: StateIdx) -> usize

Count the number of reachable states from start_idx.

Trait Implementations

impl Clone for ModelChecker

fn clone(&self) -> ModelChecker

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModelChecker

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

Formats the value using the given formatter.