Enum modelator::Error

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

Set of possible errors that can occur when running modelator.

Variants

IO

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

Tuple Fields of IO

0: String

InvalidUnicode

An error that occurs when invalid unicode is encountered.

Tuple Fields of InvalidUnicode

0: OsString

MissingTlaFileModuleName

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

Tuple Fields of MissingTlaFileModuleName

0: String

FileNotFound

An error that occurs when a file is not found.

Tuple Fields of FileNotFound

0: PathBuf

MissingJava

An error that occurs when Java is not installed.

MinimumJavaVersion

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

Tuple Fields of MinimumJavaVersion

0: usize1: usize

NoTestFound

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

Tuple Fields of NoTestFound

0: String

NoTestTraceFound

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

Tuple Fields of NoTestTraceFound

0: PathBuf

InvalidTLCOutput

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

Tuple Fields of InvalidTLCOutput

0: PathBuf

TLCFailure

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

Tuple Fields of TLCFailure

0: String

ApalacheFailure

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

Tuple Fields of ApalacheFailure

0: ApalacheError

InvalidApalacheCounterexample

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

Tuple Fields of InvalidApalacheCounterexample

0: String

Ureq

An error that occurs when using the ureq crate.

Tuple Fields of Ureq

0: String

Nom

An error that occurs when using the nom crate.

Tuple Fields of Nom

0: String

JsonParseError

An error that occurs when parsing a JSON value.

Tuple Fields of JsonParseError

0: String

UnrecognizedChecker

An error for unrecognized checker name.

Tuple Fields of UnrecognizedChecker

0: String

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.