edu.neu.ccs.jpf
Class JPFApplet

java.lang.Object
  extended byjava.awt.Component
      extended byjava.awt.Container
          extended byjava.awt.Panel
              extended byjava.applet.Applet
                  extended byjavax.swing.JApplet
                      extended byedu.neu.ccs.gui.DirectApplet
                          extended byedu.neu.ccs.jpf.JPFApplet
All Implemented Interfaces:
Accessible, ImageObserver, JPTConstants, MenuContainer, RootPaneContainer, Serializable, SwingConstants

public class JPFApplet
extends DirectApplet
implements JPTConstants

The Java Power Framework class JPFApplet provides the ability to demonstrate JPF-like code in an applet. This can be useful for pedagogical purposes.

For general information, first read the documentation for JPF.

The graphics window is shown by default.

JPFApplet has some restrictions and some alternate facilities.

Since:
2.7.0
Version:
2.7.0
See Also:
Serialized Form

Nested Class Summary
 
Nested classes inherited from class javax.swing.JApplet
JApplet.AccessibleJApplet
 
Nested classes inherited from class java.applet.Applet
Applet.AccessibleApplet
 
Nested classes inherited from class java.awt.Panel
Panel.AccessibleAWTPanel
 
Nested classes inherited from class java.awt.Container
Container.AccessibleAWTContainer
 
Nested classes inherited from class java.awt.Component
Component.AccessibleAWTComponent, Component.BltBufferStrategy, Component.FlipBufferStrategy
 
Field Summary
 PaintableSequence sequence
          The paintable sequence of the graphics buffered panel window.
protected  JPFPane thePane
          The JPF pane.
 BufferedPanel window
          The graphics buffered panel window.
 
Fields inherited from class edu.neu.ccs.gui.DirectApplet
component, initializationSuccessful
 
Fields inherited from class javax.swing.JApplet
accessibleContext, rootPane, rootPaneCheckingEnabled
 
Fields inherited from class java.applet.Applet
 
Fields inherited from class java.awt.Panel
 
Fields inherited from class java.awt.Container
 
Fields inherited from class java.awt.Component
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
 
Fields inherited from interface edu.neu.ccs.util.JPTConstants
ABOVE, ALIGNMENT, BELOW, BOTTOM_LEFT, BOTTOM_RIGHT, DEFAULT, FONT, INPUT_PROPERTIES, MANDATORY, OPTIONAL, ORIENTATION, TOP_LEFT, TOP_RIGHT, VALUE
 
Fields inherited from interface javax.swing.SwingConstants
BOTTOM, CENTER, EAST, HORIZONTAL, LEADING, LEFT, NEXT, NORTH, NORTH_EAST, NORTH_WEST, PREVIOUS, RIGHT, SOUTH, SOUTH_EAST, SOUTH_WEST, TOP, TRAILING, VERTICAL, WEST
 
Fields inherited from interface java.awt.image.ImageObserver
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
 
Constructor Summary
JPFApplet()
          Construct the JPF applet using as the given initializer the derived class that uses this constructor.
JPFApplet(MethodFilter filter)
          Construct the JPF applet using as the given initializer the derived class that uses this constructor.
 
Method Summary
 void clearGraphics()
          Clears the graphics window.
 Object createGUI()
          Implements DirectApplet by returning the JPFPane created in one of the constructors.
 void exitFramework()
          Exits the framework by calling exitFramework() on the underlying JPFPane pane object.
static JPTFrame frame(Object object)
          Frame the given object in a JPTFrame and open the frame; return the frame constructed.
static JPTFrame frame(Object object, int location)
          Frame the given object in a JPTFrame and open the frame; use the given location which should be either CENTER or one of the standard constants for one of the eight compass directions; return the frame constructed.
static JPTFrame frame(Object object, String title)
          Frame the given object in a JPTFrame and open the frame; use the given title for the frame; return the frame constructed.
static JPTFrame frame(Object object, String title, Insets insets)
          Frame the given object in a JPTFrame and open the frame; use the given title for the frame; use the given insets to inset the frame in the screen; return the frame constructed.
static JPTFrame frame(Object object, String title, int location)
          Frame the given object in a JPTFrame and open the frame; use the given title for the frame; use the given location which should be either CENTER or one of the standard constants for one of the eight compass directions; return the frame constructed.
static JPTFrame frame(Object object, String title, int location, Insets insets)
          Frame the given object in a JPTFrame and open the frame; use the given title for the frame; use the given location which should be either CENTER or one of the standard constants for one of the eight compass directions; use the given insets to inset the frame in the screen; return the frame constructed.
static GeneralDialog generalDialog(Object object, Object[][] actionData)
          Place the given object in a modal general dialog and open the dialog; use the action data to define the dialog buttons; return the dialog constructed.
static GeneralDialog generalDialog(Object object, Object[][] actionData, Object defaultAction)
          Place the given object in a modal general dialog and open the dialog; use the action data to define the dialog buttons; use the default action object to define the default button; return the dialog constructed.
static GeneralDialog generalDialog(Object object, String title, Object[][] actionData)
          Place the given object in a modal general dialog and open the dialog; use the given title for the dialog; use the action data to define the dialog buttons; return the dialog constructed.
static GeneralDialog generalDialog(Object object, String title, Object[][] actionData, Object defaultAction)
          Place the given object in a modal general dialog and open the dialog; use the given title for the dialog; use the action data to define the dialog buttons; use the default action object to define the default button; return the dialog constructed.
 void makeShapshot()
          Makes a shapshot of the graphics window and shows this snapshot in a separate frame.
static GeneralDialog OKCancelDialog(Object object)
          Place the given object in a modal OK-Cancel dialog and open the dialog; return the dialog constructed.
static GeneralDialog OKCancelDialog(Object object, String title)
          Place the given object in a modal OK-Cancel dialog and open the dialog; use the given title for the dialog; return the dialog constructed.
static GeneralDialog OKDialog(Object object)
          Place the given object in a modal OK dialog and open the dialog; return the dialog constructed.
static GeneralDialog OKDialog(Object object, String title)
          Place the given object in a modal OK dialog and open the dialog; use the given title for the dialog; return the dialog constructed.
protected  void postInit()
          Override this method to do tasks that must occur after the JPFPane pane is created.
protected  void preInit()
          Override this method to do tasks that must occur before the JPFPane pane is created.
static GeneralDialog YesNoCancelDialog(Object object)
          Place the given object in a modal Yes-No-Cancel dialog and open the dialog; return the dialog constructed.
static GeneralDialog YesNoCancelDialog(Object object, String title)
          Place the given object in a modal Yes-No-Cancel dialog and open the dialog; use the given title for the dialog; return the dialog constructed.
 
Methods inherited from class edu.neu.ccs.gui.DirectApplet
destroy, init
 
Methods inherited from class javax.swing.JApplet
addImpl, createRootPane, getAccessibleContext, getContentPane, getGlassPane, getJMenuBar, getLayeredPane, getRootPane, isRootPaneCheckingEnabled, paramString, remove, setContentPane, setGlassPane, setJMenuBar, setLayeredPane, setLayout, setRootPane, setRootPaneCheckingEnabled, update
 
Methods inherited from class java.applet.Applet
getAppletContext, getAppletInfo, getAudioClip, getAudioClip, getCodeBase, getDocumentBase, getImage, getImage, getLocale, getParameter, getParameterInfo, isActive, newAudioClip, play, play, resize, resize, setStub, showStatus, start, stop
 
Methods inherited from class java.awt.Panel
addNotify
 
Methods inherited from class java.awt.Container
add, add, add, add, add, addContainerListener, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getAlignmentX, getAlignmentY, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getInsets, getLayout, getListeners, getMaximumSize, getMinimumSize, getPreferredSize, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paint, paintComponents, preferredSize, print, printComponents, processContainerEvent, processEvent, remove, removeAll, removeContainerListener, removeNotify, setFocusCycleRoot, setFocusTraversalKeys, setFocusTraversalPolicy, setFont, transferFocusBackward, transferFocusDownCycle, validate, validateTree
 
Methods inherited from class java.awt.Component
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, checkImage, checkImage, coalesceEvents, contains, contains, createImage, createImage, createVolatileImage, createVolatileImage, disable, disableEvents, dispatchEvent, enable, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBounds, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphics, getGraphicsConfiguration, getHeight, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocation, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getSize, getToolkit, getTreeLock, getWidth, getX, getY, gotFocus, handleEvent, hasFocus, hide, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isDoubleBuffered, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isOpaque, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, printAll, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processKeyEvent, processMouseEvent, processMouseMotionEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, repaint, repaint, repaint, repaint, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, reshape, setBackground, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setEnabled, setFocusable, setFocusTraversalKeysEnabled, setForeground, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, setVisible, show, show, size, toString, transferFocus, transferFocusUpCycle
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

window

public BufferedPanel window
The graphics buffered panel window.


sequence

public PaintableSequence sequence
The paintable sequence of the graphics buffered panel window.


thePane

protected JPFPane thePane
The JPF pane.

Constructor Detail

JPFApplet

public JPFApplet()

Construct the JPF applet using as the given initializer the derived class that uses this constructor.

This constructor shows the graphics window.


JPFApplet

public JPFApplet(MethodFilter filter)

Construct the JPF applet using as the given initializer the derived class that uses this constructor.

This constructor shows the graphics window and uses the given filter to filter the methods used for buttons.

Parameters:
filter - an optional method filter to filter the methods used for buttons
Method Detail

createGUI

public final Object createGUI()

Implements DirectApplet by returning the JPFPane created in one of the constructors.

Returns the same JPFPane even if called multiple times.

This method is identical to the method getPane in class JPF but is named as it is to implement DirectApplet.

Specified by:
createGUI in class DirectApplet

preInit

protected void preInit()

Override this method to do tasks that must occur before the JPFPane pane is created.

The override method should be protected so that it does not generate an action button in the GUI.

An override of the preInit() method is the appropriate place to call LookAndFeelTools since such calls will take place before the construction of the pane.


postInit

protected void postInit()

Override this method to do tasks that must occur after the JPFPane pane is created.

The override method should be protected so that it does not generate an action button in the GUI.

An override of the postInit() method is the appropriate place to initialize state common to the entire applet and to make settings dependent on the existence of the pane.


clearGraphics

public final void clearGraphics()
Clears the graphics window.


makeShapshot

public final void makeShapshot()

Makes a shapshot of the graphics window and shows this snapshot in a separate frame.

This facility is provided to make it easy for users to create a snapshot of the graphics window that may then be saved by utilities that can capture a frame.

The programmer may make the following call to capture the graphics window to a BufferedImage in order to save the data in a specific format or to do further manipulation.

    BufferedImage snapshot = window.makeSnapshot();


exitFramework

public final void exitFramework()

Exits the framework by calling exitFramework() on the underlying JPFPane pane object. In turn, this method invokes the doClick method on the exit button. This procedure guarantees that the exit behavior will be identical to the action attached to the exit button.


frame

public static JPTFrame frame(Object object)

Frame the given object in a JPTFrame and open the frame; return the frame constructed.

Parameters:
object - the object to frame
Returns:
the frame constructed
Since:
2.3.4

frame

public static JPTFrame frame(Object object,
                             int location)

Frame the given object in a JPTFrame and open the frame; use the given location which should be either CENTER or one of the standard constants for one of the eight compass directions; return the frame constructed.

Parameters:
object - the object to frame
location - the constant representing the frame location
Returns:
the frame constructed
Since:
2.3.4

frame

public static JPTFrame frame(Object object,
                             String title)

Frame the given object in a JPTFrame and open the frame; use the given title for the frame; return the frame constructed.

Parameters:
object - the object to frame
title - the title for the frame
Returns:
the frame constructed
Since:
2.3.4

frame

public static JPTFrame frame(Object object,
                             String title,
                             int location)

Frame the given object in a JPTFrame and open the frame; use the given title for the frame; use the given location which should be either CENTER or one of the standard constants for one of the eight compass directions; return the frame constructed.

Parameters:
object - the object to frame
title - the title for the frame
location - the constant representing the frame location
Returns:
the frame constructed
Since:
2.3.4

frame

public static JPTFrame frame(Object object,
                             String title,
                             Insets insets)

Frame the given object in a JPTFrame and open the frame; use the given title for the frame; use the given insets to inset the frame in the screen; return the frame constructed.

Parameters:
object - the object to frame
title - the title for the frame
insets - the screen insets to use to adjust the location
Returns:
the frame constructed
Since:
2.3.4

frame

public static JPTFrame frame(Object object,
                             String title,
                             int location,
                             Insets insets)

Frame the given object in a JPTFrame and open the frame; use the given title for the frame; use the given location which should be either CENTER or one of the standard constants for one of the eight compass directions; use the given insets to inset the frame in the screen; return the frame constructed.

Parameters:
object - the object to frame
title - the title for the frame
location - the constant representing the frame location
insets - the screen insets to use to adjust the location
Returns:
the frame constructed
Since:
2.3.4

OKDialog

public static GeneralDialog OKDialog(Object object)

Place the given object in a modal OK dialog and open the dialog; return the dialog constructed.

Parameters:
object - the object to place in the dialog
Returns:
the dialog constructed
Since:
2.3.4

OKDialog

public static GeneralDialog OKDialog(Object object,
                                     String title)

Place the given object in a modal OK dialog and open the dialog; use the given title for the dialog; return the dialog constructed.

Parameters:
object - the object to place in the dialog
title - the title for the dialog
Returns:
the dialog constructed
Since:
2.3.4

OKCancelDialog

public static GeneralDialog OKCancelDialog(Object object)

Place the given object in a modal OK-Cancel dialog and open the dialog; return the dialog constructed.

Parameters:
object - the object to place in the dialog
Returns:
the dialog constructed
Since:
2.3.4

OKCancelDialog

public static GeneralDialog OKCancelDialog(Object object,
                                           String title)

Place the given object in a modal OK-Cancel dialog and open the dialog; use the given title for the dialog; return the dialog constructed.

Parameters:
object - the object to place in the dialog
title - the title for the dialog
Returns:
the dialog constructed
Since:
2.3.4

YesNoCancelDialog

public static GeneralDialog YesNoCancelDialog(Object object)

Place the given object in a modal Yes-No-Cancel dialog and open the dialog; return the dialog constructed.

Parameters:
object - the object to place in the dialog
Returns:
the dialog constructed
Since:
2.3.4

YesNoCancelDialog

public static GeneralDialog YesNoCancelDialog(Object object,
                                              String title)

Place the given object in a modal Yes-No-Cancel dialog and open the dialog; use the given title for the dialog; return the dialog constructed.

Parameters:
object - the object to place in the dialog
title - the title for the dialog
Returns:
the dialog constructed
Since:
2.3.4

generalDialog

public static GeneralDialog generalDialog(Object object,
                                          Object[][] actionData)

Place the given object in a modal general dialog and open the dialog; use the action data to define the dialog buttons; return the dialog constructed.

The parameter actionData is an Object[][] array that specifies each dialog Action in one of the following ways:

If the option parameter is specified, it must be one of the following values that will determine what is done to the dialog when the action is finished:

If the option parameter is not specified, it is taken to be DialogAction.AUTO_CLOSE.

Parameters:
object - the object to place in the dialog
actionData - the action data
Returns:
the dialog constructed
Since:
2.3.4

generalDialog

public static GeneralDialog generalDialog(Object object,
                                          Object[][] actionData,
                                          Object defaultAction)

Place the given object in a modal general dialog and open the dialog; use the action data to define the dialog buttons; use the default action object to define the default button; return the dialog constructed.

The parameter actionData is an Object[][] array that specifies each dialog Action in one of the following ways:

If the option parameter is specified, it must be one of the following values that will determine what is done to the dialog when the action is finished:

If the option parameter is not specified, it is taken to be DialogAction.AUTO_CLOSE.

The Object supplied for the default action must either be an Action or a name that is supplied in the action data. If the parameter is null, no default action is set.

Parameters:
object - the object to place in the dialog
actionData - the action data
defaultAction - the default action
Returns:
the dialog constructed
Since:
2.3.4

generalDialog

public static GeneralDialog generalDialog(Object object,
                                          String title,
                                          Object[][] actionData)

Place the given object in a modal general dialog and open the dialog; use the given title for the dialog; use the action data to define the dialog buttons; return the dialog constructed.

The parameter actionData is an Object[][] array that specifies each dialog Action in one of the following ways:

If the option parameter is specified, it must be one of the following values that will determine what is done to the dialog when the action is finished:

If the option parameter is not specified, it is taken to be DialogAction.AUTO_CLOSE.

Parameters:
object - the object to place in the dialog
title - the title for the dialog
actionData - the action data
Returns:
the dialog constructed
Since:
2.3.4

generalDialog

public static GeneralDialog generalDialog(Object object,
                                          String title,
                                          Object[][] actionData,
                                          Object defaultAction)

Place the given object in a modal general dialog and open the dialog; use the given title for the dialog; use the action data to define the dialog buttons; use the default action object to define the default button; return the dialog constructed.

The parameter actionData is an Object[][] array that specifies each dialog Action in one of the following ways:

If the option parameter is specified, it must be one of the following values that will determine what is done to the dialog when the action is finished:

If the option parameter is not specified, it is taken to be DialogAction.AUTO_CLOSE.

The Object supplied for the default action must either be an Action or a name that is supplied in the action data. If the parameter is null, no default action is set.

Parameters:
object - the object to place in the dialog
title - the title for the dialog
actionData - the action data
defaultAction - the default action
Returns:
the dialog constructed
Since:
2.3.4