Enum ModelChecker 

pub enum ModelChecker {
    Tlc,
    Apalache,
}

Configuration option to select the model checker to be used.

Variants

Tlc

Option representing the TLC model checker.

Apalache

Option representing the Apalache mode checker.

Trait Implementations

impl Clone for ModelChecker

fn clone(&self) -> ModelChecker

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModelChecker

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ModelChecker

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl FromStr for ModelChecker

type Err = Error

The associated error which can be returned from parsing.

fn from_str(s: &str) -> Result<Self, Self::Err>

Parses a string s to return a value of this type.

impl PartialEq for ModelChecker

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

impl Eq for ModelChecker

impl StructuralPartialEq for ModelChecker