Enum ErrorTarget 

pub enum ErrorTarget {
    Reach(UpwardsClosedSet),
    Invariant(UpwardsClosedSet),
    Ensure {
        pre: UpwardsClosedSet,
        inv: UpwardsClosedSet,
    },
    Repeat {
        pre: UpwardsClosedSet,
        inv: UpwardsClosedSet,
    },
    Top,
}

Temporal part of an ErrorAtom

Variants

Reach(UpwardsClosedSet)

<>(set): some configuration in the set is reachable

Invariant(UpwardsClosedSet)

[](set): there is an (infinite) run that never leaves the set

Ensure

<>(pre && [](inv)): there is an (infinite) run that reaches a configuration in pre and never leaves inv afterwards

Fields

pre: UpwardsClosedSet

Set of configurations to reach

inv: UpwardsClosedSet

Set of configurations that is never left after reaching pre

Repeat

[](pre && <>(inv)): there is an (infinite) run that never leaves pre and visits inv infinitely often

Fields

pre: UpwardsClosedSet

Set of configurations that is never left

inv: UpwardsClosedSet

Set of configurations that is visited infinitely often

Top

No temporal part: the atom is only a restriction on the initial configuration

Implementations

impl ErrorTarget

fn try_unify_and(&self, other: &Self) -> Option<Self>

Merge two targets that are the operands of one &&, if possible

fn try_unify_or(&self, other: &Self) -> Option<Self>

Merge two targets that are the operands of one ||, if possible

fn extract_from_inner_globally( expr: NonNegatedELTLExpression, ) -> Result<ErrorTarget, ExtractionError>

Extract the invariant or repeat target of a formula inside a []

fn extract_from_inner_eventually( expr: NonNegatedELTLExpression, ) -> Result<Disjunction<ErrorTarget>, ExtractionError>

Extract the reach and repeat targets of a formula inside an <>

impl ErrorTarget

pub fn is_bot(&self) -> bool

Check whether the target is unsatisfiable

pub fn is_top(&self) -> bool

Check whether the target is always satisfiable

pub fn new_reach(tgt: UpwardsClosedSet) -> Self

Create a new atom requiring to reach an upwards closed set of locations

pub fn new_invariant(tgt: UpwardsClosedSet) -> Self

Create a new atom requiring to never leave an upwards closed set of locations

pub fn new_ensure(pre: UpwardsClosedSet, inv: UpwardsClosedSet) -> Self

Create a new atom requiring to reach a configuration in pre while never leaving inv afterwards

pub fn new_repeat(pre: UpwardsClosedSet, inv: UpwardsClosedSet) -> Self

Create a new atom requiring to ensure that a run never leaves pre while eventually reaching inv

pub fn contains_reachability_constraint(&self) -> bool

Check whether specification contains a reachability constraint where at least one location needs to be empty

Only ErrorTarget::Reach targets are considered, the other temporal targets always return false.

fn sets(&self) -> impl Iterator<Item = &UpwardsClosedSet>

The upwards closed sets appearing in this target

Trait Implementations

impl Clone for ErrorTarget

fn clone(&self) -> ErrorTarget

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ErrorTarget

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for ErrorTarget

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for ErrorTarget

fn eq(&self, other: &ErrorTarget) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for ErrorTarget

impl TASpecification for ErrorTarget

fn locs_appearing(&self) -> impl IntoIterator<Item = &Location>

Locations appearing in the temporal part of the target

fn var_constraint(&self) -> impl IntoIterator<Item = &LIAVariableConstraint>

Variable constraints appearing in the temporal part of the target