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
123
124
125
126

use std::{fmt::Write as _, io};

use serde::{Deserialize, Serialize};

use crate::{command::*, tester::TestEnv};

#[derive(Deserialize, Clone, Debug)]
pub struct ApalacheTestBatch {
    pub description: String,
    pub model: String,
    pub length: Option<u64>,
    pub timeout: Option<u64>,
    pub tests: Vec<String>,
}

#[derive(Serialize, Deserialize, Clone, Debug)]
pub struct ApalacheTestCase {
    pub model: String,
    pub test: String,
    pub length: Option<u64>,
    pub timeout: Option<u64>,
}

pub enum ApalacheRun {
    /// Apalache has found a counterexample
    Counterexample(CommandRun),
    /// Apalache has not found a counterexample up to specified length bound
    NoCounterexample(CommandRun),
    /// Apalache has found a deadlock
    Deadlock(CommandRun),
    /// Apalache model checking run failed (e.g. a parsing error)
    ModelError(CommandRun),
    /// Apalache returned an unknown error code
    Unknown(CommandRun),
    /// The tool has reached the specified timeout without producing an answer
    Timeout(CommandRun),
}

impl ApalacheRun {
    pub fn message(&self) -> &str {
        match self {
            ApalacheRun::Counterexample(_) => "Apalache has generated a counterexample",
            ApalacheRun::NoCounterexample(_) => "Apalache failed to generate a counterexample; consider increasing the length bound, or changing your test",
            ApalacheRun::Deadlock(_) => "Apalache has found a deadlock; please inspect your model and test",
            ApalacheRun::ModelError(_) => "Apalache failed to process the model; please check it",
            ApalacheRun::Unknown(_) => "Apalache has generated an unknown outcome; please contact Apalache developers",
            ApalacheRun::Timeout(_) => "Apalache failed to generate a counterexample within given time; consider increasing the timeout, or changing your test",
        }
    }
}

pub fn run_apalache_test(dir: &str, test: ApalacheTestCase) -> io::Result<ApalacheRun> {
    let inv = format!("{}Inv", test.test);

    // Mutate the model: negate the test assertion to get the invariant to check
    let mutation_failed = || {
        io::Error::new(
            io::ErrorKind::InvalidInput,
            "failed to mutate the model and add invariant",
        )
    };
    let env = TestEnv::new(dir).ok_or_else(mutation_failed)?;
    let model = env.read_file(&test.model).unwrap();
    let mut new_model = String::new();
    for line in model.lines() {
        if line.starts_with(&inv) {
            // invariant already present; skip mutation
            new_model.clear();
            break;
        }
        if line.starts_with("======") {
            let _ = writeln!(new_model, "{} == ~{}", inv, test.test);
        }
        new_model += line;
        new_model += "\n";
    }
    if !new_model.is_empty() {
        env.write_file(&test.model, &new_model)
            .ok_or_else(mutation_failed)?;
    }

    // Run Apalache, and process the result
    let mut cmd = Command::new();
    if let Some(timeout) = test.timeout {
        cmd.program("timeout");
        cmd.arg(&timeout.to_string());
        cmd.arg("apalache-mc");
    } else {
        cmd.program("apalache-mc");
    }
    cmd.arg("check");
    cmd.arg_from_parts(vec!["--inv=", &inv]);
    cmd.arg("--init=InitTest");
    cmd.arg("--next=NextTest");
    if let Some(length) = test.length {
        cmd.arg_from_parts(vec!["--length=", &length.to_string()]);
    }
    cmd.arg(&test.model);
    if !dir.is_empty() {
        cmd.current_dir(dir);
    }
    match cmd.spawn() {
        Ok(run) => {
            if run.status.success() {
                if run.stdout.contains("The outcome is: NoError") {
                    Ok(ApalacheRun::NoCounterexample(run))
                } else if run.stdout.contains("The outcome is: Error") {
                    Ok(ApalacheRun::Counterexample(run))
                } else if run.stdout.contains("The outcome is: Deadlock") {
                    Ok(ApalacheRun::Deadlock(run))
                } else {
                    Ok(ApalacheRun::Unknown(run))
                }
            } else if let Some(code) = run.status.code() {
                match code {
                    99 => Ok(ApalacheRun::ModelError(run)),
                    124 => Ok(ApalacheRun::Timeout(run)),
                    _ => Ok(ApalacheRun::Unknown(run)),
                }
            } else {
                Ok(ApalacheRun::Timeout(run))
            }
        },
        Err(e) => Err(e),
    }
}