Module net.automatalib.modelchecker.m3c

Package net.automatalib.modelchecker.m3c.transformer

Class ADDTransformer<L,AP>

java.lang.Object

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

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

Type Parameters:

L - edge label type

AP - atomic proposition type

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

An ADDTransformer represents a property transformer for a single ADD (Algebraic Decision Diagram).

Constructor Summary

Constructors

Constructor	Description
ADDTransformer(XDDManager<BooleanVector> ddManager)	Creates the identity function.
ADDTransformer(XDDManager<BooleanVector> xddManager, L edgeLabel, TP edgeProperty, DependencyGraph<L,AP> dependGraph)	Constructor used to create the property transformer for an edge.
ADDTransformer(XDDManager<BooleanVector> xddManager, DependencyGraph<L,AP> dependGraph)	Constructor used to initialize the property transformer of a node.

Method Summary

Modifier and Type	Method	Description
ADDTransformer<L,AP>	compose(ADDTransformer<L,AP> other)	Returns the composition h of this and other such that h(x) = this(other(x)).
ADDTransformer<L,AP>	createUpdate(Set<AP> atomicPropositions, List<ADDTransformer<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.
@Nullable XDD<BooleanVector>	getAdd()	Returns the ADD which represents the property transformer.
int	hashCode()
boolean	isIdentity()	Returns whether the property transformer is the identity function.

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 Details

ADDTransformer

public ADDTransformer(XDDManager<BooleanVector> xddManager,
 DependencyGraph<L,AP> dependGraph)

Constructor used to initialize the property transformer of a node.

Parameters:

xddManager - used to create the ADD

dependGraph - of the formula that is currently being solved

ADDTransformer

public ADDTransformer(XDDManager<BooleanVector> ddManager)

Creates the identity function. This sets the internal ADD to null to avoid the construction of the ADD, which is very expensive. To prevent null-pointer exceptions when using getAdd(), it can be checked with isIdentity().

Parameters:

ddManager - used to create the ADD

ADDTransformer

public ADDTransformer(XDDManager<BooleanVector> xddManager,
 L edgeLabel,
 TP edgeProperty,
 DependencyGraph<L,AP> dependGraph)

Constructor used to create the property transformer for an edge.

Type Parameters:

TP - edge property type

Parameters:

xddManager - used to create the ADD

edgeLabel - of the edge

edgeProperty - of the edge

dependGraph - of the formula that is currently being solved

Method Details

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<ADDTransformer<L,AP>,L,AP>

Parameters:

input - a boolean array representing a set of subformulas

Returns:

the set of variable numbers of subformulas

compose

public ADDTransformer<L,AP> compose(ADDTransformer<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<ADDTransformer<L,AP>,L,AP>

Parameters:

other - function which is first applied to an input

Returns:

the composition of this and other

createUpdate

public ADDTransformer<L,AP> createUpdate(Set<AP> atomicPropositions,
 List<ADDTransformer<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<ADDTransformer<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

getAdd

public @Nullable XDD<BooleanVector> getAdd()

Returns the ADD which represents the property transformer.

Returns:

the ADD which represents the property transformer or null if the property transformer is the identity function

isIdentity

@EnsuresNonNullIf(result=false,
                  expression={"add","getAdd()"})
public boolean isIdentity()

Returns whether the property transformer is the identity function.

Returns:

true if the property transformer is the identity function, false otherwise

hashCode

public int hashCode()

Overrides:

hashCode in class Object

equals

public boolean equals(@Nullable Object o)

Overrides:

equals in class Object