pipe.gui
Class Animator

java.lang.Object
  extended by 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.


Field Summary
static int count
           
static java.util.ArrayList firedTransitions
           
 
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
 
Constructor Summary
Animator()
           
 
Method Summary
 void disableTransitions()
           
 void doRandomFiring()
          This method randomly fires one of the enabled transitions.
 void fireTransition(Transition transition)
           
 int getNumberSequences()
           
 void highlightEnabledTransitions()
           
 void restoreModel()
           
 void setNumberSequences(int numberSequences)
           
 void startRandomFiring()
           
 void stepBack()
           
 void stepForward()
           
 void stopRandomFiring()
           
 void storeModel()
           
 void unhighlightDisabledTransitions()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

firedTransitions

public static java.util.ArrayList firedTransitions

count

public static int count
Constructor Detail

Animator

public Animator()
Method Detail

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)