Struct LabeledTransitionSystem 

pub struct LabeledTransitionSystem {
    pub n_states: usize,
    pub transitions: Vec<(usize, String, usize)>,
    pub labels: Vec<Vec<String>>,
}

Labeled transition system used for bisimulation checking.

Labels on transitions are Strings.

Fields

n_states: usize

Number of states.

transitions: Vec<(usize, String, usize)>

Transitions: (from, label, to).

labels: Vec<Vec<String>>

Optional state labels (atomic propositions).

Implementations

impl LabeledTransitionSystem

pub fn new(n_states: usize) -> Self

Create a new LTS with n_states states and no transitions.

pub fn add_transition( &mut self, from: usize, label: impl Into<String>, to: usize, )

Add a labeled transition from --label--> to.

pub fn add_label(&mut self, state: usize, label: impl Into<String>)

Add an atomic proposition to a state.

Trait Implementations

impl Clone for LabeledTransitionSystem

fn clone(&self) -> LabeledTransitionSystem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LabeledTransitionSystem

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

Formats the value using the given formatter.