Enum ValidationError 

#[non_exhaustive]
pub enum ValidationError {
    TraceSpecNotFound(PathBuf),
    TraceFileNotFound(PathBuf),
    EmptyTrace(PathBuf),
    InvalidJson {
        line: usize,
        reason: String,
    },
    NonObjectState {
        found: String,
    },
    InconsistentSchema {
        line: usize,
        expected: Vec<String>,
        found: Vec<String>,
    },
    UnsupportedType {
        line: usize,
        field: String,
        reason: String,
    },
    FloatNotSupported {
        line: usize,
        field: String,
        value: f64,
    },
    TlaConversion {
        line: usize,
        reason: String,
    },
    Apalache(ApalacheError),
    WorkDir(String),
    FileCopy {
        path: PathBuf,
        reason: String,
    },
    Io(Error),
    EmitterFinished,
    InconsistentArrayType {
        field: String,
        expected: String,
        found: String,
    },
}

Error during trace validation (Approach 3).

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

TraceSpecNotFound(PathBuf)

TraceSpec file not found.

TraceFileNotFound(PathBuf)

Trace file not found.

EmptyTrace(PathBuf)

Trace file is empty.

InvalidJson

Invalid JSON in trace file.

Fields

line: usize

reason: String

NonObjectState

State must serialize to a JSON object.

Fields

found: String

InconsistentSchema

Inconsistent record schema across trace lines.

Fields

line: usize

expected: Vec<String>

found: Vec<String>

UnsupportedType

Unsupported JSON value type.

Fields

line: usize

field: String

reason: String

FloatNotSupported

Float values not supported (TLA+ uses Int).

Fields

line: usize

field: String

value: f64

TlaConversion

Failed to convert to TLA+ record.

Fields

line: usize

reason: String

Apalache(ApalacheError)

Apalache CLI error.

WorkDir(String)

Failed to create work directory.

FileCopy

Failed to copy spec files.

Fields

path: PathBuf

reason: String

Io(Error)

IO error during validation.

EmitterFinished

Cannot emit after StateEmitter has been finished.

InconsistentArrayType

Inconsistent array element types.

Fields

field: String

expected: String

found: String

Trait Implementations

impl Debug for ValidationError

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

Formats the value using the given formatter.

impl Display for ValidationError

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

Formats the value using the given formatter.

impl Error for ValidationError

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

Returns the lower-level source of this error, if any.

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

fn provide<'a>(&'a self, request: &mut Request<'a>)

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

Provides type-based access to context intended for error reports.

impl From<ApalacheError> for ValidationError

fn from(source: ApalacheError) -> Self

Converts to this type from the input type.

impl From<Error> for ValidationError

fn from(source: Error) -> Self

Converts to this type from the input type.

impl From<ValidationError> for Error

fn from(source: ValidationError) -> Self

Converts to this type from the input type.