Module 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.

To convert a GeneralThresholdAutomaton to a LIAThresholdAutomaton all guards are translated into one of these forms:

• SingleAtomConstraint: Which represents a threshold in the form x <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c where c_1, ..., c_n, c are rational constants, p_1, ..., p_n are Parameters and x is a single shared variable.
• SumAtomConstraint: Represents a threshold of the form cx_1 * x_1 + ... + cx_m * x_m <COMPARISON_OP> c_1 * p_1 + ... c_n * p_n + c where c_1, ..., c_n, cx_1, ..., cx_m, c are rational constants, p_1, ..., p_n are Parameters and x_1, …, x_m are shared variables. Additionally, all coefficients cx_1, ..., cx_m must be all positive.
• ComparisonConstraint: Comparison constraints are structured analog to a SumAtomConstraint, but allow mixing positive and negative constants in the constants cx_1, ..., cx_m.

Note that not all algorithms support all types of guards. Especially the ComparisonConstraint makes the verification problem undecidable (even without decrements and or resets). For more information see:

All Flavors of Threshold Automata - Jure Kukovec, Igor Konnov, Josef Widder - https://doi.org/10.4230/LIPIcs.CONCUR.2018.19

Modules

general_to_lia

Logic to try to convert a GeneralThresholdAutomaton into a LIAThresholdAutomaton.

integer_thresholds

This module defines abstract types for linear arithmetic constraints over parameters, variables and other Atomic values, that can be safely encoded into integer arithmetic SMT constraints.

no_sum_var_ta

TODO: Replace this logic by implementing a smarter interval logic

properties

Implementation of functionality for LIAThresholdAutomaton, LIARule and the guard types

Structs

ComparisonConstraint

Constraint over the difference between atoms / comparing atoms

LIARule

Rule type of LIAThresholdAutomaton

LIAThresholdAutomaton

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.

SingleAtomConstraint

Threshold guard over a single atom

SumAtomConstraint

Constraint over the evaluation over a sum of multiple atoms

Enums

ComparisonConstraintCreationError

Error that can occur during the creation of a comparison guard

ConstraintRewriteError

Error that can occur during the transformation of a guard

LIATransformationError

Errors that can occur when trying to transform a threshold automaton in a linear arithmetic threshold automaton

LIAVariableConstraint

Abstract constraint type for linear arithmetic formulas over shared variables

SingleAtomConstrExtractionError

Error that can occur when trying to construct a SingleAtomConstraint

SumVarConstraintCreationError

Error that can occur during the creation of a SumAtomConstraint