Struct KripkeStructure 

pub struct KripkeStructure {
    pub num_states: usize,
    pub initial_states: Vec<usize>,
    pub transition_relation: Vec<Vec<usize>>,
    pub labeling: Vec<StateLabel>,
}

A Kripke structure M = (S, S_0, R, L).

Fields

num_states: usize

Total number of states (states are 0..num_states).

initial_states: Vec<usize>

Initial states.

transition_relation: Vec<Vec<usize>>

Transition relation: transition_relation[s] = successors of s.

labeling: Vec<StateLabel>

Labeling function.

Implementations

impl KripkeStructure

pub fn new(n: usize) -> Self

Create a new Kripke structure with n states.

pub fn add_initial(&mut self, s: usize)

Mark state s as an initial state.

pub fn add_transition(&mut self, s: usize, t: usize)

Add a transition from s to t.

pub fn label_state(&mut self, s: usize, prop: impl Into<String>)

Add a proposition to a state’s label.

pub fn reachable_states(&self) -> HashSet<usize>

Return all states reachable from initial states via BFS.

pub fn is_connected(&self) -> bool

Returns true if all states are reachable from the initial states.

pub fn compute_scc(&self) -> Vec<Vec<usize>>

Compute strongly connected components (Kosaraju’s algorithm).

Trait Implementations

impl Clone for KripkeStructure

fn clone(&self) -> KripkeStructure

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for KripkeStructure

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

Formats the value using the given formatter.