Module eltl 

ELTL (LTL without next) expressions for threshold automata

This module provides the types defining ELTL expressions without a next operator for threshold automata. In the literature these formulas are also called ELTL or fault-tolerant temporal logic.

Use the ELTLSpecificationBuilder to create a new ELTL specification, which is guaranteed to only contain variables, locations and parameters that are declared in the threshold automaton associated with the builder.

Note that these ELTL formulas do not match the formal definition outlined in many papers. The reason for that is that benchmarks do not conform to the formal specification. We recommend using the more restricted internal specification types when writing a model checker.

Modules

remove_negations

Restricted version of LTL expressions without negations and implications.

Structs

ELTLSpecification

A collection of ELTLProperty that in conjunction describe correct behavior

ELTLSpecificationBuilder

Builder for building an ELTLSpecification over a threshold automaton

Enums

ELTLExpression

ELTL (LTL without next) expressions for threshold automata

ELTLExpressionBuilderError

Errors that can occur when building ELTL expressions over a threshold automaton

InternalELTLExpressionBuilderError 🔒

Internal error type without the higher level property name

Type Aliases

ELTLProperty

ELTLExpression with associated name