Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- Abstract
Domain - An abstract domain for program analysis.
- Abstract
Transformer - Abstract transformer: postτ.
- Atomic
Proposition - An atomic proposition: a named boolean predicate on states.
- BDD
- A Binary Decision Diagram (BDD).
- BDDManager
- A BDD manager: maintains a unique table and an apply cache.
- BDDModel
Checker - A symbolic model checker that uses BDDs to verify CTL properties.
- Buchi
Automaton - A Büchi automaton: (Q, Σ, δ, q_0, F).
- Counter
Example - A counterexample: a trace (sequence of states) witnessing a formula violation.
- Counter
Example Guided Refinement - CEGAR loop: counterexample-guided abstraction refinement.
- CtlModel
Checker - CTL model checker: fixpoint computation.
- Kripke
Structure - A Kripke structure M = (S, S_0, R, L).
- LtlModel
Checker - LTL model checker: automaton-theoretic approach via Büchi automata.
- MuCalculus
Evaluator - Evaluator for propositional μ-calculus formulas over finite Kripke structures.
- Parity
Game Zielonka - A parity game graph for Zielonka’s algorithm.
- ProbabilisticMC
Verifier - A probabilistic model checker for discrete-time Markov chains (DTMCs). States are 0..n-1.
- Spurious
Counterexample - A spurious counterexample: an abstract path that has no concrete realization.
- State
Label - The label of a state: the set of atomic propositions holding in that state.
- Symbolic
Transition Relation - Symbolic transition relation T(s, s’) represented as a BDD node id.
Enums§
- BDDNode
- A BDD node.
- CtlFormula
- A CTL formula.
- CtlStar
Formula - A CTL* formula: combines LTL path formulas with CTL state quantifiers.
- LtlFormula
- An LTL formula.
- MuFormula
- A μ-calculus formula (propositional modal μ-calculus).