Struct ZCSBuilder 

pub struct ZCSBuilder<'a> {
    cs: ZCS<'a>,
}

Builder for constructing a symbolic 01-CS

This builder takes a BDDManager and an IntervalThresholdAutomaton and derives the corresponding symbolic 01-counter system (ZCS).

The builder encodes the initial states, the symbolic transitions for each rule, and the symbolic transition relation as a single BDD.

Fields

cs: ZCS<'a>

01-CS (ZCS) that is constructed by the builder

Implementations

impl<'a> ZCSBuilder<'a>

pub fn new(mgr: &BDDManager, aut: &'a IntervalThresholdAutomaton) -> Self

create a new symbolic 01-CS builder

pub fn initialize(&mut self)

1. encode initial states
2. encode each rule as a transition bdd
3. encode entire transition relation

fn build_initial_states(&self) -> ZCSStates

Build the bdd that represents the set of initial states

fn build_symbolic_transitions(&self) -> Vec<SymbolicTransition>

builds all symbolic transitions for all rules of the TA

fn build_symbolic_transition(&self, rule: &IntervalTARule) -> SymbolicTransition

Build a symbolic transition for a given rule of the threshold automaton

Steps

1. constraints for locations
2. add encoded rule_id to symbolic_transition
3. check if abstract guard is satisfied
4. check if effects of rule are applied. i.e., effects of update vector and resets

fn build_location_constraints_for_rule(&self, rule: &IntervalTARule) -> BDD

builds location constraints for a given rule from location from to location to

1. from and to_prime have to be set
2. from_prime and to can either be either empty or occupied, the value for all other locations has to be equal

fn build_effect_constraints_for_rule(&self, rule: &IntervalTARule) -> BDD

builds the guard constraints for a given rule

1. reset -> primed interval is the initial interval, i.e., I_0 = [0,1)
2. increment/decrement -> primed interval is the next/previous interval or stays in the same interval
3. no effect -> primed interval stays in the same interval

fn build_reset_constraints_for_shared_var(&self, shared: &Variable) -> &BDD

builds the reset constraint for a given shared variable i.e., the primed interval is the initial interval I_0 = [0,1)

fn build_update_constraints_for_shared_var( &self, shared: &Variable, effect: &IntervalActionEffect, ) -> BDD

builds the update constraint for a given shared variable for effect which is either a increment or decrement i.e., the primed interval is the next/previous interval or stays in the same interval

fn build_symbolic_transition_relation(&self) -> BDD

builds the symbolic transition relation as a single bdd assume that all symbolic transitions are already stored in the cs

fn construct_bdd_guard(&self, guard: &IntervalConstraint) -> BDD

Given an abstract guard as an IntervalGuard, Construct a BDD that replaces every abstract Interval with its respective BDD

pub fn build(self) -> ZCS<'a>

build the symbolic 01-CS

Trait Implementations

impl<'a> Debug for ZCSBuilder<'a>

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

Formats the value using the given formatter.