de.upb.swt.epctools.simulator.explicit
Class TransitionSystem

java.lang.Object
  de.upb.swt.epctools.simulator.explicit.TransitionSystem

 class TransitionSystem
extends java.lang.Object

Implements a data structure and algorithms for calculating and accessing the semantics of an EPC. The semantics is represented as a transition system.

Author:

Ekkart Kindler, kindler@upb.de, Marcello La Rosa, marcello.larosa@gmail.com

Field Summary

private boolean	aborted Flag that indicates that the calculation of the transition system should be aborted.
private boolean	clean Indicates whether the transition system is clean.
(package private) boolean	contact Flag that indicates that a contact situation was encountered during the construction of the transition system.
(package private) EPC_DS	epc The EPC to which this transition system belongs to.
private int	index Index of property which is currently marked.
private long	maxMemory Maximal amount of memory available.
private java.util.LinkedList[]	newBackwardsOrJoinStates The newly marked states during the backwards marking algorithm for the OR-join connectors.
private java.util.LinkedList[]	newBackwardsXorJoinStates The newly marked states during the backwards marking algorithm for the XOR-join connectors.
private java.util.LinkedList	newForwardStates The new set of states of the transition system.
private java.util.LinkedList	newlyMarkedStates Newly marked states during the marking algorithms for checking some properties.
(package private) static int	NO_OF_PROP Number of properties to be marked.
(package private) static int	NOT_SOUND Index for existence of a path to proper termination.
(package private) int	noTransitions The number of transitions.
private java.lang.Runtime	runtime Runtime object in which the simulation is running.
(package private) java.util.HashMap	states The set of states of this transition system represented as a mapping from the corresponding BitSet to the State.
(package private) static int	WEAKLY_SOUND Index for existence of a path to proper termination.

Constructor Summary

TransitionSystem(EPC_DS epc)
Initializes a new empty transition system.

Method Summary

(package private) void	abort() Aborts the calculation of the transition system.
(package private) State	addState(java.util.BitSet bitset) Adds a new state to the transitions system.
(package private) Transition	addTransition(State source, Node_DS node, State target) Adds a new transition to the transitions system.
private void	backwardMarkStates() Backward marking algorithm.
(package private) void	calculate() Calculates the transition system of the EPC starting from the states that have been added to the EPC already.
private void	checkMemory() Checks whether there is still enough memory for the simulation.
(package private) void	checkProperties() Initiates the marking algorithms for calculating the properties of the EPC.
(package private) boolean	hasContact() Returns whether there were contact situations during the construction of the transition system.
(package private) boolean	isClean() Returns whether the calculated transition system is clean.
(package private) void	resume() Prepares for resuming the calulation of the transition system.

Methods inherited from class java.lang.Object

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

Field Detail

epc

EPC_DS epc

The EPC to which this transition system belongs to.

states

java.util.HashMap states

The set of states of this transition system represented as a mapping from the corresponding BitSet to the State.

contact

boolean contact

Flag that indicates that a contact situation was encountered during the construction of the transition system.

aborted

private boolean aborted

Flag that indicates that the calculation of the transition system should be aborted.

noTransitions

int noTransitions

The number of transitions.

newForwardStates

private java.util.LinkedList newForwardStates

The new set of states of the transition system. These are used while constructing the transition system in order to indicate the states for which the successors must be calculated yet.

newBackwardsOrJoinStates

private java.util.LinkedList[] newBackwardsOrJoinStates

The newly marked states during the backwards marking algorithm for the OR-join connectors.

newBackwardsXorJoinStates

private java.util.LinkedList[] newBackwardsXorJoinStates

The newly marked states during the backwards marking algorithm for the XOR-join connectors.

clean

private boolean clean

Indicates whether the transition system is clean.

runtime

private java.lang.Runtime runtime

Runtime object in which the simulation is running.

maxMemory

private long maxMemory

Maximal amount of memory available.

newlyMarkedStates

private java.util.LinkedList newlyMarkedStates

Newly marked states during the marking algorithms for checking some properties.

index

private int index

Index of property which is currently marked.

NO_OF_PROP

static final int NO_OF_PROP

Number of properties to be marked.

See Also:

Constant Field Values

WEAKLY_SOUND

static final int WEAKLY_SOUND

Index for existence of a path to proper termination.

See Also:

Constant Field Values

NOT_SOUND

static final int NOT_SOUND

Index for existence of a path to proper termination.

See Also:

Constant Field Values

Constructor Detail

TransitionSystem

TransitionSystem(EPC_DS epc)

Initializes a new empty transition system.

Parameters:

epc - the EPC to which the transition system belongs

Method Detail

addState

State addState(java.util.BitSet bitset)

Adds a new state to the transitions system. If the state with the same folder assignment exists already, it will not be added. Note that, for efficiency reasons, the bitset is not copied here; the bistet passed to this method should not be modified by the caller later!

Parameters:

bitset - the assignment of folders of the state to be added

Returns:

the added state.

addTransition

Transition addTransition(State source,
                         Node_DS node,
                         State target)

Adds a new transition to the transitions system. Both states should belong to the transition system.

Parameters:

source - the source state of the transition

node - the firing node

target - the target state of the transition

Returns:

the added transition.

isClean

boolean isClean()

Returns whether the calculated transition system is clean.

Returns:

true if the transition system is clean

hasContact

boolean hasContact()

Returns whether there were contact situations during the construction of the transition system.

Returns:

true if there were contact situations

abort

void abort()

Aborts the calculation of the transition system. The calculation can be resumed by first calling resume() and then calling calculate() again.

resume

void resume()

Prepares for resuming the calulation of the transition system. After aborting the calculation of the transition system by abort(), this method must be called before calling calculate() again.

checkMemory

private void checkMemory()
                  throws EPCSimulationException

Checks whether there is still enough memory for the simulation. If not an runtime exception is thrown.

Throws:

EPCSimulationException - if not enough memory is available

calculate

void calculate()
         throws EPCSimulationException

Calculates the transition system of the EPC starting from the states that have been added to the EPC already.

Throws:

EPCSimulationException - if not enough memory is available

backwardMarkStates

private void backwardMarkStates()
                         throws EPCSimulationException

Backward marking algorithm. Marks all states that are backward reachable from the states in the list of newlyMarkedStates.

Throws:

EPCSimulationException

checkProperties

void checkProperties()
               throws EPCSimulationException

Initiates the marking algorithms for calculating the properties of the EPC.

Throws:

EPCSimulationException