Struct ZCS 

pub struct ZCS<'a> {
    bdd_mgr: BddVarManager,
    ata: &'a IntervalThresholdAutomaton,
    initial_states: ZCSStates,
    transitions: Vec<SymbolicTransition>,
    transition_relation: BDD,
}

Type representing a symbolic 01-CS (ZCS)

Fields

bdd_mgr: BddVarManager

bdd manager to perform all bdd operations

ata: &'a IntervalThresholdAutomaton

underlying abstract threshold automaton

initial_states: ZCSStates

initial states of the 01-CS (ZCS)

transitions: Vec<SymbolicTransition>

set of transitions of the 01-CS (ZCS)

transition_relation: BDD

transition relation of the 01-CS (ZCS) as a single bdd

Implementations

impl ZCS<'_>

pub fn compute_successor( &self, from: ZCSStates, with: SymbolicTransition, ) -> ZCSStates

Computes the set of successors for a symbolic state from rule_ids for with are not abstracted

pub fn compute_predecessor(&self, to: ZCSStates) -> ZCSStates

Computes the set of predecessors for a symbolic state to Bdd variables for rule_ids are not abstracted

pub fn new_empty_sym_state(&self) -> ZCSStates

returns a new empty set of states

pub fn new_full_sym_state(&self) -> ZCSStates

returns a new “full” set of states

pub fn get_sym_state_for_loc(&self, loc: &Location) -> ZCSStates

returns the set of states where a given location is occupied

pub fn get_sym_state_for_shared_interval( &self, shared: &Variable, interval: &Interval, ) -> ZCSStates

returns the set of states where a given shared variable is in the given ‘interval’

pub fn get_sym_state_for_rule(&self, rule: &IntervalTARule) -> ZCSStates

returns the set of states where the rule_id of a given ‘rule’ is applied

pub fn abstract_rule_vars(&self, states: ZCSStates) -> ZCSStates

returns the symbolic states that abstracts rule_ids from ‘states’

pub fn initial_states(&self) -> ZCSStates

set of initial states of the 01-CS (ZCS)

pub fn transitions(&self) -> impl Iterator<Item = &SymbolicTransition>

returns an iterator over the encoded transition rules

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

returns an iterator over the locations of the underlying threshold automaton

pub fn variables(&self) -> impl Iterator<Item = &Variable>

returns an iterator over the shared variables of the underlying threshold automaton

pub fn get_ordered_intervals_for_shared( &self, shared: &Variable, ) -> &Vec<Interval>

returns an iterator over the ordered intervals for a given shared variable

pub fn get_sym_var_assignment( &self, assign: VariableAssignment, ) -> SymbolicVariableAssignment

returns the symbolic variable assignment for a given variable assignment

pub fn has_decrements(&self) -> bool

returns if the underlying threshold automaton contains any decrementing rules

Trait Implementations

impl<'a> Clone for ZCS<'a>

fn clone(&self) -> ZCS<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for ZCS<'a>

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

Formats the value using the given formatter.