edu.wis.jtlv.env.module
Class ModuleBDDDefine

java.lang.Object
  edu.wis.jtlv.env.module.ModuleEntity
      edu.wis.jtlv.env.module.ModuleBDDDefine

public class ModuleBDDDefine
extends ModuleEntity

This object represents a define declaration field. It is degenerate in a way by not supporting the 'other', 'prime', and 'unprime' procedures.

Since define can refer to other defines, fields, values, etc., and has no real entity of its own (i.e. marco), define is declared in two stages. The first is only for declaring its existence. The second is for real evaluation. The second stage is done just-in-time (per demand), i.e. if not refer to, the second stage will not be execute.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

ModuleBDDDefine(java.lang.String a_path, java.lang.String name)
The main public constructor.

Method Summary

void	attachStmt(edu.wis.jtlv.env.core.smv.eval.StmtDefineOperator stmt) Attach an expression to the define.
BDD	evalBDD() Evaluate the statement, and return the BDD value.
java.lang.Integer[]	evalInt() Evaluate the statement, and return an array of integer values.
edu.wis.jtlv.env.core.smv.eval.AbstractElement	getStmt() Getter for the parsing statement.
boolean	isInitiated() Check whether this define was attached with an expression.

Methods inherited from class edu.wis.jtlv.env.module.ModuleEntity

equals, getName, getPath, getSimpleArrayName, strongEquals, toFullString, toString

Methods inherited from class java.lang.Object

getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

ModuleBDDDefine

public ModuleBDDDefine(java.lang.String a_path,
                       java.lang.String name)

The main public constructor. Given a path, a name, a new define field is created with no associated statement.
In order to complete the instantiation properly, an expression most be attached.

Parameters:

a_path - A path to the field.

name - A name for this field.

See Also:

attachStmt(StmtDefineOperator)

Method Detail

attachStmt

public void attachStmt(edu.wis.jtlv.env.core.smv.eval.StmtDefineOperator stmt)

Attach an expression to the define.

Parameters:

stmt - The parsing statement to attach.

See Also:

ModuleBDDDefine(String, String), getStmt()

getStmt

public edu.wis.jtlv.env.core.smv.eval.AbstractElement getStmt()

Getter for the parsing statement.

Returns:

The parsing statement attached to this define.

See Also:

attachStmt(StmtDefineOperator)

isInitiated

public boolean isInitiated()

Check whether this define was attached with an expression. (i.e. this define can continue to the second stage.)

Returns:

true if this define is attached with an expression, false otherwise.

See Also:

attachStmt(StmtDefineOperator)

evalBDD

public BDD evalBDD()

Evaluate the statement, and return the BDD value.

Returns:

The BDD value of the statement.

See Also:

attachStmt(StmtDefineOperator), evalInt()

evalInt

public java.lang.Integer[] evalInt()

Evaluate the statement, and return an array of integer values.

Returns:

An array of integer values of the statement.

See Also:

attachStmt(StmtDefineOperator), evalBDD()