Expand description
This module contains the different model checkers that are available in
TACO.
Every model checker needs to implement the ModelChecker trait.
Modules§
- eltl
- ELTL (LTL without next) expressions for threshold automata
- preprocessing
- Preprocessing for threshold automata
- reachability_
specification - Reachability specification for model checkers
Structs§
- Dummy
Error - Error that should never be built
- SMTBdd
Context - Simple context for model checkers containing SMT solver and BDD manager
Enums§
- Model
Checker Result - Result type for a model checking run
- Model
Checker Setup Error - Result type for initialization of a model checker
Traits§
- Model
Checker - The
ModelCheckertrait defines the interface for all model checkers in TACO. - Model
Checker Context - Trait of contexts for model checker
- Specification
Trait - Trait that needs to be implemented by an internal specification representation
- TATrait
- Trait that needs to be implemented by an internal threshold automaton representation
- Target
Spec - Common trait implemented by types that specify a target configuration in model checking