Expand description
A ThresholdAutomaton representation for efficient operations on counter systems and counter configurations
This module and its submodule define the ACSThresholdAutomaton type,
along with the ACSTAConfig type, which are compact representations of
counter states in a threshold automaton.
The main goal of these types is to have a representation of configurations
with a small memory footprint, which allow for efficient computations of
(certain) predecessor configurations.
Therefore, internally a configuration is just implemented as a vector of integers, to indicate the current interval and the number of processes per variable.
These types correspond to the ACS described in the paper
Parameterized Verification of Round-based Distributed Algorithms via
Extended Threshold Automata
Modules§
- configuration
- Configurations of a
ACSThresholdAutomaton - index_
ctx 🔒 - This module defines the
IndexCtxtype that serves as a mapping from indices (usize) to elements in an [IntervalThresholdAutomaton].
Structs§
- ACSInterval
- An interval in a
ACSThresholdAutomaton - ACSLocation
- A location in a
ACSThresholdAutomaton - ACSThreshold
Automaton - A variant of an [
IntervalThresholdAutomaton] allowing for low-memory representations of configurations (by aACSTAConfig) and efficient predecessor computations - CSInterval
Action - Effect of the application of a
CSRuleonCSVariable - CSRule
- Rule of a
ACSThresholdAutomatonthat can be directly applied to a the cs types - CSVariable
- A variable in a
ACSThresholdAutomaton
Enums§
- CSInterval
Constraint - Constraints on interval states operating on
ACSIntervals andCSVariables