Crate taco_zcs_model_checker 

This module contains the different symbolic model checkers (ZCS model checkers) that operate on threshold automata and the 01-CS (ZCS).

Modules

paths 🔒

This file contains the definitions of steady error paths that are used in the symbolic model checker (ZCS model checker).

smt_encoder_steady

This module contains the definition of an smt_encoder which is used to check if a steady error path is spurious or not. It stores and manages all the smt variables that are constructed for the smt solver.

zcs

This module contains the symbolic representation of a 01-CS (ZCS) for a given IntervalThresholdAutomaton.

zcs_error_graph

This module contains the symbolic error graph (ZCS error graph) for a given property and a 01-CS (ZCS).

Structs

ZCSModelChecker

This struct defines a symbolic model checker (ZCS model checker) It can be used to check reachability and coverability specifications Depending on the chosen search heuristics:

ZCSModelCheckerContext

This struct contains all the necessary configurations when using the symbolic model checker (ZCS model checker)

Enums

ZCSModelCheckerError

Custom Error type to indicate an error when running a symbolic model checker (ZCS model checker)

ZCSModelCheckerHeuristics

this enum defines SymbolicModelChecker Heuristics, such a heuristics defines which symbolic paths are ignored and which specifications and threshold automata can be checked

ZCSModelCheckerInitializationError

Custom Error type to indicate an error when initializing a symbolic model checker (ZCS model checker)