Enum ZCSModelCheckerHeuristics 

pub enum ZCSModelCheckerHeuristics {
    ResetHeuristics,
    DecrementAndIncrementHeuristics,
    CanonicalHeuristics,
    EmptyErrorGraphHeuristics,
}

this enum defines SymbolicModelChecker Heuristics, such a heuristics defines which symbolic paths are ignored and which specifications and threshold automata can be checked

Additionally it describes a greedy heuristics which only checks if the symbolic error graph is empty.

Variants

ResetHeuristics

this heuristics yields a semi-decision procedure by unfolding cycles if the given ta contains resets it can be used to verify extended threshold automata for coverability or reachability specifications

DecrementAndIncrementHeuristics

this heuristics yields a semi-decision procedure by unfolding cycles if the given ta contains increments and decrements it can be used to verify extended threshold automata for coverability or reachability specifications

CanonicalHeuristics

this heuristics yields a decision procedure by only traversing cycles once it can be used to verify canonical threshold automata (no resets/decrements) for coverability or reachability specifications

EmptyErrorGraphHeuristics

this is a greedy heuristics that only checks if the symbolic error graph is empty it is neither complete nor sound but guarantees termination if the error graph is empty the property holds, otherwise no conclusion can be drawn

Implementations

impl ZCSModelCheckerHeuristics

pub fn new_reset_heuristics() -> Self

returns a new ResetHeuristics

pub fn new_decrement_and_increment_heuristics() -> Self

returns a new DecrementsAndIncrementHeuristics

pub fn new_canonical_heuristics() -> Self

returns a new CanonicalHeuristics

pub fn new_empty_error_graph_heuristics() -> Self

returns a new CanonicalHeuristics

pub fn is_monotonic(&self) -> bool

returns true iff the heuristics ensures that every steady path is monotonic

Trait Implementations

impl Clone for ZCSModelCheckerHeuristics

fn clone(&self) -> ZCSModelCheckerHeuristics

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ZCSModelCheckerHeuristics

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

Formats the value using the given formatter.

impl PartialEq for ZCSModelCheckerHeuristics

fn eq(&self, other: &ZCSModelCheckerHeuristics) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for ZCSModelCheckerHeuristics