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)

Tuple Fields

0: String

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

InvalidUnicode(OsString)

Tuple Fields

0: OsString

An error that occurs when invalid unicode is encountered.

MissingTlaFileModuleName(String)

Tuple Fields

0: String

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

FileNotFound(PathBuf)

Tuple Fields

0: PathBuf

An error that occurs when a file is not found.

MissingJava

An error that occurs when Java is not installed.

MinimumJavaVersion(usize, usize)

Tuple Fields

0: usize

1: usize

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

NoTestFound(String)

Tuple Fields

0: String

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

TlaOperatorNameParseError(String)

Tuple Fields

0: String

Tla operator name parse error

NoTestTraceFound(PathBuf)

Tuple Fields

0: PathBuf

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

InvalidTLCOutput(PathBuf)

Tuple Fields

0: PathBuf

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

TLCFailure(String)

Tuple Fields

0: String

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

ApalacheFailure(ApalacheError)

Tuple Fields

0: ApalacheError

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

InvalidApalacheCounterexample(String)

Tuple Fields

0: String

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

Ureq(String)

Tuple Fields

0: String

An error that occurs when using the ureq crate.

Nom(String)

Tuple Fields

0: String

An error that occurs when using the nom crate.

JsonParseError(String)

Tuple Fields

0: String

An error that occurs when parsing a JSON value.

UnrecognizedChecker(String)

Tuple Fields

0: String

An error for unrecognized checker name.

UnsupportedOutputFormat(String)

Tuple Fields

0: 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.