smc_scan_core 0.1.0

//! Implementation of the CS model of computation.
//!
//! Channel systems comprises multiple program graphs executing asynchronously
//! while sending and retrieving messages from channels.
//!
//! A channel system is given by:
//!
//! - A finite set of PGs.
//! - A finite set of channels, each of which has:
//!     - a given type;
//!     - a FIFO queue that can contain values of the channel's type;
//!     - a queue capacity limit: from zero (handshake communication) to infinite.
//! - Some PG actions are communication actions:
//!     - `send` actions push the computed value of an expression to the rear of the channel queue;
//!     - `receive` actions pop the value in front of the channel queue and write it onto a given PG variable;
//!     - `probe_empty_queue` actions can only be executed if the given channel has an empty queue;
//!     - `probe_full_queue` actions can only be executed if the given channel has a full queue;
//!
//! Analogously to PGs, a CS is defined through a [`ChannelSystemBuilder`],
//! by adding new PGs and channels.
//! Each PG in the CS can be given new locations, actions, effects, guards and transitions.
//! Then, a [`ChannelSystem`] is built from the [`ChannelSystemBuilder`]
//! and can be executed by performing transitions,
//! though the definition of the CS itself can no longer be altered.
//!
//! ```
//! # use scan_core::*;
//! # use scan_core::channel_system::*;
//! // Create a new CS builder
//! let mut cs_builder = ChannelSystemBuilder::new();
//!
//! // Add a new PG to the CS
//! let pg_1 = cs_builder.new_program_graph();
//!
//! // Get initial location of pg_1
//! let initial_1 = cs_builder
//!     .new_initial_location(pg_1)
//!     .expect("every PG has an initial location");
//!
//! // Create new channel
//! let chn = cs_builder.new_channel(vec![Type::Integer], Some(1));
//!
//! // Create new send communication action
//! let send = cs_builder
//!     .new_send(pg_1, chn, vec![CsExpression::from(1i64)])
//!     .expect("always possible to add new actions");
//!
//! // Add transition sending a message to the channel
//! cs_builder.add_transition(pg_1, initial_1, send, initial_1, None)
//!     .expect("transition is well-defined");
//!
//! // Add a new PG to the CS
//! let pg_2 = cs_builder.new_program_graph();
//!
//! // Get initial location of pg_2
//! let initial_2 = cs_builder
//!     .new_initial_location(pg_2)
//!     .expect("every PG has an initial location");
//!
//! // Add new variable to pg_2
//! let var = cs_builder
//!     .new_var(pg_2, Val::from(0i64))
//!     .expect("always possible to add new variable");
//!
//! // Create new receive communication action
//! let receive = cs_builder
//!     .new_receive(pg_2, chn, vec![var])
//!     .expect("always possible to add new actions");
//!
//! // Add transition sending a message to the channel
//! cs_builder.add_transition(pg_2, initial_2, receive, initial_2, None)
//!     .expect("transition is well-defined");
//!
//! // Build the CS from its builder
//! // The builder is always guaranteed to build a well-defined CS and building cannot fail
//! let cs = cs_builder.build();
//! let mut instance = cs.new_instance();
//!
//! // Since the channel is empty, only pg_1 can transition (with send)
//! {
//! let mut iter = instance.possible_transitions();
//! let (pg, action, mut trans) = iter.next().unwrap();
//! assert_eq!(pg, pg_1);
//! assert_eq!(action, send);
//! let post_locs: Vec<Location> = trans.next().unwrap().collect();
//! assert_eq!(post_locs, vec![initial_1]);
//! assert!(iter.next().is_none());
//! }
//!
//! // Perform the transition, which sends a value to the channel queue
//! // After this, the channel is full
//! instance.transition(pg_1, send, &[initial_1])
//!     .expect("transition is possible");
//!
//! // Since the channel is now full, only pg_2 can transition (with receive)
//! {
//! let mut iter = instance.possible_transitions();
//! let (pg, action, mut trans) = iter.next().unwrap();
//! assert_eq!(pg, pg_2);
//! assert_eq!(action, receive);
//! let post_locs: Vec<Location> = trans.next().unwrap().collect();
//! assert_eq!(post_locs, vec![initial_2]);
//! assert!(iter.next().is_none());
//! }
//!
//! // Perform the transition, which receives a value to the channel queue
//! // After this, the channel is empty
//! instance.transition(pg_2, receive, &[initial_2])
//!     .expect("transition is possible");
//! ```

mod builder;

use crate::program_graph::{
    Action as PgAction, Clock as PgClock, Location as PgLocation, Var as PgVar, *,
};
use crate::{Time, grammar::*};
pub use builder::*;
use rand::rngs::SmallRng;
use rand::seq::IteratorRandom;
use rand::{RngExt, SeedableRng};
use smallvec::SmallVec;
use std::collections::VecDeque;
use thiserror::Error;

/// An indexing object for PGs in a CS.
///
/// These cannot be directly created or manipulated,
/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
pub struct PgId(u16);

impl From<PgId> for u16 {
    #[inline]
    fn from(val: PgId) -> Self {
        val.0
    }
}

/// An indexing object for channels in a CS.
///
/// These cannot be directly created or manipulated,
/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
pub struct Channel(u16);

impl From<Channel> for u16 {
    #[inline]
    fn from(val: Channel) -> Self {
        val.0
    }
}

/// An indexing object for locations in a CS.
///
/// These cannot be directly created or manipulated,
/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
pub struct Location(PgId, PgLocation);

/// An indexing object for actions in a CS.
///
/// These cannot be directly created or manipulated,
/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
pub struct Action(PgId, PgAction);

/// An indexing object for typed variables in a CS.
///
/// These cannot be directly created or manipulated,
/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
pub struct Var(PgId, PgVar);

/// An indexing object for clocks in a CS.
///
/// These cannot be directly created or manipulated,
/// but have to be generated and/or provided by a [`ChannelSystemBuilder`] or [`ChannelSystem`].
///
/// See also [`PgClock`].
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
pub struct Clock(PgId, PgClock);

type TimeConstraint = (Clock, Option<Time>, Option<Time>);

/// A message to be sent through a CS's channel.
#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)]
pub enum Message {
    /// Sending the computed value of an expression to a channel.
    Send,
    /// Retrieving a value out of a channel and associating it to a variable.
    Receive,
    /// Checking whether a channel is empty.
    ProbeEmptyQueue,
    /// Checking whether a channel is full.
    ProbeFullQueue,
}

/// The error type for operations with [`ChannelSystemBuilder`]s and [`ChannelSystem`]s.
#[derive(Debug, Clone, Copy, Error)]
pub enum CsError {
    /// A PG within the CS returned an error of its own.
    #[error("error from program graph {0:?}")]
    ProgramGraph(PgId, #[source] PgError),
    /// There is no such PG in the CS.
    #[error("program graph {0:?} does not belong to the channel system")]
    MissingPg(PgId),
    /// The channel is at full capacity and can accept no more incoming messages.
    #[error("channel {0:?} is at full capacity")]
    OutOfCapacity(Channel),
    /// Channel is not full
    #[error("the channel still has free space {0:?}")]
    NotFull(Channel),
    /// The channel is empty and there is no message to be retrieved.
    #[error("channel {0:?} is empty")]
    Empty(Channel),
    /// The channel is not empty.
    #[error("channel {0:?} is not empty")]
    NotEmpty(Channel),
    /// There is no such communication action in the CS.
    #[error("communication {0:?} has not been defined")]
    NoCommunication(Action),
    /// The action does not belong to the PG.
    #[error("action {0:?} does not belong to program graph {1:?}")]
    ActionNotInPg(Action, PgId),
    /// The variable does not belong to the PG.
    #[error("variable {0:?} does not belong to program graph {1:?}")]
    VarNotInPg(Var, PgId),
    /// The location does not belong to the PG.
    #[error("location {0:?} does not belong to program graph {1:?}")]
    LocationNotInPg(Location, PgId),
    /// The clock does not belong to the PG.
    #[error("clock {0:?} does not belong to program graph {1:?}")]
    ClockNotInPg(Clock, PgId),
    /// The given PGs do not match.
    #[error("program graphs {0:?} and {1:?} do not match")]
    DifferentPgs(PgId, PgId),
    /// Action is a communication.
    ///
    /// Is returned when trying to associate an effect to a communication action.
    #[error("action {0:?} is a communication")]
    ActionIsCommunication(Action),
    /// There is no such channel in the CS.
    #[error("channel {0:?} does not exists")]
    MissingChannel(Channel),
    /// Cannot probe an handshake channel
    #[error("cannot probe handshake {0:?}")]
    ProbingHandshakeChannel(Channel),
    /// Cannot probe for fullness an infinite capacity channel
    #[error("cannot probe for fullness the infinite capacity {0:?}")]
    ProbingInfiniteQueue(Channel),
    /// A type error
    #[error("type error")]
    Type(#[source] TypeError),
}

/// A Channel System event related to a channel.
#[derive(Debug, Clone, PartialEq)]
pub struct Event {
    /// The PG producing the event in the course of a transition.
    pub pg_id: PgId,
    /// The channel involved in the event.
    pub channel: Channel,
    /// The type of event produced.
    pub event_type: EventType,
}

/// A Channel System event type related to a channel.
#[derive(Debug, Clone, PartialEq)]
pub enum EventType {
    /// Sending a value to a channel.
    Send(SmallVec<[Val; 2]>),
    /// Retrieving a value out of a channel.
    Receive(SmallVec<[Val; 2]>),
    /// Checking whether a channel is empty.
    ProbeEmptyQueue,
    /// Checking whether a channel is full.
    ProbeFullQueue,
}

/// A definition object for a CS.
/// It represents the abstract definition of a CS.
///
/// The only way to produce a [`ChannelSystem`] is through a [`ChannelSystemBuilder`].
/// This guarantees that there are no type errors involved in the definition of its PGs,
/// and thus the CS will always be in a consistent state.
///
/// The only way to execute the [`ChannelSystem`] is to generate a new [`ChannelSystemRun`] through [`ChannelSystem::new_instance`].
/// The [`ChannelSystemRun`] cannot outlive its [`ChannelSystem`], as it holds references to it.
/// This allows to cheaply generate multiple [`ChannelSystemRun`]s from the same [`ChannelSystem`].
///
/// Example:
///
/// ```
/// # use scan_core::channel_system::ChannelSystemBuilder;
/// // Create and populate a CS builder object
/// let mut cs_builder = ChannelSystemBuilder::new();
/// let pg_id = cs_builder.new_program_graph();
/// let initial = cs_builder.new_initial_location(pg_id).expect("create new location");
/// cs_builder.add_autonomous_transition(pg_id, initial, initial, None).expect("add transition");
///
/// // Build the builder object to get a CS definition object.
/// let cs_def = cs_builder.build();
///
/// // Instantiate a CS with the previously built definition.
/// let mut cs = cs_def.new_instance();
///
/// // Perform the (unique) active transition available.
/// let (pg_id_trans, e, mut post_locs) = cs.possible_transitions().last().expect("autonomous transition");
/// assert_eq!(pg_id_trans, pg_id);
/// let post_loc = post_locs.last().expect("post location").last().expect("post location");
/// assert_eq!(post_loc, initial);
/// cs.transition(pg_id, e, &[initial]).expect("transition is active");
/// ```
#[derive(Debug, Clone)]
pub struct ChannelSystem {
    channels: Vec<(Vec<Type>, Option<usize>)>,
    communications: Vec<Option<(Channel, Message)>>,
    communications_pg_idxs: Vec<usize>,
    program_graphs: Vec<ProgramGraph>,
}

impl ChannelSystem {
    /// Creates a new [`ChannelSystemRun`] which allows to execute the CS as defined.
    ///
    /// The new instance borrows the caller to refer to the CS definition without copying its data,
    /// so that spawning instances is (relatively) inexpensive.
    ///
    /// See also [`ProgramGraph::new_instance`].
    pub fn new_instance<'def>(&'def self) -> ChannelSystemRun<'def> {
        ChannelSystemRun {
            rng: rand::make_rng(),
            time: 0,
            program_graphs: Vec::from_iter(
                self.program_graphs.iter().map(|pgdef| pgdef.new_instance()),
            ),
            message_queue: Vec::from_iter(self.channels.iter().map(|(types, cap)| {
                cap.map_or_else(VecDeque::new, |cap| {
                    VecDeque::with_capacity(types.len() * cap)
                })
            })),
            def: self,
        }
    }

    #[inline]
    fn communication(&self, pg_id: PgId, pg_action: PgAction) -> Option<(Channel, Message)> {
        if pg_action == EPSILON {
            None
        } else {
            let start = self.communications_pg_idxs[pg_id.0 as usize];
            self.communications[start + ActionIdx::from(pg_action) as usize]
        }
    }

    /// Returns the list of defined channels, given as the pair of their type and capacity
    /// (where `None` denotes channels with infinite capacity, and `Some` denotes channels with finite capacity).
    #[inline]
    pub fn channels(&self) -> &Vec<(Vec<Type>, Option<usize>)> {
        &self.channels
    }
}

/// Representation of a CS that can be executed transition-by-transition.
///
/// The structure of the CS cannot be changed,
/// meaning that it is not possible to introduce new PGs or modifying them, or add new channels.
/// Though, this restriction makes it so that cloning the [`ChannelSystem`] is cheap,
/// because only the internal state needs to be duplicated.
#[derive(Debug, Clone)]
pub struct ChannelSystemRun<'def> {
    rng: SmallRng,
    time: Time,
    message_queue: Vec<VecDeque<Val>>,
    program_graphs: Vec<ProgramGraphRun<'def>>,
    def: &'def ChannelSystem,
}

impl<'def> ChannelSystemRun<'def> {
    /// Returns the current time of the CS.
    #[inline]
    pub fn time(&self) -> Time {
        self.time
    }

    /// Iterates over all transitions that can be admitted in the current state.
    ///
    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
    /// (the pre-state being necessarily the current state of the machine).
    /// The (eventual) guard is guaranteed to be satisfied.
    ///
    /// See also [`ProgramGraphRun::possible_transitions`].
    pub fn possible_transitions(
        &self,
    ) -> impl Iterator<
        Item = (
            PgId,
            Action,
            impl Iterator<Item = impl Iterator<Item = Location> + '_> + '_,
        ),
    > + '_ {
        self.program_graphs
            .iter()
            .enumerate()
            .flat_map(move |(id, pg)| {
                let pg_id = PgId(id as u16);
                pg.possible_transitions().filter_map(move |(action, post)| {
                    let action = Action(pg_id, action);
                    self.check_communication(pg_id, action).ok().map(move |()| {
                        let post = post.map(move |locs| locs.map(move |loc| Location(pg_id, loc)));
                        (pg_id, action, post)
                    })
                })
            })
    }

    pub(crate) fn montecarlo_execution(&mut self) -> Option<Event> {
        let pgs = self.program_graphs.len();
        let mut pg_vec = Vec::from_iter((0..pgs as u16).map(PgId));
        let mut rand1 = SmallRng::from_rng(&mut self.rng);
        let mut rand2 = SmallRng::from_rng(&mut self.rng);
        while !pg_vec.is_empty() {
            let pg_id = pg_vec.swap_remove(self.rng.random_range(0..pg_vec.len()));
            // Execute randomly chosen transitions on the picked PG until an event is generated,
            // or no more transition is possible
            if self.program_graphs[pg_id.0 as usize].current_states().len() == 1 {
                while let Some((action, post_state)) = self.program_graphs[pg_id.0 as usize]
                    .nosync_possible_transitions()
                    .filter(|&(action, _)| {
                        self.def
                            .communication(pg_id, action)
                            .is_none_or(|(channel, message)| self.check_message(channel, message))
                    })
                    .filter_map(|(action, post_states)| {
                        post_states
                            .choose(&mut rand1)
                            .map(|loc| (action, Location(pg_id, loc)))
                    })
                    .choose(&mut rand2)
                {
                    let event = self
                        .transition(pg_id, Action(pg_id, action), &[post_state])
                        .expect("successful transition");
                    if event.is_some() {
                        return event;
                    }
                }
            } else {
                while let Some((action, post_states)) = self.program_graphs[pg_id.0 as usize]
                    .possible_transitions()
                    .filter(|&(action, _)| {
                        self.def
                            .communication(pg_id, action)
                            .is_none_or(|(channel, message)| self.check_message(channel, message))
                    })
                    .filter_map(|(action, post_states)| {
                        post_states
                            .map(|locs| locs.choose(&mut rand1).map(|loc| Location(pg_id, loc)))
                            .collect::<Option<SmallVec<[Location; 4]>>>()
                            .map(|locs| (action, locs))
                    })
                    .choose(&mut rand2)
                {
                    let event = self
                        .transition(pg_id, Action(pg_id, action), post_states.as_slice())
                        .expect("successful transition");
                    if event.is_some() {
                        return event;
                    }
                }
            }
        }
        None
    }

    #[inline]
    fn check_message(&self, channel: Channel, message: Message) -> bool {
        let channel_idx = channel.0 as usize;
        let (_, capacity) = self.def.channels[channel_idx];
        let len = self.message_queue[channel_idx].len();
        // Channel capacity must never be exceeded!
        debug_assert!(capacity.is_none_or(|cap| len <= cap));
        // NOTE FIXME currently handshake is unsupported
        // !matches!(capacity, Some(0))
        match message {
            Message::Send => capacity.is_none_or(|cap| len < cap),
            Message::Receive => len > 0,
            Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap),
            Message::ProbeEmptyQueue => len == 0,
        }
    }

    fn check_communication(&self, pg_id: PgId, action: Action) -> Result<(), CsError> {
        if pg_id.0 >= self.program_graphs.len() as u16 {
            Err(CsError::MissingPg(pg_id))
        } else if action.0 != pg_id {
            Err(CsError::ActionNotInPg(action, pg_id))
        } else if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
            let (_, capacity) = self.def.channels[channel.0 as usize];
            let len = self.message_queue[channel.0 as usize].len();
            // Channel capacity must never be exceeded!
            assert!(capacity.is_none_or(|cap| len <= cap));
            match message {
                Message::Send if capacity.is_some_and(|cap| len >= cap) => {
                    Err(CsError::OutOfCapacity(channel))
                }
                Message::Receive if len == 0 => Err(CsError::Empty(channel)),
                Message::ProbeEmptyQueue | Message::ProbeFullQueue
                    if matches!(capacity, Some(0)) =>
                {
                    Err(CsError::ProbingHandshakeChannel(channel))
                }
                Message::ProbeFullQueue if capacity.is_none() => {
                    Err(CsError::ProbingInfiniteQueue(channel))
                }
                Message::ProbeEmptyQueue if len > 0 => Err(CsError::NotEmpty(channel)),
                Message::ProbeFullQueue if capacity.is_some_and(|cap| len < cap) => {
                    Err(CsError::NotFull(channel))
                }
                _ => Ok(()),
            }
        } else {
            Ok(())
        }
    }

    /// Executes a transition on the given PG characterized by the argument action and post-state.
    ///
    /// Fails if the requested transition is not admissible.
    ///
    /// See also [`ProgramGraphRun::transition`].
    pub fn transition(
        &mut self,
        pg_id: PgId,
        action: Action,
        post: &[Location],
    ) -> Result<Option<Event>, CsError> {
        // If action is a communication, check it is legal
        if pg_id.0 >= self.program_graphs.len() as u16 {
            return Err(CsError::MissingPg(pg_id));
        } else if action.0 != pg_id {
            return Err(CsError::ActionNotInPg(action, pg_id));
        } else if let Some(post) = post.iter().find(|l| l.0 != pg_id) {
            return Err(CsError::LocationNotInPg(*post, pg_id));
        }
        // If the action is a communication, send/receive the message
        if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
            let (_, capacity) = self.def.channels[channel.0 as usize];
            let event_type = match message {
                Message::Send
                    if capacity
                        .is_some_and(|cap| self.message_queue[channel.0 as usize].len() >= cap) =>
                {
                    return Err(CsError::OutOfCapacity(channel));
                }
                Message::Send => {
                    let vals = self.program_graphs[pg_id.0 as usize]
                        .send(
                            action.1,
                            post.iter()
                                .map(|loc| loc.1)
                                .collect::<SmallVec<[PgLocation; 8]>>()
                                .as_slice(),
                            &mut self.rng,
                        )
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
                    self.message_queue[channel.0 as usize].extend(vals.iter().copied());
                    EventType::Send(vals)
                }
                Message::Receive if self.message_queue[channel.0 as usize].is_empty() => {
                    return Err(CsError::Empty(channel));
                }
                Message::Receive => {
                    let (types, _) = &self.def.channels[channel.0 as usize];
                    let vals = self.message_queue[channel.0 as usize]
                        .drain(..types.len())
                        .collect::<SmallVec<[Val; 2]>>();
                    self.program_graphs[pg_id.0 as usize]
                        .receive(
                            action.1,
                            post.iter()
                                .map(|loc| loc.1)
                                .collect::<SmallVec<[PgLocation; 8]>>()
                                .as_slice(),
                            vals.as_slice(),
                        )
                        .expect("communication has been verified before");
                    EventType::Receive(vals)
                }
                Message::ProbeEmptyQueue | Message::ProbeFullQueue
                    if matches!(capacity, Some(0)) =>
                {
                    return Err(CsError::ProbingHandshakeChannel(channel));
                }
                Message::ProbeEmptyQueue if !self.message_queue[channel.0 as usize].is_empty() => {
                    return Err(CsError::NotEmpty(channel));
                }
                Message::ProbeEmptyQueue => {
                    let _ = self.program_graphs[pg_id.0 as usize]
                        .send(
                            action.1,
                            post.iter()
                                .map(|loc| loc.1)
                                .collect::<SmallVec<[PgLocation; 8]>>()
                                .as_slice(),
                            &mut self.rng,
                        )
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
                    EventType::ProbeEmptyQueue
                }
                Message::ProbeFullQueue
                    if capacity
                        .is_some_and(|cap| self.message_queue[channel.0 as usize].len() < cap) =>
                {
                    return Err(CsError::NotFull(channel));
                }
                Message::ProbeFullQueue if capacity.is_none() => {
                    return Err(CsError::ProbingInfiniteQueue(channel));
                }
                Message::ProbeFullQueue => {
                    let _ = self.program_graphs[pg_id.0 as usize]
                        .send(
                            action.1,
                            post.iter()
                                .map(|loc| loc.1)
                                .collect::<SmallVec<[PgLocation; 8]>>()
                                .as_slice(),
                            &mut self.rng,
                        )
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
                    EventType::ProbeFullQueue
                }
            };
            Ok(Some(Event {
                pg_id,
                channel,
                event_type,
            }))
        } else {
            // Transition the program graph
            self.program_graphs[pg_id.0 as usize]
                .transition(
                    action.1,
                    post.iter()
                        .map(|loc| loc.1)
                        .collect::<SmallVec<[PgLocation; 8]>>()
                        .as_slice(),
                    &mut self.rng,
                )
                .map_err(|err| CsError::ProgramGraph(pg_id, err))
                .map(|()| None)
        }
    }

    /// Tries waiting for the given delta of time.
    /// Returns error if any of the PG cannot wait due to some time invariant.
    pub fn wait(&mut self, delta: Time) -> Result<(), CsError> {
        if let Some(pg) = self
            .program_graphs
            .iter()
            .position(|pg| !pg.can_wait(delta))
        {
            Err(CsError::ProgramGraph(PgId(pg as u16), PgError::Invariant))
        } else {
            self.program_graphs.iter_mut().for_each(|pg| {
                pg.wait(delta).expect("wait");
            });
            self.time += delta;
            Ok(())
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn builder() {
        let _cs: ChannelSystemBuilder = ChannelSystemBuilder::new();
    }

    #[test]
    fn new_pg() {
        let mut cs = ChannelSystemBuilder::new();
        let _ = cs.new_program_graph();
    }

    #[test]
    fn new_action() -> Result<(), CsError> {
        let mut cs = ChannelSystemBuilder::new();
        let pg = cs.new_program_graph();
        let _action = cs.new_action(pg)?;
        Ok(())
    }

    #[test]
    fn new_var() -> Result<(), CsError> {
        let mut cs = ChannelSystemBuilder::new();
        let pg = cs.new_program_graph();
        let _var1 = cs.new_var(pg, Val::from(false))?;
        let _var2 = cs.new_var(pg, Val::from(0i64))?;
        Ok(())
    }

    #[test]
    fn add_effect() -> Result<(), CsError> {
        let mut cs = ChannelSystemBuilder::new();
        let pg = cs.new_program_graph();
        let action = cs.new_action(pg)?;
        let var1 = cs.new_var(pg, Val::from(false))?;
        let var2 = cs.new_var(pg, Val::from(0i64))?;
        let effect_1 = CsExpression::from(2i64);
        cs.add_effect(pg, action, var1, effect_1.clone())
            .expect_err("type mismatch");
        let effect_2 = CsExpression::from(true);
        cs.add_effect(pg, action, var1, effect_2.clone())?;
        cs.add_effect(pg, action, var2, effect_2)
            .expect_err("type mismatch");
        cs.add_effect(pg, action, var2, effect_1)?;
        Ok(())
    }

    #[test]
    fn new_location() -> Result<(), CsError> {
        let mut cs = ChannelSystemBuilder::new();
        let pg = cs.new_program_graph();
        let initial = cs.new_initial_location(pg)?;
        let location = cs.new_location(pg)?;
        assert_ne!(initial, location);
        Ok(())
    }

    #[test]
    fn add_transition() -> Result<(), CsError> {
        let mut cs = ChannelSystemBuilder::new();
        let pg = cs.new_program_graph();
        let initial = cs.new_initial_location(pg)?;
        let action = cs.new_action(pg)?;
        let var1 = cs.new_var(pg, Val::from(false))?;
        let var2 = cs.new_var(pg, Val::from(0i64))?;
        let effect_1 = CsExpression::from(0i64);
        let effect_2 = CsExpression::from(true);
        cs.add_effect(pg, action, var1, effect_2)?;
        cs.add_effect(pg, action, var2, effect_1)?;
        let post = cs.new_location(pg)?;
        cs.add_transition(pg, initial, action, post, None)?;
        Ok(())
    }

    #[test]
    fn add_communication() -> Result<(), CsError> {
        let mut cs = ChannelSystemBuilder::new();
        let ch = cs.new_channel(vec![Type::Boolean], Some(1));

        let pg1 = cs.new_program_graph();
        let initial1 = cs.new_initial_location(pg1)?;
        let post1 = cs.new_location(pg1)?;
        let effect = CsExpression::from(true);
        let send = cs.new_send(pg1, ch, vec![effect.clone()])?;
        let _ = cs.new_send(pg1, ch, vec![effect])?;
        cs.add_transition(pg1, initial1, send, post1, None)?;

        let var1 = cs.new_var(pg1, Val::from(0i64))?;
        let effect = CsExpression::from(0i64);
        cs.add_effect(pg1, send, var1, effect)
            .expect_err("send is a message so it cannot have effects");

        let pg2 = cs.new_program_graph();
        let initial2 = cs.new_initial_location(pg2)?;
        let post2 = cs.new_location(pg2)?;
        let var2 = cs.new_var(pg2, Val::from(false))?;
        let receive = cs.new_receive(pg2, ch, vec![var2])?;
        let _ = cs.new_receive(pg2, ch, vec![var2])?;
        let _ = cs.new_receive(pg2, ch, vec![var2])?;
        cs.add_transition(pg2, initial2, receive, post2, None)?;

        let cs_def = cs.build();
        let mut cs = cs_def.new_instance();
        // assert_eq!(cs.possible_transitions().count(), 1);
        assert_eq!(cs.def.communications_pg_idxs, vec![0, 2, 5]);

        cs.transition(pg1, send, &[post1])?;
        cs.transition(pg2, receive, &[post2])?;
        // assert_eq!(cs.possible_transitions().count(), 0);
        Ok(())
    }
}