scan_core/
transition_system.rs

1use std::sync::Arc;
2use std::sync::atomic::{AtomicBool, Ordering};
3
4use bumpalo::Bump;
5use bumpalo::collections::CollectIn;
6use log::trace;
7use rand::rngs::SmallRng;
8use rand::seq::IteratorRandom;
9use rand::{RngExt, SeedableRng, make_rng};
10use thiserror::Error;
11
12use crate::channel_system::{
13    Action, Channel, ChannelSystem, ChannelSystemRun, CsError, Event, EventType, Location, PgId,
14};
15use crate::{BooleanExpr, Oracle, RunOutcome, Time, Tracer, Val};
16
17/// Errors produced by a [`TransitionSystem`].
18#[derive(Debug, Clone, Copy, Error)]
19pub enum TsError {
20    /// The CS returned an error of its own.
21    #[error("error from channel system {0:?}")]
22    ChannelSystem(CsError),
23    /// The default value set for the port is not the right type,
24    /// i.e., the type of messages of the channel.
25    #[error("default port value is not the type of the channel {0:?}")]
26    WrongPortType(Channel),
27}
28
29impl From<CsError> for TsError {
30    fn from(value: CsError) -> Self {
31        Self::ChannelSystem(value)
32    }
33}
34
35/// An atomic variable exposed by the [`ChannelSystem to the TransitionSystem`].
36#[derive(Debug, Clone, Copy)]
37pub enum Atom {
38    /// A predicate.
39    State(Channel, usize),
40    /// A send event.
41    Event(Channel),
42}
43
44/// A definition type that instances new [`CsModelRun`].
45#[derive(Debug, Clone)]
46pub struct TransitionSystem {
47    cs: ChannelSystem,
48    // ports are supposed to be ordered by channel
49    ports: Vec<Channel>,
50    vals: Vec<Vec<Val>>,
51    predicates: Vec<BooleanExpr<Atom>>,
52}
53
54impl TransitionSystem {
55    /// Creates a new [`CsModel`] from a [`ChannelSystemBuilder`].
56    pub fn new(cs: ChannelSystem) -> Self {
57        Self {
58            ports: Vec::new(),
59            vals: Vec::new(),
60            cs,
61            predicates: Vec::new(),
62        }
63    }
64
65    /// Adds a new port to the [`CsModel`],
66    /// which is given by an [`Channel`] and a default [`Val`] value.
67    pub fn add_port(&mut self, channel: Channel, mut value: Vec<Val>) -> Result<(), TsError> {
68        let types = self.cs.channel(channel)?.0;
69        if types.len() != value.len() || types.iter().zip(&value).any(|(t, val)| val.r#type() != *t)
70        {
71            return Err(TsError::WrongPortType(channel));
72        }
73        // Keep ports list ordered
74        // Don't insert duplicated ports
75        if let Err(index) = self.ports.binary_search(&channel) {
76            self.ports.insert(index, channel);
77            value.shrink_to_fit();
78            self.vals.insert(index, value);
79        }
80        assert!(self.ports.is_sorted());
81        assert_eq!(self.ports.len(), self.vals.len());
82        Ok(())
83    }
84
85    /// Adds a new predicate to the [`CsModel`],
86    /// which is an expression over the CS's channels.
87    pub fn add_predicate(&mut self, predicate: BooleanExpr<Atom>) -> Result<(), TsError> {
88        // Make sure predicate type-checks
89        let _ = predicate.eval::<SmallRng>(
90            &|port| match port {
91                Atom::State(channel, idx) => {
92                    let index = self
93                        .ports
94                        .binary_search(&channel)
95                        .expect("port must have been initialized");
96                    self.vals[index][idx]
97                }
98                Atom::Event(..) => Val::Boolean(false),
99            },
100            None,
101        );
102        self.predicates.push(predicate);
103        Ok(())
104    }
105
106    /// Shrink ports storage to optimize space use.
107    /// To be called after having added all ports.
108    pub fn shrink(&mut self) {
109        self.ports.shrink_to_fit();
110        self.vals.shrink_to_fit();
111    }
112
113    /// Generates an executable run of the model.
114    pub fn new_run(&self) -> TransitionSystemRun<'_> {
115        let mut vals = self.vals.clone();
116        vals.shrink_to_fit();
117        let mut pg_list = Vec::from_iter(self.cs.program_graph_ids());
118        pg_list.shrink_to_fit();
119        TransitionSystemRun {
120            cs: self.cs.new_instance(),
121            ports: &self.ports,
122            vals,
123            predicates: &self.predicates,
124            last_event: None,
125            pg_list,
126            rng: make_rng(),
127            bump: Bump::new(),
128        }
129    }
130}
131
132/// Transition system model based on a [`ChannelSystem`].
133///
134/// It is essentially a CS which keeps track of the [`Event`]s produced by the execution
135/// and determining a set of predicates.
136#[derive(Debug)]
137pub struct TransitionSystemRun<'def> {
138    cs: ChannelSystemRun<'def>,
139    ports: &'def [Channel],
140    vals: Vec<Vec<Val>>,
141    predicates: &'def [BooleanExpr<Atom>],
142    last_event: Option<(Action, Event)>,
143    pg_list: Vec<PgId>,
144    rng: SmallRng,
145    bump: Bump,
146}
147
148impl<'def> Clone for TransitionSystemRun<'def> {
149    fn clone(&self) -> Self {
150        Self {
151            cs: self.cs.clone(),
152            ports: self.ports,
153            vals: self.vals.clone(),
154            predicates: self.predicates,
155            last_event: self.last_event.clone(),
156            pg_list: self.pg_list.clone(),
157            rng: self.rng.clone(),
158            bump: Bump::new(),
159        }
160    }
161}
162
163impl<'def> TransitionSystemRun<'def> {
164    /// Perform a random transition.
165    ///
166    /// Used to generate Montecarlo-like executions
167    pub fn transition(&mut self) {
168        self.last_event = self.montecarlo_transition();
169        if let Some((_, ref event)) = self.last_event
170            && let EventType::Send(ref vals) = event.event_type
171            && let Ok(index) = self.ports.binary_search(&event.channel)
172        {
173            // Since we have to update old values,
174            // the vectors are already allocated and their is always the same.
175            // Copying from slice should be faster than cloning.
176            self.vals[index].copy_from_slice(vals);
177        }
178    }
179
180    /// Returns last event processed by model.
181    #[inline]
182    pub fn last_event(&self) -> Option<&(Action, Event)> {
183        self.last_event.as_ref()
184    }
185
186    #[inline]
187    fn time(&self) -> Time {
188        self.cs.time()
189    }
190
191    #[inline]
192    fn time_tick(&mut self) {
193        self.cs.wait(1).expect("time error")
194    }
195
196    fn labels(&self) -> impl Iterator<Item = bool> {
197        self.predicates.iter().map(|prop| {
198            prop.eval::<SmallRng>(
199                &|port| match port {
200                    Atom::State(channel, idx) => {
201                        let port_idx = self
202                            .ports
203                            .binary_search(&channel)
204                            .expect("port must exist and be initialized");
205                        self.vals[port_idx][idx]
206                    }
207                    Atom::Event(channel) => {
208                        Val::Boolean(self.last_event.as_ref().is_some_and(|(_, e)| {
209                            e.channel == channel && matches!(e.event_type, EventType::Send(..))
210                        }))
211                    }
212                },
213                None,
214            )
215        })
216    }
217
218    #[inline]
219    fn state(&self) -> &[Vec<Val>] {
220        &self.vals
221    }
222
223    /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`] and returns a [`RunOutcome`].
224    pub(crate) fn experiment<O: Oracle>(
225        &mut self,
226        mut oracle: O,
227        running: Arc<AtomicBool>,
228    ) -> RunOutcome {
229        // reuse vector to avoid allocations
230        let mut labels = Vec::from_iter(self.labels());
231        // Initialize oracle with TS initial state
232        oracle.update_state(&labels);
233        while oracle.output_guarantees().any(|b| b.is_none()) {
234            self.transition();
235            if !running.load(Ordering::Relaxed) {
236                trace!("run stopped");
237                return None;
238            } else if self.last_event().is_some() {
239                labels.clear();
240                labels.extend(self.labels());
241                oracle.update_state(&labels);
242            } else if self.cs.is_waiting() {
243                self.time_tick();
244                oracle.update_time(self.time());
245            } else {
246                break;
247            }
248        }
249        trace!("run complete");
250        let verified = Vec::from_iter(oracle.final_output_guarantees());
251        Some(verified)
252    }
253
254    /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`]
255    /// and process the execution trace via the given [`Tracer`].
256    pub(crate) fn trace<T, O: Oracle>(
257        &mut self,
258        mut oracle: O,
259        mut tracer: T,
260        model_data: &T::ModelData,
261    ) -> RunOutcome
262    where
263        T: Tracer,
264    {
265        trace!("new run starting");
266        // reuse vector to avoid allocations
267        let mut labels = Vec::from_iter(self.labels());
268        // Initialize oracle with TS initial state
269        oracle.update_state(&labels);
270        // WARN FIXME TODO: Initial state is not written as there is no corresponding action/event
271        // Same issue for time-tick events
272        while oracle.output_guarantees().any(|b| b.is_none()) {
273            self.transition();
274            if let Some((action, event)) = self.last_event() {
275                tracer.trace(model_data, *action, event, self.time(), self.state());
276                labels.clear();
277                labels.extend(self.labels());
278                oracle.update_state(&labels);
279            } else if self.cs.is_waiting() {
280                self.time_tick();
281                oracle.update_time(self.time());
282            } else {
283                break;
284            }
285        }
286        trace!("run complete");
287        let verified = Vec::from_iter(oracle.final_output_guarantees());
288        Some(verified)
289    }
290
291    fn montecarlo_transition(&mut self) -> Option<(Action, Event)> {
292        let mut rand1 = SmallRng::from_rng(&mut self.rng);
293        // Setting pgs_left as length resets the queue
294        let mut pgs_left = self.pg_list.len();
295        while pgs_left > 0 {
296            // Select random pg within 0..pgs_left
297            let pg_select = self.rng.random_range(0..pgs_left);
298            let pg_id = self.pg_list[pg_select];
299            // Swap selected pg with last element of the queue (possibly itself, probably not worth checking)
300            // Decrease the length of the queue (so that selected element is removed)
301            pgs_left -= 1;
302            self.pg_list.swap(pg_select, pgs_left);
303            // Execute randomly chosen transitions on the picked PG until an event is generated,
304            // or no more transition is possible
305            // NOTE: Special treatment for PGs with single-location state for optimization of this common case.
306            // Hopefully it will be possible to treat all cases in a general way eventually.
307            if self
308                .cs
309                .program_graph(pg_id)
310                .expect("pg exists")
311                .current_states()
312                .len()
313                == 1
314            {
315                while let Some((action, post_state)) = self
316                    .cs
317                    .nosync_possible_transitions_pg(pg_id)
318                    .expect("pg exists")
319                    .filter_map(|(action, post_states)| {
320                        post_states.choose(&mut rand1).map(|loc| (action, loc))
321                    })
322                    .choose(&mut self.rng)
323                {
324                    let event = self
325                        .cs
326                        .transition(pg_id, action, &[post_state])
327                        .expect("successful transition");
328                    if event.is_some() {
329                        return event.map(|ev| (action, ev));
330                    }
331                }
332            } else {
333                use bumpalo::collections::Vec as BumpVec;
334
335                self.bump.reset();
336                while let Some((action, post_states)) = self
337                    .cs
338                    .possible_transitions_pg(pg_id)
339                    .expect("pg exists")
340                    .filter_map(|(action, post_states)| {
341                        post_states
342                            .map(|locs| locs.choose(&mut rand1))
343                            .collect_in::<Option<BumpVec<Location>>>(&self.bump)
344                            // .collect::<Option<Vec<Location>>>()
345                            .map(|locs| (action, locs))
346                    })
347                    .choose(&mut self.rng)
348                {
349                    let event = self
350                        .cs
351                        .transition(pg_id, action, post_states.as_slice())
352                        .expect("successful transition");
353                    if event.is_some() {
354                        return event.map(|ev| (action, ev));
355                    }
356                }
357            }
358        }
359        None
360    }
361}
scan_core/transition_system.rs

scan_core/
transition_system.rs
