Struct Configuration 

pub struct Configuration {
    variable_assignment: HashMap<Variable, u32>,
    location_assignment: HashMap<Location, u32>,
}

Global configuration of in a threshold automaton

A configuration specifies how many processes are in each location of the threshold automaton and the valuation of the shared variables

Fields

variable_assignment: HashMap<Variable, u32>

Valuation of the shared variables

location_assignment: HashMap<Location, u32>

Number of processes per location

Implementations

impl Configuration

pub fn new<T, S>(variable_assignment: T, location_assignment: S) -> Self

where T: Into<HashMap<Variable, u32>>, S: Into<HashMap<Location, u32>>,

Create a new configuration

This function creates a new configuration with the given variable and location assignments.

The variable and location assignments are represented as HashMaps, where the keys are the variables and locations, and the values are the number of processes in the respective location or the value of the variable.

pub fn get_processes_in_location(&self, loc: &Location) -> u32

Number of processes in location loc

This function returns the number of processes in the given location loc. If the location is not known in the configuration, the function returns 0.

pub fn get_variable_value(&self, var: &Variable) -> u32

Current value of variable

This function returns the value of the variable var in the configuration. If the variable is not known in the configuration, the function returns 0.

pub fn variable_assignment(&self) -> impl Iterator<Item = (&Variable, &u32)>

Iterator over the variable assignment

This function returns an iterator over the variable assignment, where each item is a tuple of the variable and its value.

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

Iterator over the location assignment

This function returns an iterator over the location assignment, where each item is a tuple of the location and the number of processes in it.

pub fn apply_rule(&self, tr: &Transition) -> Option<Self>

Create the successor configuration after applying a transition

Returns None if the transition cannot be applied to the configuration. This can for example happen if the source location of the applied rule has no processes or not enough processes to apply the rule.

pub fn display_compact(&self) -> String

Returns a compact representation of the configuration skipping locations and variables which are assigned 0

Trait Implementations

impl Clone for Configuration

fn clone(&self) -> Configuration

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Configuration

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

Formats the value using the given formatter.

impl Display for Configuration

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

Formats the value using the given formatter.

impl PartialEq for Configuration

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