Trait clock_zones::Zone[−][src]

pub trait Zone<B: Bound> {

Show methods    fn new_unconstrained(num_variables: usize) -> Self;

    fn new_zero(num_variables: usize) -> Self;

    fn with_constraints<U>(num_variables: usize, constraints: U) -> Self
    where
        U: IntoIterator<Item = Constraint<B>>;

    fn num_variables(&self) -> usize;

    fn num_clocks(&self) -> usize;

    fn get_bound(&self, left: impl AnyClock, right: impl AnyClock) -> &B;

    fn is_empty(&self) -> bool;

    fn add_constraint(&mut self, constraint: Constraint<B>);

    fn add_constraints<U>(&mut self, constraints: U)
    where
        U: IntoIterator<Item = Constraint<B>>;

    fn intersect(&mut self, other: &Self);

    fn future(&mut self);

    fn past(&mut self);

    fn reset(&mut self, clock: Variable, value: B::Constant);

    fn is_unbounded(&self, clock: impl AnyClock) -> bool;

    fn get_upper_bound(&self, clock: impl AnyClock) -> Option<B::Constant>;

    fn get_lower_bound(&self, clock: impl AnyClock) -> Option<B::Constant>;

    fn is_satisfied(&self, constraint: Constraint<B>) -> bool;

    fn includes(&self, other: &Self) -> bool;

    fn resize(&self, num_variables: usize) -> Self;

}

Represents a zone with a specific bound type.

Required methods

fn new_unconstrained(num_variables: usize) -> Self[src]

Constructs a new zone without any constraints besides clocks being positive.

fn new_zero(num_variables: usize) -> Self[src]

Constructs a new zone where all clocks are set to zero.

fn with_constraints<U>(num_variables: usize, constraints: U) -> Self where
    U: IntoIterator<Item = Constraint<B>>, [src]

Constructs a new zone from the given iterable of constraints.

fn num_variables(&self) -> usize[src]

Returns the number of clock variables of this zone.

fn num_clocks(&self) -> usize[src]

Returns the number of clocks of this zone.

Note: This is always num_variables + 1 as there is the constant zero clock plus the clock variables.

fn get_bound(&self, left: impl AnyClock, right: impl AnyClock) -> &B[src]

Retrieves the difference bound for left - right.

fn is_empty(&self) -> bool[src]

Checks whether the zone is empty.

fn add_constraint(&mut self, constraint: Constraint<B>)[src]

Adds a constraint to the zone.

fn add_constraints<U>(&mut self, constraints: U) where
    U: IntoIterator<Item = Constraint<B>>, [src]

Adds all constraints from the given iterable to the zone.

fn intersect(&mut self, other: &Self)[src]

Intersects two zones.

fn future(&mut self)[src]

Computes the future of the zone by removing all upper bounds.

This operation is sometimes also known as up.

fn past(&mut self)[src]

Computes the past of the zone by removing all lower bounds.

This operation is sometimes also known as down.

fn reset(&mut self, clock: Variable, value: B::Constant)[src]

Resets the given clock variable to the specified constant.

fn is_unbounded(&self, clock: impl AnyClock) -> bool[src]

Checks whether the value of the given clock is unbounded.

fn get_upper_bound(&self, clock: impl AnyClock) -> Option<B::Constant>[src]

Returns the upper bound for the value of the given clock.

fn get_lower_bound(&self, clock: impl AnyClock) -> Option<B::Constant>[src]

Returns the lower bound for the value of the given clock.

fn is_satisfied(&self, constraint: Constraint<B>) -> bool[src]

Checks whether the given constraint is satisfied by the zone.

fn includes(&self, other: &Self) -> bool[src]

Checks whether the zone includes the other zone.

fn resize(&self, num_variables: usize) -> Self[src]

Creates a resized copy of the zone by adding or removing clocks.

Added clocks will be unconstrained.

Loading content...

Implementors

impl<B: Bound, L: Layout<B>> Zone<B> for Dbm<B, L>[src]

Loading content...