Trait clock_zones::storage::Layout[−][src]

pub trait Layout<B: Bound> {
    fn new(num_variables: usize, init: B) -> Self;

    fn set(&mut self, left: impl AnyClock, right: impl AnyClock, bound: B);

    unsafe fn set_unchecked(
        &mut self, 
        left: impl AnyClock, 
        right: impl AnyClock, 
        bound: B
    );

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

    unsafe fn get_unchecked(
        &self, 
        left: impl AnyClock, 
        right: impl AnyClock
    ) -> &B;
}

Represents a storage layout for Dbm.

Required methods

fn new(num_variables: usize, init: B) -> Self[src]

Initializes the storage for num_variables clock variables using init as initial bound for all differences.

fn set(&mut self, left: impl AnyClock, right: impl AnyClock, bound: B)[src]

Sets the bound for the clock difference left - right.

unsafe fn set_unchecked(
    &mut self,
    left: impl AnyClock,
    right: impl AnyClock,
    bound: B
)[src]

Sets the bound for the clock difference left - right.

Safety

Assumes that the indices of each clock are strictly less than num_variables. Causes undefined behavior otherwise.

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

Retrieves the bound for the clock difference left - right.

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

Retrieves the bound for the clock difference left - right.

Safety

Assumes that the indices of each clock are strictly less than num_variables. Causes undefined behavior otherwise.

Loading content...

Implementors

impl<B: Bound> Layout<B> for LinearLayout<B>[src]

impl<B: Bound> Layout<B> for MatrixLayout<B>[src]

Loading content...