Skip to main content

scan_core/program_graph/
builder.rs

1use super::{
2    Action, ActionIdx, Clock, EPSILON, Effect, Location, LocationData, LocationIdx, PgError,
3    PgExpression, ProgramGraph, TimeConstraint, Var,
4};
5use crate::{
6    grammar::{BooleanExpr, Type, Val},
7    program_graph::PgGuard,
8};
9use log::info;
10use smallvec::SmallVec;
11
12// type TransitionBuilder = (Location, Option<PgExpression>, Vec<TimeConstraint>);
13pub(crate) type Transition = (Location, Option<BooleanExpr<Var>>, Vec<TimeConstraint>);
14
15/// Defines and builds a PG.
16#[derive(Debug, Clone)]
17pub struct ProgramGraphBuilder {
18    // initial_states: Vec<Location>,
19    initial_states: SmallVec<[Location; 8]>,
20    // Effects are indexed by actions
21    effects: Vec<Effect>,
22    // Transitions are indexed by locations
23    // Time invariants of each location
24    locations: Vec<LocationData>,
25    // Local variables with initial value.
26    vars: Vec<Val>,
27    // Number of clocks
28    clocks: u16,
29}
30
31impl Default for ProgramGraphBuilder {
32    fn default() -> Self {
33        Self::new()
34    }
35}
36
37impl ProgramGraphBuilder {
38    /// Creates a new [`ProgramGraphBuilder`].
39    /// At creation, this will only have the initial location with no variables, no actions and no transitions.
40    pub fn new() -> Self {
41        Self {
42            initial_states: SmallVec::new(),
43            effects: Vec::new(),
44            vars: Vec::new(),
45            locations: Vec::new(),
46            clocks: 0,
47        }
48    }
49
50    // Gets the type of a variable.
51    pub(crate) fn var_type(&self, var: Var) -> Result<Type, PgError> {
52        self.vars
53            .get(var.0 as usize)
54            .map(|val| Val::r#type(*val))
55            .ok_or(PgError::MissingVar(var))
56    }
57
58    /// Adds a new variable with the given initial value (and the inferred type) to the PG.
59    /// It creates and uses a default RNG for probabilistic expressions.
60    ///
61    /// It fails if the expression giving the initial value of the variable is not well-typed.
62    ///
63    /// ```
64    /// # use scan_core::program_graph::{PgExpression, ProgramGraphBuilder};
65    /// # let mut pg_builder = ProgramGraphBuilder::new();
66    /// // Create a new action
67    /// let action = pg_builder.new_action();
68    ///
69    /// // Create a value to assign the expression.
70    /// let val = (PgExpression::from(40i64) + PgExpression::from(40i64)).unwrap().eval_constant().unwrap();
71    ///
72    /// // Create a new variable
73    /// let var = pg_builder
74    ///     .new_var(val)
75    ///     .unwrap();
76    /// ```
77    pub fn new_var(&mut self, val: Val) -> Result<Var, PgError> {
78        let idx = self.vars.len();
79        self.vars.push(val);
80        Ok(Var(idx as u16))
81    }
82
83    /// Adds a new clock and returns a [`Clock`] id object.
84    ///
85    /// See also [`crate::channel_system::ChannelSystemBuilder::new_clock`].
86    pub fn new_clock(&mut self) -> Clock {
87        // We adopt the convention of indexing n clocks from 0 to n-1
88        let idx = self.clocks;
89        self.clocks += 1;
90        Clock(idx)
91    }
92
93    /// Adds a new action to the PG.
94    ///
95    /// ```
96    /// # use scan_core::program_graph::{Action, ProgramGraphBuilder};
97    /// # let mut pg_builder = ProgramGraphBuilder::new();
98    /// // Create a new action
99    /// let action: Action = pg_builder.new_action();
100    /// ```
101    #[inline(always)]
102    pub fn new_action(&mut self) -> Action {
103        let idx = self.effects.len();
104        self.effects.push(Effect::Effects(Vec::new(), Vec::new()));
105        Action(idx as ActionIdx)
106    }
107
108    /// Associates a clock reset to an action.
109    ///
110    /// Returns an error if the clock to be reset does not belong to the Program Graph.
111    ///
112    /// ```
113    /// # use scan_core::program_graph::{Clock, ProgramGraphBuilder};
114    /// # let mut pg_builder = ProgramGraphBuilder::new();
115    /// # let mut other_pg_builder = ProgramGraphBuilder::new();
116    /// let action = pg_builder.new_action();
117    /// let clock = other_pg_builder.new_clock();
118    /// // Associate action with clock reset
119    /// pg_builder
120    ///     .add_reset(action, clock)
121    ///     .expect_err("the clock does not belong to this PG");
122    /// ```
123    pub fn add_reset(&mut self, action: Action, clock: Clock) -> Result<(), PgError> {
124        if action == EPSILON {
125            return Err(PgError::NoEffects);
126        }
127        if clock.0 >= self.clocks {
128            return Err(PgError::MissingClock(clock));
129        }
130        match self
131            .effects
132            .get_mut(action.0 as usize)
133            .ok_or(PgError::MissingAction(action))?
134        {
135            Effect::Effects(_, resets) => {
136                resets.push(clock);
137                Ok(())
138            }
139            Effect::Send(_) => Err(PgError::EffectOnSend),
140            Effect::Receive(_) => Err(PgError::EffectOnReceive),
141        }
142    }
143
144    /// Adds an effect to the given action.
145    /// Requires specifying which variable is assigned the value of which expression whenever the action triggers a transition.
146    ///
147    /// It fails if the type of the variable and that of the expression do not match.
148    ///
149    /// ```
150    /// # use scan_core::program_graph::{Action, PgExpression, ProgramGraphBuilder, Var};
151    /// # use scan_core::Val;
152    /// # let mut pg_builder = ProgramGraphBuilder::new();
153    /// // Create a new action
154    /// let action: Action = pg_builder.new_action();
155    ///
156    /// // Create a new variable
157    /// let var: Var = pg_builder.new_var(Val::from(true)).expect("expression is well-typed");
158    ///
159    /// // Add an effect to the action
160    /// pg_builder
161    ///     .add_effect(action, var, PgExpression::from(1i64))
162    ///     .expect_err("var is of type bool but expression is of type integer");
163    /// pg_builder
164    ///     .add_effect(action, var, PgExpression::from(false))
165    ///     .expect("var and expression type match");
166    /// ```
167    pub fn add_effect(
168        &mut self,
169        action: Action,
170        var: Var,
171        effect: PgExpression,
172    ) -> Result<(), PgError> {
173        if action == EPSILON {
174            return Err(PgError::NoEffects);
175        }
176        effect
177            .context(&|var| self.vars.get(var.0 as usize).map(|val| Val::r#type(*val)))
178            .map_err(PgError::Type)?;
179        let var_type = self
180            .vars
181            .get(var.0 as usize)
182            .map(|val| Val::r#type(*val))
183            .ok_or_else(|| PgError::MissingVar(var.to_owned()))?;
184        if var_type == effect.r#type() {
185            match self
186                .effects
187                .get_mut(action.0 as usize)
188                .ok_or(PgError::MissingAction(action))?
189            {
190                Effect::Effects(effects, _) => {
191                    effects.push((var, effect));
192                    Ok(())
193                }
194                Effect::Send(_) => Err(PgError::EffectOnSend),
195                Effect::Receive(_) => Err(PgError::EffectOnReceive),
196            }
197        } else {
198            Err(PgError::TypeMismatch)
199        }
200    }
201
202    pub(crate) fn new_send(&mut self, msgs: Vec<PgExpression>) -> Result<Action, PgError> {
203        // Check message is well-typed
204        msgs.iter()
205            .try_for_each(|msg| {
206                msg.context(&|var| self.vars.get(var.0 as usize).map(|val| Val::r#type(*val)))
207            })
208            .map_err(PgError::Type)?;
209        // Actions are indexed progressively
210        let idx = self.effects.len();
211        self.effects.push(Effect::Send(msgs.into()));
212        Ok(Action(idx as ActionIdx))
213    }
214
215    pub(crate) fn new_receive(&mut self, vars: Vec<Var>) -> Result<Action, PgError> {
216        if let Some(var) = vars.iter().find(|var| self.vars.len() as u16 <= var.0) {
217            Err(PgError::MissingVar(var.to_owned()))
218        } else {
219            // Actions are indexed progressively
220            let idx = self.effects.len();
221            self.effects.push(Effect::Receive(vars.into()));
222            Ok(Action(idx as ActionIdx))
223        }
224    }
225
226    /// Adds a new location to the PG and returns its [`Location`] indexing object.
227    #[inline(always)]
228    pub fn new_location(&mut self) -> Location {
229        self.new_timed_location(Vec::new())
230            .expect("new untimed location")
231    }
232
233    /// Adds a new location to the PG with the given time invariants,
234    /// and returns its [`Location`] indexing object.
235    pub fn new_timed_location(
236        &mut self,
237        invariants: Vec<TimeConstraint>,
238    ) -> Result<Location, PgError> {
239        if let Some((clock, _, _)) = invariants.iter().find(|(c, _, _)| c.0 >= self.clocks) {
240            Err(PgError::MissingClock(*clock))
241        } else {
242            // Locations are indexed progressively
243            let idx = self.locations.len();
244            self.locations.push((Vec::new(), invariants));
245            Ok(Location(idx as LocationIdx))
246        }
247    }
248
249    /// Adds a new (synchronous) process to the PG starting from the given [`Location`].
250    pub fn new_process(&mut self, location: Location) -> Result<(), PgError> {
251        self.locations
252            .get(location.0 as usize)
253            .ok_or(PgError::MissingLocation(location))?
254            .1 // location's time invariants
255            .iter()
256            .all(|(_, l, u)| {
257                // All clocks start at time 0
258                l.is_none_or(|l| l == 0) && u.is_none_or(|u| u > 0)
259            })
260            .then(|| self.initial_states.push(location))
261            .ok_or(PgError::Invariant)
262    }
263
264    /// Adds a new process starting at a new location to the PG and returns the [`Location`] indexing object.
265    #[inline(always)]
266    pub fn new_initial_location(&mut self) -> Location {
267        self.new_initial_timed_location(Vec::new())
268            .expect("new untimed location")
269    }
270
271    /// Adds a new process starting at a new location to the PG with the given time invariants,
272    /// and returns the [`Location`] indexing object.
273    pub fn new_initial_timed_location(
274        &mut self,
275        invariants: Vec<TimeConstraint>,
276    ) -> Result<Location, PgError> {
277        let location = self.new_timed_location(invariants)?;
278        self.new_process(location)?;
279        Ok(location)
280    }
281
282    /// Adds a transition to the PG.
283    /// Requires specifying:
284    ///
285    /// - state pre-transition,
286    /// - action triggering the transition,
287    /// - state post-transition, and
288    /// - (optionally) boolean expression guarding the transition.
289    ///
290    /// Fails if the provided guard is not a boolean expression.
291    ///
292    /// ```
293    /// # use scan_core::program_graph::ProgramGraphBuilder;
294    /// # use scan_core::BooleanExpr;
295    /// # let mut pg_builder = ProgramGraphBuilder::new();
296    /// // The builder is initialized with an initial location
297    /// let initial_loc = pg_builder.new_initial_location();
298    ///
299    /// // Create a new action
300    /// let action = pg_builder.new_action();
301    ///
302    /// // Add a transition
303    /// pg_builder
304    ///     .add_transition(initial_loc, action, initial_loc, None)
305    ///     .expect("this transition can be added");
306    /// pg_builder
307    ///     .add_transition(initial_loc, action, initial_loc, Some(BooleanExpr::from(false)))
308    ///     .expect("this one too");
309    /// ```
310    #[inline(always)]
311    pub fn add_transition(
312        &mut self,
313        pre: Location,
314        action: Action,
315        post: Location,
316        guard: Option<PgGuard>,
317    ) -> Result<(), PgError> {
318        self.add_timed_transition(pre, action, post, guard, Vec::new())
319    }
320
321    /// Adds a timed transition to the PG under timed constraints.
322    /// Requires specifying the same data as [`ProgramGraphBuilder::add_transition`],
323    /// plus a slice of time constraints.
324    ///
325    /// Fails if the provided guard is not a boolean expression.
326    ///
327    /// ```
328    /// # use scan_core::program_graph::ProgramGraphBuilder;
329    /// # use scan_core::BooleanExpr;
330    /// # let mut pg_builder = ProgramGraphBuilder::new();
331    /// // The builder is initialized with an initial location
332    /// let initial_loc = pg_builder.new_initial_location();
333    ///
334    /// // Create a new action
335    /// let action = pg_builder.new_action();
336    ///
337    /// // Add a new clock
338    /// let clock = pg_builder.new_clock();
339    ///
340    /// // Add a timed transition
341    /// pg_builder
342    ///     .add_timed_transition(initial_loc, action, initial_loc, None, vec![(clock, None, Some(1))])
343    ///     .expect("this transition can be added");
344    /// pg_builder
345    ///     .add_timed_transition(initial_loc, action, initial_loc, Some(BooleanExpr::from(false)), vec![(clock, Some(1), None)])
346    ///     .expect("this one too");
347    /// ```
348    pub fn add_timed_transition(
349        &mut self,
350        pre: Location,
351        action: Action,
352        post: Location,
353        guard: Option<PgGuard>,
354        constraints: Vec<TimeConstraint>,
355    ) -> Result<(), PgError> {
356        // Check 'pre' and 'post' locations exists
357        if self.locations.len() as LocationIdx <= pre.0 {
358            Err(PgError::MissingLocation(pre))
359        } else if self.locations.len() as LocationIdx <= post.0 {
360            Err(PgError::MissingLocation(post))
361        } else if action != EPSILON && self.effects.len() as ActionIdx <= action.0 {
362            // Check 'action' exists
363            Err(PgError::MissingAction(action))
364        } else if let Some((clock, _, _)) = constraints.iter().find(|(c, _, _)| c.0 >= self.clocks)
365        {
366            Err(PgError::MissingClock(*clock))
367        } else {
368            if let Some(ref guard) = guard {
369                guard
370                    .context(&|var| self.vars.get(var.0 as usize).map(|val| Val::r#type(*val)))
371                    .map_err(PgError::Type)?;
372            }
373            let (transitions, _) = &mut self.locations[pre.0 as usize];
374            let transition = (post, guard, constraints);
375            match transitions.binary_search_by_key(&action, |(a, _)| *a) {
376                Ok(idx) => transitions[idx].1.push(transition),
377                Err(idx) => transitions.insert(idx, (action, vec![transition])),
378            }
379            Ok(())
380        }
381    }
382
383    /// Adds an autonomous transition to the PG, i.e., a transition enabled by the epsilon action.
384    /// Requires specifying:
385    ///
386    /// - state pre-transition,
387    /// - state post-transition, and
388    /// - (optionally) boolean expression guarding the transition.
389    ///
390    /// Fails if the provided guard is not a boolean expression.
391    ///
392    /// ```
393    /// # use scan_core::program_graph::ProgramGraphBuilder;
394    /// # use scan_core::BooleanExpr;
395    /// # let mut pg_builder = ProgramGraphBuilder::new();
396    /// // The builder is initialized with an initial location
397    /// let initial_loc = pg_builder.new_initial_location();
398    ///
399    /// // Add a transition
400    /// pg_builder
401    ///     .add_autonomous_transition(initial_loc, initial_loc, None)
402    ///     .expect("this autonomous transition can be added");
403    /// pg_builder
404    ///     .add_autonomous_transition(initial_loc, initial_loc, Some(BooleanExpr::from(false)))
405    ///     .expect("this one too");
406    /// ```
407    #[inline(always)]
408    pub fn add_autonomous_transition(
409        &mut self,
410        pre: Location,
411        post: Location,
412        guard: Option<PgGuard>,
413    ) -> Result<(), PgError> {
414        self.add_transition(pre, EPSILON, post, guard)
415    }
416
417    /// Adds an autonomous timed transition to the PG, i.e., a transition enabled by the epsilon action under time constraints.
418    /// Requires specifying the same data as [`ProgramGraphBuilder::add_autonomous_transition`],
419    /// plus a slice of time constraints.
420    ///
421    /// Fails if the provided guard is not a boolean expression.
422    ///
423    /// ```
424    /// # use scan_core::program_graph::ProgramGraphBuilder;
425    /// # use scan_core::BooleanExpr;
426    /// # let mut pg_builder = ProgramGraphBuilder::new();
427    /// // The builder is initialized with an initial location
428    /// let initial_loc = pg_builder.new_initial_location();
429    ///
430    /// // Add a new clock
431    /// let clock = pg_builder.new_clock();
432    ///
433    /// // Add an autonomous timed transition
434    /// pg_builder
435    ///     .add_autonomous_timed_transition(initial_loc, initial_loc, None, vec![(clock, None, Some(1))])
436    ///     .expect("this transition can be added");
437    /// pg_builder
438    ///     .add_autonomous_timed_transition(initial_loc, initial_loc, Some(BooleanExpr::from(false)), vec![(clock, Some(1), None)])
439    ///     .expect("this one too");
440    /// ```
441    #[inline(always)]
442    pub fn add_autonomous_timed_transition(
443        &mut self,
444        pre: Location,
445        post: Location,
446        guard: Option<PgGuard>,
447        constraints: Vec<TimeConstraint>,
448    ) -> Result<(), PgError> {
449        self.add_timed_transition(pre, EPSILON, post, guard, constraints)
450    }
451
452    /// Produces a [`ProgramGraph`] defined by the [`ProgramGraphBuilder`]'s data and consuming it.
453    ///
454    /// Since the construction of the builder is already checked ad every step,
455    /// this method cannot fail.
456    pub fn build(mut self) -> ProgramGraph {
457        // Since vectors of effects and transitions will become immutable,
458        // they should be shrunk to take as little space as possible
459        self.effects.iter_mut().for_each(|effect| {
460            if let Effect::Effects(_, resets) = effect {
461                resets.sort_unstable();
462            }
463        });
464        self.effects.shrink_to_fit();
465        // Vars are not going to be immutable,
466        // but their number will be constant anyway
467        self.vars.shrink_to_fit();
468        let mut locations = self
469            .locations
470            .into_iter()
471            .map(|(a_transitions, mut invariants)| {
472                let mut a_transitions = a_transitions
473                    .into_iter()
474                    .map(|(a, mut loc_transitions)| {
475                        loc_transitions.sort_unstable_by_key(|(p, ..)| *p);
476                        (
477                            a,
478                            loc_transitions
479                                .into_iter()
480                                .map(|(p, guard, mut c)| {
481                                    c.sort_unstable();
482                                    (p, guard, c)
483                                })
484                                .collect::<Vec<_>>(),
485                        )
486                    })
487                    .collect::<Vec<_>>();
488                assert!(a_transitions.is_sorted_by_key(|(a, ..)| *a));
489                a_transitions.shrink_to_fit();
490                invariants.sort_unstable();
491                invariants.shrink_to_fit();
492                (a_transitions, invariants)
493            })
494            .collect::<Vec<_>>();
495        locations.shrink_to_fit();
496        // Build program graph
497        info!(
498            "create Program Graph with:\n{} locations\n{} actions\n{} vars",
499            locations.len(),
500            self.effects.len(),
501            self.vars.len()
502        );
503        self.initial_states.sort_unstable();
504        self.initial_states.shrink_to_fit();
505        ProgramGraph {
506            initial_states: self.initial_states,
507            effects: self.effects.into_iter().collect(),
508            locations,
509            vars: self.vars,
510            clocks: self.clocks,
511        }
512    }
513}