Expand description
Concrete Paths in a Threshold Automaton
This module defines the types for concrete paths in a threshold automaton. Such a path can, for example, be used to represent a counterexample to a specification.
A full path is represented by a Path object that contains a sequence of
Configurations and Transitions.
To construct a Path, a PathBuilder should be used, as it will ensure
that the constructed path is valid in the threshold automaton.
Structs§
- Configuration
- Global configuration of in a threshold automaton
- Initialized
Path Builder - Builder for creating a validated
Pathof aGeneralThresholdAutomatonthat has been initialized with a threshold automaton and a parameter assignment. - Path
- Concrete path in a
GeneralThresholdAutomaton - Path
Builder - Builder for creating a path of a
GeneralThresholdAutomaton - Transition
- Transition that applying a rule a certain number of times
Enums§
- Path
Builder Error - Error that can occur when building a path using a
PathBuilder
Functions§
- display_
assignment 🔒 - Display a an assignment for example of parameters, locations or variables