smc_scan_core 0.1.0

use super::{
    Action, Channel, ChannelSystem, Clock, CsError, Location, Message, PgError, PgExpression, PgId,
    ProgramGraphBuilder, TimeConstraint, Var,
};
use crate::grammar::{BooleanExpr, Type};
use crate::program_graph::ProgramGraph;
use crate::{Expression, Val};
use log::info;
use std::collections::BTreeMap;

/// An expression using CS's [`Var`] as variables.
pub type CsExpression = Expression<Var>;

/// A Boolean expression using CS's [`Var`] as variables.
pub type CsGuard = BooleanExpr<Var>;

// WARN: This method should probably not be exposed to the public API.
// TODO: Turn into a private method.
impl From<(PgId, CsExpression)> for PgExpression {
    fn from((pg_id, expr): (PgId, CsExpression)) -> Self {
        expr.map(&|cs_var: Var| {
            assert_eq!(cs_var.0, pg_id);
            cs_var.1
        })
    }
}

/// The object used to define and build a CS.
pub struct ChannelSystemBuilder {
    program_graphs: Vec<ProgramGraphBuilder>,
    channels: Vec<(Vec<Type>, Option<usize>)>,
    communications: BTreeMap<Action, Option<(Channel, Message)>>,
}

impl Default for ChannelSystemBuilder {
    fn default() -> Self {
        Self::new()
    }
}

impl ChannelSystemBuilder {
    /// Create a new [`ProgramGraphBuilder`] with the given RNG (see also `ChannelSystemBuilder::new`).
    /// At creation, this will be completely empty.
    pub fn new() -> Self {
        Self {
            program_graphs: Vec::new(),
            channels: Vec::new(),
            communications: BTreeMap::new(),
        }
    }

    /// Add a new PG to the CS.
    pub fn new_program_graph(&mut self) -> PgId {
        let pg_id = PgId(self.program_graphs.len() as u16);
        let pg = ProgramGraphBuilder::new();
        self.program_graphs.push(pg);
        pg_id
    }

    /// Add a new variable of the given type to the given PG.
    ///
    /// It fails if the CS contains no such PG, or if the expression is badly-typed.
    ///
    /// See [`ProgramGraphBuilder::new_var`] for more info.
    pub fn new_var(&mut self, pg_id: PgId, val: Val) -> Result<Var, CsError> {
        let pg = self
            .program_graphs
            .get_mut(pg_id.0 as usize)
            .ok_or(CsError::MissingPg(pg_id))?;
        let var = pg
            .new_var(val)
            .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
        Ok(Var(pg_id, var))
    }

    /// Adds a new clock to the given PG and returns a [`Clock`] id object.
    ///
    /// It fails if the CS contains no such PG.
    ///
    /// See also [`ProgramGraphBuilder::new_clock`].
    pub fn new_clock(&mut self, pg_id: PgId) -> Result<Clock, CsError> {
        self.program_graphs
            .get_mut(pg_id.0 as usize)
            .ok_or(CsError::MissingPg(pg_id))
            .map(|pg| Clock(pg_id, pg.new_clock()))
    }

    /// Adds a new action to the given PG.
    ///
    /// It fails if the CS contains no such PG.
    ///
    /// See also [`ProgramGraphBuilder::new_action`].
    pub fn new_action(&mut self, pg_id: PgId) -> Result<Action, CsError> {
        self.program_graphs
            .get_mut(pg_id.0 as usize)
            .ok_or(CsError::MissingPg(pg_id))
            .map(|pg| Action(pg_id, pg.new_action()))
            .inspect(|&action| {
                self.communications.insert(action, None);
            })
    }

    /// Adds resetting the clock as an effect of the given action.
    ///
    /// Fails if either the PG does not belong to the CS,
    /// or either the action or the clock do not belong to the PG.
    ///
    /// See also [`ProgramGraphBuilder::add_reset`].
    pub fn add_reset(&mut self, pg_id: PgId, action: Action, clock: Clock) -> Result<(), CsError> {
        if action.0 != pg_id {
            return Err(CsError::ActionNotInPg(action, pg_id));
        }
        if clock.0 != pg_id {
            return Err(CsError::ClockNotInPg(clock, pg_id));
        }
        self.program_graphs
            .get_mut(pg_id.0 as usize)
            .ok_or(CsError::MissingPg(pg_id))
            .and_then(|pg| {
                pg.add_reset(action.1, clock.1)
                    .map_err(|err| CsError::ProgramGraph(pg_id, err))
            })
    }

    /// Add an effect to the given action of the given PG.
    /// It fails if:
    ///
    /// - the CS contains no such PG;
    /// - the given action does not belong to it;
    /// - the given variable does not belong to it;
    /// - trying to add an effect to a communication action.
    ///
    /// ```
    /// # 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 = cs_builder.new_program_graph();
    ///
    /// // 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, chn, vec![CsExpression::from(1i64)])
    ///     .expect("always possible to add new actions");
    ///
    /// // Add new variable to pg
    /// let var = cs_builder
    ///     .new_var(pg, Val::from(0i64))
    ///     .expect("always possible to add new variable");
    ///
    /// // It is not allowed to associate effects to communication actions
    /// cs_builder.add_effect(pg, send, var, Expression::from(1i64))
    ///     .expect_err("cannot add effect to receive, which is a communication");
    /// ```
    ///
    /// See [`ProgramGraphBuilder::add_effect`] for more info.
    pub fn add_effect(
        &mut self,
        pg_id: PgId,
        action: Action,
        var: Var,
        effect: CsExpression,
    ) -> Result<(), CsError> {
        if action.0 != pg_id {
            Err(CsError::ActionNotInPg(action, pg_id))
        } else if var.0 != pg_id {
            Err(CsError::VarNotInPg(var, pg_id))
        } else if self
            .communications
            .get(&action)
            .ok_or(CsError::ProgramGraph(
                action.0,
                PgError::MissingAction(action.1),
            ))?
            .is_some()
        {
            // Communications cannot have effects
            Err(CsError::ActionIsCommunication(action))
        } else {
            let effect = PgExpression::from((pg_id, effect));
            self.program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))
                .and_then(|pg| {
                    pg.add_effect(action.1, var.1, effect)
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))
                })
        }
    }

    /// Adds a new location to the given PG.
    ///
    /// It fails if the CS contains no such PG.
    ///
    /// See also [`ProgramGraphBuilder::new_location`].
    pub fn new_location(&mut self, pg_id: PgId) -> Result<Location, CsError> {
        self.program_graphs
            .get_mut(pg_id.0 as usize)
            .ok_or(CsError::MissingPg(pg_id))
            .map(|pg| Location(pg_id, pg.new_location()))
    }

    /// Adds a new location to the given PG with the given time invariants,
    /// and returns its [`Location`] indexing object.
    ///
    /// It fails if the CS contains no such PG.
    ///
    /// See also [`ProgramGraphBuilder::new_timed_location`].
    pub fn new_timed_location(
        &mut self,
        pg_id: PgId,
        invariants: &[TimeConstraint],
    ) -> Result<Location, CsError> {
        let invariants = invariants
            .iter()
            .map(|(c, l, u)| {
                if c.0 == pg_id {
                    Ok((c.1, *l, *u))
                } else {
                    Err(CsError::DifferentPgs(pg_id, c.0))
                }
            })
            .collect::<Result<Vec<_>, CsError>>()?;
        self.program_graphs
            .get_mut(pg_id.0 as usize)
            .ok_or(CsError::MissingPg(pg_id))
            .and_then(|pg| {
                pg.new_timed_location(invariants)
                    .map(|loc| Location(pg_id, loc))
                    .map_err(|err| CsError::ProgramGraph(pg_id, err))
            })
    }

    /// Adds a new process to the given PG starting at the given location.
    ///
    /// It fails if the CS contains no such PG, or if the PG does not contain such location.
    ///
    /// See also [`ProgramGraphBuilder::new_process`].
    pub fn new_process(&mut self, pg_id: PgId, location: Location) -> Result<(), CsError> {
        if location.0 != pg_id {
            Err(CsError::LocationNotInPg(location, pg_id))
        } else {
            self.program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))
                .and_then(|pg| {
                    pg.new_process(location.1)
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))
                })
        }
    }

    /// Adds a new initial location to the given PG.
    ///
    /// It fails if the CS contains no such PG.
    ///
    /// See also [`ProgramGraphBuilder::new_initial_location`].
    pub fn new_initial_location(&mut self, pg_id: PgId) -> Result<Location, CsError> {
        self.new_initial_timed_location(pg_id, &[])
    }

    /// Adds a new initial location to the given PG with the given time invariants,
    /// and returns its [`Location`] indexing object.
    ///
    /// It fails if the CS contains no such PG.
    ///
    /// See also [`ProgramGraphBuilder::new_initial_timed_location`].
    pub fn new_initial_timed_location(
        &mut self,
        pg_id: PgId,
        invariants: &[TimeConstraint],
    ) -> Result<Location, CsError> {
        let invariants = invariants
            .iter()
            .map(|(c, l, u)| {
                if c.0 == pg_id {
                    Ok((c.1, *l, *u))
                } else {
                    Err(CsError::DifferentPgs(pg_id, c.0))
                }
            })
            .collect::<Result<Vec<_>, CsError>>()?;
        self.program_graphs
            .get_mut(pg_id.0 as usize)
            .ok_or(CsError::MissingPg(pg_id))
            .and_then(|pg| {
                pg.new_initial_timed_location(invariants)
                    .map(|loc| Location(pg_id, loc))
                    .map_err(|err| CsError::ProgramGraph(pg_id, err))
            })
    }

    /// Adds a transition to the PG.
    ///
    /// Fails if the CS contains no such PG, or if the given action, variable or locations do not belong to it.
    ///
    /// See also [`ProgramGraphBuilder::add_transition`].
    pub fn add_transition(
        &mut self,
        pg_id: PgId,
        pre: Location,
        action: Action,
        post: Location,
        guard: Option<CsGuard>,
    ) -> Result<(), CsError> {
        if action.0 != pg_id {
            Err(CsError::ActionNotInPg(action, pg_id))
        } else if pre.0 != pg_id {
            Err(CsError::LocationNotInPg(pre, pg_id))
        } else if post.0 != pg_id {
            Err(CsError::LocationNotInPg(post, pg_id))
        } else {
            // Turn CsExpression into a PgExpression for Program Graph pg_id
            let guard = guard.map(|guard| {
                guard.map(&|cs_var: Var| {
                    assert_eq!(cs_var.0, pg_id);
                    cs_var.1
                })
            });
            self.program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))
                .and_then(|pg| {
                    pg.add_transition(pre.1, action.1, post.1, guard)
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))
                })
        }
    }

    /// Adds a timed transition to the PG with the given time constraints.
    ///
    /// Fails if the CS contains no such PG, or if the given action, variable or locations do not belong to it.
    ///
    /// See also [`ProgramGraphBuilder::add_timed_transition`].
    pub fn add_timed_transition(
        &mut self,
        pg_id: PgId,
        pre: Location,
        action: Action,
        post: Location,
        guard: Option<CsGuard>,
        constraints: &[TimeConstraint],
    ) -> Result<(), CsError> {
        if action.0 != pg_id {
            Err(CsError::ActionNotInPg(action, pg_id))
        } else if pre.0 != pg_id {
            Err(CsError::LocationNotInPg(pre, pg_id))
        } else if post.0 != pg_id {
            Err(CsError::LocationNotInPg(post, pg_id))
        } else {
            // Turn CsExpression into a PgExpression for Program Graph pg_id
            let guard = guard.map(|guard| {
                guard.map(&|cs_var: Var| {
                    assert_eq!(cs_var.0, pg_id);
                    cs_var.1
                })
            });
            let constraints = constraints
                .iter()
                .map(|(c, l, u)| {
                    if c.0 == pg_id {
                        Ok((c.1, *l, *u))
                    } else {
                        Err(CsError::DifferentPgs(pg_id, c.0))
                    }
                })
                .collect::<Result<Vec<_>, CsError>>()?;
            self.program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))
                .and_then(|pg| {
                    pg.add_timed_transition(pre.1, action.1, post.1, guard, constraints)
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))
                })
        }
    }

    /// Adds an autonomous transition to the PG.
    ///
    /// Fails if the CS contains no such PG, or if the given variable or locations do not belong to it.
    ///
    /// See also [`ProgramGraphBuilder::add_autonomous_transition`].
    pub fn add_autonomous_transition(
        &mut self,
        pg_id: PgId,
        pre: Location,
        post: Location,
        guard: Option<CsGuard>,
    ) -> Result<(), CsError> {
        if pre.0 != pg_id {
            Err(CsError::LocationNotInPg(pre, pg_id))
        } else if post.0 != pg_id {
            Err(CsError::LocationNotInPg(post, pg_id))
        } else {
            // Turn CsExpression into a PgExpression for Program Graph pg_id
            let guard = guard.map(|guard| {
                guard.map(&|cs_var: Var| {
                    assert_eq!(cs_var.0, pg_id);
                    cs_var.1
                })
            });
            self.program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))
                .and_then(|pg| {
                    pg.add_autonomous_transition(pre.1, post.1, guard)
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))
                })
        }
    }

    /// Adds an autonomous timed transition to the PG with the given time constraints.
    ///
    /// Fails if the CS contains no such PG, or if the given variable or locations do not belong to it.
    ///
    /// See also [`ProgramGraphBuilder::add_autonomous_timed_transition`].
    pub fn add_autonomous_timed_transition(
        &mut self,
        pg_id: PgId,
        pre: Location,
        post: Location,
        guard: Option<CsGuard>,
        constraints: &[TimeConstraint],
    ) -> Result<(), CsError> {
        if pre.0 != pg_id {
            Err(CsError::LocationNotInPg(pre, pg_id))
        } else if post.0 != pg_id {
            Err(CsError::LocationNotInPg(post, pg_id))
        } else {
            // Turn CsExpression into a PgExpression for Program Graph pg_id
            let guard = guard.map(|guard| {
                guard.map(&|cs_var: Var| {
                    assert_eq!(cs_var.0, pg_id);
                    cs_var.1
                })
            });
            let constraints = constraints
                .iter()
                .map(|(c, l, u)| {
                    if c.0 == pg_id {
                        Ok((c.1, *l, *u))
                    } else {
                        Err(CsError::DifferentPgs(pg_id, c.0))
                    }
                })
                .collect::<Result<Vec<_>, CsError>>()?;
            self.program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))
                .and_then(|pg| {
                    pg.add_autonomous_timed_transition(pre.1, post.1, guard, constraints)
                        .map_err(|err| CsError::ProgramGraph(pg_id, err))
                })
        }
    }

    /// Adds a new channel of the given type and capacity to the CS.
    ///
    /// - [`None`] capacity means that the channel's capacity is unlimited.
    /// - [`Some(0)`] capacity means the channel uses the handshake protocol (NOT YET IMPLEMENTED!)
    pub fn new_channel(&mut self, var_types: Vec<Type>, capacity: Option<usize>) -> Channel {
        let channel = Channel(self.channels.len() as u16);
        self.channels.push((var_types, capacity));
        channel
    }

    /// Adds a new Send communication action to the given PG.
    ///
    /// Fails if the channel and message types do not match.
    pub fn new_send(
        &mut self,
        pg_id: PgId,
        channel: Channel,
        msgs: Vec<CsExpression>,
    ) -> Result<Action, CsError> {
        let channel_type = self
            .channels
            .get(channel.0 as usize)
            .ok_or(CsError::MissingChannel(channel))?
            .0
            .to_owned();
        let message_type = msgs.iter().map(|msg| msg.r#type()).collect::<Vec<_>>();
        let msg = msgs
            .into_iter()
            .map(|msg| PgExpression::from((pg_id, msg)))
            .collect::<Vec<_>>();
        if channel_type != message_type {
            Err(CsError::ProgramGraph(pg_id, PgError::TypeMismatch))
        } else {
            let action = self.program_graphs[pg_id.0 as usize]
                .new_send(msg)
                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
            let action = Action(pg_id, action);
            self.communications
                .insert(action, Some((channel, Message::Send)));
            Ok(action)
        }
    }

    /// Adds a new Receive communication action to the given PG.
    ///
    /// Fails if the channel and message types do not match.
    pub fn new_receive(
        &mut self,
        pg_id: PgId,
        channel: Channel,
        vars: Vec<Var>,
    ) -> Result<Action, CsError> {
        if let Some(var) = vars.iter().find(|var| pg_id != var.0) {
            Err(CsError::VarNotInPg(*var, pg_id))
        } else {
            let channel_type = self
                .channels
                .get(channel.0 as usize)
                .ok_or(CsError::MissingChannel(channel))?
                .0
                .to_owned();
            let pg = self
                .program_graphs
                .get(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))?;
            let message_type = vars
                .iter()
                .map(|var| pg.var_type(var.1))
                .collect::<Result<Vec<_>, _>>()
                .map_err(|err| CsError::ProgramGraph(pg_id, err))?
                .to_owned();
            if channel_type != message_type {
                Err(CsError::ProgramGraph(pg_id, PgError::TypeMismatch))
            } else {
                let action = self.program_graphs[pg_id.0 as usize]
                    .new_receive(vars.iter().map(|var| var.1).collect())
                    .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
                let action = Action(pg_id, action);
                self.communications
                    .insert(action, Some((channel, Message::Receive)));
                Ok(action)
            }
        }
    }

    /// Adds a new ProbeEmptyQueue communication action to the given PG.
    ///
    /// Fails if the queue uses the handshake protocol.
    pub fn new_probe_empty_queue(
        &mut self,
        pg_id: PgId,
        channel: Channel,
    ) -> Result<Action, CsError> {
        let (_, cap) = self
            .channels
            .get(channel.0 as usize)
            .ok_or(CsError::MissingChannel(channel))?;
        if matches!(cap, Some(0)) {
            // it makes no sense to probe an handshake channel
            Err(CsError::ProbingHandshakeChannel(channel))
        } else {
            let action = self
                .program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))?
                // create a vacuous send action so the PG knows it's a communication
                .new_send(Vec::new())
                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
            let action = Action(pg_id, action);
            self.communications
                .insert(action, Some((channel, Message::ProbeEmptyQueue)));
            Ok(action)
        }
    }

    /// Adds a new ProbeFullQueue communication action to the given PG.
    ///
    /// Fails if the queue uses the handshake protocol or it has infinite capacity.
    pub fn new_probe_full_queue(
        &mut self,
        pg_id: PgId,
        channel: Channel,
    ) -> Result<Action, CsError> {
        let (_, cap) = self
            .channels
            .get(channel.0 as usize)
            .ok_or(CsError::MissingChannel(channel))?;
        if matches!(cap, Some(0)) {
            // it makes no sense to probe an handshake channel
            Err(CsError::ProbingHandshakeChannel(channel))
        } else if cap.is_none() {
            // it makes no sense to probe for fullness an handshake channel
            Err(CsError::ProbingInfiniteQueue(channel))
        } else {
            let action = self
                .program_graphs
                .get_mut(pg_id.0 as usize)
                .ok_or(CsError::MissingPg(pg_id))?
                // create a vacuous send action so the PG knows it's a communication
                .new_send(Vec::new())
                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
            let action = Action(pg_id, action);
            self.communications
                .insert(action, Some((channel, Message::ProbeFullQueue)));
            Ok(action)
        }
    }

    /// Produces a [`ChannelSystem`] defined by the [`ChannelSystemBuilder`]'s data and consuming it.
    pub fn build(mut self) -> ChannelSystem {
        info!(
            "create Channel System with:\n{} Program Graphs\n{} channels",
            self.program_graphs.len(),
            self.channels.len(),
        );
        let mut program_graphs: Vec<ProgramGraph> = self
            .program_graphs
            .into_iter()
            .map(|builder| builder.build())
            .collect();

        program_graphs.shrink_to_fit();
        self.channels.shrink_to_fit();
        let communications_map = Vec::from_iter(self.communications);
        let communications = Vec::from_iter(communications_map.iter().map(|&(_, comm)| comm));
        let mut index = 0;
        let mut communications_pg_idxs = Vec::<usize>::with_capacity(program_graphs.len() + 1);
        communications_pg_idxs.push(index);
        for pg_id in (0..program_graphs.len() as u16).map(PgId) {
            index = communications_map[index..]
                .iter()
                .position(|(a, ..)| a.0.0 > pg_id.0)
                .map_or(communications_map.len(), |pos| pos + index);
            communications_pg_idxs.push(index);
        }

        assert_eq!(communications_pg_idxs.len(), program_graphs.len() + 1);

        ChannelSystem {
            channels: self.channels,
            communications,
            communications_pg_idxs,
            program_graphs,
        }
    }
}