Module expressions 

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

This module contains the low-level expressions that make up a threshold automaton. These expressions are for example, what here is named Atomic expressions, such as

• Parameters
• Locations, and
• Variables.

These expressions all have to implement the Atomic trait, which allows them to be used in constraints.

Constraints, in the most general form are represented by IntegerExpressions that are combined into BooleanExpressions by comparing them using Comparison operators (ComparisonOp).

Note that the expressions defined here, are more general than what is allowed in the theoretical threshold automaton framework, which is why most model checkers work on a transformed version.

Modules

fraction

This module contains the implementation of the Fraction type and its operations.

properties

This module implements functionality for expressions, such as evaluations under environments, and interfaces for expressions

Structs

Location

Location of a threshold automaton

Parameter

Parameter appearing in a threshold automaton

Variable

Shared variable used in a threshold automaton

Enums

BooleanConnective

Connectives for boolean expressions

BooleanExpression

Boolean constraint over type T

ComparisonOp

Operators for comparing integer values

IntegerExpression

Integer expressions over objects of type T, parameters and integers

IntegerOp

Binary operators for Integer expressions

Traits

Atomic

Atomic trait implemented by atomic expressions

IsDeclared

Trait for checking if an object of type T has already been declared