tla-checker 0.6.0

A TLA+ model checker written in Rust
Documentation 
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

use std::fmt::Write;
use std::path::Path;

use super::beat::run_beat;
use super::manifest::Manifest;

pub fn render_doc(manifest_dir: &Path, manifest: &Manifest) -> (String, bool) {
    let mut out = String::new();
    let title = manifest
        .title
        .clone()
        .unwrap_or_else(|| "TLA+ demo".to_string());
    let _ = writeln!(out, "# {}\n", title);

    let mut all_passed = true;
    for (idx, beat) in manifest.beats.iter().enumerate() {
        let report = run_beat(manifest_dir, manifest, beat);
        let passed = report.passed();
        all_passed &= passed;
        let mark = if passed { "✓" } else { "✗" };

        let _ = writeln!(out, "## {}. {} {}\n", idx + 1, report.title, mark);
        if let Some(note) = &report.note {
            let _ = writeln!(out, "{}\n", note);
        }

        if !beat.scenario.is_empty() {
            let _ = writeln!(out, "Scenario:\n");
            let _ = writeln!(out, "```");
            for line in &beat.scenario {
                let _ = writeln!(out, "{}", line);
            }
            let _ = writeln!(out, "```\n");
        } else if let Some(replay) = &beat.replay {
            let _ = writeln!(out, "Replay: `{}`\n", replay);
        }

        for run in &report.runs {
            let _ = write!(out, "**Variant `{}`**", run.variant);
            if let Some(v) = manifest.variants.get(&run.variant) {
                let _ = write!(out, " — spec `{}`", v.spec);
                if let Some(cfg) = &v.config {
                    let _ = write!(out, ", config `{}`", cfg);
                }
                if !v.constants.is_empty() {
                    let consts: Vec<String> = v
                        .constants
                        .iter()
                        .map(|(k, val)| format!("{}={}", k, val))
                        .collect();
                    let _ = write!(out, ", constants {}", consts.join(", "));
                }
            }
            let _ = writeln!(out, "\n");

            if let Some(failure) = &run.failure {
                let _ = writeln!(out, "- **error:** {}", failure);
            }
            for assertion in &run.assertions {
                let m = if assertion.passed { "✓" } else { "✗" };
                match &assertion.detail {
                    Some(d) if !assertion.passed => {
                        let _ = writeln!(out, "- {} `{}` — {}", m, assertion.raw, d);
                    }
                    _ => {
                        let _ = writeln!(out, "- {} `{}`", m, assertion.raw);
                    }
                }
            }
            let _ = writeln!(out);
        }
    }

    (out, all_passed)
}