Enum modelator::Error

pub enum Error {
    IO(String),
    InvalidUnicode(OsString),
    MissingTlaFileModuleName(String),
    FileNotFound(PathBuf),
    MissingJava,
    MinimumJavaVersion(usize, usize),
    NoTestFound(String),
    TlaOperatorNameParseError(String),
    NoTestTraceFound(PathBuf),
    InvalidTLCOutput(PathBuf),
    TLCFailure(String),
    ApalacheFailure(ApalacheError),
    InvalidApalacheCounterexample(String),
    Ureq(String),
    Nom(String),
    JsonParseError(String),
    UnrecognizedChecker(String),
    UnsupportedOutputFormat(String),
}

Set of possible errors that can occur when running modelator.

Variants

IO(String)

An error that occurs when there’s an IO error.

InvalidUnicode(OsString)

An error that occurs when invalid unicode is encountered.

MissingTlaFileModuleName(String)

An error that occurs when a TLA file does not have a module name.

FileNotFound(PathBuf)

An error that occurs when a file is not found.

MissingJava

An error that occurs when Java is not installed.

MinimumJavaVersion(usize, usize)

An error that occurs when the version Java installed is too low.

NoTestFound(String)

An error that occurs when a TLA+ file representing a set of tests contains no test.

TlaOperatorNameParseError(String)

Tla operator name parse error

NoTestTraceFound(PathBuf)

An error that occurs when the model checker isn’t able to generate a test trace.

InvalidTLCOutput(PathBuf)

An error that occurs when the output of TLC is unexpected.

TLCFailure(String)

An error that occurs when the output of TLC returns an error.

ApalacheFailure(ApalacheError)

An error that occurs when the output of Apalache returns an error.

InvalidApalacheCounterexample(String)

An error that occurs when the counterexample produced by Apalache is unexpected.

Ureq(String)

An error that occurs when using the ureq crate.

Nom(String)

An error that occurs when using the nom crate.

JsonParseError(String)

An error that occurs when parsing a JSON value.

UnrecognizedChecker(String)

An error for unrecognized checker name.

UnsupportedOutputFormat(String)

An error for unsupported output format.

Trait Implementations

impl Debug for Error

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

Formats the value using the given formatter.

impl Display for Error

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

Formats the value using the given formatter.

impl Error for Error

fn source(&self) -> Option<&(dyn Error + 'static)>

The lower-level source of this error, if any.

fn backtrace(&self) -> Option<&Backtrace>

🔬 This is a nightly-only experimental API. (backtrace)

Returns a stack backtrace, if available, of where this error occurred.

fn description(&self) -> &str

👎 Deprecated since 1.42.0:

use the Display impl or to_string()

fn cause(&self) -> Option<&dyn Error>

👎 Deprecated since 1.33.0:

replaced by Error::source, which can support downcasting

impl From<Err<Error<&'_ str>>> for Error

fn from(err: Err<Error<&str>>) -> Self

Performs the conversion.

impl From<Error> for Error

fn from(err: Error) -> Self

Performs the conversion.

impl From<Error> for Error

fn from(err: Error) -> Self

Performs the conversion.

impl Serialize for Error

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error> where
    __S: Serializer, 

Serialize this value into the given Serde serializer.