anysystem 0.2.0

A framework for deterministic simulation and testing of distributed systems
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

/// Runs model checking with given settings
#[macro_export]
macro_rules! run_mc {
    ($sys:expr, $config:expr, $strategy:ident) => {
        match $strategy {
            "bfs" => ModelChecker::new(&$sys).run::<Bfs>($config),
            "dfs" => ModelChecker::new(&$sys).run::<Dfs>($config),
            s => panic!("Unknown strategy name: {}", s),
        }
    };
    ($sys:expr, $config:expr, $strategy:ident, $callback:expr) => {
        match $strategy {
            "bfs" => ModelChecker::new(&$sys).run_with_change::<Bfs>($config, $callback),
            "dfs" => ModelChecker::new(&$sys).run_with_change::<Dfs>($config, $callback),
            s => panic!("Unknown strategy name: {}", s),
        }
    };
    ($sys:expr, $config:expr, $strategy:ident, $states:ident, $callback:expr) => {
        match $strategy {
            "bfs" => ModelChecker::new(&$sys).run_from_states_with_change::<Bfs>($config, $states, $callback),
            "dfs" => ModelChecker::new(&$sys).run_from_states_with_change::<Dfs>($config, $states, $callback),
            s => panic!("Unknown strategy name: {}", s),
        }
    };
}