engin
Class Engin

java.lang.Object
  engin.Engin

public class Engin
extends java.lang.Object

Engin

This is where all the computations take place. The engine can be set into three different threaded mode :

• verifying the formula from the initial state
• getting all the states verifying a formula
• LMP constraints verifications

Copyright(c) 2005 Université Laval, LSFM research group.

Version:

1.0

Author:

Nicolas Richard

Nested Class Summary

class

Engin.Runner Runner This class is a thread which starts the computation.

Field Summary

static int	GET_STATES_VERIFYING_A_FORMULA_MODE In this mode, the thread will determines which states from the state space verify the formula
static int	USE_BIGDECIMAL In this mode, the engine will use BigDecimal structures for increased accuracy at the expense of reduces performance.
static int	USE_DOUBLE In this mode, the engine will use simple double real numbers.
static int	USE_HASH In this mode, the engine will use regular has table based data structures.
static int	USE_MTBDD In this mode, the engine will use multiterminal binary decison diagrams (MTBDDs) in order to save memory.
static int	VERIFY_A_FORMULA_MODE In this mode, the thread will verify if the initial state verifies the formula
static int	VERIFY_CONSTRAINT_MODE In this mode, the thread will verify if all the LMP constraints are verified by the system

Constructor Summary

Engin()
Default constructor.

Engin(java.lang.String str, int mode)
Test constructor, to compute the system size.

Method Summary

void	addEnginListener(EnginListener e) Registers a listener to the engine
java.util.HashMap	computeProbabilities(IntervalList list, java.lang.String act) Compute the probability P[a](x, list), i.e. the probability to reach a certain point of the list from any x point.
java.util.ArrayList	findZeroes(Expression exp, Variable var, Interval inter, double threshold) This method finds the intersection points between a mathematical expression and a threshold, on the interval closure inter.
java.util.ArrayList	findZeroesBigDecimal(Expression exp, Variable var, Interval inter, double threshold) This method finds the intersection points between a mathematical expression and a threshold, on the interval closure inter.
java.util.ArrayList	findZeroesDouble(Expression exp, Variable var, Interval inter, double threshold) This method finds the intersection points between a mathematical expression and a threshold, on the interval closure inter.
int	getCalculationMode() Returns the calculation mode used ...
Formula	getFormula() Returns the formula stored in the engine.
LogicParser	getLogicParser() Returns the logical parser used by the engine to analyse formulae
int	getNbIteration() Returns the maximum number of iterations the function findZeroes can make to find polarity change.
Parser	getParser() Returns the expression parser used by the engine used to analyse the expressions attached to the transitions
double	getPrecision() Returns the smallest unit used during the computation of findZeroes.
ProbSystem	getProbSystem() Returns the probabilistic on which the engine performs the computations
int	getSegmentation() Returns the number of segments that the findZeroes function will build while attempting to find a polarity switch.
IntervalList	getStatesVerifying(Formula f) Returns all the states verifying a formula using the system loaded in the engine.
IntervalList	getStatesVerifying(Formula f, int level) Returns all the states verifying a formula using the system loaded in the engine.
int	getStructMode() Returns the current data structure mode used.
Variable	getX() Returns the x variable definition
Variable	getY() Returns the y variable definition
boolean	highestPForTransition(Transition transition, double q) Returns true if q is the highest probability of the transition.
void	libere(ProbSystem s) Free the memory used by the previous probabilitic system.
java.lang.String	loadFormula(java.io.File file) Loads the formula history from the specified file
void	loadProbSystem(java.io.File filename) Loads a probabilistic system from a file.
void	loadProbSystem(java.io.Reader reader, int numberOfLines) Loads a probabilistic system from a reader.
void	loadProbSystem(java.lang.String s) Loads a probabilistic system from a string.
ExpressionProgram	parseExp(java.lang.String exp) Parse a string representing an expression attached to a transition to build an expression object recognizable by the JavaMath library.
Formula	parseFormula(java.lang.String formula) Parse a string representing a formula (usually from the formula history) in order to build a formula tree that can be analysedby the engine.
void	removeEnginListener(EnginListener e) Remove a listener from the engine
void	run(int mode) Use to perform ths computation in a separate thread.
boolean	satisfies(ProbSystem s, Formula f) Checks wether of not a probabilistic system does verify a formula.
IntervalList	separation(java.util.HashMap fct, Variable var, double q) Returns all the x values for which the probability obtained from the probabilistic expression is greater than q.
void	setCalculationMode(int calculationMode) Sets the calculation mode for the findZeroes method.
void	setEnginTrace(EnginTraceDialog trace) Register a trace verification object for use during formula verification
void	setFormula(Formula formula) This method register a formula to the engine, in order to perform its verification.
void	setNbIteration(int nbIter) Sets the maximum number of iterations the findZeroes can make to find zeroes.
void	setPrecision(double precision) Sets the smalles unit to be used by the function findZeroes.
void	setProbSystem(ProbSystem s) This method replace the currently attached probabilistic system with a new one.
void	setProgress(ProgressDialog progress) Attach a progress bar to the engine.
void	setSegmentation(int segmentation) Sets the number of segments the findZeroes method must build in order to attempt to find a switch of polarity.
void	setStructMode(int structMode) Type of data structures used to store the system.
boolean	verifySystemConstraints() This function verifies that the system does indeed satisfies the LMP constraints : 0 <= P_a(x,S) < 1

Methods inherited from class java.lang.Object

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

Field Detail

VERIFY_A_FORMULA_MODE

public static final int VERIFY_A_FORMULA_MODE

In this mode, the thread will verify if the initial state verifies the formula

See Also:

Constant Field Values

GET_STATES_VERIFYING_A_FORMULA_MODE

public static final int GET_STATES_VERIFYING_A_FORMULA_MODE

In this mode, the thread will determines which states from the state space verify the formula

See Also:

Constant Field Values

VERIFY_CONSTRAINT_MODE

public static final int VERIFY_CONSTRAINT_MODE

In this mode, the thread will verify if all the LMP constraints are verified by the system

See Also:

Constant Field Values

USE_DOUBLE

public static final int USE_DOUBLE

In this mode, the engine will use simple double real numbers.

See Also:

Constant Field Values

USE_BIGDECIMAL

public static final int USE_BIGDECIMAL

In this mode, the engine will use BigDecimal structures for increased accuracy at the expense of reduces performance.

See Also:

Constant Field Values

USE_MTBDD

public static final int USE_MTBDD

In this mode, the engine will use multiterminal binary decison diagrams (MTBDDs) in order to save memory.

See Also:

Constant Field Values

USE_HASH

public static final int USE_HASH

In this mode, the engine will use regular has table based data structures. They accelerate the operations, but consume more memory.

See Also:

Constant Field Values

Constructor Detail

Engin

public Engin()

Default constructor. Initialize a new expression parser, a new logical parser(for formulas) and a standard reduced centered normal law table.

Engin

public Engin(java.lang.String str,
             int mode)

Test constructor, to compute the system size. Used only the tests involving the sizeOf class.

Parameters:

str - the name of the file to load

mode - the engine mode (MTBDDs or Hashtable)

Method Detail

getParser

public Parser getParser()

Returns the expression parser used by the engine used to analyse the expressions attached to the transitions

Returns:

the expression parser used by the engine

getLogicParser

public LogicParser getLogicParser()

Returns the logical parser used by the engine to analyse formulae

Returns:

the logical parser used by the engine

getX

public Variable getX()

Returns the x variable definition

Returns:

a Variable object representing x

getY

public Variable getY()

Returns the y variable definition

Returns:

a Variable object representing y

getProbSystem

public ProbSystem getProbSystem()

Returns the probabilistic on which the engine performs the computations

Returns:

the probabilistic attached to the engine

libere

public void libere(ProbSystem s)

Free the memory used by the previous probabilitic system.

Parameters:

s - the probabilistic system to free from the memory.

setProbSystem

public void setProbSystem(ProbSystem s)

This method replace the currently attached probabilistic system with a new one. The atomic propositions need to be purged because they no longer apply. Also note that the system is not verified against the LMP constraints.

Parameters:

s - the new probabilistic system to be attached to the engine

setProgress

public void setProgress(ProgressDialog progress)

Attach a progress bar to the engine. Very useful to provide feedback to the user.

Parameters:

progress - the progress bar to attach

parseExp

public ExpressionProgram parseExp(java.lang.String exp)

Parse a string representing an expression attached to a transition to build an expression object recognizable by the JavaMath library.

Parameters:

exp - the string to convert into an expression

Returns:

an expression recognizable by JavaMath

parseFormula

public Formula parseFormula(java.lang.String formula)

Parse a string representing a formula (usually from the formula history) in order to build a formula tree that can be analysedby the engine.

Parameters:

formula - a string representing the formula tree

Returns:

a formula tree analysable by the engine

setEnginTrace

public void setEnginTrace(EnginTraceDialog trace)

Register a trace verification object for use during formula verification

Parameters:

trace - a trace verification object

getPrecision

public double getPrecision()

Returns the smallest unit used during the computation of findZeroes.

Returns:

the smallest unit (usually 1E-precision)

See Also:

Engine#findZeroes

setPrecision

public void setPrecision(double precision)

Sets the smalles unit to be used by the function findZeroes. This value must be stricty positive, else this methods does nothing.

Parameters:

precision - the smallest unit to be used during findZeroes computation

See Also:

findZeroes(edu.hws.jcm.data.Expression, edu.hws.jcm.data.Variable, data.Interval, double)

setSegmentation

public void setSegmentation(int segmentation)

Sets the number of segments the findZeroes method must build in order to attempt to find a switch of polarity. The value must be positive, else the method won't do anything.

Parameters:

segmentation - the number of segments to build

getSegmentation

public int getSegmentation()

Returns the number of segments that the findZeroes function will build while attempting to find a polarity switch.

Returns:

the number of segments in which the intervals will be split

See Also:

Engine#findZeroes

setNbIteration

public void setNbIteration(int nbIter)

Sets the maximum number of iterations the findZeroes can make to find zeroes.

Parameters:

nbIter - the maximum number of iterations made by the findZeroes function

getNbIteration

public int getNbIteration()

Returns the maximum number of iterations the function findZeroes can make to find polarity change.

Returns:

the maximum number of iterations of findZeroes

setFormula

public void setFormula(Formula formula)

This method register a formula to the engine, in order to perform its verification.

Parameters:

formula - a logical formula

See Also:

parseFormula(java.lang.String), Engin#getStatesVerifing

computeProbabilities

public java.util.HashMap computeProbabilities(IntervalList list,
                                              java.lang.String act)

Compute the probability P[a](x, list), i.e. the probability to reach a certain point of the list from any x point. This method then returns a hashmap of Interval -> Exp(x) with Exp(x) no being equal to exacly zero on Interval. If no x has a probability greater than zero, then an empty hashmap is returned. Note that Exp(x) is a probability distribution function.

Parameters:

list - the state set which may be reached from x.

act - the action to be applied.

Returns:

a hashma with the starting interval as a key, and the expression representing the probabilistic function as the target.

separation

public IntervalList separation(java.util.HashMap fct,
                               Variable var,
                               double q)

Returns all the x values for which the probability obtained from the probabilistic expression is greater than q.

Parameters:

fct - a association of Interval -> probability for each x set for which the expression returns a probability greater than q

var - represents the x variable in the expression

q - the minimum probabity (not included)

Returns:

the intervals representing the set of x for which the probability is greater than q

satisfies

public boolean satisfies(ProbSystem s,
                         Formula f)

Checks wether of not a probabilistic system does verify a formula.

Parameters:

s - the probabilistic system to verify the formula from

f - the formula to verify

Returns:

'True' if the system verifies the formula

getStatesVerifying

public IntervalList getStatesVerifying(Formula f)

Returns all the states verifying a formula using the system loaded in the engine.

Parameters:

f - the formula to verify

Returns:

a list of intervals representing all the states that verify the formula f. This list may be empty if no state can verify the formula.

See Also:

setProbSystem(data.ProbSystem)

getStatesVerifying

public IntervalList getStatesVerifying(Formula f,
                                       int level)

Returns all the states verifying a formula using the system loaded in the engine.

Parameters:

f - the formula to verify

level - the depth of the expression evaluated in power of two. If a logical operator is used, then the signs are switched from each side.

Returns:

a list of intervals representing all the states that verify the formula f. This list may be empty if no state can verify the formula.

See Also:

setProbSystem(data.ProbSystem)

findZeroes

public java.util.ArrayList findZeroes(Expression exp,
                                      Variable var,
                                      Interval inter,
                                      double threshold)

This method finds the intersection points between a mathematical expression and a threshold, on the interval closure inter. It is possible zeroes will not be found by the procedure, which analyse the signs of each segments. An application of the secant method estimates the zero value when a sign difference is found.

Parameters:

exp - the expression to analyse

var - the Variable object representing x

inter - the interval to analyse

threshold - the threshold

Returns:

a list of zeroes

See Also:

setPrecision(double), setSegmentation(int), setNbIteration(int)

findZeroesDouble

public java.util.ArrayList findZeroesDouble(Expression exp,
                                            Variable var,
                                            Interval inter,
                                            double threshold)

This method finds the intersection points between a mathematical expression and a threshold, on the interval closure inter. It is possible zeroes will not be found by the procedure, which analyse the signs of each segments. An application of the secant method estimates the zero value when a sign difference is found. Double numbers are used.

Parameters:

exp - the expression to analyse

var - the Variable object representing x

inter - the interval to analyse

threshold - the threshold

Returns:

a list of zeroes

See Also:

setPrecision(double), setSegmentation(int), setNbIteration(int)

findZeroesBigDecimal

public java.util.ArrayList findZeroesBigDecimal(Expression exp,
                                                Variable var,
                                                Interval inter,
                                                double threshold)

This method finds the intersection points between a mathematical expression and a threshold, on the interval closure inter. It is possible zeroes will not be found by the procedure, which analyse the signs of each segments. An application of the secant method estimates the zero value when a sign difference is found. BigDecimal numbers are used.

Parameters:

exp - the expression to analyse

var - the Variable object representing x

inter - the interval to analyse

threshold - the threshold

Returns:

a list of zeroes

See Also:

setPrecision(double), setSegmentation(int), setNbIteration(int)

highestPForTransition

public boolean highestPForTransition(Transition transition,
                                     double q)

Returns true if q is the highest probability of the transition.

Parameters:

transition - the transition to analyse

q - the maximum probabity to check

Returns:

true if q is the highest probability of the transition

addEnginListener

public void addEnginListener(EnginListener e)

Registers a listener to the engine

Parameters:

e - the listener to add

removeEnginListener

public void removeEnginListener(EnginListener e)

Remove a listener from the engine

Parameters:

e - the listener to remove

getFormula

public Formula getFormula()

Returns the formula stored in the engine.

Returns:

the formula to be verified.

loadProbSystem

public void loadProbSystem(java.io.File filename)
                    throws DataParserException,
                           ProbSystemException

Loads a probabilistic system from a file.

Parameters:

filename - the file name from which to load the system.

Throws:

DataParserException - should an invalid expression be detected

ProbSystemException - should an invalid probabilistic system be present in the reader

loadProbSystem

public void loadProbSystem(java.lang.String s)
                    throws java.io.IOException,
                           DataParserException,
                           ProbSystemException

Loads a probabilistic system from a string. Used to convert the system to different data structures.

Parameters:

s - a string representing the system

Throws:

java.io.IOException - should an error occur while reading the string

DataParserException - should an error exist in the system's representation

ProbSystemException - if the system could not be created

loadProbSystem

public void loadProbSystem(java.io.Reader reader,
                           int numberOfLines)
                    throws java.io.IOException,
                           DataParserException,
                           ProbSystemException

Loads a probabilistic system from a reader. The reader can be a file, a string or any object with reader as parent class.

Parameters:

reader - the reader object from which to load the system

numberOfLines - number of lines in the reader, 0 if unknown

Throws:

java.io.IOException - should an error occur while reading data

DataParserException - should an invalid expression be detected

ProbSystemException - should an invalid probabilistic system be present in the reader

verifySystemConstraints

public boolean verifySystemConstraints()
                                throws java.lang.Exception

This function verifies that the system does indeed satisfies the LMP constraints : 0 <= P_a(x,S) < 1

Returns:

true should the system satisfy the constraints

Throws:

java.lang.Exception - if one constraint is violated

setCalculationMode

public void setCalculationMode(int calculationMode)

Sets the calculation mode for the findZeroes method.

Parameters:

calculationMode - Eighter USE_BIGDECIMAL or USE_DOUBLE, else nothing will happen.

See Also:

USE_DOUBLE, USE_BIGDECIMAL

setStructMode

public void setStructMode(int structMode)
                   throws java.lang.Exception

Type of data structures used to store the system.

Parameters:

structMode - USE_MTBDD or USE_HASH, else nothing will happen.

Throws:

java.lang.Exception - if mode change was unsuccesful

See Also:

USE_MTBDD, USE_HASH

run

public void run(int mode)

Use to perform ths computation in a separate thread.

Parameters:

mode - the operation to be performed

See Also:

VERIFY_A_FORMULA_MODE, GET_STATES_VERIFYING_A_FORMULA_MODE, VERIFY_CONSTRAINT_MODE

getCalculationMode

public int getCalculationMode()

Returns the calculation mode used ...

Returns:

int USE_DOUBLE or USE_BIGDECIMAL

See Also:

USE_DOUBLE, USE_BIGDECIMAL

getStructMode

public int getStructMode()

Returns the current data structure mode used.

Returns:

int USE_HASH or USE_MTBDD

See Also:

USE_MTBDD, USE_HASH

loadFormula

public java.lang.String loadFormula(java.io.File file)
                             throws java.io.IOException,
                                    DataParserException,
                                    ProbSystemException

Loads the formula history from the specified file

Parameters:

file - the file from which to load the formula history

Returns:

a string containing the formula history

Throws:

java.io.IOException - should a file access error occur

DataParserException - should the file contain an invalid formula

ProbSystemException - should the history be empty