Struct momba_explore::time::Float64Zone

pub struct Float64Zone { /* fields omitted */ }

A time representation using f64 clock zones.

Trait Implementations

impl Clone for Float64Zone

pub fn clone(&self) -> Float64Zone

Returns a copy of the value.

pub fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Float64Zone

pub fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Float64Zone

pub fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
    __D: Deserializer<'de>, 

Deserialize this value from the given Serde deserializer.

impl Eq for Float64Zone

impl PartialEq<Float64Zone> for Float64Zone

pub fn eq(&self, other: &Float64Zone) -> bool

This method tests for self and other values to be equal, and is used by ==.

pub fn ne(&self, other: &Float64Zone) -> bool

This method tests for !=.

impl Serialize for Float64Zone

pub fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error> where
    __S: Serializer, 

Serialize this value into the given Serde serializer.

impl StructuralEq for Float64Zone

impl StructuralPartialEq for Float64Zone

impl TimeType for Float64Zone

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

Type used to represent potentially infinite sets of clock valuations.

type CompiledDifference = (usize, usize)

Type used to represent the difference between two clocks.

type CompiledClocks = Vec<usize>

Type used to represent a compiled set of clocks.

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

Crates a new instance of TimeType for the given network.

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

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

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

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

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

Checks the provided set of valuations is empty.

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

Creates a set of valuations based on the given constraints.

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

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

Resets the clocks of the given set to 0.

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

Extrapolates the future of the given valuations.