TimeType

Trait TimeType 

Source
pub trait TimeType: Sized {
    type Valuations: Eq + PartialEq + Hash + Clone;
    type External: Eq + PartialEq + Hash + Clone;
    type CompiledDifference: Clone;
    type CompiledClocks: Clone;

    // Required methods
    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;
}
Expand description

An interface for dealing with different ways of representing time.

Required Associated Types§

Source

type Valuations: Eq + PartialEq + Hash + Clone

Type used to represent potentially infinite sets of clock valuations.

Source

type External: Eq + PartialEq + Hash + Clone

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

Source

type CompiledDifference: Clone

Type used to represent the difference between two clocks.

Source

type CompiledClocks: Clone

Type used to represent a compiled set of clocks.

Required Methods§

Source

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

Crates a new instance of TimeType for the given network.

Source

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

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

Source

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

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

Source

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

Checks the provided set of valuations is empty.

Source

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

Creates a set of valuations based on the given constraints.

Source

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

Constrain a set of valuations with the given constraint.

Source

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

Resets the clocks of the given set to 0.

Source

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

Extrapolates the future of the given valuations.

Source

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

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§