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
- internal_
spec - Internal specification types
- preprocessing
- Preprocessing for threshold automata
Structs§
- 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
- TASpecification
- Common trait implemented by specifications
- TATrait
- Trait that needs to be implemented by an internal threshold automaton representation
Type Aliases§
- Context
Error Of - Error that can occur while creating the context of the model checker
M - Context
Of - The context type used by the model checker
M - Context
Options Of - Options accepted by the context of the model checker
M - Internal
Spec Of - The internal specification type the model checker
Mworks on - Preprocessor
Of - Preprocessor that can be applied before the threshold automaton is
transformed into the internal representation of the model checker
M - Spec
Error Of - Error that can occur while transforming an ELTL specification into the
internal specification of the model checker
M - TAError
Of - Error that can occur while transforming a general threshold automaton into
the internal representation of the model checker
M - TASpec
Of - A specification paired with all threshold automata that need to be checked to verify it, and the name of the property it was derived from