Crate taco_threshold_automaton 

A library to interact with threshold automata

This crate contains the definitions of the types used to represent and interact with threshold automata. In particular, it contains the traits:

• ThresholdAutomaton: common interface for all flavors of threshold automata
• RuleDefinition: common interface for rules in a threshold automaton
• ActionDefinition: trait to represent different flavors of actions
• VariableConstraint: different forms of constraints over variables

The most general type implementing the interface is the general_threshold_automaton::GeneralThresholdAutomaton type. However, the type is more general than the theoretical definition of threshold automata, as it for example allows variable comparisons or resets.

To the best of our knowledge, verification algorithms for threshold automata only exist for threshold automata that use linear integer arithmetic in their guards / thresholds. Therefore, when implementing a new model checker, you will usually want to work with the lia_threshold_automaton::LIAThresholdAutomaton flavor of threshold automata.

Modules

dot

Visualization of threshold automata in DOT format

expressions

Type definitions for arithmetic and boolean expressions over components of a threshold automaton

general_threshold_automaton

Module implementing the most general form of threshold automata GeneralThresholdAutomaton.

lia_threshold_automaton

A linear arithmetic threshold automaton or LIAThresholdAutomaton is a threshold automaton containing linear arithmetic guards. The goal of the LIAThresholdAutomaton is to stay as close to the formal definition of a threshold automaton as possible.

path

Concrete Paths in a Threshold Automaton

Traits

ActionDefinition

Trait implemented by all flavors of actions

ModifiableThresholdAutomaton

Trait for threshold automata that can be modified

RuleDefinition

Trait implemented by all flavors of rules

ThresholdAutomaton

Common trait for different types of threshold automata

VariableConstraint

Trait implemented by all flavors of constraints over variables that can serve as Guards

Type Aliases

BooleanVarConstraint

Constraint over the valuation of the shared variables

LocationConstraint

Constraint over the number of processes in a certain location

ParameterConstraint

Constraint over the valuation of parameters