Trait momba_explore::time::TimeType[][src]

pub trait TimeType: Sized {
    type Valuations: Eq + PartialEq + Hash + Clone;
    type External: Eq + PartialEq + Hash + Clone;
    type CompiledDifference: Clone;
    type CompiledClocks: Clone;
    fn new(network: &Network) -> Result<Self, String>;
fn compile_difference(
        &self,
        left: &Clock,
        right: &Clock
    ) -> Self::CompiledDifference;
fn compile_clocks(&self, clocks: &HashSet<Clock>) -> Self::CompiledClocks;
fn is_empty(&self, valuations: &Self::Valuations) -> bool;
fn create_valuations(
        &self,
        constraints: Vec<Constraint<Self>>
    ) -> Result<Self::Valuations, String>;
fn constrain(
        &self,
        valuations: Self::Valuations,
        difference: &Self::CompiledDifference,
        is_strict: bool,
        bound: Value
    ) -> Self::Valuations;
fn reset(
        &self,
        valuations: Self::Valuations,
        clocks: &Self::CompiledClocks
    ) -> Self::Valuations;
fn future(&self, valuations: Self::Valuations) -> Self::Valuations;
fn externalize(&self, valuations: Self::Valuations) -> Self::External; }

An interface for dealing with different ways of representing time.

Associated Types

type Valuations: Eq + PartialEq + Hash + Clone[src]

Type used to represent potentially infinite sets of clock valuations.

type External: Eq + PartialEq + Hash + Clone[src]

Type used to represent partially infinite sets of clock valuations externally.

type CompiledDifference: Clone[src]

Type used to represent the difference between two clocks.

type CompiledClocks: Clone[src]

Type used to represent a compiled set of clocks.

Loading content...

Required methods

fn new(network: &Network) -> Result<Self, String>[src]

Crates a new instance of TimeType for the given network.

fn compile_difference(
    &self,
    left: &Clock,
    right: &Clock
) -> Self::CompiledDifference
[src]

Takes two clocks and returns a compiled difference between left and right.

fn compile_clocks(&self, clocks: &HashSet<Clock>) -> Self::CompiledClocks[src]

Takes a set of clocks and returns a compiled set of clocks.

fn is_empty(&self, valuations: &Self::Valuations) -> bool[src]

Checks the provided set of valuations is empty.

fn create_valuations(
    &self,
    constraints: Vec<Constraint<Self>>
) -> Result<Self::Valuations, String>
[src]

Creates a set of valuations based on the given constraints.

fn constrain(
    &self,
    valuations: Self::Valuations,
    difference: &Self::CompiledDifference,
    is_strict: bool,
    bound: Value
) -> Self::Valuations
[src]

Constrain a set of valuations with the given constraint.

fn reset(
    &self,
    valuations: Self::Valuations,
    clocks: &Self::CompiledClocks
) -> Self::Valuations
[src]

Resets the clocks of the given set to 0.

fn future(&self, valuations: Self::Valuations) -> Self::Valuations[src]

Extrapolates the future of the given valuations.

fn externalize(&self, valuations: Self::Valuations) -> Self::External[src]

Loading content...

Implementors

impl TimeType for Float64Zone[src]

type Valuations = DBM<ConstantBound<NotNan<f64>>>

type External = Self::Valuations

type CompiledDifference = (usize, usize)

type CompiledClocks = Vec<usize>

fn future(&self, valuations: Self::Valuations) -> Self::Valuations[src]

Extrapolates the future of the given valuations.

impl TimeType for GlobalTime[src]

type Valuations = GlobalValuations

type External = Self::Valuations

type CompiledDifference = (usize, usize)

type CompiledClocks = Vec<usize>

fn future(&self, valuations: Self::Valuations) -> Self::Valuations[src]

Extrapolates the future of the given valuations.

impl TimeType for NoClocks[src]

type Valuations = ()

type External = ()

type CompiledDifference = ()

type CompiledClocks = ()

Loading content...