clock_zones/lib.rs
1//! A library for handling *[clock zones]* as they appear in the context of
2//! *[timed automata]*.
3//!
4//! [Timed automata] have been pioneered by [Rajeev Alur] and [David Dill] in
5//! 1994 to model real-time systems [[1]].
6//! Timed automata extend finite automata with real-valued *clocks*.
7//! This crate provides an implementation of the *[difference bound matrix]*
8//! (DBM) data structure to efficiently represent [clock zones].
9//! The implementation is mostly based on [[2]].
10//!
11//!
12//! ## Architecture
13//!
14//! The trait [Zone] provides a general abstraction for clock zones.
15//! The struct [Dbm] is the heart of this crate and implements the DBM data structure
16//! using a variable *[bound type][Bound]* and *[storage layout][storage::Layout]*.
17//! The storage layout determines how the bounds are stored while the bound type
18//! determines the data structure used to store the individual bounds.
19//!
20//!
21//! ## Example
22//!
23//! ```rust
24//! use clock_zones::*;
25//!
26//! // create a DBM with three clock variables using `i64` as bound type
27//! let mut zone: Dbm<i64> = Dbm::new_zero(3);
28//!
29//! // applies the *future operator* to the zone removing all upper bounds
30//! zone.future();
31//!
32//! // the lower bound of the first variable is still `0` but there is no upper bound
33//! assert_eq!(zone.get_lower_bound(Clock::variable(0)), Some(0));
34//! assert_eq!(zone.get_upper_bound(Clock::variable(0)), None);
35//! ```
36//!
37//! [clock zones]: https://en.wikipedia.org/wiki/Difference_bound_matrix#Zone
38//! [timed automata]: https://en.wikipedia.org/wiki/Timed_automaton
39//! [difference bound matrix]: https://en.wikipedia.org/wiki/Difference_bound_matrix
40//!
41//! [Rajeev Alur]: https://www.cis.upenn.edu/~alur/
42//! [David Dill]: https://profiles.stanford.edu/david-dill
43//!
44//! [1]: https://www.cis.upenn.edu/~alur/TCS94.pdf
45//! [2]: https://doi.org/10.1007/978-3-540-27755-2_3
46
47mod bounds;
48mod clocks;
49mod constants;
50mod zones;
51
52pub mod storage;
53
54pub use clocks::{AnyClock, Clock, Variable};
55
56pub use bounds::*;
57pub use constants::*;
58pub use zones::*;