Package net.automatalib.modelchecker.m3c.transformer

Class BDDTransformer<L,AP>

java.lang.Object

net.automatalib.modelchecker.m3c.transformer.AbstractPropertyTransformer<BDDTransformer<L,AP>,L,AP>

net.automatalib.modelchecker.m3c.transformer.BDDTransformer<L,AP>

Type Parameters:

L - edge label type

AP - atomic proposition type

public class BDDTransformer<L,AP>
extends AbstractPropertyTransformer<BDDTransformer<L,AP>,L,AP>

A BDDTransformer represents a property transformer for a list of BDDs (Binary Decision Diagrams), one per subformula.

Constructor Summary

Constructors

Constructor	Description
BDDTransformer(BDDManager bddManager, int numberOfVars)	The Property Transformer representing the identity function.
BDDTransformer(BDDManager bddManager, L edgeLabel, TP edgeProperty, DependencyGraph<L,AP> dependencyGraph)	Constructor used to create the property transformer for an edge.
BDDTransformer(BDDManager bddManager, DependencyGraph<L,AP> dependencyGraph)	Constructor used to initialize the property transformer of a node.

Method Summary

Modifier and Type	Method	Description
BDDTransformer<L,AP>	compose(BDDTransformer<L,AP> other)	Returns the composition h of this and other such that h(x) = this(other(x)).
BDDTransformer<L,AP>	createUpdate(Set<AP> atomicPropositions, List<BDDTransformer<L,AP>> compositions, EquationalBlock<L,AP> currentBlock)	Returns the updated property transformer of a node.
boolean	equals(@Nullable Object o)
BitSet	evaluate(boolean[] input)	Returns the set of variable numbers of subformulas y with f(input)=y, where f is the property transformer represented by this.
BDD	getBDD(int var)	Returns the BDD used to compute the satisfiability of subformula with variable number var.
int	getNumberOfVars()	Returns the number of subformulas.
int	hashCode()

Methods inherited from class net.automatalib.modelchecker.m3c.transformer.AbstractPropertyTransformer

isMust

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

BDDTransformer

public BDDTransformer(BDDManager bddManager,
                      DependencyGraph<L,AP> dependencyGraph)

Constructor used to initialize the property transformer of a node.

Parameters:

bddManager - used to create the BDDs

dependencyGraph - of the formula that is currently being solved

BDDTransformer

public BDDTransformer(BDDManager bddManager,
                      L edgeLabel,
                      TP edgeProperty,
                      DependencyGraph<L,AP> dependencyGraph)

Constructor used to create the property transformer for an edge.

Type Parameters:

TP - edge property type

Parameters:

bddManager - used to create the BDDs

edgeLabel - of the edge

edgeProperty - of the edge

dependencyGraph - of the formula that is currently being solved

BDDTransformer

public BDDTransformer(BDDManager bddManager,
                      int numberOfVars)

The Property Transformer representing the identity function.

Parameters:

bddManager - used to create the BDDs

numberOfVars - the number of subformulas

Method Detail

evaluate

public BitSet evaluate(boolean[] input)

Description copied from class: AbstractPropertyTransformer

Returns the set of variable numbers of subformulas y with f(input)=y, where f is the property transformer represented by this.

Specified by:

evaluate in class AbstractPropertyTransformer<BDDTransformer<L,AP>,L,AP>

Parameters:

input - a boolean array representing a set of subformulas

Returns:

the set of variable numbers of subformulas

compose

public BDDTransformer<L,AP> compose(BDDTransformer<L,AP> other)

Description copied from class: AbstractPropertyTransformer

Returns the composition h of this and other such that h(x) = this(other(x)). The isMust attribute of the composition is set to the isMust attribute of this.

Specified by:

compose in class AbstractPropertyTransformer<BDDTransformer<L,AP>,L,AP>

Parameters:

other - function which is first applied to an input

Returns:

the composition of this and other

createUpdate

public BDDTransformer<L,AP> createUpdate(Set<AP> atomicPropositions,
                                               List<BDDTransformer<L,AP>> compositions,
                                               EquationalBlock<L,AP> currentBlock)

Description copied from class: AbstractPropertyTransformer

Returns the updated property transformer of a node.

Specified by:

createUpdate in class AbstractPropertyTransformer<BDDTransformer<L,AP>,L,AP>

Parameters:

atomicPropositions - of the node

compositions - of the property transformers belonging to the outgoing edges and their target nodes

currentBlock - the block which is considered during this update

Returns:

the updated property transformer of a node

getBDD

public BDD getBDD(int var)

Returns the BDD used to compute the satisfiability of subformula with variable number var.

Parameters:

var - index of the BDD to return

Returns:

the BDD used to compute the satisfiability of subformula with variable number var

getNumberOfVars

public int getNumberOfVars()

Returns the number of subformulas.

Returns:

the number of subformulas

hashCode

public int hashCode()

Overrides:

hashCode in class Object

equals

public boolean equals(@Nullable Object o)

Overrides:

equals in class Object