scan_core/channel_system.rs
1//! Implementation of the CS model of computation.
2//!
3//! Channel systems comprises multiple program graphs executing asynchronously
4//! while sending and retrieving messages from channels.
5//!
6//! A channel system is given by:
7//!
8//! - A finite set of PGs.
9//! - A finite set of channels, each of which has:
10//! - a given type;
11//! - a FIFO queue that can contain values of the channel's type;
12//! - a queue capacity limit: from zero (handshake communication) to infinite.
13//! - Some PG actions are communication actions:
14//! - `send` actions push the computed value of an expression to the rear of the channel queue;
15//! - `receive` actions pop the value in front of the channel queue and write it onto a given PG variable;
16//! - `probe_empty_queue` actions can only be executed if the given channel has an empty queue;
17//! - `probe_full_queue` actions can only be executed if the given channel has a full queue;
18//!
19//! Analogously to PGs, a CS is defined through a [`ChannelSystemBuilder`],
20//! by adding new PGs and channels.
21//! Each PG in the CS can be given new locations, actions, effects, guards and transitions.
22//! Then, a [`ChannelSystem`] is built from the [`ChannelSystemBuilder`]
23//! and can be executed by performing transitions,
24//! though the definition of the CS itself can no longer be altered.
25//!
26//! ```
27//! # use scan_core::*;
28//! # use scan_core::channel_system::*;
29//! // Create a new CS builder
30//! let mut cs_builder = ChannelSystemBuilder::new();
31//!
32//! // Add a new PG to the CS
33//! let pg_1 = cs_builder.new_program_graph();
34//!
35//! // Get initial location of pg_1
36//! let initial_1 = cs_builder
37//! .new_initial_location(pg_1)
38//! .expect("every PG has an initial location");
39//!
40//! // Create new channel
41//! let chn = cs_builder.new_channel(vec![Type::Integer], Some(1));
42//!
43//! // Create new send communication action
44//! let send = cs_builder
45//! .new_send(pg_1, chn, vec![CsExpression::from(1i64)])
46//! .expect("always possible to add new actions");
47//!
48//! // Add transition sending a message to the channel
49//! cs_builder.add_transition(pg_1, initial_1, send, initial_1, None)
50//! .expect("transition is well-defined");
51//!
52//! // Add a new PG to the CS
53//! let pg_2 = cs_builder.new_program_graph();
54//!
55//! // Get initial location of pg_2
56//! let initial_2 = cs_builder
57//! .new_initial_location(pg_2)
58//! .expect("every PG has an initial location");
59//!
60//! // Add new variable to pg_2
61//! let var = cs_builder
62//! .new_var(pg_2, Val::from(0i64))
63//! .expect("always possible to add new variable");
64//!
65//! // Create new receive communication action
66//! let receive = cs_builder
67//! .new_receive(pg_2, chn, vec![var])
68//! .expect("always possible to add new actions");
69//!
70//! // Add transition sending a message to the channel
71//! cs_builder.add_transition(pg_2, initial_2, receive, initial_2, None)
72//! .expect("transition is well-defined");
73//!
74//! // Build the CS from its builder
75//! // The builder is always guaranteed to build a well-defined CS and building cannot fail
76//! let cs = cs_builder.build();
77//! let mut instance = cs.new_instance();
78//!
79//! // Since the channel is empty, only pg_1 can transition (with send)
80//! {
81//! let mut iter = instance.possible_transitions();
82//! let (pg, action, mut trans) = iter.next().unwrap();
83//! assert_eq!(pg, pg_1);
84//! assert_eq!(action, send);
85//! let post_locs: Vec<Location> = trans.next().unwrap().collect();
86//! assert_eq!(post_locs, vec![initial_1]);
87//! assert!(iter.next().is_none());
88//! }
89//!
90//! // Perform the transition, which sends a value to the channel queue
91//! // After this, the channel is full
92//! instance.transition(pg_1, send, &[initial_1])
93//! .expect("transition is possible");
94//!
95//! // Since the channel is now full, only pg_2 can transition (with receive)
96//! {
97//! let mut iter = instance.possible_transitions();
98//! let (pg, action, mut trans) = iter.next().unwrap();
99//! assert_eq!(pg, pg_2);
100//! assert_eq!(action, receive);
101//! let post_locs: Vec<Location> = trans.next().unwrap().collect();
102//! assert_eq!(post_locs, vec![initial_2]);
103//! assert!(iter.next().is_none());
104//! }
105//!
106//! // Perform the transition, which receives a value to the channel queue
107//! // After this, the channel is empty
108//! instance.transition(pg_2, receive, &[initial_2])
109//! .expect("transition is possible");
110//! ```
111
112mod builder;
113
114use crate::program_graph::{
115 Action as PgAction, Clock as PgClock, Location as PgLocation, Var as PgVar, *,
116};
117use crate::{Time, grammar::*};
118pub use builder::*;
119use rand::rngs::SmallRng;
120use rand::seq::IteratorRandom;
121use rand::{RngExt, SeedableRng};
122use smallvec::SmallVec;
123use std::collections::VecDeque;
124use thiserror::Error;
125
126/// An indexing object for PGs in a CS.
127///
128/// These cannot be directly created or manipulated,
129/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
130#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
131pub struct PgId(u16);
132
133impl From<PgId> for u16 {
134 #[inline]
135 fn from(val: PgId) -> Self {
136 val.0
137 }
138}
139
140/// An indexing object for channels in a CS.
141///
142/// These cannot be directly created or manipulated,
143/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
144#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
145pub struct Channel(u16);
146
147impl From<Channel> for u16 {
148 #[inline]
149 fn from(val: Channel) -> Self {
150 val.0
151 }
152}
153
154/// An indexing object for locations in a CS.
155///
156/// These cannot be directly created or manipulated,
157/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
158#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
159pub struct Location(PgId, PgLocation);
160
161/// An indexing object for actions in a CS.
162///
163/// These cannot be directly created or manipulated,
164/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
165#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
166pub struct Action(PgId, PgAction);
167
168/// An indexing object for typed variables in a CS.
169///
170/// These cannot be directly created or manipulated,
171/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
172#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
173pub struct Var(PgId, PgVar);
174
175/// An indexing object for clocks in a CS.
176///
177/// These cannot be directly created or manipulated,
178/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
179///
180/// See also [`PgClock`].
181#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
182pub struct Clock(PgId, PgClock);
183
184type TimeConstraint = (Clock, Option<Time>, Option<Time>);
185
186/// A message to be sent through a CS's channel.
187#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
188pub enum Message {
189 /// Sending the computed value of an expression to a channel.
190 Send,
191 /// Retrieving a value out of a channel and associating it to a variable.
192 Receive,
193 /// Checking whether a channel is empty.
194 ProbeEmptyQueue,
195 /// Checking whether a channel is full.
196 ProbeFullQueue,
197}
198
199/// The error type for operations with [`ChannelSystemBuilder`]s and [`ChannelSystem`]s.
200#[derive(Debug, Clone, Copy, Error)]
201pub enum CsError {
202 /// A PG within the CS returned an error of its own.
203 #[error("error from program graph {0:?}")]
204 ProgramGraph(PgId, #[source] PgError),
205 /// There is no such PG in the CS.
206 #[error("program graph {0:?} does not belong to the channel system")]
207 MissingPg(PgId),
208 /// The channel is at full capacity and can accept no more incoming messages.
209 #[error("channel {0:?} is at full capacity")]
210 OutOfCapacity(Channel),
211 /// Channel is not full
212 #[error("the channel still has free space {0:?}")]
213 NotFull(Channel),
214 /// The channel is empty and there is no message to be retrieved.
215 #[error("channel {0:?} is empty")]
216 Empty(Channel),
217 /// The channel is not empty.
218 #[error("channel {0:?} is not empty")]
219 NotEmpty(Channel),
220 /// There is no such communication action in the CS.
221 #[error("communication {0:?} has not been defined")]
222 NoCommunication(Action),
223 /// The action does not belong to the PG.
224 #[error("action {0:?} does not belong to program graph {1:?}")]
225 ActionNotInPg(Action, PgId),
226 /// The variable does not belong to the PG.
227 #[error("variable {0:?} does not belong to program graph {1:?}")]
228 VarNotInPg(Var, PgId),
229 /// The location does not belong to the PG.
230 #[error("location {0:?} does not belong to program graph {1:?}")]
231 LocationNotInPg(Location, PgId),
232 /// The clock does not belong to the PG.
233 #[error("clock {0:?} does not belong to program graph {1:?}")]
234 ClockNotInPg(Clock, PgId),
235 /// The given PGs do not match.
236 #[error("program graphs {0:?} and {1:?} do not match")]
237 DifferentPgs(PgId, PgId),
238 /// Action is a communication.
239 ///
240 /// Is returned when trying to associate an effect to a communication action.
241 #[error("action {0:?} is a communication")]
242 ActionIsCommunication(Action),
243 /// There is no such channel in the CS.
244 #[error("channel {0:?} does not exists")]
245 MissingChannel(Channel),
246 /// Cannot probe an handshake channel
247 #[error("cannot probe handshake {0:?}")]
248 ProbingHandshakeChannel(Channel),
249 /// Cannot probe for fullness an infinite capacity channel
250 #[error("cannot probe for fullness the infinite capacity {0:?}")]
251 ProbingInfiniteQueue(Channel),
252 /// A type error
253 #[error("type error")]
254 Type(#[source] TypeError),
255}
256
257/// A Channel System event related to a channel.
258#[derive(Debug, Clone, PartialEq)]
259pub struct Event {
260 /// The PG producing the event in the course of a transition.
261 pub pg_id: PgId,
262 /// The channel involved in the event.
263 pub channel: Channel,
264 /// The type of event produced.
265 pub event_type: EventType,
266}
267
268/// A Channel System event type related to a channel.
269#[derive(Debug, Clone, PartialEq)]
270pub enum EventType {
271 /// Sending a value to a channel.
272 Send(SmallVec<[Val; 2]>),
273 /// Retrieving a value out of a channel.
274 Receive(SmallVec<[Val; 2]>),
275 /// Checking whether a channel is empty.
276 ProbeEmptyQueue,
277 /// Checking whether a channel is full.
278 ProbeFullQueue,
279}
280
281/// A definition object for a CS.
282/// It represents the abstract definition of a CS.
283///
284/// The only way to produce a [`ChannelSystem`] is through a [`ChannelSystemBuilder`].
285/// This guarantees that there are no type errors involved in the definition of its PGs,
286/// and thus the CS will always be in a consistent state.
287///
288/// The only way to execute the [`ChannelSystem`] is to generate a new [`ChannelSystemRun`] through [`ChannelSystem::new_instance`].
289/// The [`ChannelSystemRun`] cannot outlive its [`ChannelSystem`], as it holds references to it.
290/// This allows to cheaply generate multiple [`ChannelSystemRun`]s from the same [`ChannelSystem`].
291///
292/// Example:
293///
294/// ```
295/// # use scan_core::channel_system::ChannelSystemBuilder;
296/// // Create and populate a CS builder object
297/// let mut cs_builder = ChannelSystemBuilder::new();
298/// let pg_id = cs_builder.new_program_graph();
299/// let initial = cs_builder.new_initial_location(pg_id).expect("create new location");
300/// cs_builder.add_autonomous_transition(pg_id, initial, initial, None).expect("add transition");
301///
302/// // Build the builder object to get a CS definition object.
303/// let cs_def = cs_builder.build();
304///
305/// // Instantiate a CS with the previously built definition.
306/// let mut cs = cs_def.new_instance();
307///
308/// // Perform the (unique) active transition available.
309/// let (pg_id_trans, e, mut post_locs) = cs.possible_transitions().last().expect("autonomous transition");
310/// assert_eq!(pg_id_trans, pg_id);
311/// let post_loc = post_locs.last().expect("post location").last().expect("post location");
312/// assert_eq!(post_loc, initial);
313/// cs.transition(pg_id, e, &[initial]).expect("transition is active");
314/// ```
315#[derive(Debug, Clone)]
316pub struct ChannelSystem {
317 channels: Vec<(Vec<Type>, Option<usize>)>,
318 communications: Vec<Option<(Channel, Message)>>,
319 communications_pg_idxs: Vec<usize>,
320 program_graphs: Vec<ProgramGraph>,
321}
322
323impl ChannelSystem {
324 /// Creates a new [`ChannelSystemRun`] which allows to execute the CS as defined.
325 ///
326 /// The new instance borrows the caller to refer to the CS definition without copying its data,
327 /// so that spawning instances is (relatively) inexpensive.
328 ///
329 /// See also [`ProgramGraph::new_instance`].
330 pub fn new_instance<'def>(&'def self) -> ChannelSystemRun<'def> {
331 ChannelSystemRun {
332 rng: rand::make_rng(),
333 time: 0,
334 program_graphs: Vec::from_iter(
335 self.program_graphs.iter().map(|pgdef| pgdef.new_instance()),
336 ),
337 message_queue: Vec::from_iter(self.channels.iter().map(|(types, cap)| {
338 cap.map_or_else(VecDeque::new, |cap| {
339 VecDeque::with_capacity(types.len() * cap)
340 })
341 })),
342 def: self,
343 }
344 }
345
346 #[inline]
347 fn communication(&self, pg_id: PgId, pg_action: PgAction) -> Option<(Channel, Message)> {
348 if pg_action == EPSILON {
349 None
350 } else {
351 let start = self.communications_pg_idxs[pg_id.0 as usize];
352 self.communications[start + ActionIdx::from(pg_action) as usize]
353 }
354 }
355
356 /// Returns the list of defined channels, given as the pair of their type and capacity
357 /// (where `None` denotes channels with infinite capacity, and `Some` denotes channels with finite capacity).
358 #[inline]
359 pub fn channels(&self) -> &Vec<(Vec<Type>, Option<usize>)> {
360 &self.channels
361 }
362}
363
364/// Representation of a CS that can be executed transition-by-transition.
365///
366/// The structure of the CS cannot be changed,
367/// meaning that it is not possible to introduce new PGs or modifying them, or add new channels.
368/// Though, this restriction makes it so that cloning the [`ChannelSystem`] is cheap,
369/// because only the internal state needs to be duplicated.
370#[derive(Debug, Clone)]
371pub struct ChannelSystemRun<'def> {
372 rng: SmallRng,
373 time: Time,
374 message_queue: Vec<VecDeque<Val>>,
375 program_graphs: Vec<ProgramGraphRun<'def>>,
376 def: &'def ChannelSystem,
377}
378
379impl<'def> ChannelSystemRun<'def> {
380 /// Returns the current time of the CS.
381 #[inline]
382 pub fn time(&self) -> Time {
383 self.time
384 }
385
386 /// Iterates over all transitions that can be admitted in the current state.
387 ///
388 /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
389 /// (the pre-state being necessarily the current state of the machine).
390 /// The (eventual) guard is guaranteed to be satisfied.
391 ///
392 /// See also [`ProgramGraphRun::possible_transitions`].
393 pub fn possible_transitions(
394 &self,
395 ) -> impl Iterator<
396 Item = (
397 PgId,
398 Action,
399 impl Iterator<Item = impl Iterator<Item = Location> + '_> + '_,
400 ),
401 > + '_ {
402 self.program_graphs
403 .iter()
404 .enumerate()
405 .flat_map(move |(id, pg)| {
406 let pg_id = PgId(id as u16);
407 pg.possible_transitions().filter_map(move |(action, post)| {
408 let action = Action(pg_id, action);
409 self.check_communication(pg_id, action).ok().map(move |()| {
410 let post = post.map(move |locs| locs.map(move |loc| Location(pg_id, loc)));
411 (pg_id, action, post)
412 })
413 })
414 })
415 }
416
417 pub(crate) fn montecarlo_execution(&mut self) -> Option<Event> {
418 let pgs = self.program_graphs.len();
419 let mut pg_vec = Vec::from_iter((0..pgs as u16).map(PgId));
420 let mut rand1 = SmallRng::from_rng(&mut self.rng);
421 let mut rand2 = SmallRng::from_rng(&mut self.rng);
422 while !pg_vec.is_empty() {
423 let pg_id = pg_vec.swap_remove(self.rng.random_range(0..pg_vec.len()));
424 // Execute randomly chosen transitions on the picked PG until an event is generated,
425 // or no more transition is possible
426 if self.program_graphs[pg_id.0 as usize].current_states().len() == 1 {
427 while let Some((action, post_state)) = self.program_graphs[pg_id.0 as usize]
428 .nosync_possible_transitions()
429 .filter(|&(action, _)| {
430 self.def
431 .communication(pg_id, action)
432 .is_none_or(|(channel, message)| self.check_message(channel, message))
433 })
434 .filter_map(|(action, post_states)| {
435 post_states
436 .choose(&mut rand1)
437 .map(|loc| (action, Location(pg_id, loc)))
438 })
439 .choose(&mut rand2)
440 {
441 let event = self
442 .transition(pg_id, Action(pg_id, action), &[post_state])
443 .expect("successful transition");
444 if event.is_some() {
445 return event;
446 }
447 }
448 } else {
449 while let Some((action, post_states)) = self.program_graphs[pg_id.0 as usize]
450 .possible_transitions()
451 .filter(|&(action, _)| {
452 self.def
453 .communication(pg_id, action)
454 .is_none_or(|(channel, message)| self.check_message(channel, message))
455 })
456 .filter_map(|(action, post_states)| {
457 post_states
458 .map(|locs| locs.choose(&mut rand1).map(|loc| Location(pg_id, loc)))
459 .collect::<Option<SmallVec<[Location; 4]>>>()
460 .map(|locs| (action, locs))
461 })
462 .choose(&mut rand2)
463 {
464 let event = self
465 .transition(pg_id, Action(pg_id, action), post_states.as_slice())
466 .expect("successful transition");
467 if event.is_some() {
468 return event;
469 }
470 }
471 }
472 }
473 None
474 }
475
476 #[inline]
477 fn check_message(&self, channel: Channel, message: Message) -> bool {
478 let channel_idx = channel.0 as usize;
479 let (_, capacity) = self.def.channels[channel_idx];
480 let len = self.message_queue[channel_idx].len();
481 // Channel capacity must never be exceeded!
482 debug_assert!(capacity.is_none_or(|cap| len <= cap));
483 // NOTE FIXME currently handshake is unsupported
484 // !matches!(capacity, Some(0))
485 match message {
486 Message::Send => capacity.is_none_or(|cap| len < cap),
487 Message::Receive => len > 0,
488 Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap),
489 Message::ProbeEmptyQueue => len == 0,
490 }
491 }
492
493 fn check_communication(&self, pg_id: PgId, action: Action) -> Result<(), CsError> {
494 if pg_id.0 >= self.program_graphs.len() as u16 {
495 Err(CsError::MissingPg(pg_id))
496 } else if action.0 != pg_id {
497 Err(CsError::ActionNotInPg(action, pg_id))
498 } else if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
499 let (_, capacity) = self.def.channels[channel.0 as usize];
500 let len = self.message_queue[channel.0 as usize].len();
501 // Channel capacity must never be exceeded!
502 assert!(capacity.is_none_or(|cap| len <= cap));
503 match message {
504 Message::Send if capacity.is_some_and(|cap| len >= cap) => {
505 Err(CsError::OutOfCapacity(channel))
506 }
507 Message::Receive if len == 0 => Err(CsError::Empty(channel)),
508 Message::ProbeEmptyQueue | Message::ProbeFullQueue
509 if matches!(capacity, Some(0)) =>
510 {
511 Err(CsError::ProbingHandshakeChannel(channel))
512 }
513 Message::ProbeFullQueue if capacity.is_none() => {
514 Err(CsError::ProbingInfiniteQueue(channel))
515 }
516 Message::ProbeEmptyQueue if len > 0 => Err(CsError::NotEmpty(channel)),
517 Message::ProbeFullQueue if capacity.is_some_and(|cap| len < cap) => {
518 Err(CsError::NotFull(channel))
519 }
520 _ => Ok(()),
521 }
522 } else {
523 Ok(())
524 }
525 }
526
527 /// Executes a transition on the given PG characterized by the argument action and post-state.
528 ///
529 /// Fails if the requested transition is not admissible.
530 ///
531 /// See also [`ProgramGraphRun::transition`].
532 pub fn transition(
533 &mut self,
534 pg_id: PgId,
535 action: Action,
536 post: &[Location],
537 ) -> Result<Option<Event>, CsError> {
538 // If action is a communication, check it is legal
539 if pg_id.0 >= self.program_graphs.len() as u16 {
540 return Err(CsError::MissingPg(pg_id));
541 } else if action.0 != pg_id {
542 return Err(CsError::ActionNotInPg(action, pg_id));
543 } else if let Some(post) = post.iter().find(|l| l.0 != pg_id) {
544 return Err(CsError::LocationNotInPg(*post, pg_id));
545 }
546 // If the action is a communication, send/receive the message
547 if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
548 let (_, capacity) = self.def.channels[channel.0 as usize];
549 let event_type = match message {
550 Message::Send
551 if capacity
552 .is_some_and(|cap| self.message_queue[channel.0 as usize].len() >= cap) =>
553 {
554 return Err(CsError::OutOfCapacity(channel));
555 }
556 Message::Send => {
557 let vals = self.program_graphs[pg_id.0 as usize]
558 .send(
559 action.1,
560 post.iter()
561 .map(|loc| loc.1)
562 .collect::<SmallVec<[PgLocation; 8]>>()
563 .as_slice(),
564 &mut self.rng,
565 )
566 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
567 self.message_queue[channel.0 as usize].extend(vals.iter().copied());
568 EventType::Send(vals)
569 }
570 Message::Receive if self.message_queue[channel.0 as usize].is_empty() => {
571 return Err(CsError::Empty(channel));
572 }
573 Message::Receive => {
574 let (types, _) = &self.def.channels[channel.0 as usize];
575 let vals = self.message_queue[channel.0 as usize]
576 .drain(..types.len())
577 .collect::<SmallVec<[Val; 2]>>();
578 self.program_graphs[pg_id.0 as usize]
579 .receive(
580 action.1,
581 post.iter()
582 .map(|loc| loc.1)
583 .collect::<SmallVec<[PgLocation; 8]>>()
584 .as_slice(),
585 vals.as_slice(),
586 )
587 .expect("communication has been verified before");
588 EventType::Receive(vals)
589 }
590 Message::ProbeEmptyQueue | Message::ProbeFullQueue
591 if matches!(capacity, Some(0)) =>
592 {
593 return Err(CsError::ProbingHandshakeChannel(channel));
594 }
595 Message::ProbeEmptyQueue if !self.message_queue[channel.0 as usize].is_empty() => {
596 return Err(CsError::NotEmpty(channel));
597 }
598 Message::ProbeEmptyQueue => {
599 let _ = self.program_graphs[pg_id.0 as usize]
600 .send(
601 action.1,
602 post.iter()
603 .map(|loc| loc.1)
604 .collect::<SmallVec<[PgLocation; 8]>>()
605 .as_slice(),
606 &mut self.rng,
607 )
608 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
609 EventType::ProbeEmptyQueue
610 }
611 Message::ProbeFullQueue
612 if capacity
613 .is_some_and(|cap| self.message_queue[channel.0 as usize].len() < cap) =>
614 {
615 return Err(CsError::NotFull(channel));
616 }
617 Message::ProbeFullQueue if capacity.is_none() => {
618 return Err(CsError::ProbingInfiniteQueue(channel));
619 }
620 Message::ProbeFullQueue => {
621 let _ = self.program_graphs[pg_id.0 as usize]
622 .send(
623 action.1,
624 post.iter()
625 .map(|loc| loc.1)
626 .collect::<SmallVec<[PgLocation; 8]>>()
627 .as_slice(),
628 &mut self.rng,
629 )
630 .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
631 EventType::ProbeFullQueue
632 }
633 };
634 Ok(Some(Event {
635 pg_id,
636 channel,
637 event_type,
638 }))
639 } else {
640 // Transition the program graph
641 self.program_graphs[pg_id.0 as usize]
642 .transition(
643 action.1,
644 post.iter()
645 .map(|loc| loc.1)
646 .collect::<SmallVec<[PgLocation; 8]>>()
647 .as_slice(),
648 &mut self.rng,
649 )
650 .map_err(|err| CsError::ProgramGraph(pg_id, err))
651 .map(|()| None)
652 }
653 }
654
655 /// Tries waiting for the given delta of time.
656 /// Returns error if any of the PG cannot wait due to some time invariant.
657 pub fn wait(&mut self, delta: Time) -> Result<(), CsError> {
658 if let Some(pg) = self
659 .program_graphs
660 .iter()
661 .position(|pg| !pg.can_wait(delta))
662 {
663 Err(CsError::ProgramGraph(PgId(pg as u16), PgError::Invariant))
664 } else {
665 self.program_graphs.iter_mut().for_each(|pg| {
666 pg.wait(delta).expect("wait");
667 });
668 self.time += delta;
669 Ok(())
670 }
671 }
672}
673
674#[cfg(test)]
675mod tests {
676 use super::*;
677
678 #[test]
679 fn builder() {
680 let _cs: ChannelSystemBuilder = ChannelSystemBuilder::new();
681 }
682
683 #[test]
684 fn new_pg() {
685 let mut cs = ChannelSystemBuilder::new();
686 let _ = cs.new_program_graph();
687 }
688
689 #[test]
690 fn new_action() -> Result<(), CsError> {
691 let mut cs = ChannelSystemBuilder::new();
692 let pg = cs.new_program_graph();
693 let _action = cs.new_action(pg)?;
694 Ok(())
695 }
696
697 #[test]
698 fn new_var() -> Result<(), CsError> {
699 let mut cs = ChannelSystemBuilder::new();
700 let pg = cs.new_program_graph();
701 let _var1 = cs.new_var(pg, Val::from(false))?;
702 let _var2 = cs.new_var(pg, Val::from(0i64))?;
703 Ok(())
704 }
705
706 #[test]
707 fn add_effect() -> Result<(), CsError> {
708 let mut cs = ChannelSystemBuilder::new();
709 let pg = cs.new_program_graph();
710 let action = cs.new_action(pg)?;
711 let var1 = cs.new_var(pg, Val::from(false))?;
712 let var2 = cs.new_var(pg, Val::from(0i64))?;
713 let effect_1 = CsExpression::from(2i64);
714 cs.add_effect(pg, action, var1, effect_1.clone())
715 .expect_err("type mismatch");
716 let effect_2 = CsExpression::from(true);
717 cs.add_effect(pg, action, var1, effect_2.clone())?;
718 cs.add_effect(pg, action, var2, effect_2)
719 .expect_err("type mismatch");
720 cs.add_effect(pg, action, var2, effect_1)?;
721 Ok(())
722 }
723
724 #[test]
725 fn new_location() -> Result<(), CsError> {
726 let mut cs = ChannelSystemBuilder::new();
727 let pg = cs.new_program_graph();
728 let initial = cs.new_initial_location(pg)?;
729 let location = cs.new_location(pg)?;
730 assert_ne!(initial, location);
731 Ok(())
732 }
733
734 #[test]
735 fn add_transition() -> Result<(), CsError> {
736 let mut cs = ChannelSystemBuilder::new();
737 let pg = cs.new_program_graph();
738 let initial = cs.new_initial_location(pg)?;
739 let action = cs.new_action(pg)?;
740 let var1 = cs.new_var(pg, Val::from(false))?;
741 let var2 = cs.new_var(pg, Val::from(0i64))?;
742 let effect_1 = CsExpression::from(0i64);
743 let effect_2 = CsExpression::from(true);
744 cs.add_effect(pg, action, var1, effect_2)?;
745 cs.add_effect(pg, action, var2, effect_1)?;
746 let post = cs.new_location(pg)?;
747 cs.add_transition(pg, initial, action, post, None)?;
748 Ok(())
749 }
750
751 #[test]
752 fn add_communication() -> Result<(), CsError> {
753 let mut cs = ChannelSystemBuilder::new();
754 let ch = cs.new_channel(vec![Type::Boolean], Some(1));
755
756 let pg1 = cs.new_program_graph();
757 let initial1 = cs.new_initial_location(pg1)?;
758 let post1 = cs.new_location(pg1)?;
759 let effect = CsExpression::from(true);
760 let send = cs.new_send(pg1, ch, vec![effect.clone()])?;
761 let _ = cs.new_send(pg1, ch, vec![effect])?;
762 cs.add_transition(pg1, initial1, send, post1, None)?;
763
764 let var1 = cs.new_var(pg1, Val::from(0i64))?;
765 let effect = CsExpression::from(0i64);
766 cs.add_effect(pg1, send, var1, effect)
767 .expect_err("send is a message so it cannot have effects");
768
769 let pg2 = cs.new_program_graph();
770 let initial2 = cs.new_initial_location(pg2)?;
771 let post2 = cs.new_location(pg2)?;
772 let var2 = cs.new_var(pg2, Val::from(false))?;
773 let receive = cs.new_receive(pg2, ch, vec![var2])?;
774 let _ = cs.new_receive(pg2, ch, vec![var2])?;
775 let _ = cs.new_receive(pg2, ch, vec![var2])?;
776 cs.add_transition(pg2, initial2, receive, post2, None)?;
777
778 let cs_def = cs.build();
779 let mut cs = cs_def.new_instance();
780 // assert_eq!(cs.possible_transitions().count(), 1);
781 assert_eq!(cs.def.communications_pg_idxs, vec![0, 2, 5]);
782
783 cs.transition(pg1, send, &[post1])?;
784 cs.transition(pg2, receive, &[post2])?;
785 // assert_eq!(cs.possible_transitions().count(), 0);
786 Ok(())
787 }
788}