Package net.automatalib.modelchecker.m3c.formula

Class DependencyGraph<L,AP>

java.lang.Object

net.automatalib.modelchecker.m3c.formula.DependencyGraph<L,AP>

Type Parameters:

L - edge label type

AP - atomic proposition type

public class DependencyGraph<L,AP>
extends Object

A dependency graph is used to represent a hierarchical equational system.

Constructor Summary

Constructors

Constructor	Description
DependencyGraph(FormulaNode<L,AP> root)

Method Summary

Modifier and Type	Method	Description
FormulaNode<L,AP>	getAST()	Returns the abstract syntax tree of the input formula after it has been transformed into negation normal form.
EquationalBlock<L,AP>	getBlock(int index)	Returns the equational block for the given index.
List<EquationalBlock<L,AP>>	getBlocks()	Returns all equational blocks of the equational system.
List<FormulaNode<L,AP>>	getFormulaNodes()	Returns the list of all subformulas.
int	getNumVariables()	Returns the number of variables which is equal to the number of subformulas.
boolean[]	toBoolArray(BitSet satisfiedVars)	Returns a boolean array that is sized according to getNumVariables() such that every index provided in satisfiedVars is set to true.

Methods inherited from class java.lang.Object

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

Constructor Detail

DependencyGraph

public DependencyGraph(FormulaNode<L,AP> root)

Method Detail

getBlock

public EquationalBlock<L,AP> getBlock(int index)

Returns the equational block for the given index.

Parameters:

index - index of the equational block to return

Returns:

the equational block at the given index.

getNumVariables

public int getNumVariables()

Returns the number of variables which is equal to the number of subformulas.

Returns:

the number of variables.

getFormulaNodes

public List<FormulaNode<L,AP>> getFormulaNodes()

Returns the list of all subformulas.

Returns:

the list of all subformulas.

getBlocks

public List<EquationalBlock<L,AP>> getBlocks()

Returns all equational blocks of the equational system.

Returns:

all equational blocks of the equational system.

getAST

public FormulaNode<L,AP> getAST()

Returns the abstract syntax tree of the input formula after it has been transformed into negation normal form.

Returns:

the abstract syntax tree in negation normal form.

toBoolArray

public boolean[] toBoolArray(BitSet satisfiedVars)

Returns a boolean array that is sized according to getNumVariables() such that every index provided in satisfiedVars is set to true.

Parameters:

satisfiedVars - the set of indices that should be set to true

Returns:

a boolean array that is sized according to getNumVariables() such that every index provided in satisfiedVars is set to true.