Struct CtlModelChecker 

pub struct CtlModelChecker {
    pub kripke: KripkeStructure,
}

CTL model checker: fixpoint computation.

Fields

kripke: KripkeStructure

The Kripke structure to check.

Implementations

impl CtlModelChecker

pub fn new(kripke: KripkeStructure) -> Self

Create a new CTL model checker.

pub fn sat_ex(&self, phi_states: &HashSet<usize>) -> HashSet<usize>

Compute sat(EX φ): states with at least one φ-successor.

pub fn sat_eu( &self, phi_states: &HashSet<usize>, psi_states: &HashSet<usize>, ) -> HashSet<usize>

Compute sat(EU(φ, ψ)): least fixpoint of ψ ∨ (φ ∧ EX(EU)).

pub fn sat_eg(&self, phi_states: &HashSet<usize>) -> HashSet<usize>

Compute sat(EG φ): greatest fixpoint of φ ∧ EX(EG).

pub fn sat(&self, formula: &CtlFormula) -> HashSet<usize>

Evaluate a CTL formula and return the set of satisfying states.

pub fn check_ctl(&self, formula: &CtlFormula) -> bool

Check whether all initial states satisfy the CTL formula.

pub fn find_counterexample( &self, formula: &CtlFormula, ) -> Option<CounterExample>

Find a counterexample state for a CTL formula.

Trait Implementations

impl Clone for CtlModelChecker

fn clone(&self) -> CtlModelChecker

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CtlModelChecker

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

Formats the value using the given formatter.