Timed automata have been pioneered by Rajeev Alur and David Dill in 1994 to model real-time systems . Timed automata extend finite automata with real-valued clocks. This crate provides an implementation of the difference bound matrix (DBM) data structure to efficiently represent clock zones. The implementation is mostly based on .
The trait Zone provides a general abstraction for clock zones. The struct Dbm is the heart of this crate and implements the DBM data structure using a variable bound type and storage layout. The storage layout determines how the bounds are stored while the bound type determines the data structure used to store the individual bounds.
use clock_zones::*; // create a DBM with three clock variables using `i64` as bound type let mut zone: Dbm<i64> = Dbm::new_zero(3); // applies the *future operator* to the zone removing all upper bounds zone.future(); // the lower bound of the first variable is still `0` but there is no upper bound assert_eq!(zone.get_lower_bound(Clock::variable(0)), Some(0)); assert_eq!(zone.get_upper_bound(Clock::variable(0)), None);
Different storage layouts for DBMs.
Represents either the constant zero clock or a clock variable.
A bound for a generic Constant.
A clock constraint bounding the difference between two clocks.
An implementation of Zone as difference bound matrix.
Represents a clock variable.
Represents a bound.
Represents a constant.
Represents a zone with a specific bound type.
Returns an iterator over the clocks of a zone.
Returns an iterator over the variables of a zone.
A 32-bit floating-point zone.
A 64-bit floating-point zone.
A 32-bit signed integer zone.
A 64-bit signed integer zone.