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
use crate::{command::*, tester::TestEnv};
use serde::{Deserialize, Serialize};
use std::io;
#[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 {
Counterexample(CommandRun),
NoCounterexample(CommandRun),
Deadlock(CommandRun),
ModelError(CommandRun),
Unknown(CommandRun),
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);
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) {
new_model.clear();
break;
}
if line.starts_with("======") {
new_model += &format!("{} == ~{}\n", 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)?;
}
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),
}
}