Skip to main content

scan_core/channel_system/
run.rs

1use super::{
2    Action, Channel, ChannelCapacity, ChannelSystem, CsError, Event, EventType, Location, Message,
3    PgId, PgLocation,
4};
5use crate::{
6    Time, Val,
7    program_graph::{PgError, ProgramGraphRun},
8};
9use bumpalo::{Bump, collections::CollectIn};
10use rand::rngs::SmallRng;
11use std::collections::VecDeque;
12
13/// Representation of a CS that can be executed transition-by-transition.
14///
15/// The structure of the CS cannot be changed,
16/// meaning that it is not possible to introduce new PGs or modifying them, or add new channels.
17/// Though, this restriction makes it so that cloning the [`ChannelSystem`] is cheap,
18/// because only the internal state needs to be duplicated.
19#[derive(Debug)]
20pub struct ChannelSystemRun<'def> {
21    rng: SmallRng,
22    time: Time,
23    message_queue: Vec<VecDeque<Val>>,
24    program_graphs: Vec<ProgramGraphRun<'def>>,
25    def: &'def ChannelSystem,
26    bump: Bump,
27}
28
29impl<'def> Clone for ChannelSystemRun<'def> {
30    fn clone(&self) -> Self {
31        Self {
32            rng: self.rng.clone(),
33            time: self.time,
34            message_queue: self.message_queue.clone(),
35            program_graphs: self.program_graphs.clone(),
36            def: self.def,
37            bump: Bump::new(),
38        }
39    }
40}
41
42impl<'def> ChannelSystemRun<'def> {
43    /// Creates a new [`ChannelSystemRun`] which allows to execute the CS as defined.
44    ///
45    /// The new instance borrows the [`ChannelSystem`] to refer to the CS definition without copying its data,
46    /// so that spawning instances is (relatively) inexpensive.
47    ///
48    /// See also [`ProgramGraphRun::new`].
49    pub fn new(cs: &'def ChannelSystem) -> Self {
50        let pgs = cs.program_graphs.len() as u16;
51        let mut pg_list = Vec::from_iter((0..pgs).map(PgId));
52        pg_list.shrink_to_fit();
53
54        ChannelSystemRun {
55            rng: rand::make_rng(),
56            time: 0,
57            program_graphs: Vec::from_iter(
58                cs.program_graphs.iter().map(|pgdef| pgdef.new_instance()),
59            ),
60            message_queue: Vec::from_iter(cs.channels.iter().map(|(types, cap)| match cap {
61                ChannelCapacity::Queue(queue) => queue.map_or_else(VecDeque::new, |cap| {
62                    VecDeque::with_capacity(types.len() * cap)
63                }),
64                ChannelCapacity::Sink => VecDeque::new(),
65            })),
66            def: cs,
67            bump: Bump::new(),
68        }
69    }
70
71    /// Returns a reference to the underlying [`ChannelSystem`] defining the execution.
72    pub fn def(&self) -> &ChannelSystem {
73        self.def
74    }
75
76    /// Returns the current time of the CS.
77    #[inline]
78    pub fn time(&self) -> Time {
79        self.time
80    }
81
82    /// Returns an immutable reference to the [`ProgramGraphRun`]s of the Channel System associated to the given [`PgId`].
83    #[inline]
84    pub fn program_graph(&self, pg_id: PgId) -> Result<&ProgramGraphRun<'_>, CsError> {
85        self.program_graphs
86            .get(pg_id.0 as usize)
87            .ok_or(CsError::MissingPg(pg_id))
88    }
89
90    /// Iterates over all transitions that can be admitted in the current state.
91    ///
92    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
93    /// (the pre-state being necessarily the current state of the machine).
94    /// The (eventual) guard is guaranteed to be satisfied.
95    ///
96    /// See also [`ProgramGraphRun::possible_transitions`].
97    pub fn possible_transitions(
98        &self,
99    ) -> impl Iterator<
100        Item = (
101            PgId,
102            Action,
103            impl Iterator<Item = impl Iterator<Item = Location>>,
104        ),
105    > {
106        self.def.program_graph_ids().flat_map(move |pg_id| {
107            self.possible_transitions_pg(pg_id)
108                .expect("pg exists")
109                .map(move |(action, transitions)| (pg_id, action, transitions))
110        })
111    }
112
113    /// Iterates over all transitions that can be admitted in the current state for the [`ProgramGraph`] associated to the given [`PgId`].
114    ///
115    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
116    /// (the pre-state being necessarily the current state of the machine).
117    /// The (eventual) guard is guaranteed to be satisfied.
118    ///
119    /// See also [`ProgramGraphRun::possible_transitions`].
120    pub fn possible_transitions_pg(
121        &self,
122        pg_id: PgId,
123    ) -> Result<
124        impl Iterator<Item = (Action, impl Iterator<Item = impl Iterator<Item = Location>>)>,
125        CsError,
126    > {
127        self.program_graph(pg_id).map(|pg| {
128            pg.possible_transitions().filter_map(move |(action, post)| {
129                let action = Action(pg_id, action);
130                if let Some((channel, message)) = self.def.communication(pg_id, action.1)
131                    && !self.check_message(channel, message)
132                {
133                    None
134                } else {
135                    let post = post.map(move |locs| locs.map(move |loc| Location(pg_id, loc)));
136                    Some((action, post))
137                }
138            })
139        })
140    }
141
142    /// Iterates over all transitions that can be admitted in the current state for the [`ProgramGraph`] associated to the given [`PgId`],
143    /// optimized for the special (but common) case in which the state of the PG is given by a single location.
144    ///
145    /// An admissible transition is characterized by the PG it executes on, the required action and the post-state
146    /// (the pre-state being necessarily the current state of the machine).
147    /// The (eventual) guard is guaranteed to be satisfied.
148    ///
149    /// See also [`ProgramGraphRun::nosync_possible_transitions`].
150    pub fn nosync_possible_transitions_pg(
151        &self,
152        pg_id: PgId,
153    ) -> Result<impl Iterator<Item = (Action, impl Iterator<Item = Location>)>, CsError> {
154        self.program_graph(pg_id)?
155            .nosync_possible_transitions()
156            .map_err(|err| CsError::ProgramGraph(pg_id, err))
157            .map(|transitions| {
158                transitions.filter_map(move |(action, post)| {
159                    let action = Action(pg_id, action);
160                    if let Some((channel, message)) = self.def.communication(pg_id, action.1)
161                        && !self.check_message(channel, message)
162                    {
163                        None
164                    } else {
165                        let post = post.map(move |loc| Location(pg_id, loc));
166                        Some((action, post))
167                    }
168                })
169            })
170    }
171
172    fn check_message(&self, channel: Channel, message: Message) -> bool {
173        let channel_idx = channel.0 as usize;
174        let (_, capacity) = self.def.channels[channel_idx];
175        let len = self.message_queue[channel_idx].len();
176        // Channel capacity must never be exceeded!
177        // debug_assert!(capacity.is_none_or(|cap| len <= cap));
178        // NOTE FIXME currently handshake is unsupported
179        // !matches!(capacity, Some(0))
180        match capacity {
181            ChannelCapacity::Queue(capacity) => match message {
182                Message::Send => capacity.is_none_or(|cap| len < cap),
183                Message::Receive => len > 0,
184                Message::ProbeFullQueue => capacity.is_some_and(|cap| len == cap),
185                Message::ProbeEmptyQueue => len == 0,
186            },
187            ChannelCapacity::Sink => match message {
188                Message::Send | Message::ProbeEmptyQueue => true,
189                Message::Receive | Message::ProbeFullQueue => false,
190            },
191        }
192    }
193
194    /// Executes a transition on the given PG characterized by the argument action and post-state.
195    ///
196    /// Fails if the requested transition is not admissible.
197    ///
198    /// See also [`ProgramGraphRun::transition`].
199    pub fn transition(
200        &mut self,
201        pg_id: PgId,
202        action: Action,
203        post: &[Location],
204    ) -> Result<Option<Event>, CsError> {
205        use bumpalo::collections::Vec as BumpVec;
206
207        self.bump.reset();
208
209        // If action is a communication, check it is legal
210        if pg_id.0 >= self.program_graphs.len() as u16 {
211            return Err(CsError::MissingPg(pg_id));
212        } else if action.0 != pg_id {
213            return Err(CsError::ActionNotInPg(action, pg_id));
214        } else if let Some(post) = post.iter().find(|l| l.0 != pg_id) {
215            return Err(CsError::LocationNotInPg(*post, pg_id));
216        }
217        // If the action is a communication, send/receive the message
218        if let Some((channel, message)) = self.def.communication(pg_id, action.1) {
219            let (_, capacity) = self.def.channels[channel.0 as usize];
220            let event_type = match message {
221                Message::Send
222                    if let ChannelCapacity::Queue(capacity) = capacity
223                        && capacity.is_some_and(|cap| {
224                            self.message_queue[channel.0 as usize].len() >= cap
225                        }) =>
226                {
227                    return Err(CsError::OutOfCapacity(channel));
228                }
229                Message::Send => {
230                    let vals = self.program_graphs[pg_id.0 as usize]
231                        .send(
232                            action.1,
233                            post.iter()
234                                .map(|loc| loc.1)
235                                .collect_in::<BumpVec<PgLocation>>(&self.bump)
236                                .as_slice(),
237                            &mut self.rng,
238                        )
239                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
240                    if matches!(capacity, ChannelCapacity::Queue(_)) {
241                        self.message_queue[channel.0 as usize].extend(&vals);
242                    }
243                    EventType::Send(vals)
244                }
245                Message::Receive if self.message_queue[channel.0 as usize].is_empty() => {
246                    return Err(CsError::Empty(channel));
247                }
248                Message::Receive => {
249                    let (types, _) = &self.def.channels[channel.0 as usize];
250                    let vals = self.message_queue[channel.0 as usize]
251                        .drain(..types.len())
252                        .collect::<Vec<Val>>();
253                    self.program_graphs[pg_id.0 as usize]
254                        .receive(
255                            action.1,
256                            post.iter()
257                                .map(|loc| loc.1)
258                                .collect_in::<BumpVec<PgLocation>>(&self.bump)
259                                .as_slice(),
260                            vals.as_slice(),
261                        )
262                        .expect("communication has been verified before");
263                    EventType::Receive(vals)
264                }
265                Message::ProbeEmptyQueue | Message::ProbeFullQueue
266                    if matches!(capacity, ChannelCapacity::Queue(Some(0))) =>
267                {
268                    return Err(CsError::ProbingHandshakeChannel(channel));
269                }
270                Message::ProbeEmptyQueue if !self.message_queue[channel.0 as usize].is_empty() => {
271                    return Err(CsError::NotEmpty(channel));
272                }
273                Message::ProbeEmptyQueue => {
274                    let _ = self.program_graphs[pg_id.0 as usize]
275                        .send(
276                            action.1,
277                            post.iter()
278                                .map(|loc| loc.1)
279                                .collect_in::<BumpVec<PgLocation>>(&self.bump)
280                                .as_slice(),
281                            &mut self.rng,
282                        )
283                        .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
284                    EventType::ProbeEmptyQueue
285                }
286                Message::ProbeFullQueue => match capacity {
287                    ChannelCapacity::Queue(None) => {
288                        return Err(CsError::ProbingInfiniteQueue(channel));
289                    }
290                    ChannelCapacity::Queue(Some(capacity)) => {
291                        if self.message_queue[channel.0 as usize].len() >= capacity {
292                            let _ = self.program_graphs[pg_id.0 as usize]
293                                .send(
294                                    action.1,
295                                    post.iter()
296                                        .map(|loc| loc.1)
297                                        .collect_in::<BumpVec<PgLocation>>(&self.bump)
298                                        .as_slice(),
299                                    &mut self.rng,
300                                )
301                                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
302                            EventType::ProbeFullQueue
303                        } else {
304                            return Err(CsError::NotFull(channel));
305                        }
306                    }
307                    ChannelCapacity::Sink => return Err(CsError::NotFull(channel)),
308                },
309            };
310            Ok(Some(Event {
311                pg_id,
312                channel,
313                event_type,
314            }))
315        } else {
316            // Transition the program graph
317            self.program_graphs[pg_id.0 as usize]
318                .transition(
319                    action.1,
320                    post.iter()
321                        .map(|loc| loc.1)
322                        .collect_in::<BumpVec<PgLocation>>(&self.bump)
323                        .as_slice(),
324                    &mut self.rng,
325                )
326                .map_err(|err| CsError::ProgramGraph(pg_id, err))?;
327            Ok(None)
328        }
329    }
330
331    /// Tries waiting for the given delta of time.
332    /// Returns error if any of the PG cannot wait due to some time invariant.
333    pub fn wait(&mut self, delta: Time) -> Result<(), CsError> {
334        if let Some(pg) = self
335            .program_graphs
336            .iter()
337            .position(|pg| !pg.can_wait(delta))
338        {
339            Err(CsError::ProgramGraph(PgId(pg as u16), PgError::Invariant))
340        } else {
341            self.program_graphs.iter_mut().for_each(|pg| {
342                pg.wait(delta).expect("wait");
343            });
344            self.time += delta;
345            Ok(())
346        }
347    }
348
349    /// Checks if it is possible to wait a given amount of time-units without violating the time invariants.
350    #[inline]
351    pub fn can_wait(&self, delta: Time) -> bool {
352        self.program_graphs.iter().all(|pg| pg.can_wait(delta))
353    }
354
355    /// Returns `true` if there is any transition from the current state that will be unlocked at some point in the future.
356    #[inline]
357    pub fn is_waiting(&self) -> bool {
358        self.can_wait(1) && self.program_graphs.iter().any(|pg| pg.is_waiting())
359    }
360}