Struct ErrorAtom 

pub struct ErrorAtom {
    init_restriction: InitRestriction,
    target: ErrorTarget,
}

Specification that can be checked in a single model checker run

An atom is of the form init && target, where init restricts the initial configuration (and parameters) of the runs to consider and target is the temporal part of the specification.

Fields

init_restriction: InitRestriction

Restriction on the initial configuration

target: ErrorTarget

Temporal part of the atom

Implementations

impl ErrorAtom

fn try_and(self, other: Self) -> Result<Self, ExtractionError>

Conjunction of two atoms that are the operands of one &&

Create conjunction of initial constraints and check whether targets can be unified with ErrorTarget::try_unify_and. Otherwise throws ExtractionError::UnsupportedConjunction

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

Disjunction of two atoms if a sound merge exists

impl ErrorAtom

pub fn new(init_restriction: InitRestriction, target: ErrorTarget) -> Self

Create a new atom

pub fn init_restriction(&self) -> &InitRestriction

Get the restriction on the initial configuration

pub fn target(&self) -> &ErrorTarget

Get the temporal part of the atom

pub fn is_top(&self) -> bool

Check whether this atom is trivially satisfied by every run

pub fn is_bot(&self) -> bool

Check whether this atom is unsatisfiable

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

The upwards closed sets appearing in the temporal part of this atom

Trait Implementations

impl Clone for ErrorAtom

fn clone(&self) -> ErrorAtom

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ErrorAtom

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

Formats the value using the given formatter.

impl Display for ErrorAtom

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

Formats the value using the given formatter.

impl PartialEq for ErrorAtom

fn eq(&self, other: &ErrorAtom) -> 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 ErrorAtom

impl TASpecification for ErrorAtom

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

Get the locations that appear in the specification

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

Get the variable constraints that appear in target