momba_explore/
time.rs

1//! Algorithms and data structures for representing time.
2
3use std::collections::HashSet;
4
5use num_traits::cast::FromPrimitive;
6
7use indexmap::IndexSet;
8
9use serde::{Deserialize, Serialize};
10
11use clock_zones;
12use clock_zones::Zone;
13
14use crate::Explorer;
15
16use super::model;
17
18#[derive(Eq, PartialEq, Hash, Clone, Debug)]
19pub struct Constraint<T: TimeType> {
20    pub(crate) difference: T::CompiledDifference,
21    pub(crate) is_strict: bool,
22    pub(crate) bound: model::Value,
23}
24
25/// An interface for dealing with different ways of representing time.
26pub trait TimeType: Sized {
27    /// Type used to represent potentially infinite sets of clock valuations.
28    type Valuations: Eq + PartialEq + std::hash::Hash + Clone;
29
30    /// Type used to represent partially infinite sets of clock valuations externally.
31    type External: Eq + PartialEq + std::hash::Hash + Clone;
32
33    /// Type used to represent the difference between two clocks.
34    type CompiledDifference: Clone;
35
36    /// Type used to represent a compiled set of clocks.
37    type CompiledClocks: Clone;
38
39    /// Crates a new instance of [TimeType] for the given network.
40    fn new(network: &model::Network) -> Result<Self, String>;
41
42    /// Takes two clocks and returns a compiled difference between `left` and `right`.
43    fn compile_difference(
44        &self,
45        left: &model::Clock,
46        right: &model::Clock,
47    ) -> Self::CompiledDifference;
48
49    /// Takes a set of clocks and returns a compiled set of clocks.
50    fn compile_clocks(&self, clocks: &HashSet<model::Clock>) -> Self::CompiledClocks;
51
52    /// Checks the provided set of valuations is empty.
53    fn is_empty(&self, valuations: &Self::Valuations) -> bool;
54
55    /// Creates a set of valuations based on the given constraints.
56    fn create_valuations(
57        &self,
58        constraints: Vec<Constraint<Self>>,
59    ) -> Result<Self::Valuations, String>;
60
61    /// Constrain a set of valuations with the given constraint.
62    fn constrain(
63        &self,
64        valuations: Self::Valuations,
65        difference: &Self::CompiledDifference,
66        is_strict: bool,
67        bound: model::Value,
68    ) -> Self::Valuations;
69
70    /// Resets the clocks of the given set to 0.
71    fn reset(
72        &self,
73        valuations: Self::Valuations,
74        clocks: &Self::CompiledClocks,
75    ) -> Self::Valuations;
76
77    /// Extrapolates the future of the given valuations.
78    fn future(&self, valuations: Self::Valuations) -> Self::Valuations;
79
80    fn externalize(&self, valuations: Self::Valuations) -> Self::External;
81}
82
83/// A time representation not supporting any real-valued clocks.
84#[derive(Serialize, Deserialize, Eq, PartialEq, Hash, Clone, Debug)]
85pub struct NoClocks();
86
87impl TimeType for NoClocks {
88    type Valuations = ();
89
90    type External = ();
91
92    type CompiledDifference = ();
93
94    type CompiledClocks = ();
95
96    fn new(network: &model::Network) -> Result<Self, String> {
97        if network.declarations.clock_variables.len() > 0 {
98            Err("time type `NoClocks` does not allow any clocks".to_string())
99        } else {
100            Ok(NoClocks())
101        }
102    }
103
104    fn compile_difference(
105        &self,
106        _left: &model::Clock,
107        _right: &model::Clock,
108    ) -> Self::CompiledDifference {
109        panic!("time type `NoClocks` does not allow any clocks")
110    }
111
112    fn compile_clocks(&self, clocks: &HashSet<model::Clock>) -> Self::CompiledClocks {
113        if clocks.len() > 0 {
114            panic!("time type `NoClocks` does not allow any clocks")
115        }
116    }
117
118    fn is_empty(&self, _valuations: &Self::Valuations) -> bool {
119        false
120    }
121
122    fn create_valuations(
123        &self,
124        constraints: Vec<Constraint<Self>>,
125    ) -> Result<Self::Valuations, String> {
126        if constraints.len() > 0 {
127            Err("time type `NoClocks` does not allow any clocks".to_string())
128        } else {
129            Ok(())
130        }
131    }
132
133    fn constrain(
134        &self,
135        _valuations: Self::Valuations,
136        _difference: &Self::CompiledDifference,
137        _is_strict: bool,
138        _bound: model::Value,
139    ) -> Self::Valuations {
140        panic!("time type `NoClocks` does not allow any clocks")
141    }
142
143    fn reset(
144        &self,
145        _valuations: Self::Valuations,
146        _clocks: &Self::CompiledClocks,
147    ) -> Self::Valuations {
148        ()
149    }
150
151    fn future(&self, _valuations: Self::Valuations) -> Self::Valuations {
152        ()
153    }
154
155    fn externalize(&self, valuations: Self::Valuations) -> Self::External {
156        valuations
157    }
158}
159
160/// A time representation using [f64] clock zones.
161#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
162pub struct Float64Zone {
163    clock_variables: IndexSet<String>,
164}
165
166impl Float64Zone {
167    fn clock_to_index(&self, clock: &model::Clock) -> usize {
168        match clock {
169            model::Clock::Zero => 0,
170            model::Clock::Variable { identifier } => {
171                self.clock_variables.get_index_of(identifier).unwrap() + 1
172            }
173        }
174    }
175
176    fn apply_constraint(
177        &self,
178        zone: &mut <Self as TimeType>::Valuations,
179        constraint: Constraint<Self>,
180    ) {
181        let bound = match constraint.bound {
182            model::Value::Int64(value) => ordered_float::NotNan::from_i64(value).unwrap(),
183            model::Value::Float64(value) => value,
184            _ => panic!("unable to convert {:?} to clock bound", constraint.bound),
185        };
186        if constraint.is_strict {
187            zone.add_constraint(clock_zones::Constraint::new_diff_lt(
188                constraint.difference.0,
189                constraint.difference.1,
190                bound,
191            ));
192        } else {
193            zone.add_constraint(clock_zones::Constraint::new_diff_le(
194                constraint.difference.0,
195                constraint.difference.1,
196                bound,
197            ));
198        }
199    }
200}
201
202impl TimeType for Float64Zone {
203    type Valuations = clock_zones::DBM<clock_zones::ConstantBound<ordered_float::NotNan<f64>>>;
204
205    type External = Self::Valuations;
206
207    type CompiledDifference = (usize, usize);
208
209    type CompiledClocks = Vec<usize>;
210
211    fn new(network: &model::Network) -> Result<Self, String> {
212        Ok(Float64Zone {
213            clock_variables: network.declarations.clock_variables.clone(),
214        })
215    }
216
217    fn compile_difference(
218        &self,
219        left: &model::Clock,
220        right: &model::Clock,
221    ) -> Self::CompiledDifference {
222        (self.clock_to_index(left), self.clock_to_index(right))
223    }
224
225    fn compile_clocks(&self, clocks: &HashSet<model::Clock>) -> Self::CompiledClocks {
226        clocks
227            .iter()
228            .map(|clock| self.clock_to_index(clock))
229            .collect()
230    }
231
232    fn is_empty(&self, valuations: &Self::Valuations) -> bool {
233        valuations.is_empty()
234    }
235
236    fn create_valuations(
237        &self,
238        constraints: Vec<Constraint<Self>>,
239    ) -> Result<Self::Valuations, String> {
240        let mut valuations = Self::Valuations::new_unconstrained(self.clock_variables.len());
241        for constraint in constraints {
242            self.apply_constraint(&mut valuations, constraint);
243        }
244        Ok(valuations)
245    }
246
247    fn constrain(
248        &self,
249        mut valuations: Self::Valuations,
250        difference: &Self::CompiledDifference,
251        is_strict: bool,
252        bound: model::Value,
253    ) -> Self::Valuations {
254        self.apply_constraint(
255            &mut valuations,
256            Constraint {
257                difference: difference.clone(),
258                is_strict,
259                bound,
260            },
261        );
262        valuations
263    }
264
265    fn reset(
266        &self,
267        mut valuations: Self::Valuations,
268        clocks: &Self::CompiledClocks,
269    ) -> Self::Valuations {
270        for clock in clocks {
271            valuations.reset(*clock, ordered_float::NotNan::new(0.0).unwrap());
272        }
273        valuations
274    }
275
276    /// Extrapolates the future of the given valuations.
277    fn future(&self, mut valuations: Self::Valuations) -> Self::Valuations {
278        valuations.future();
279        valuations
280    }
281
282    fn externalize(&self, valuations: Self::Valuations) -> Self::External {
283        valuations
284    }
285}
286
287/// A time representation using [f64] clock zones.
288#[derive(Serialize, Deserialize, Eq, PartialEq, Clone, Debug)]
289pub struct GlobalTime {
290    clock_variables: IndexSet<String>,
291    global_clock: usize,
292}
293
294impl GlobalTime {
295    fn clock_to_index(&self, clock: &model::Clock) -> usize {
296        match clock {
297            model::Clock::Zero => 0,
298            model::Clock::Variable { identifier } => {
299                self.clock_variables.get_index_of(identifier).unwrap() + 1
300            }
301        }
302    }
303
304    fn apply_constraint(
305        &self,
306        valuations: &mut <Self as TimeType>::Valuations,
307        constraint: Constraint<Self>,
308    ) {
309        let bound = match constraint.bound {
310            model::Value::Int64(value) => ordered_float::NotNan::from_i64(value).unwrap(),
311            model::Value::Float64(value) => value,
312            _ => panic!("unable to convert {:?} to clock bound", constraint.bound),
313        };
314        if constraint.is_strict {
315            valuations
316                .zone
317                .add_constraint(clock_zones::Constraint::new_diff_lt(
318                    constraint.difference.0,
319                    constraint.difference.1,
320                    bound,
321                ));
322        } else {
323            valuations
324                .zone
325                .add_constraint(clock_zones::Constraint::new_diff_le(
326                    constraint.difference.0,
327                    constraint.difference.1,
328                    bound,
329                ));
330        }
331    }
332}
333#[derive(Eq, PartialEq, Hash, Clone, Debug)]
334pub struct GlobalValuations {
335    zone: clock_zones::DBM<clock_zones::ConstantBound<ordered_float::NotNan<f64>>>,
336    global_clock: usize,
337}
338
339impl GlobalValuations {
340    fn new_unconstrained(num_clocks: usize) -> Self {
341        GlobalValuations {
342            zone: clock_zones::DBM::new_unconstrained(num_clocks),
343            global_clock: num_clocks,
344        }
345    }
346
347    pub fn global_time_lower_bound(&self) -> Option<ordered_float::NotNan<f64>> {
348        self.zone.get_lower_bound(self.global_clock)
349    }
350
351    pub fn global_time_upper_bound(&self) -> Option<ordered_float::NotNan<f64>> {
352        self.zone.get_upper_bound(self.global_clock)
353    }
354
355    pub fn set_global_time(&mut self, value: ordered_float::NotNan<f64>) {
356        self.zone
357            .add_constraint(clock_zones::Constraint::new_le(self.global_clock, value));
358        self.zone
359            .add_constraint(clock_zones::Constraint::new_ge(self.global_clock, value));
360    }
361}
362
363impl TimeType for GlobalTime {
364    type Valuations = GlobalValuations;
365
366    type External = Self::Valuations;
367
368    type CompiledDifference = (usize, usize);
369
370    type CompiledClocks = Vec<usize>;
371
372    fn new(network: &model::Network) -> Result<Self, String> {
373        Ok(GlobalTime {
374            clock_variables: network.declarations.clock_variables.clone(),
375            global_clock: network.declarations.clock_variables.len() + 1,
376        })
377    }
378
379    fn compile_difference(
380        &self,
381        left: &model::Clock,
382        right: &model::Clock,
383    ) -> Self::CompiledDifference {
384        (self.clock_to_index(left), self.clock_to_index(right))
385    }
386
387    fn compile_clocks(&self, clocks: &HashSet<model::Clock>) -> Self::CompiledClocks {
388        clocks
389            .iter()
390            .map(|clock| self.clock_to_index(clock))
391            .collect()
392    }
393
394    fn is_empty(&self, valuations: &Self::Valuations) -> bool {
395        valuations.zone.is_empty()
396    }
397
398    fn create_valuations(
399        &self,
400        constraints: Vec<Constraint<Self>>,
401    ) -> Result<Self::Valuations, String> {
402        let mut valuations = Self::Valuations::new_unconstrained(self.clock_variables.len() + 1);
403        for constraint in constraints {
404            self.apply_constraint(&mut valuations, constraint);
405        }
406        valuations
407            .zone
408            .reset(self.global_clock, ordered_float::NotNan::new(0.0).unwrap());
409        Ok(valuations)
410    }
411
412    fn constrain(
413        &self,
414        mut valuations: Self::Valuations,
415        difference: &Self::CompiledDifference,
416        is_strict: bool,
417        bound: model::Value,
418    ) -> Self::Valuations {
419        self.apply_constraint(
420            &mut valuations,
421            Constraint {
422                difference: difference.clone(),
423                is_strict,
424                bound,
425            },
426        );
427        valuations
428    }
429
430    fn reset(
431        &self,
432        mut valuations: Self::Valuations,
433        clocks: &Self::CompiledClocks,
434    ) -> Self::Valuations {
435        for clock in clocks {
436            valuations
437                .zone
438                .reset(*clock, ordered_float::NotNan::new(0.0).unwrap());
439        }
440        valuations
441    }
442
443    /// Extrapolates the future of the given valuations.
444    fn future(&self, mut valuations: Self::Valuations) -> Self::Valuations {
445        valuations.zone.future();
446        valuations
447    }
448
449    fn externalize(&self, valuations: Self::Valuations) -> Self::External {
450        valuations
451    }
452}
momba_explore/time.rs

momba_explore/
time.rs
