BDDFactory

onera.pmlanalyzer.views.interference.model.formalisation.BDDFactory
class BDDFactory extends BaseBDDFactory[Int, BDD]

Class for a classic BDD Factory (variable are integer and BDD are JavaBDD)

Attributes

Graph
Supertypes
trait BaseBDDFactory[Int, BDD]
class Object
trait Matchable
class Any

Members list

Concise view

Value members

Concrete methods

def andBDD(left: BDD, right: BDD): BDD

Delegate BDD AND to JavaBDD factory

Delegate BDD AND to JavaBDD factory

Attributes

left

BDD

right

BDD

Returns:

the resulting BDD

def dispose(): Unit

Send dispose signal to JavaBDD factory

Send dispose signal to JavaBDD factory

Attributes

def getIthVar(i: Int): BDD

Return the ith var of the JavaBDD factory

Return the ith var of the JavaBDD factory

Attributes

i

the index of the BDD node

Returns:

BDD node

def getVar(variable: Int): BDD

Increment the number of produced variable and return the corresponding BDD

Increment the number of produced variable and return the corresponding BDD

Attributes

variable

the variable

Returns:

a BDD node

def getVarMap: Map[BDD, Int]

Build the map from BDD identifier to BDD

Build the map from BDD identifier to BDD

Attributes

Returns:

the mapping from BDD to labelled variable

def initFactory(numberOfVar: Int, cacheSize: Int): BDDFactory

Initialise a JavaBDD factory

Initialise a JavaBDD factory

Attributes

cacheSize

initial size of the cache table containing BDD nodes

numberOfVar

maximum number of variables in BDDs

Returns:

JavaBDD factory

def mkNode(variable: Int, high: BDD, low: BDD): BDD

Build a BDD bu applying the formula v.high + (neg v).low

Build a BDD bu applying the formula v.high + (neg v).low

Attributes

high

the high son

low

the low son

variable

the variable labelling the BDD

Returns:

the resulting BDD

def notBDD(arg: BDD): BDD

Delegate BDD NOT to JavaBDD

Delegate BDD NOT to JavaBDD

Attributes

arg

initial BDD

Returns:

negated BDD

def one(): BDD

Attributes

Returns:

one terminal

def orBDD(left: BDD, right: BDD): BDD

Delegate BDD OR to JavaBDD factory

Delegate BDD OR to JavaBDD factory

Attributes

left

BDD

right

BDD

Returns:

the resulting BDD

def produceVar(): BDD

Build a variable labelled by the current number of variable produced by the factory

Build a variable labelled by the current number of variable produced by the factory

Attributes

Returns:

BDD

def replaceVar(replace: Int, by: Int, in: BDD): BDD

Use JavaBDD replace to build new BDD where a given variable is replaced by another one

Use JavaBDD replace to build new BDD where a given variable is replaced by another one

Attributes

by

the new variable

in

the BDD

replace

the initial variable to replace

Returns:

the modified BDD

def reset(): Unit

Reinitialise the JavaBDD factory to initial variable number

Reinitialise the JavaBDD factory to initial variable number

Attributes

def zero(): BDD

Attributes

Returns:

zero terminal

Inherited methods

def andBDD(s: Iterable[BDD]): MyBDD

n-ary BDD and

n-ary BDD and

Attributes

s

set of BDD

Returns:

the resulting BDD

Inherited from:
BaseBDDFactory
def importBDD[OtherBDD <: BDD](bdd: OtherBDD, bddVar: Map[Int, OtherBDD]): MyBDD

Import a BDD in this factory from one coming from another factory

Import a BDD in this factory from one coming from another factory

Attributes

OtherBDD

the type of the other BDD

bdd

the other factory BDD

bddVar

the map from BDD node to variables

Returns:

the BDD imported in this factory

Inherited from:
BaseBDDFactory
def mkExactlyK(vs: Seq[Int], k: Int): MyBDD

Exactly k elements out of an ordered sequence of variables

Exactly k elements out of an ordered sequence of variables

Attributes

k

the number of variables that must be true

vs

the ordered sequence of variables

Returns:

the resulting BDD

Inherited from:
BaseBDDFactory
def mkImplies(left: BDD, right: BDD): MyBDD

BDD implication

BDD implication

Attributes

left

BDD

right

BDD

Returns:

the resulting BDD

Inherited from:
BaseBDDFactory
def orBDD(s: Iterable[BDD]): MyBDD

n-ary BDD or

n-ary BDD or

Attributes

s

the set of BDD

Returns:

the resulting BDD

Inherited from:
BaseBDDFactory