pub enum ModelChecker {
Tlc,
Apalache,
}
Expand description
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
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
Auto Trait Implementations
impl RefUnwindSafe for ModelChecker
impl Send for ModelChecker
impl Sync for ModelChecker
impl Unpin for ModelChecker
impl UnwindSafe for ModelChecker
Blanket Implementations
Mutably borrows from an owned value. Read more
Compare self to key
and return true
if they are equal.
Attaches the provided Subscriber
to this type, returning a
WithDispatch
wrapper. Read more
Attaches the current default Subscriber
to this type, returning a
WithDispatch
wrapper. Read more