scan_core/
transition_system.rs

1use crate::{Oracle, RunOutcome, Time, Val};
2use log::trace;
3use std::sync::{
4    Arc,
5    atomic::{AtomicBool, Ordering},
6};
7
8/// Trait that handles streaming of traces,
9/// e.g., to print them to file.
10pub trait Tracer<A> {
11    /// Initialize new streaming.
12    ///
13    /// This method needs to be called once, before calls to [`Self::trace`].
14    fn init(&mut self);
15
16    /// Stream a new state of the trace.
17    fn trace<I: IntoIterator<Item = Val>>(&mut self, action: &A, time: Time, ports: I);
18
19    /// Finalize and close streaming.
20    ///
21    /// This method needs to be called at the end of the execution.
22    fn finalize(self, outcome: &RunOutcome);
23}
24
25// Dummy Tracer that does nothing
26impl<A> Tracer<A> for () {
27    fn init(&mut self) {}
28
29    fn trace<I: IntoIterator<Item = Val>>(&mut self, _action: &A, _time: Time, _ports: I) {}
30
31    fn finalize(self, _outcome: &RunOutcome) {}
32}
33
34/// A type that can generate instances of a [`TransitionSystem`].
35pub trait TransitionSystemGenerator {
36    /// The type of [`TransitionSystem`] to be generated.
37    type Ts<'a>: TransitionSystem
38    where
39        Self: 'a;
40
41    /// Generate a new instance of the [`TransitionSystem`].
42    fn generate<'a>(&'a self) -> Self::Ts<'a>;
43}
44
45/// Trait for types that can execute like a transition system.
46///
47/// Together with an [`Oracle`], it provides a verifiable system.
48pub trait TransitionSystem {
49    /// The type of events produced by the execution of the system.
50    type Event;
51
52    /// Performs a (random) transition on the [`TransitionSystem`] and returns the raised `Event`,
53    /// unless the execution is terminated and no further events can happen.
54    fn transition(&mut self) -> Option<Self::Event>;
55
56    /// Current time of the [`TransitionSystem`] (for timed systems).
57    fn time(&self) -> Time;
58
59    /// Increase current time of the [`TransitionSystem`] (for timed systems).
60    fn time_tick(&mut self);
61
62    /// The current values of the [`TransitionSystem`]'s labels.
63    fn labels(&self) -> impl Iterator<Item = bool>;
64
65    /// The current internal state of the [`TransitionSystem`].
66    fn state(&self) -> impl Iterator<Item = Val>;
67
68    /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`] and returns a [`RunOutcome`].
69    fn experiment<O: Oracle>(
70        &mut self,
71        duration: Time,
72        mut oracle: O,
73        running: Arc<AtomicBool>,
74    ) -> RunOutcome {
75        trace!("new run starting");
76        let mut time;
77        // reuse vector to avoid allocations
78        let mut labels = Vec::new();
79        while self.time() <= duration {
80            if let Some(_event) = self.transition() {
81                labels.clear();
82                labels.extend(self.labels());
83                oracle.update_state(&labels);
84            } else {
85                self.time_tick();
86                time = self.time();
87                oracle.update_time(time);
88            }
89            if !running.load(Ordering::Relaxed) {
90                trace!("run stopped");
91                return RunOutcome::Incomplete;
92            } else if oracle.output_guarantees().all(|b| b.is_some()) {
93                trace!("run complete early");
94                let verified = Vec::from_iter(oracle.output_guarantees().map(Option::unwrap));
95                return RunOutcome::Verified(verified);
96            }
97        }
98        trace!("run complete");
99        let verified = Vec::from_iter(oracle.final_output_guarantees());
100        RunOutcome::Verified(verified)
101    }
102
103    /// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`]
104    /// and process the execution trace via the given [`Tracer`].
105    fn trace<T, O: Oracle>(&mut self, duration: Time, mut oracle: O, mut tracer: T)
106    where
107        T: Tracer<Self::Event>,
108    {
109        // let mut current_len = 0;
110        trace!("new run starting");
111        let mut time;
112        // reuse vector to avoid allocations
113        let mut labels = Vec::new();
114        tracer.init();
115        while self.time() <= duration {
116            if let Some(event) = self.transition() {
117                labels.clear();
118                labels.extend(self.labels());
119                time = self.time();
120                tracer.trace(&event, time, self.state());
121                oracle.update_state(&labels);
122            } else {
123                self.time_tick();
124                time = self.time();
125                oracle.update_time(time);
126            }
127        }
128        trace!("run complete");
129        let verified = Vec::from_iter(oracle.final_output_guarantees());
130        tracer.finalize(&RunOutcome::Verified(verified));
131    }
132}
scan_core/transition_system.rs

scan_core/
transition_system.rs
