Struct UpwardsClosedClause 

pub struct UpwardsClosedClause {
    locs_no_procs: HashSet<Location>,
    locs_lower_bounds: HashMap<Location, u32>,
    variable_constr: LIAVariableConstraint,
}

Description of an upwards closed set of configurations of a threshold automaton

An upwards closed set of configurations can be seen as the conjunction of three different types of constraints:

• a set of locations which are not allowed to contain any processes
• a map of locations to integer bounds, where the bounds represent minimal the number of processes that need to be present in the respective location
• constraints on the shared variable evaluations

Any configuration of a threshold automaton that fulfills the constraints is then said to be in the set.

This type should usually not be created directly. Instead, use the UpwardsClosedSet type (with a single clause).

Fields

locs_no_procs: HashSet<Location>

Location should not be covered by any processes

locs_lower_bounds: HashMap<Location, u32>

Map with location + number of processes at least in there

variable_constr: LIAVariableConstraint

conjunct of variable constraints

Implementations

impl UpwardsClosedClause

pub fn variable_constr(&self) -> &LIAVariableConstraint

Get the constraint over the shared variable valuations

pub fn locs_to_cover(&self) -> impl Iterator<Item = (&Location, &u32)>

Returns an iterator over locations and the respective lower bound on how many processes need to be in the location to be in the set

pub fn locs_to_uncover(&self) -> impl Iterator<Item = &Location>

Returns the locations where no process is allowed to be in

pub fn new_top() -> Self

Create a new upwards closed set that contains all possible configurations

pub fn is_top(&self) -> bool

Check whether this clause is a tautology, i.e., contains all possible configurations

fn new() -> Self

Creates a new empty set of atomic propositions

Such an upwards closed set is equivalent to a constraint true or the set of all configurations

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

Add a locations where at least one process must be present

If a lower bound constraint for a specific location has been previously added, this function will merge the constraints by taking the maximum of the lower bounds

fn with_lower_bounds<I: Borrow<Location>, N: Into<u32>, L: IntoIterator<Item = (I, N)>>( self, cover: L, ) -> Self

Add lower bounds for a set of locations

If a lower bound constraint for a specific location has been previously added, this function will merge the constraints by taking the maximum of the lower bounds

fn with_locs_to_empty<I: Borrow<Location>, L: IntoIterator<Item = I>>( self, locs: L, ) -> Self

Add locations which are not allowed to be covered

fn with_variable_constraint(self, constr: LIAVariableConstraint) -> Self

Add a constraint on the shared variable valuation

If a constraint has been previously added, the resulting variable constraint will be the conjunction of the previous and the new one

fn contains_reachability_constraint(&self) -> bool

Check whether the upwards closed set contains a reachability constraint, i.e., a constraint where at least one location is not allowed to be covered

Trait Implementations

impl And for UpwardsClosedClause

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

Get the conjunction of self and other

impl BitAnd for UpwardsClosedClause

type Output = UpwardsClosedClause

The resulting type after applying the & operator.

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

Performs the & operation.

impl Clone for UpwardsClosedClause

fn clone(&self) -> UpwardsClosedClause

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UpwardsClosedClause

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

Formats the value using the given formatter.

impl Display for UpwardsClosedClause

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

Formats the value using the given formatter.

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

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

Encode the type into an SMT expression

impl PartialEq for UpwardsClosedClause

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

impl TASpecification for UpwardsClosedClause

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