Expand description
Module for encoding possible paths between configurations in a threshold automaton
This module implements an encoding of potential paths in an (extended) threshold automaton. The encoding is described in the paper “Complexity of Verification and Synthesis of Threshold Automata” by A. R. Balasubramanian, Javier Esparza, Marijana Lazic.
The paper does not provide a complete encoding of the threshold automata, instead many implementation details are not provided. As we were not provided with the source code (nor an executable) of the implementation used in the paper, we had to make some assumptions about the implementation details.
We will explicitly mark functions that are not directly described in the paper.
Structs§
- Lazy
Step Context - Context for rule applications in a path on a threshold automaton
Traits§
- StepSMT
- Trait implemented by symbolic steps