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
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

//! Implementation of model checking DFS search strategy.

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

/// The search strategy based on the [DFS](https://en.wikipedia.org/wiki/Depth-first_search) algorithm.
pub struct Dfs {
    prune: PruneFn,
    goal: GoalFn,
    invariant: InvariantFn,
    collect: CollectFn,
    execution_mode: ExecutionMode,
    stats: McStats,
    visited: VisitedStates,
}

impl Dfs {
    fn dfs(&mut self, system: &mut McSystem, state: McState) -> Result<(), McError> {
        let available_events = system.available_events();

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

        for event_id in available_events {
            self.process_event(system, event_id)?;
        }
        Ok(())
    }
}

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

    fn run(&mut self, system: &mut McSystem) -> McResult {
        let state = system.get_state();

        let res = self.dfs(system, state);
        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.dfs(system, state)
    }

    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) {}
}