scan_core/
cs_model.rs

1use crate::TransitionSystemGenerator;
2use crate::channel_system::{
3    Channel, ChannelSystem, ChannelSystemBuilder, ChannelSystemRun, Event, EventType,
4};
5use crate::{DummyRng, Expression, Time, Val, transition_system::TransitionSystem};
6
7/// An atomic variable for [`crate::Pmtl`] formulae.
8#[derive(Debug, Clone)]
9pub enum Atom {
10    /// A predicate.
11    State(Channel, usize),
12    /// An event.
13    Event(Event),
14}
15
16/// A definition type that instances new [`CsModelRun`].
17#[derive(Debug, Clone)]
18pub struct CsModel {
19    cs: ChannelSystem,
20    ports: Vec<Vec<Option<Val>>>,
21    predicates: Vec<Expression<Atom>>,
22}
23
24impl CsModel {
25    /// Creates a new [`CsModel`] from a [`ChannelSystemBuilder`].
26    pub fn new(cs: ChannelSystemBuilder) -> Self {
27        // TODO: Check predicates are Boolean expressions and that conversion does not fail
28        let cs = cs.build();
29        Self {
30            ports: cs
31                .channels()
32                .iter()
33                .map(|(types, _)| vec![None; types.len()])
34                .collect(),
35            cs,
36            predicates: Vec::new(),
37        }
38    }
39
40    /// Adds a new port to the [`CsModel`],
41    /// which is given by an [`Channel`] and a default [`Val`] value.
42    pub fn add_port(&mut self, channel: Channel, idx: usize, default: Val) {
43        // TODO FIXME: error handling and type checking.
44        self.ports[u16::from(channel) as usize][idx] = Some(default);
45    }
46
47    /// Adds a new predicate to the [`CsModel`],
48    /// which is an expression over the CS's channels.
49    pub fn add_predicate(&mut self, predicate: Expression<Atom>) -> usize {
50        let _ = predicate.eval(
51            &|port| match port {
52                Atom::State(channel, idx) => self.ports[u16::from(*channel) as usize][*idx]
53                    .expect("port must have been initialized"),
54                Atom::Event(_event) => Val::Boolean(false),
55            },
56            &mut DummyRng,
57        );
58        self.predicates.push(predicate);
59        self.predicates.len() - 1
60    }
61}
62
63impl TransitionSystemGenerator for CsModel {
64    type Ts<'a>
65        = CsModelRun<'a>
66    where
67        Self: 'a;
68
69    fn generate<'a>(&'a self) -> Self::Ts<'a> {
70        CsModelRun {
71            cs: self.cs.new_instance(),
72            ports: self.ports.clone(),
73            predicates: &self.predicates,
74            last_event: None,
75        }
76    }
77}
78
79/// Transition system model based on a [`ChannelSystem`].
80///
81/// It is essentially a CS which keeps track of the [`Event`]s produced by the execution
82/// and determining a set of predicates.
83#[derive(Debug, Clone)]
84pub struct CsModelRun<'def> {
85    cs: ChannelSystemRun<'def>,
86    ports: Vec<Vec<Option<Val>>>,
87    // TODO: predicates should not use rng
88    predicates: &'def [Expression<Atom>],
89    last_event: Option<Event>,
90}
91
92impl<'def> TransitionSystem for CsModelRun<'def> {
93    type Event = Event;
94
95    fn transition(&mut self) -> Option<Event> {
96        let event = self.cs.montecarlo_execution();
97        if let Some(ref event) = event
98            && let EventType::Send(ref vals) = event.event_type
99        {
100            let port = self
101                .ports
102                .get_mut(u16::from(event.channel) as usize)
103                .expect("port must exist");
104            port.iter_mut().zip(vals).for_each(|(p, &v)| {
105                if p.is_some() {
106                    *p = Some(v)
107                }
108            });
109        }
110        self.last_event = event.clone();
111        event
112    }
113
114    #[inline]
115    fn time(&self) -> Time {
116        self.cs.time()
117    }
118
119    #[inline]
120    fn time_tick(&mut self) {
121        self.cs.wait(1).expect("time error")
122    }
123
124    fn labels(&self) -> impl Iterator<Item = bool> {
125        self.predicates.iter().map(|prop| {
126            if let Val::Boolean(b) = prop.eval(
127                &|port| match port {
128                    Atom::State(channel, idx) => self.ports[u16::from(*channel) as usize][*idx]
129                        .expect("port must exist and be initialized"),
130                    Atom::Event(event) => {
131                        Val::Boolean(self.last_event.as_ref().is_some_and(|e| e == event))
132                    }
133                },
134                &mut DummyRng,
135            ) {
136                b
137            } else {
138                // FIXME: handle error or guarantee it won't happen
139                panic!("propositions should evaluate to boolean values")
140            }
141        })
142    }
143
144    #[inline]
145    fn state(&self) -> impl Iterator<Item = Val> {
146        self.ports.iter().flat_map(|p| p.iter().filter_map(|p| *p))
147    }
148}
scan_core/cs_model.rs

scan_core/
cs_model.rs
