Enum modelator::Error [−][src]
pub enum Error {
Show 18 variants
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),
}
Expand description
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)
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
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
Auto Trait Implementations
impl RefUnwindSafe for Error
impl UnwindSafe for Error
Blanket Implementations
Mutably borrows from an owned value. Read more
pub fn vzip(self) -> V
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