Struct InitRestriction 

pub struct InitRestriction {
    precondition_par: Conjunction<BooleanExpression<Parameter>>,
    precondition_loc: Conjunction<BooleanExpression<Location>>,
    precondition_var: Conjunction<BooleanExpression<Variable>>,
}

Restriction on the initial configuration of a run

The restriction is a conjunction of arbitrary boolean constraints, split by the kind of atoms they range over. Constraints on parameters are rigid, i.e., they hold at every position of a run.

Fields

precondition_par: Conjunction<BooleanExpression<Parameter>>

Conjunction of conditions on the parameters

precondition_loc: Conjunction<BooleanExpression<Location>>

Conjunction of conditions on the initial distribution of processes in the threshold automaton

precondition_var: Conjunction<BooleanExpression<Variable>>

Conjunction of conditions on the initial valuation of the shared variables

Implementations

impl InitRestriction

pub fn new_top() -> Self

Create a restriction that allows every initial configuration

pub fn new_parameter_constraint(constr: BooleanExpression<Parameter>) -> Self

Create a restriction consisting of a single parameter constraint

pub fn new_location_constraint(constr: BooleanExpression<Location>) -> Self

Create a restriction consisting of a single constraint on the initial distribution of processes

pub fn new_variable_constraint(constr: BooleanExpression<Variable>) -> Self

Create a restriction consisting of a single constraint on the initial valuation of the shared variables

pub fn is_top(&self) -> bool

Check whether the restriction allows every initial configuration

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

Disjunction of two restrictions, if a sound merge exists

The restriction is a conjunction of one condition per kind of atom. Because of this, the disjunction is only representable if both restrictions differ in at most one kind: (p && l1 && v) || (p && l2 && v) is equal to p && (l1 || l2) && v.

pub fn parameter_constraints( &self, ) -> &Conjunction<BooleanExpression<Parameter>>

Conditions on the parameters

pub fn location_constraints(&self) -> &Conjunction<BooleanExpression<Location>>

Conditions on the initial distribution of processes

pub fn variable_constraints(&self) -> &Conjunction<BooleanExpression<Variable>>

Conditions on the initial valuation of the shared variables

Trait Implementations

impl And for InitRestriction

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

Get the conjunction of self and other

impl BitAnd for InitRestriction

type Output = InitRestriction

The resulting type after applying the & operator.

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

Performs the & operation.

impl Clone for InitRestriction

fn clone(&self) -> InitRestriction

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InitRestriction

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

Formats the value using the given formatter.

impl Default for InitRestriction

fn default() -> InitRestriction

Returns the “default value” for a type.

impl Display for InitRestriction

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

Formats the value using the given formatter.

impl PartialEq for InitRestriction

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