Struct TargetConfig 

pub struct TargetConfig {
    lower_bounds: HashMap<Location, u32>,
    locations_not_covered: HashSet<Location>,
    variable_constr: LIAVariableConstraint,
}

Upward closed set of configurations representing a target set of configurations

This type specifies an upwards closed set of configurations. It can be seen as a minimal basis specifying a set of configurations

Fields

lower_bounds: HashMap<Location, u32>

Map with location + number of processes at least in there Set of locations where no process should be

locations_not_covered: HashSet<Location>

Location should not be covered by any processes

variable_constr: LIAVariableConstraint

conjunct of variable constraints

Implementations

impl TargetConfig

fn new_unconstrained() -> Self

Create a new specification object that contains all possible configurations

fn new_loc_not_covered(loc: Location) -> Self

Create a new specification that contains all configurations where loc is not covered by any processes

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

Create a new specification that requires all configurations in cover to be covered by at least one process

pub fn new_general_cover<L: IntoIterator<Item = (Location, u32)>>( cover: L, ) -> Result<Self, ReachabilityTransformationError>

Create a new specification that requires all configurations in cover to be covered by at the given amount of processes

pub fn new_reach<LI: IntoIterator<Item = Location>, LII: IntoIterator<Item = Location>>( cover: LI, uncover: LII, ) -> Result<Self, ReachabilityTransformationError>

Create a new specification that requires all configurations in cover to be covered by at least one process and all locations in uncover to be empty

pub fn new_general_reach<U: IntoIterator<Item = Location>, C: IntoIterator<Item = (Location, u32)>>( cover: C, uncover: U, ) -> Result<Self, ReachabilityTransformationError>

Create a new specification that requires all configurations in cover to be covered by at least the specified amount of processes and all locations in uncover to be empty

pub fn get_locations_appearing(&self) -> HashSet<&Location>

Get all locations that appear in the target specification

pub fn get_variable_constraint(&self) -> &LIAVariableConstraint

Get the variable constraint appearing in the target configuration

pub fn new_reach_with_var_constr<LC: Into<HashMap<Location, u32>>, LU: Into<HashSet<Location>>>( locs: LC, uncover: LU, var_constr: BooleanExpression<Variable>, ) -> Result<Self, ReachabilityTransformationError>

Create a new target configuration constraint

fn new_with_var_constr( var_constr: BooleanExpression<Variable>, ) -> Result<Self, ReachabilityTransformationError>

Create a new specification contains all configurations where var_constr holds

fn is_reachability_constraint(&self) -> bool

Check whether this constraint is a reachability constraint

A reachability constraint requires at least one location to be empty.

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

Get iterator over the locations that should be covered by processes with the least amount of processes

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

Locations that should not be covered

pub fn into_disjunct_with_name<S: ToString>( self, name: S, ) -> DisjunctionTargetConfig

Create a DisjunctionTargetConfig with the given name from the single target location

fn try_from_loc_constr( constr: (IntegerExpression<Location>, ComparisonOp, IntegerExpression<Location>), ) -> Result<Self, ReachabilityTransformationError>

Attempt to parse an DisjunctionTargetConfig from a location constraint

This function can be used to attempt to extract an upwards closed set of configurations from a single boolean constraint over location variables

This function returns an error if the specification does not correspond to an upwards closed set of configurations. See

Trait Implementations

impl And for TargetConfig

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

Get the conjunction of self and other

impl Clone for TargetConfig

fn clone(&self) -> TargetConfig

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TargetConfig

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

Formats the value using the given formatter.

impl Display for TargetConfig

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

Formats the value using the given formatter.

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

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

Encode the type into an SMT expression

impl PartialEq for TargetConfig

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