Expand description
This module implements the encoding of query on threshold automata into SMT expressions. The algorithm is based on the encoding 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.
Modules§
- smt_
encoding - This module implements the encoding of query on threshold automata into SMT expressions. The algorithm is based on the encoding described in the paper “Complexity of Verification and Synthesis of Threshold Automata” by A. R. Balasubramanian, Javier Esparza, Marijana Lazic.
Structs§
- SMTModel
Checker - SMTModel
Checker Options - Options to the SMT model checker
Enums§
- SMTModel
Checker Initialization Error - Errors that can occur during the initialization of the SMT model checker