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 typeAP
- 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
All Methods Instance Methods Concrete Methods Modifier and Type Method Description ADDTransformer<L,AP>
compose(ADDTransformer<L,AP> other)
Returns the compositionh
ofthis
andother
such thath(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 bythis
.@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
-
-
-
-
Constructor Detail
-
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 ADDdependGraph
- of the formula that is currently being solved
-
ADDTransformer
public ADDTransformer(XDDManager<BooleanVector> ddManager)
Creates the identity function. This sets the internalADD
tonull
to avoid the construction of the ADD, which is very expensive. To prevent null-pointer exceptions when usinggetAdd()
, it can be checked withisIdentity()
.- 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 ADDedgeLabel
- of the edgeedgeProperty
- of the edgedependGraph
- of the formula that is currently being solved
-
-
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 bythis
.- Specified by:
evaluate
in classAbstractPropertyTransformer<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 compositionh
ofthis
andother
such thath(x) = this(other(x))
. TheisMust
attribute of the composition is set to theisMust
attribute ofthis
.- Specified by:
compose
in classAbstractPropertyTransformer<ADDTransformer<L,AP>,L,AP>
- Parameters:
other
- function which is first applied to an input- Returns:
- the composition of
this
andother
-
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 classAbstractPropertyTransformer<ADDTransformer<L,AP>,L,AP>
- Parameters:
atomicPropositions
- of the nodecompositions
- of the property transformers belonging to the outgoing edges and their target nodescurrentBlock
- 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
-
-