pipe.gui
Class Animator
java.lang.Object
pipe.gui.Animator
- All Implemented Interfaces:
- Constants
public class Animator
- extends java.lang.Object
- implements Constants
This class is used to process clicks by the user to manually step
through enabled transitions in the net.
Fields inherited from interface pipe.gui.Constants |
ADDTOKEN, ANIMATE, ANNOTATION, ANNOTATION_DEFAULT_FONT, ANNOTATION_DEFAULT_FONT_SIZE, ANNOTATION_LAYER_OFFSET, ANNOTATION_MIN_WIDTH, ANNOTATION_SIZE_OFFSET, ARC, ARC_CONTROL_POINT_CONSTANT, ARC_LAYER_OFFSET, ARC_PATH_PROXIMITY_WIDTH, ARC_PATH_SELECTION_WIDTH, ARC_POINT_LAYER_OFFSET, CLASS_FILE_DESC, CLASS_FILE_EXTENSION, CREATING, DEFAULT_ELEMENT_TYPE, DELETE, DELTOKEN, DRAG, DRAW, ELEMENT_FILL_COLOUR, ELEMENT_LINE_COLOUR, ENABLED_TRANSITION_COLOUR, FIRE, GRID, IMMTRANS, LOWEST_LAYER_OFFSET, NOTE_DISABLED_COLOUR, NOTE_EDITING_COLOUR, PLACE, PLACE_TRANSITION_HEIGHT, PLACE_TRANSITION_LAYER_OFFSET, PLACE_TRANSITION_PROXIMITY_RADIUS, PROPERTY_FILE_DESC, PROPERTY_FILE_EXTENSION, RANDOM, RESERVED_BORDER, RESIZE_POINT_DOWN_COLOUR, SELECT, SELECTION_FILL_COLOUR, SELECTION_LAYER_OFFSET, SELECTION_LINE_COLOUR, START, STEPBACKWARD, STEPFORWARD, STOP, TIMEDTRANS |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
firedTransitions
public static java.util.ArrayList firedTransitions
count
public static int count
Animator
public Animator()
highlightEnabledTransitions
public void highlightEnabledTransitions()
unhighlightDisabledTransitions
public void unhighlightDisabledTransitions()
disableTransitions
public void disableTransitions()
storeModel
public void storeModel()
restoreModel
public void restoreModel()
startRandomFiring
public void startRandomFiring()
stopRandomFiring
public void stopRandomFiring()
doRandomFiring
public void doRandomFiring()
- This method randomly fires one of the
enabled transitions. It then records the
information about this by calling the
recordFiredTransition method.
stepBack
public void stepBack()
stepForward
public void stepForward()
fireTransition
public void fireTransition(Transition transition)
getNumberSequences
public int getNumberSequences()
setNumberSequences
public void setNumberSequences(int numberSequences)