smc_scan_core 0.1.0

Core module for the Scan model checker.
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

use rand::rngs::SmallRng;

use crate::{
    Expression, Time, TransitionSystem, Val,
    program_graph::{
        Action, PgExpression, ProgramGraph, ProgramGraphBuilder, ProgramGraphRun, Var,
    },
    transition_system::TransitionSystemGenerator,
};

/// A [`ProgramGraph`]-based model implementing [`TransitionSystem`] with synchronous concurrency.
#[derive(Debug, Clone)]
pub struct PgModel {
    pg: ProgramGraph,
    global_vars: Vec<Var>,
    predicates: Vec<Expression<Var>>,
}

impl PgModel {
    /// Create a new [`PgModel`] from the given [`ProgramGraph`] and predicates over its internal state.
    pub fn new(
        pg: ProgramGraphBuilder,
        global_vars: Vec<Var>,
        predicates: Vec<PgExpression>,
    ) -> Self {
        let pg = pg.build();
        Self {
            pg,
            global_vars,
            predicates,
        }
    }
}

impl TransitionSystemGenerator for PgModel {
    type Ts<'a>
        = PgModelRun<'a>
    where
        Self: 'a;

    fn generate<'a>(&'a self) -> Self::Ts<'a> {
        PgModelRun {
            pg: self.pg.new_instance(),
            rng: rand::make_rng(),
            global_vars: &self.global_vars,
            predicates: &self.predicates,
            time: 0,
        }
    }
}

/// A model based on a single [`ProgramGraph`],
/// with predicates over the PG's variables.
#[derive(Debug, Clone)]
pub struct PgModelRun<'def> {
    pg: ProgramGraphRun<'def>,
    rng: SmallRng,
    global_vars: &'def [Var],
    predicates: &'def [Expression<Var>],
    time: Time,
}

impl<'def> TransitionSystem for PgModelRun<'def> {
    type Event = Action;

    fn transition(&mut self) -> Option<Action> {
        self.pg.montecarlo(&mut self.rng)
    }

    fn time(&self) -> Time {
        self.time
    }

    fn time_tick(&mut self) {
        self.time += 1;
    }

    fn labels(&self) -> impl Iterator<Item = bool> {
        self.predicates.iter().map(|p| {
            if let Val::Boolean(b) = self.pg.eval(p) {
                b
            } else {
                panic!("non-bool pred")
            }
        })
    }

    fn state(&self) -> impl Iterator<Item = Val> {
        self.global_vars
            .as_ref()
            .iter()
            .map(|var| self.pg.val(*var).expect("value"))
    }
}