Enum EnvironmentAnalysisMode 

pub enum EnvironmentAnalysisMode {
    AlwaysAvailable,
    Bounded {
        max_tokens: usize,
    },
    Ignore,
}

How environment places should be treated during verification. Controls how environment places (external event sources) are treated during formal analysis.

Variants

AlwaysAvailable

Environment places are always considered to have tokens available. Transitions reading from environment places are always enabled.

Bounded

Environment places are treated as having at most max_tokens tokens. Explores states where 0..=max_tokens tokens are injected.

Fields

max_tokens: usize

Ignore

Environment places are treated as regular places (no special handling).

Trait Implementations

impl Clone for EnvironmentAnalysisMode

fn clone(&self) -> EnvironmentAnalysisMode

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EnvironmentAnalysisMode

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

Formats the value using the given formatter.

impl PartialEq for EnvironmentAnalysisMode

fn eq(&self, other: &EnvironmentAnalysisMode) -> 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 Eq for EnvironmentAnalysisMode

impl StructuralPartialEq for EnvironmentAnalysisMode