Enum ExecStrategy

pub enum ExecStrategy {
    Default,
    Naive,
    Decay,
}

Verification strategy.

This can considerably alter how the verification proceeds, with potential drastic change in verification time and memory needed.

Variants

Default

The default verification strategy.

Currently makes inputs imprecise at first, but keeps the states precise.

Naive

A naïve verification strategy, essentially brute-force model checking.

Makes the inputs and states completely precise, with no advantage gained by abstraction and no refinements necessary.

This strategy is only reasonable for comparison, not for serious use.

Decay

A verification strategy that additionally decays state precision.

Both inputs and newly generated states will be imprecise before refinement. This can make the verification faster or slower depending on the system.

Trait Implementations

impl Clone for ExecStrategy

fn clone(&self) -> ExecStrategy

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExecStrategy

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

Formats the value using the given formatter.

impl ValueEnum for ExecStrategy

fn value_variants<'a>() -> &'a [Self]

All possible argument values, in display order.

fn to_possible_value<'a>(&self) -> Option<PossibleValue>

The canonical argument value.

fn from_str(input: &str, ignore_case: bool) -> Result<Self, String>

Parse an argument into Self.