# 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 |

ConstantBound | A bound for a generic Constant. |

Constraint | A |

Dbm | An implementation of Zone as |

Variable | Represents a |

## Traits

AnyClock | |

Bound | Represents a bound. |

Constant | Represents a constant. |

Zone | Represents a zone with a specific |

## 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. |