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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
use crate::{Oracle, RunOutcome, Time, Val};
use log::trace;
use std::sync::{
Arc,
atomic::{AtomicBool, Ordering},
};
/// Trait that handles streaming of traces,
/// e.g., to print them to file.
pub trait Tracer<A> {
/// Initialize new streaming.
///
/// This method needs to be called once, before calls to [`Self::trace`].
fn init(&mut self);
/// Stream a new state of the trace.
fn trace<I: IntoIterator<Item = Val>>(&mut self, action: &A, time: Time, ports: I);
/// Finalize and close streaming.
///
/// This method needs to be called at the end of the execution.
fn finalize(self, outcome: &RunOutcome);
}
// Dummy Tracer that does nothing
impl<A> Tracer<A> for () {
fn init(&mut self) {}
fn trace<I: IntoIterator<Item = Val>>(&mut self, _action: &A, _time: Time, _ports: I) {}
fn finalize(self, _outcome: &RunOutcome) {}
}
/// A type that can generate instances of a [`TransitionSystem`].
pub trait TransitionSystemGenerator {
/// The type of [`TransitionSystem`] to be generated.
type Ts<'a>: TransitionSystem
where
Self: 'a;
/// Generate a new instance of the [`TransitionSystem`].
fn generate<'a>(&'a self) -> Self::Ts<'a>;
}
/// Trait for types that can execute like a transition system.
///
/// Together with an [`Oracle`], it provides a verifiable system.
pub trait TransitionSystem {
/// The type of events produced by the execution of the system.
type Event;
/// Performs a (random) transition on the [`TransitionSystem`] and returns the raised `Event`,
/// unless the execution is terminated and no further events can happen.
fn transition(&mut self) -> Option<Self::Event>;
/// Current time of the [`TransitionSystem`] (for timed systems).
fn time(&self) -> Time;
/// Increase current time of the [`TransitionSystem`] (for timed systems).
fn time_tick(&mut self);
/// The current values of the [`TransitionSystem`]'s labels.
fn labels(&self) -> impl Iterator<Item = bool>;
/// The current internal state of the [`TransitionSystem`].
fn state(&self) -> impl Iterator<Item = Val>;
/// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`] and returns a [`RunOutcome`].
fn experiment<O: Oracle>(
&mut self,
duration: Time,
mut oracle: O,
running: Arc<AtomicBool>,
) -> RunOutcome {
trace!("new run starting");
let mut time;
// reuse vector to avoid allocations
let mut labels = Vec::new();
while self.time() <= duration {
if let Some(_event) = self.transition() {
labels.clear();
labels.extend(self.labels());
oracle.update_state(&labels);
} else {
self.time_tick();
time = self.time();
oracle.update_time(time);
}
if !running.load(Ordering::Relaxed) {
trace!("run stopped");
return RunOutcome::Incomplete;
} else if oracle.output_guarantees().all(|b| b.is_some()) {
trace!("run complete early");
let verified = Vec::from_iter(oracle.output_guarantees().map(Option::unwrap));
return RunOutcome::Verified(verified);
}
}
trace!("run complete");
let verified = Vec::from_iter(oracle.final_output_guarantees());
RunOutcome::Verified(verified)
}
/// Runs a single execution of the [`TransitionSystem`] with a given [`Oracle`]
/// and process the execution trace via the given [`Tracer`].
fn trace<T, O: Oracle>(&mut self, duration: Time, mut oracle: O, mut tracer: T)
where
T: Tracer<Self::Event>,
{
// let mut current_len = 0;
trace!("new run starting");
let mut time;
// reuse vector to avoid allocations
let mut labels = Vec::new();
tracer.init();
while self.time() <= duration {
if let Some(event) = self.transition() {
labels.clear();
labels.extend(self.labels());
time = self.time();
tracer.trace(&event, time, self.state());
oracle.update_state(&labels);
} else {
self.time_tick();
time = self.time();
oracle.update_time(time);
}
}
trace!("run complete");
let verified = Vec::from_iter(oracle.final_output_guarantees());
tracer.finalize(&RunOutcome::Verified(verified));
}
}