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 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	Either a Clock or a Variable.
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.