Struct DropUnreachableLocations 

pub struct DropUnreachableLocations {}

Preprocessor that drops unreachable locations from the threshold automaton

This preprocessor constructs the underlying graph of the threshold automaton without considering the guards of the transition rules.

It then performs a reachability analysis to determine the reachable locations. If a location is not reachable, i.e. it is not reachable through any transition and not initial, it is removed from the threshold automaton. If there are any outgoing rules, they are also removed from the threshold automaton.

This step should generally be applied, when rules have been removed from the threshold automaton, or if locations are no longer considered to be initial.

Implementations

impl DropUnreachableLocations

pub fn new() -> Self

Create a new instance of the DropUnreachableLocations preprocessor

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

Compute the set of unreachable locations in the threshold automaton

Trait Implementations

impl Default for DropUnreachableLocations

fn default() -> DropUnreachableLocations

Returns the “default value” for a type.

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

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

Preprocessor that drops unreachable locations from the threshold automaton

This preprocessing step constructs the graph of the threshold automaton without considering the guards of the transition rules.

It then performs a reachability analysis to determine the reachable locations. If a location is not reachable, it is removed from the threshold automaton.