anysystem 0.1.2

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

//! Implementation of model checking BFS search strategy.

use std::collections::VecDeque;

use crate::mc::{
    CollectFn, ExecutionMode, GoalFn, InvariantFn, McError, McResult, McState, McStats, McSystem, PruneFn, Strategy,
    StrategyConfig, VisitedStates,
};

/// The search strategy based on the [BFS](https://en.wikipedia.org/wiki/Breadth-first_search) algorithm.
pub struct Bfs {
    prune: PruneFn,
    goal: GoalFn,
    invariant: InvariantFn,
    collect: CollectFn,
    states_queue: VecDeque<McState>,
    execution_mode: ExecutionMode,
    stats: McStats,
    visited: VisitedStates,
}

impl Bfs {
    fn bfs(&mut self, system: &mut McSystem) -> Result<(), McError> {
        // Start search from initial state
        self.states_queue.push_back(system.get_state());

        while !self.states_queue.is_empty() {
            let state = self.states_queue.pop_front().unwrap();

            if let Some(result) = self.check_state(&state) {
                result?;
                continue;
            }

            system.set_state(state);
            let available_events = system.available_events();
            for event_id in available_events {
                self.process_event(system, event_id)?;
            }
        }

        Ok(())
    }
}

impl Strategy for Bfs {
    fn build(config: StrategyConfig) -> Self {
        Bfs {
            prune: config.prune,
            goal: config.goal,
            invariant: config.invariant,
            collect: config.collect,
            execution_mode: config.execution_mode,
            states_queue: VecDeque::default(),
            stats: McStats::default(),
            visited: config.visited_states,
        }
    }

    fn run(&mut self, system: &mut McSystem) -> McResult {
        let res = self.bfs(system);
        match res {
            Ok(()) => Ok(self.stats.clone()),
            Err(err) => Err(err),
        }
    }

    fn search_step_impl(&mut self, _system: &mut McSystem, state: McState) -> Result<(), McError> {
        self.states_queue.push_back(state);
        Ok(())
    }

    fn execution_mode(&self) -> &ExecutionMode {
        &self.execution_mode
    }

    fn visited(&mut self) -> &mut VisitedStates {
        &mut self.visited
    }

    fn prune(&mut self) -> &mut PruneFn {
        &mut self.prune
    }

    fn goal(&mut self) -> &mut GoalFn {
        &mut self.goal
    }

    fn invariant(&mut self) -> &mut InvariantFn {
        &mut self.invariant
    }

    fn collect(&mut self) -> &mut CollectFn {
        &mut self.collect
    }

    fn stats(&mut self) -> &mut McStats {
        &mut self.stats
    }

    fn reset(&mut self) {
        self.states_queue.clear();
    }
}