1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

use serde::Serialize;
use std::fmt::Debug;
use thiserror::Error;

use crate::model::checker::ApalacheError;

/// Set of possible errors that can occur when running `modelator`.
#[allow(clippy::upper_case_acronyms)]
#[derive(Error, Debug, Serialize)]
pub enum Error {
    /// An error that occurs when there's an IO error.
    #[error("IO error: {0}")]
    IO(String),

    /// An error that occurs when invalid unicode is encountered.
    #[error("Invalid unicode: {0:?}")]
    InvalidUnicode(std::ffi::OsString),

    /// An error that occurs when a TLA file does not have a module name.
    #[error("Unable to parse module name of: {0}")]
    MissingTlaFileModuleName(String),

    /// An error that occurs when a file is not found.
    #[error("File not found: {0}")]
    FileNotFound(std::path::PathBuf),

    /// An error that occurs when `Java` is not installed.
    #[error("Missing Java. Please install it.")]
    MissingJava,

    /// An error that occurs when the version `Java` installed is too low.
    #[error("Current Java version is: {0}. Minimum Java version supported is: {1}")]
    MinimumJavaVersion(usize, usize),

    /// An error that occurs when a TLA+ file representing a set of tests contains no test.
    #[error("No test found in {0}")]
    NoTestFound(String),

    /// An error that occurs when the model checker isn't able to generate a test trace.
    #[error("No trace found in {0}")]
    NoTestTraceFound(std::path::PathBuf),

    /// An error that occurs when the output of TLC is unexpected.
    #[error("Invalid TLC output: {0}")]
    InvalidTLCOutput(std::path::PathBuf),

    /// An error that occurs when the output of TLC returns an error.
    #[error("TLC failure: {0}")]
    TLCFailure(String),

    /// An error that occurs when the output of Apalache returns an error.
    #[error("Apalache failure: {0}")]
    ApalacheFailure(ApalacheError),

    /// An error that occurs when the counterexample produced by Apalache is unexpected.
    #[error("Invalid Apalache counterexample: {0}")]
    InvalidApalacheCounterexample(String),

    /// An error that occurs when using the `ureq` crate.
    #[error("Ureq error: {0}")]
    Ureq(String),

    /// An error that occurs when using the `nom` crate.
    #[error("Nom error: {0}")]
    Nom(String),

    /// An error that occurs when parsing a JSON value.
    #[error("JSON parse error: {0}")]
    JsonParseError(String),

    /// An error for unrecognized checker name.
    #[error("Unrecognized checker: {0}")]
    UnrecognizedChecker(String),
}

impl From<std::io::Error> for Error {
    fn from(err: std::io::Error) -> Self {
        Error::IO(err.to_string())
    }
}

impl From<ureq::Error> for Error {
    fn from(err: ureq::Error) -> Self {
        Error::Ureq(err.to_string())
    }
}

impl From<nom::Err<nom::error::Error<&str>>> for Error {
    fn from(err: nom::Err<nom::error::Error<&str>>) -> Self {
        Error::Nom(err.to_string())
    }
}

/// Set of possible errors that can occur when running a test using `modelator`.
#[derive(Error, Debug)]
pub enum TestError {
    /// A `modelator` [enum@Error].
    #[error("Error while running modelator: {0}")]
    Modelator(Error),

    /// A error that occurs when a test fails.
    #[error("Unhandled test: {test}")]
    UnhandledTest {
        /// Test content
        test: String,
        /// System under test
        system: String,
    },

    /// A error that occurs when a test fails.
    #[error("Test failed: {message}\n   {location}")]
    FailedTest {
        /// Failure message.
        message: String,
        /// Failure location.
        location: String,
        /// Test content
        test: String,
        /// System under test
        system: String,
    },
}