Struct UpwardsClosedSet 

pub struct UpwardsClosedSet {
    clauses: Disjunction<UpwardsClosedClause>,
}

Type representing an upwards closed set of configurations

This type represents an upwards closed set of configurations symbolically. Therefore, it can be seen as disjunction over UpwardsClosedClause (i.e., since the clauses build a disjunction, it can be seen as a formula in DNF). Its purpose is to serve as the low-level characterization of an error state when model checking.

To create a new UpwardsClosedSet use the new methods and combine them using the [And] and [Or] implementations. For an UpwardsClosedSet they can also be thought of as taking the intersection or the union.

Fields

clauses: Disjunction<UpwardsClosedClause>

Set of clauses treated as a disjunction over all clauses

Implementations

impl UpwardsClosedSet

pub fn new_top() -> Self

Create a new UpwardsClosedSet which is unconstrained, i.e., contains all possible configurations

pub fn is_top(&self) -> bool

Check whether this set contains all possible configurations / is a tautology

pub fn new_bot() -> Self

Create a new UpwardsClosedSet that is not inhabited, i.e., it contains no configurations

pub fn is_bot(&self) -> bool

Check whether the current set of constraints is unsatisfiable

pub fn new_var_constraint(var_constr: LIAVariableConstraint) -> Self

Create new UpwardsClosedSet which contains all configurations satisfying given constrain

pub fn new_cover<L: Borrow<Location>, I: IntoIterator<Item = L>>( cover: I, ) -> Self

Create a new UpwardsClosedSet which contains all configurations for which all locations given in cover are occupied by at least one process

pub fn new_cover_int<L: Borrow<Location>, I: IntoIterator<Item = (L, u32)>>( cover: I, ) -> Self

Create a new UpwardsClosedSet requiring each location in cover to contain at least the given number of processes

pub fn new_reach<L: Borrow<Location>, I: IntoIterator<Item = (L, u32)>, II: IntoIterator<Item = L>>( cover: I, empty: II, ) -> Self

Create a new UpwardsClosedSet requiring each location in cover to contain at least the given number of processes, and each location in empty to contain no processes

fn new_from_clause(clause: UpwardsClosedClause) -> Self

Create a new UpwardsClosedSet from a single clause

pub fn contains_reachability_constraint(&self) -> bool

Check whether this constraint contains a reachability constraint

A reachability constraint requires at least one location to be empty, this function checks whether any of the clauses (see UpwardsClosedClause) contains a reachability specification.

pub fn upwards_closed_clauses( &self, ) -> impl Iterator<Item = &UpwardsClosedClause>

Iterator over the individual upwards closed clauses

Trait Implementations

impl And for UpwardsClosedSet

fn and(self, other: Self) -> Self

Get the conjunction of self and other

impl BitAnd for UpwardsClosedSet

type Output = UpwardsClosedSet

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> Self::Output

Performs the & operation.

impl BitOr for UpwardsClosedSet

type Output = UpwardsClosedSet

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> Self::Output

Performs the | operation.

impl Clone for UpwardsClosedSet

fn clone(&self) -> UpwardsClosedSet

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UpwardsClosedSet

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

Formats the value using the given formatter.

impl DeriveFromIntegerComp<Location, UpwardsClosedSetExtractionError> for UpwardsClosedSet

fn form_ordered_constr( scaled_t: HashMap<Location, Fraction>, thr_constr: ThresholdConstraint, ) -> Result<Self, UpwardsClosedSetExtractionError>

Derive from threshold and map scaled values of T

fn from_integer_expr( lhs: IntegerExpression<T>, op: ComparisonOp, rhs: IntegerExpression<T>, ) -> Result<Self, E>

Derive the the type T from the integer expression

impl Display for UpwardsClosedSet

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

Formats the value using the given formatter.

impl<C: SMTVariableContext<Location> + SMTVariableContext<Variable> + SMTVariableContext<Parameter>> EncodeToSMT<UpwardsClosedSet, C> for UpwardsClosedSet

fn encode_to_smt_with_ctx( &self, solver: &SMTSolver, ctx: &C, ) -> Result<SMTExpr, SMTSolverError>

Encode the type into an SMT expression

impl Or for UpwardsClosedSet

fn or(self, other: Self) -> Self

Get the disjunction of self and other

impl PartialEq for UpwardsClosedSet

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

impl TASpecification for UpwardsClosedSet

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