Module error_graph 

Error Graph

This module contains the error graph construction based on the counter system of a threshold automaton. The error graph is computed backwards from the error states, until no new states are discovered.

An error graph is said to be “empty” if it does not contain any initial states, which implies that no error state is reachable from the initial states.

If the error graph is not empty, all possible paths need to be checked, whether an actual non-spurious path exists. Such a path would be a counter example to the property.

The core logic for this exploration is implemented in the node module.

Modules

edge 🔒

Edge type for the error graph

node 🔒

Node type of the error graph

spurious_path_checker 🔒

Check an error graph for non spurious paths

Structs

ErrorGraph

Error Graph storing all paths from initial abstract configurations to error configurations

Type Aliases

NodeRef 🔒

Type alias for references to nodes in the error graph