Struct CollapseLocations 

pub struct CollapseLocations {}

Preprocessor that collapses locations that have the same outgoing transitions and are not mentioned in the specification into one location

This preprocessor checks whether there exists locations that can be collapsed together and handles the collapsing in that case.

Locations are collapsable if they have the same outgoing transitions and are not mentioned in the specification.

Implementations

impl CollapseLocations

pub fn new() -> Self

Create a new instance of the CollapsableLocations preprocessor

fn compute_collapsable_locations<T: ThresholdAutomaton>( &self, ta: &T, locs_to_keep: &HashSet<&Location>, ) -> Vec<Vec<Location>>

where <T as ThresholdAutomaton>::Rule: Eq + Hash,

Return all the different sets of collapsable locations

fn have_same_outgoing_transitions<T: ThresholdAutomaton>( ta: &T, loc1: &Location, loc2: &Location, ) -> bool

where <T as ThresholdAutomaton>::Rule: Eq + Hash,

Return true if the two locations have the same outgoing transitions

Trait Implementations

impl Default for CollapseLocations

fn default() -> Self

Returns the “default value” for a type.

impl<S: TargetSpec, C: ModelCheckerContext> Preprocessor<GeneralThresholdAutomaton, S, C> for CollapseLocations

fn process(&self, ta: &mut GeneralThresholdAutomaton, spec: &S, _ctx: &C)

Process the threshold automaton and attempt to simplify it