scan_core/
pg_model.rs

1use rand::rngs::SmallRng;
2
3use crate::{
4    Expression, Time, TransitionSystem, Val,
5    program_graph::{
6        Action, PgExpression, ProgramGraph, ProgramGraphBuilder, ProgramGraphRun, Var,
7    },
8    transition_system::TransitionSystemGenerator,
9};
10
11/// A [`ProgramGraph`]-based model implementing [`TransitionSystem`] with synchronous concurrency.
12#[derive(Debug, Clone)]
13pub struct PgModel {
14    pg: ProgramGraph,
15    global_vars: Vec<Var>,
16    predicates: Vec<Expression<Var>>,
17}
18
19impl PgModel {
20    /// Create a new [`PgModel`] from the given [`ProgramGraph`] and predicates over its internal state.
21    pub fn new(
22        pg: ProgramGraphBuilder,
23        global_vars: Vec<Var>,
24        predicates: Vec<PgExpression>,
25    ) -> Self {
26        let pg = pg.build();
27        Self {
28            pg,
29            global_vars,
30            predicates,
31        }
32    }
33}
34
35impl TransitionSystemGenerator for PgModel {
36    type Ts<'a>
37        = PgModelRun<'a>
38    where
39        Self: 'a;
40
41    fn generate<'a>(&'a self) -> Self::Ts<'a> {
42        PgModelRun {
43            pg: self.pg.new_instance(),
44            rng: rand::make_rng(),
45            global_vars: &self.global_vars,
46            predicates: &self.predicates,
47            time: 0,
48        }
49    }
50}
51
52/// A model based on a single [`ProgramGraph`],
53/// with predicates over the PG's variables.
54#[derive(Debug, Clone)]
55pub struct PgModelRun<'def> {
56    pg: ProgramGraphRun<'def>,
57    rng: SmallRng,
58    global_vars: &'def [Var],
59    predicates: &'def [Expression<Var>],
60    time: Time,
61}
62
63impl<'def> TransitionSystem for PgModelRun<'def> {
64    type Event = Action;
65
66    fn transition(&mut self) -> Option<Action> {
67        self.pg.montecarlo(&mut self.rng)
68    }
69
70    fn time(&self) -> Time {
71        self.time
72    }
73
74    fn time_tick(&mut self) {
75        self.time += 1;
76    }
77
78    fn labels(&self) -> impl Iterator<Item = bool> {
79        self.predicates.iter().map(|p| {
80            if let Val::Boolean(b) = self.pg.eval(p) {
81                b
82            } else {
83                panic!("non-bool pred")
84            }
85        })
86    }
87
88    fn state(&self) -> impl Iterator<Item = Val> {
89        self.global_vars
90            .as_ref()
91            .iter()
92            .map(|var| self.pg.val(*var).expect("value"))
93    }
94}
scan_core/pg_model.rs

scan_core/
pg_model.rs
