Module internal_spec 

Internal specification types

This module defines the specification format that model checkers in TACO operate on. An ErrorSpec describes the erroneous behavior of a threshold automaton, i.e., it is the negation of an ELTL property. A property is violated if there exists a run of the threshold automaton satisfying the error formula.

Modules

extraction 🔒

Module implementing the extraction of internal specification type from general LTL formulas

upwards_closed_set

Module for implementing atomic proposition types for model checking of threshold automata

Structs

Conjunction

Conjunction of T

Disjunction

Disjunction of T.

ErrorAtom

Specification that can be checked in a single model checker run

ErrorSpec

Named specification of erroneous behavior

InitRestriction

Restriction on the initial configuration of a run

Enums

ErrorTarget

Temporal part of an ErrorAtom

Functions

contains_globally 🔒

Check whether the expression contains a [] operator

dedup 🔒

Remove duplicate elements from a vector in place

or_conjunctions 🔒

Build the disjunction of two conjunctions of boolean expressions as a single boolean expression

Type Aliases

ErrorFormula

Boolean combination of ErrorAtoms