Struct IndexCtx 

pub struct IndexCtx {
    loc_to_index: HashMap<Location, ACSLocation>,
    index_to_loc: HashMap<ACSLocation, Location>,
    var_to_index: HashMap<Variable, CSVariable>,
    index_to_var: HashMap<CSVariable, Variable>,
    interval_to_index: Vec<HashMap<Interval, ACSInterval>>,
    index_to_interval: Vec<HashMap<ACSInterval, Interval>>,
}

Context providing a mapping from locations, variables and intervals to indices or in this case types that can be used as indices

Fields

loc_to_index: HashMap<Location, ACSLocation>

Map from [Location]s to ACSLocations

index_to_loc: HashMap<ACSLocation, Location>

Map from ACSLocations to [Location]s

var_to_index: HashMap<Variable, CSVariable>

Map from [Variable]s to CSVariables

index_to_var: HashMap<CSVariable, Variable>

Map from CSVariables to [Variable]s

interval_to_index: Vec<HashMap<Interval, ACSInterval>>

Map from a CSVariable and an [Interval] to ACSInterval

index_to_interval: Vec<HashMap<ACSInterval, Interval>>

Map from a CSVariable and an ACSInterval to an [Interval]

Implementations

impl IndexCtx

pub fn new(ta: &IntervalThresholdAutomaton) -> Self

Create a new IndexCtx for the given interval threshold automaton

pub fn to_cs_loc(&self, loc: &Location) -> ACSLocation

Translate from a [Location] to the corresponding ACSLocation

pub fn get_loc(&self, loc: &ACSLocation) -> &Location

Translate from a ACSLocation to the corresponding [Location]

pub fn locations(&self) -> impl Iterator<Item = (&Location, &ACSLocation)>

Iterate over all locations in the index

pub fn to_cs_var(&self, var: &Variable) -> CSVariable

Translate from a [Variable] to the corresponding CSVariable

pub fn get_var(&self, var: &CSVariable) -> &Variable

Translate from a CSVariable to the corresponding [Variable]

pub fn variables(&self) -> impl Iterator<Item = (&Variable, &CSVariable)>

Iterate over all variables in the context

pub fn to_cs_interval(&self, var: &CSVariable, i: &Interval) -> ACSInterval

Translate from an [Interval] of CSVariable to the corresponding ACSInterval

pub fn get_interval(&self, var: &CSVariable, i: &ACSInterval) -> &Interval

Translate from an ACSInterval of CSVariable to the corresponding [Interval]

pub fn interval_exists(&self, var: &CSVariable, interval: ACSInterval) -> bool

Check whether the interval ACSInterval for variable CSVariable exists

pub fn intervals( &self, var: &CSVariable, ) -> impl Iterator<Item = (&Interval, &ACSInterval)>

Iterate over all intervals of the given CSVariable

Trait Implementations

impl Clone for IndexCtx

fn clone(&self) -> IndexCtx

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IndexCtx

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

Formats the value using the given formatter.

impl PartialEq for IndexCtx

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for IndexCtx