Module preprocessing 

Preprocessing for threshold automata

This module contains the logic for preprocessing threshold automata. The goal of this preprocessing is to simplify the threshold automaton, such that the threshold automaton is easier to analyze.

The following preprocessors are implemented:

• DropSelfLoops: Removes self loops from the threshold automaton if the transition rule has no effect on the shared variables.
• DropUnreachableLocations: Removes unreachable locations from the threshold automaton.
• ReplaceTrivialGuardsStatic: Replaces some frequently generated guards that are always enabled with true.
• ReplaceTrivialGuardsSMT: Replaces guards which are always satisfied, uses SMT to determine which guards are always satisfied.
• CollapseLocations: Collapse locations which have the same incoming rules
• DropUnsatisfiableRules: Removes rules where the guards are unsatisfiable.
• CheckInitCondSatSMT: Checks whether the initial condition of a threshold automaton are satisfiable, if not, removes all rules, locations and adds false to the initial locations.

Structs

CheckInitCondSatSMT

Preprocessor that checks whether the initial conditions of threshold automaton are satisfiable at all. If this is not the case, replaces them with false and deletes all rules

CollapseLocations

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

DropSelfLoops

Preprocessor that drops self loops from the threshold automaton if the transition rule has no effect on the shared variables

DropUnreachableLocations

Preprocessor that drops unreachable locations from the threshold automaton

DropUnsatisfiableRules

Preprocessor that drops rules where the guards are unsatisfiable

RemoveUnusedVariables

Preprocessor that removes unused variables from the threshold automaton

ReplaceTrivialGuardsSMT

Preprocessor that checks for trivial guards using an SMT solver

ReplaceTrivialGuardsStatic

A lot of automatically generated benchmarks have guards of the form (var1 >= 1 || var1 == 0) or var >= 0 which are satisfied. This preprocessor replaces these guards with true.

Enums

ExistingPreprocessors

Enum representing all available preprocessors

Traits

Preprocessor

Trait for preprocessing threshold automata