de.upb.swt.epctools.simulator.symbolic
Class SimEPC

java.lang.Object
  de.upb.swt.epctools.model.EPC
      de.upb.swt.epctools.simulator.symbolic.SimEPC

All Implemented Interfaces:

ModelListener

public class SimEPC
extends EPC
implements ModelListener

This class represents a complete EPC diagram with event and function nodes, connectors and arcs

Nested Class Summary

class	SimEPC.ModelEPC
class	SimEPC.SimulationData

Nested classes/interfaces inherited from class de.upb.swt.epctools.model.EPC

EPC.MappingCopy

Field Summary

static int	ALG_BFS_BOTTOM_UP
static int	ALG_BFS_TOP_DOWN
static int	ALG_BFS_UNDIRECTED
static int	ALG_ITERATIVE
static int	ALG_RANDOM
static java.lang.String	DIALOG_TITLE
private java.util.HashMap	m_arc_map A map from getArcs() to m_model_epc.getArcs().
private java.util.HashMap	m_arc_map_reverse A map from m_model_epc.getArcs() to getArcs().
private de.upb.swt.mcie.robdds.Assignment	m_assignment
private boolean	m_assignment_up_to_date
private de.upb.swt.mcie.robdds.Context	m_context
private SimEPC.SimulationData	m_data
private SimEPC.ModelEPC	m_model_epc
private java.util.HashMap	m_node_map A map from getNodes() to m_model_epc.getNodes().
private EPC	m_original_epc The original EPC without simulation capability
private de.upb.swt.mcie.robdds.ROBDD	m_state
private boolean	m_state_up_to_date
private SimEPC	m_this_sim_epc
static int	NO_THREAD_COMPUTATION_MAXIMUM

Fields inherited from class de.upb.swt.epctools.model.EPC

FALSE, m_this, STRONG, TRUE, UNKNOWN, WEAK

Fields inherited from interface de.upb.swt.epctools.model.tools.ModelListener

MSG_ARC_ADDED, MSG_ARC_RECONNECTED, MSG_ARC_REMOVED, MSG_BEND_POINT_CHANGE, MSG_CHANGED_ALGORITHM, MSG_CONSTRAINT_CHANGED, MSG_DESCRIPTION_CHANGED, MSG_FOLDERS_CHANGED, MSG_HIGHLIGHTING_CHANGED, MSG_IN_ARC_ADDED, MSG_IN_ARC_REMOVED, MSG_INFO_CHANGED, MSG_LOCATION_CHANGED, MSG_NAME_CHANGED, MSG_NODE_ADDED, MSG_NODE_REMOVED, MSG_OUT_ARC_ADDED, MSG_OUT_ARC_REMOVED, MSG_SIZE_CHANGED, MSG_SOURCE_CHANGED, MSG_STRUCTURE_CHANGED, MSG_TARGET_CHANGED

Constructor Summary

SimEPC(EPC original_epc)
Initialization

Method Summary

private de.upb.swt.mcie.robdds.ROBDD	computeAllSuccessors(de.upb.swt.mcie.robdds.ROBDD state, boolean optimistic)
private de.upb.swt.mcie.robdds.ROBDD	computeCompleteTransitionRelation(boolean optimistic) Returns the complete transition relation
de.upb.swt.mcie.formulas.Formula	computeContactFormula() Computes a formula corresponding to alle state of "this" EPC where there is a contact situation.
private void	computeCurrentAssignment() Returns an Assignment for the current state of "this"
private void	computeCurrentState() Returns an ROBDD for the current state of "this"
private de.upb.swt.mcie.robdds.ROBDD	computeEquiFormula()
private void	computeFormulas() This function computes all formulas for each Node.
void	computeHighlightedNonLocalNodes(boolean optimistic) This function computes the correct highlighting state for all Nodes.
private void	computeOrderedVariables(int algorithm)
private void	computeSimulationData() This function makes the transition relation up to date.
void	copyNonLocalHighlightingToOriginalEPC() This function transfers the highlighting of the EPC copy to the original EPC.
de.upb.swt.mcie.robdds.ROBDD	ex(de.upb.swt.mcie.robdds.ROBDD f)
private java.util.Vector	getAllAssignments(de.upb.swt.mcie.robdds.ROBDD r) Returns all assignments for one ROBDD.
java.util.HashMap	getArcMap() This returns a map to the original EPC.
de.upb.swt.mcie.robdds.Context	getContext()
void	getMessage(int msg_id, java.lang.Object modelObject) This function is called upon changes on the model object.
java.util.HashMap	getNodeMap() This returns a map to the original EPC.
int	hasIdealSemantics() Returns TRUE if true, FALSE if false or UNKNOWN if the transition relation is outdated.
byte	hasReachableContactSituation(boolean optimistic) Returns true if there is an accessible state with a contact situation.
int	hasReachableDeadlockSituation(boolean optimistic) Returns true if there is an accessible state with a deadlock.
byte	isInContactSituation() Returns true if the EPC is in a contact situation in the actual state.
int	isInIdealState() Returns TRUE if true, FALSE if false or UNKNOWN if the transition relation is outdated.
boolean	isSimulationDataUpToDate() Returns true if the simulation data has been computed and can be retrieved quickly.
byte	isSound() Calculates the soundness property of the EPC.
java.lang.String	printDebugInformation() Prints some information about the transition relation
private java.lang.String	printTransitionRelation(de.upb.swt.mcie.robdds.ROBDD relation) Prints the transition relation to a String

Methods inherited from class de.upb.swt.epctools.model.EPC

addListener, allowMultipleFolders, allowsMultipleFolders, forwardMessage, getArc, getArcs, getCopy, getExactCopy, getIdManager, getMessage, getNode, getNodes, hasOnlyLocalNodes, isConsistent, isReadyForSimulation, removeListener, resetFolders, resetHighlighting

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.upb.swt.epctools.model.tools.ModelListener

getMessage

Field Detail

m_original_epc

private EPC m_original_epc

The original EPC without simulation capability

m_model_epc

private SimEPC.ModelEPC m_model_epc

m_this_sim_epc

private SimEPC m_this_sim_epc

m_node_map

private java.util.HashMap m_node_map

A map from getNodes() to m_model_epc.getNodes(). The map is up to date only if the Node Vector from the EPC copy was not changed!!!

m_arc_map

private java.util.HashMap m_arc_map

A map from getArcs() to m_model_epc.getArcs(). The map is up to date only if the Node Vector from the EPC copy was not changed!!!

m_arc_map_reverse

private java.util.HashMap m_arc_map_reverse

A map from m_model_epc.getArcs() to getArcs(). The map is up to date only if the Node Vector from the EPC copy was not changed!!!

m_data

private SimEPC.SimulationData m_data

m_context

private de.upb.swt.mcie.robdds.Context m_context

m_assignment

private de.upb.swt.mcie.robdds.Assignment m_assignment

m_state

private de.upb.swt.mcie.robdds.ROBDD m_state

m_assignment_up_to_date

private boolean m_assignment_up_to_date

m_state_up_to_date

private boolean m_state_up_to_date

DIALOG_TITLE

public static final java.lang.String DIALOG_TITLE

See Also:

Constant Field Values

NO_THREAD_COMPUTATION_MAXIMUM

public static final int NO_THREAD_COMPUTATION_MAXIMUM

See Also:

Constant Field Values

ALG_BFS_TOP_DOWN

public static final int ALG_BFS_TOP_DOWN

See Also:

Constant Field Values

ALG_BFS_BOTTOM_UP

public static final int ALG_BFS_BOTTOM_UP

See Also:

Constant Field Values

ALG_ITERATIVE

public static final int ALG_ITERATIVE

See Also:

Constant Field Values

ALG_RANDOM

public static final int ALG_RANDOM

See Also:

Constant Field Values

ALG_BFS_UNDIRECTED

public static final int ALG_BFS_UNDIRECTED

See Also:

Constant Field Values

Constructor Detail

SimEPC

public SimEPC(EPC original_epc)

Initialization

Method Detail

getNodeMap

public java.util.HashMap getNodeMap()

This returns a map to the original EPC. Note it could be better to return only a copy here, but since the SimEPC is a very specialized class only used by the EPC simulator, we simply handle all extern user as friends.

getArcMap

public java.util.HashMap getArcMap()

This returns a map to the original EPC. Note it could be better to return only a copy here, but since the SimEPC is a very specialized class only used by the EPC simulator, we simply handle all extern user as friends.

getMessage

public void getMessage(int msg_id,
                       java.lang.Object modelObject)

This function is called upon changes on the model object. This function belongs to the ModelListener interface.

isSimulationDataUpToDate

public boolean isSimulationDataUpToDate()

Returns true if the simulation data has been computed and can be retrieved quickly.

hasIdealSemantics

public int hasIdealSemantics()
                      throws EPCComputationException

Returns TRUE if true, FALSE if false or UNKNOWN if the transition relation is outdated.

Throws:

EPCComputationException

isInIdealState

public int isInIdealState()
                   throws EPCComputationException

Returns TRUE if true, FALSE if false or UNKNOWN if the transition relation is outdated.

Throws:

EPCComputationException

hasReachableContactSituation

public byte hasReachableContactSituation(boolean optimistic)
                                  throws EPCComputationException

Returns true if there is an accessible state with a contact situation.

Throws:

EPCComputationException

hasReachableDeadlockSituation

public int hasReachableDeadlockSituation(boolean optimistic)
                                  throws EPCComputationException

Returns true if there is an accessible state with a deadlock.

Throws:

EPCComputationException

isInContactSituation

public byte isInContactSituation()

Description copied from class: EPC

Returns true if the EPC is in a contact situation in the actual state.

Overrides:

isInContactSituation in class EPC

isSound

public byte isSound()

Calculates the soundness property of the EPC. Returns TRUE if the EPC is sound, WEAK if the EPC is weakly sound, and FALSE if it is not weakly sound (in the current state).

Returns:

soundness property of EPC

computeContactFormula

public de.upb.swt.mcie.formulas.Formula computeContactFormula()

Computes a formula corresponding to alle state of "this" EPC where there is a contact situation.

computeHighlightedNonLocalNodes

public void computeHighlightedNonLocalNodes(boolean optimistic)
                                     throws EPCComputationException

This function computes the correct highlighting state for all Nodes. "optimistic" can be set to true, then the highlighting will be computed corresponding to the optimistic semantics, otherwise the pessimistic semantics will be used.

Throws:

EPCComputationException

copyNonLocalHighlightingToOriginalEPC

public void copyNonLocalHighlightingToOriginalEPC()

This function transfers the highlighting of the EPC copy to the original EPC. Note that this function does not work anymore if the original EPC was changed!!!

computeCurrentAssignment

private void computeCurrentAssignment()

Returns an Assignment for the current state of "this"

computeCurrentState

private void computeCurrentState()

Returns an ROBDD for the current state of "this"

computeSimulationData

private void computeSimulationData()
                            throws EPCComputationException

This function makes the transition relation up to date. This function is private because certain conditions must be fulfilled so that the relation can be computed without problems (e.g. isEPCReadyForSimulation() must be true).

Throws:

EPCComputationException

computeAllSuccessors

private de.upb.swt.mcie.robdds.ROBDD computeAllSuccessors(de.upb.swt.mcie.robdds.ROBDD state,
                                                          boolean optimistic)

computeEquiFormula

private de.upb.swt.mcie.robdds.ROBDD computeEquiFormula()

computeOrderedVariables

private void computeOrderedVariables(int algorithm)

computeFormulas

private void computeFormulas()

This function computes all formulas for each Node.

computeCompleteTransitionRelation

private de.upb.swt.mcie.robdds.ROBDD computeCompleteTransitionRelation(boolean optimistic)
                                                                throws EPCComputationException

Returns the complete transition relation

Throws:

EPCComputationException

printDebugInformation

public java.lang.String printDebugInformation()

Prints some information about the transition relation

printTransitionRelation

private java.lang.String printTransitionRelation(de.upb.swt.mcie.robdds.ROBDD relation)

Prints the transition relation to a String

getAllAssignments

private java.util.Vector getAllAssignments(de.upb.swt.mcie.robdds.ROBDD r)

Returns all assignments for one ROBDD. The returned Vector contains only instance of the type Assignment!

ex

public de.upb.swt.mcie.robdds.ROBDD ex(de.upb.swt.mcie.robdds.ROBDD f)

getContext

public de.upb.swt.mcie.robdds.Context getContext()