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 typeAP
- 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
All Methods Instance Methods Concrete Methods Modifier and Type Method Description BDDTransformer<L,AP>
compose(BDDTransformer<L,AP> other)
Returns the compositionh
ofthis
andother
such thath(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 bythis
.BDD
getBDD(int var)
Returns theBDD
used to compute the satisfiability of subformula with variable numbervar
.int
getNumberOfVars()
Returns the number of subformulas.int
hashCode()
-
Methods inherited from class net.automatalib.modelchecker.m3c.transformer.AbstractPropertyTransformer
isMust
-
-
-
-
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 BDDsdependencyGraph
- 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 BDDsedgeLabel
- of the edgeedgeProperty
- of the edgedependencyGraph
- 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 BDDsnumberOfVars
- 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 bythis
.- Specified by:
evaluate
in classAbstractPropertyTransformer<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 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<BDDTransformer<L,AP>,L,AP>
- Parameters:
other
- function which is first applied to an input- Returns:
- the composition of
this
andother
-
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 classAbstractPropertyTransformer<BDDTransformer<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
-
getBDD
public BDD getBDD(int var)
Returns theBDD
used to compute the satisfiability of subformula with variable numbervar
.- Parameters:
var
- index of the BDD to return- Returns:
- the
BDD
used to compute the satisfiability of subformula with variable numbervar
-
getNumberOfVars
public int getNumberOfVars()
Returns the number of subformulas.- Returns:
- the number of subformulas
-
-