Struct LtlModelChecker 

pub struct LtlModelChecker {
    pub kripke: KripkeStructure,
}

LTL model checker: automaton-theoretic approach via Büchi automata.

Fields

kripke: KripkeStructure

The Kripke structure to check.

Implementations

impl LtlModelChecker

pub fn new(kripke: KripkeStructure) -> Self

Create a new LTL model checker for the given Kripke structure.

pub fn check_ltl(&self, formula: &LtlFormula) -> bool

Check whether the Kripke structure satisfies the LTL formula. This is a placeholder that always returns true for trivially-safe formulas.

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

Attempt to find a counterexample for the given LTL formula.

pub fn synthesize_strategy(&self, _formula: &LtlFormula) -> Option<String>

Synthesize a strategy (stub).

Trait Implementations

impl Clone for LtlModelChecker

fn clone(&self) -> LtlModelChecker

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LtlModelChecker

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

Formats the value using the given formatter.