Crate clock_zones[−][src]
A library for handling clock zones as they appear in the context of timed automata.
Timed automata have been pioneered by Rajeev Alur and David Dill in 1994 to model real-time systems [1]. 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 [2].
Architecture
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.
Example
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);
Modules
storage | Different storage layouts for DBMs. |
Structs
Clock | Represents either the constant zero clock or a clock variable. |
ConstantBound | A bound for a generic Constant. |
Constraint | A clock constraint bounding the difference between two clocks. |
Dbm | An implementation of Zone as difference bound matrix. |
Variable | Represents a clock variable. |
Traits
AnyClock | |
Bound | Represents a bound. |
Constant | Represents a constant. |
Zone | Represents a zone with a specific bound type. |
Functions
clocks | Returns an iterator over the clocks of a zone. |
variables | Returns an iterator over the variables of a zone. |
Type Definitions
ZoneF32 | A 32-bit floating-point zone. |
ZoneF64 | A 64-bit floating-point zone. |
ZoneI32 | A 32-bit signed integer zone. |
ZoneI64 | A 64-bit signed integer zone. |