Skip to content

Commit bfc7c63

Browse files
Merge pull request #26 from convince-project/y2review
Y2review
2 parents 35f7d7b + 6013946 commit bfc7c63

File tree

9 files changed

+258
-267
lines changed

9 files changed

+258
-267
lines changed

Diff for: scan_core/src/channel_system.rs

+41-14
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,8 @@ mod builder;
9696
// use ahash::AHashMap as HashMap;
9797
pub use builder::*;
9898
use hashbrown::HashMap;
99+
use rand::seq::SliceRandom;
100+
use rand::Rng;
99101

100102
use crate::program_graph::{
101103
Action as PgAction, Clock as PgClock, Location as PgLocation, Var as PgVar, *,
@@ -295,24 +297,49 @@ impl ChannelSystem {
295297
})
296298
}
297299

298-
pub(crate) fn resolve_deterministic_transitions(&mut self) {
299-
for (pg_id, pg) in self.program_graphs.iter_mut().enumerate() {
300-
let pg_id = PgId(pg_id);
301-
loop {
302-
// `take(2)` because we need no more to establish the transition is non-deterministic
303-
let trans: Vec<_> = pg.possible_transitions().take(2).collect();
304-
if trans.len() == 1 {
305-
let (action, post) = trans[0];
306-
if self.communications.contains_key(&Action(pg_id, action)) {
307-
break;
308-
} else {
309-
pg.transition(action, post).expect("transition is possible");
300+
pub(crate) fn monaco_execution<R: Rng>(
301+
&mut self,
302+
rng: &mut R,
303+
duration: Time,
304+
) -> Option<Event> {
305+
let pg_list = Vec::from_iter((0..self.program_graphs.len()).map(PgId));
306+
let mut shuffle = pg_list.to_owned();
307+
while self.time <= duration {
308+
while self.possible_transitions().any(|_| true) {
309+
shuffle.shuffle(rng);
310+
for &pg_id in &shuffle {
311+
let mut possible_transitions = self.program_graphs[pg_id.0]
312+
.possible_transitions()
313+
.collect::<Vec<_>>();
314+
possible_transitions.shuffle(rng);
315+
while let Some((action, post)) = possible_transitions.pop() {
316+
let cs_action = Action(pg_id, action);
317+
if self.communications.contains_key(&cs_action) {
318+
if self.check_communication(pg_id, cs_action).is_ok() {
319+
let cs_post = Location(pg_id, post);
320+
let event = self
321+
.transition(pg_id, cs_action, cs_post)
322+
.expect("successful transition");
323+
assert!(event.is_some(), "must be a communication event");
324+
return event;
325+
} else {
326+
continue;
327+
}
328+
} else {
329+
self.program_graphs[pg_id.0]
330+
.transition(action, post)
331+
.expect("success");
332+
possible_transitions = self.program_graphs[pg_id.0]
333+
.possible_transitions()
334+
.collect::<Vec<_>>();
335+
possible_transitions.shuffle(rng);
336+
}
310337
}
311-
} else {
312-
break;
313338
}
314339
}
340+
self.wait(1).ok()?;
315341
}
342+
None
316343
}
317344

318345
fn check_communication(&self, pg_id: PgId, action: Action) -> Result<(), CsError> {

Diff for: scan_core/src/model.rs

+21-39
Original file line numberDiff line numberDiff line change
@@ -24,21 +24,19 @@ impl CsModelBuilder {
2424
}
2525
}
2626

27-
pub fn add_port(&mut self, channel: Channel, default: Val) -> Result<(), ()> {
27+
pub fn add_port(&mut self, channel: Channel, default: Val) {
2828
if let std::collections::hash_map::Entry::Vacant(e) = self.vals.entry(channel) {
2929
e.insert(default);
30-
Ok(())
3130
} else {
32-
Err(())
31+
panic!("entry is already taken");
3332
}
3433
}
3534

36-
pub fn add_predicate(&mut self, predicate: Expression<Channel>) -> Result<usize, ()> {
35+
pub fn add_predicate(&mut self, predicate: Expression<Channel>) -> usize {
3736
let predicate = FnExpression::<Channel>::from(predicate);
3837
let _ = predicate.eval(&|port| self.vals.get(&port).unwrap().clone());
39-
// let _ = predicate.eval(&|port| self.vals.get(&port).cloned());
4038
self.predicates.push(predicate);
41-
Ok(self.predicates.len() - 1)
39+
self.predicates.len() - 1
4240
}
4341

4442
/// Creates a new [`CsModel`] with the given underlying [`ChannelSystem`] and set of predicates.
@@ -69,6 +67,7 @@ pub struct CsModel {
6967

7068
impl CsModel {
7169
/// Gets the underlying [`ChannelSystem`].
70+
#[inline(always)]
7271
pub fn channel_system(&self) -> &ChannelSystem {
7372
&self.cs
7473
}
@@ -81,10 +80,7 @@ impl TransitionSystem for CsModel {
8180
self.predicates
8281
.iter()
8382
.map(|prop| {
84-
if let Val::Boolean(b) = prop.eval(&|port| self.vals.get(&port).unwrap().clone())
85-
// .eval(&|port| self.vals.get(&port).cloned())
86-
// .expect("boolean value")
87-
{
83+
if let Val::Boolean(b) = prop.eval(&|port| self.vals.get(&port).unwrap().clone()) {
8884
Some(b)
8985
} else {
9086
None
@@ -95,36 +91,22 @@ impl TransitionSystem for CsModel {
9591
.unwrap()
9692
}
9793

98-
fn transitions(mut self) -> Vec<(Event, CsModel)> {
99-
// IntoIterator::into_iter(self.clone().list_transitions())
100-
// Perform all transitions that are deterministic and do not interact with channels.
101-
// The order in which these are performed does not matter.
102-
self.cs.resolve_deterministic_transitions();
103-
if self.cs.possible_transitions().next().is_none() {
104-
self.cs.wait(1).ok();
105-
}
106-
self.cs
107-
.possible_transitions()
108-
.flat_map(|(pg_id, action, post)| {
109-
let mut model = self.clone();
110-
let event = model
111-
.cs
112-
.transition(pg_id, action, post)
113-
.expect("transition is possible");
114-
model.last_event = event.clone();
115-
if let Some(event) = event {
116-
if let EventType::Send(ref val) = event.event_type {
117-
model.vals.insert(event.channel, val.to_owned());
118-
}
119-
vec![(event, model)]
120-
} else {
121-
model.transitions()
122-
}
123-
})
124-
.collect::<Vec<_>>()
125-
}
126-
94+
#[inline(always)]
12795
fn time(&self) -> Time {
12896
self.cs.time()
12997
}
98+
99+
fn monaco_transition<R: rand::Rng>(
100+
&mut self,
101+
rng: &mut R,
102+
duration: Time,
103+
) -> Option<Self::Action> {
104+
self.last_event = self.cs.monaco_execution(rng, duration);
105+
if let Some(event) = self.last_event.as_ref() {
106+
if let EventType::Send(ref val) = event.event_type {
107+
self.vals.insert(event.channel, val.to_owned());
108+
}
109+
}
110+
self.last_event.to_owned()
111+
}
130112
}

0 commit comments

Comments
 (0)