Crate clock_zones

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 clocks 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 clock is still `0` but there is no upper bound
// note: clock indices start at `1` because `0` is the constant *zero clock*
assert_eq!(zone.get_lower_bound(1), Some(0));
assert_eq!(zone.get_upper_bound(1), None);

Structs

ConstantBound	A bound for a generic Constant.
Constraint	A clock constraint bounding the difference of two clocks.
DBM	An implementation of Zone as difference bound matrix.
LinearLayout	A storage layout using a one-dimensional array.
MatrixLayout	A storage layout using a two-dimensional array.

Traits

Bound	Represents a bound.
Constant	Represents a constant.
Layout	Represents a storage layout for DBM.
Zone	Represents a zone with a specific bound type.

Type Definitions

Clock

Represents a clock.