Skip to main content

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}