machine-check 0.6.1

Formal verification tool for digital systems
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
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185

//! This module tests the examples from the chapters of the book.
//!
//! If an example is a normal example but also in book, properties may be tested twice.

use crate::examples::harness::{test_example, test_example_expect_panic, TestConfig};

#[test]
fn book_ch1_quickstart() {
    // chapter 1: recovery property
    test_example(
        "book_quickstart",
        TestConfig::new_property("AG![EF![value == 0]]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":16,"num_generated_states":48,"num_final_states":16,"num_generated_transitions":64,"num_final_transitions":33,"inherent_panic_message":null}}"#,
    );
}

#[test]
fn book_ch2_properties() {
    // chapter 2a: is the value zero at the start of the computation?
    test_example(
        "book_quickstart",
        TestConfig::new_property("value == 0"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":0,"num_generated_states":6,"num_final_states":5,"num_generated_transitions":6,"num_final_transitions":6,"inherent_panic_message":null}}"#,
    );

    // chapter 2b: with AX
    test_example(
        "book_quickstart",
        TestConfig::new_property("AX![value == 0]"),
        r#"{"result":{"Ok":"False"},"stats":{"num_refinements":1,"num_generated_states":8,"num_final_states":5,"num_generated_transitions":9,"num_final_transitions":7,"inherent_panic_message":null}}"#,
    );

    // chapter 2c: with EX
    test_example(
        "book_quickstart",
        TestConfig::new_property("EX![value == 0]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":1,"num_generated_states":8,"num_final_states":5,"num_generated_transitions":9,"num_final_transitions":7,"inherent_panic_message":null}}"#,
    );

    // chapter 2d: globally, on all paths, value (unsigned) is at most 15
    test_example(
        "book_quickstart",
        TestConfig::new_property("AG![as_unsigned(value) <= 15]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":0,"num_generated_states":6,"num_final_states":5,"num_generated_transitions":6,"num_final_transitions":6,"inherent_panic_message":null}}"#,
    );

    // chapter 2e: there exists a path where value is globally zero
    test_example(
        "book_quickstart",
        TestConfig::new_property("EG![value == 0]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":1,"num_generated_states":8,"num_final_states":5,"num_generated_transitions":9,"num_final_transitions":7,"inherent_panic_message":null}}"#,
    );

    // chapter 2f: there exists a path where value is globally 3
    test_example(
        "book_quickstart",
        TestConfig::new_property("EG![value == 3]"),
        r#"{"result":{"Ok":"False"},"stats":{"num_refinements":0,"num_generated_states":6,"num_final_states":5,"num_generated_transitions":6,"num_final_transitions":6,"inherent_panic_message":null}}"#,
    );

    // chapter 2g: there exists a path where value is eventually 3
    test_example(
        "book_quickstart",
        TestConfig::new_property("EF![as_unsigned(value) == 3]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":3,"num_generated_states":13,"num_final_states":6,"num_generated_transitions":16,"num_final_transitions":10,"inherent_panic_message":null}}"#,
    );

    // chapter 2h: there exists a path that eventually reaches a state
    // where there exists a path s.t. the value is globally 3
    test_example(
        "book_quickstart",
        TestConfig::new_property("EF![EG![value == 3]]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":4,"num_generated_states":17,"num_final_states":8,"num_generated_transitions":21,"num_final_transitions":13,"inherent_panic_message":null}}"#,
    );

    // chapter 2i: until
    test_example(
        "book_quickstart",
        TestConfig::new_property("EU![as_unsigned(value) < 3, value == 3]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":3,"num_generated_states":13,"num_final_states":6,"num_generated_transitions":16,"num_final_transitions":10,"inherent_panic_message":null}}"#,
    );

    // chapter 2j: release
    test_example(
        "book_quickstart",
        TestConfig::new_property("AR![value == 3, as_unsigned(value) <= 3]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":3,"num_generated_states":13,"num_final_states":6,"num_generated_transitions":16,"num_final_transitions":10,"inherent_panic_message":null}}"#,
    );

    // chapter 2k: implication using logical operators
    test_example(
        "book_quickstart",
        TestConfig::new_property("AG![!(value == 5) || AX![value == 5 || value == 6]]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":16,"num_generated_states":48,"num_final_states":16,"num_generated_transitions":64,"num_final_transitions":33,"inherent_panic_message":null}}"#,
    );

    // chapter 2l: recovery property
    test_example(
        "book_quickstart",
        TestConfig::new_property("AG![EF![value == 0]]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":16,"num_generated_states":48,"num_final_states":16,"num_generated_transitions":64,"num_final_transitions":33,"inherent_panic_message":null}}"#,
    );
}

#[test]
fn book_ch3() {
    // chapter 3.1a: checking existence of path where eventually value is 10, field max_value set to 5
    test_example(
        "book_instances_input",
        TestConfig::new_property("EF![value == 10]").with_input("5"),
        r#"Write the maximum system value: {"result":{"Ok":"False"},"stats":{"num_refinements":6,"num_generated_states":19,"num_final_states":6,"num_generated_transitions":25,"num_final_transitions":13,"inherent_panic_message":null}}"#,
    );

    // chapter 3.1b: checking existence of path where eventually value is 10, field max_value set to 12
    test_example(
        "book_instances_input",
        TestConfig::new_property("EF![value == 10]").with_input("12"),
        r#"Write the maximum system value: {"result":{"Ok":"True"},"stats":{"num_refinements":10,"num_generated_states":33,"num_final_states":13,"num_generated_transitions":43,"num_final_transitions":24,"inherent_panic_message":null}}"#,
    );

    // chapter 3.1c: checking existence of path where eventually value is 10, field max_value set to 20
    // this should panic
    test_example_expect_panic(
        "book_instances_input",
        TestConfig::new_property("EF![value == 10]").with_input("20"),
    );

    // chapter 3.1d: checking inherent where field max_value is set to 10, inherent should not hold
    test_example(
        "book_instances_todo",
        TestConfig::new_inherent().with_input("10"),
        r#"Write the maximum system value: {"result":{"Ok":"False"},"stats":{"num_refinements":11,"num_generated_states":36,"num_final_states":14,"num_generated_transitions":47,"num_final_transitions":26,"inherent_panic_message":"not yet implemented: Zero the next value when it is greater than max value"}}"#,
    );

    // chapter 3.1e: checking inherent where field max_value is set to 15, inherent should hold
    test_example(
        "book_instances_todo",
        TestConfig::new_inherent().with_input("15"),
        r#"Write the maximum system value: {"result":{"Ok":"True"},"stats":{"num_refinements":0,"num_generated_states":6,"num_final_states":5,"num_generated_transitions":6,"num_final_transitions":6,"inherent_panic_message":null}}"#,
    );
}

#[test]
fn book_ch9_parametric() {
    // chapter 9a: whether the property holds depends on parameters
    test_example(
        "parametric",
        TestConfig::new_property("AG![value == 0]"),
        r#"{"result":{"Ok":"Dependent"},"stats":{"num_refinements":5,"num_generated_states":69,"num_final_states":33,"num_generated_transitions":96,"num_final_transitions":50,"inherent_panic_message":null}}"#,
    );

    // chapter 9b: a property that does not hold independently of parameters
    test_example(
        "parametric",
        TestConfig::new_property("AF![as_unsigned(value) > 0]"),
        r#"{"result":{"Ok":"False"},"stats":{"num_refinements":64,"num_generated_states":368,"num_final_states":151,"num_generated_transitions":784,"num_final_transitions":287,"inherent_panic_message":null}}"#,
    );
}

#[test]
fn book_ch10_mu_calculus() {
    // chapter 10a: holds in even positions
    test_example(
        "mu_even",
        TestConfig::new_property("gfp![Z, value == 0 && AX![AX![Z]]]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":0,"num_generated_states":3,"num_final_states":2,"num_generated_transitions":3,"num_final_transitions":3,"inherent_panic_message":null}}"#,
    );

    // chapter 10b: whether holds eventually forever (AF[AG[p == 1]])
    test_example(
        "mu_infinitely_often",
        TestConfig::new_property("AF![AG![p == 1]]"),
        r#"{"result":{"Ok":"False"},"stats":{"num_refinements":1,"num_generated_states":8,"num_final_states":3,"num_generated_transitions":9,"num_final_transitions":5,"inherent_panic_message":null}}"#,
    );

    // chapter 10c: whether p == 1 holds infinitely often for all paths (AFG[p == 1])
    // This is the translation to mu-calculus as per Cranen, Groote & Reniers,
    // "A linear translation from LTL to the first-order modal μ-calculus"
    // ( https://doi.org/10.1016/j.tcs.2011.02.034 ) page 6.
    test_example(
        "mu_infinitely_often",
        TestConfig::new_property("lfp![X,gfp![Y, AX![X] || (p == 1 && AX![Y])]]"),
        r#"{"result":{"Ok":"True"},"stats":{"num_refinements":1,"num_generated_states":8,"num_final_states":3,"num_generated_transitions":9,"num_final_transitions":5,"inherent_panic_message":null}}"#,
    );
}