edu.neu.ccs.jpf
Class JPFApplet

java.lang.Object
  java.awt.Component
      java.awt.Container
          java.awt.Panel
              java.applet.Applet
                  javax.swing.JApplet
                      edu.neu.ccs.gui.DirectApplet
                          edu.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.

• The JPFApplet class is not ConsoleAware. This is because the console has methods to save the console window data to a file. Such methods are forbidden in an applet.
• There is no button to toggle the visibility of the graphics window. This is because the pane for the applet is embedded in a web page and we did not wish the dimensions of the pane to change after the pane is rendered on the page.
• There are two methods preInit() and postInit() that by default do nothing but are available for override. The method preInit() is called before the construction of the JPFPane object and the method postInit() is called after that construction. This allows changes to be made to settings at the appropriate time if desired.

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:

• A subarray { action } with an Action
• A subarray { name } with an action name
• A subarray { name, icon } with an action name and icon
• A subarray { action, option }
• A subarray { name, option }
• A subarray { name, icon, option }

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:

• DialogAction.KEEP_OPEN
• DialogAction.AUTO_CLOSE
• DialogAction.SET_CANCEL

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:

• A subarray { action } with an Action
• A subarray { name } with an action name
• A subarray { name, icon } with an action name and icon
• A subarray { action, option }
• A subarray { name, option }
• A subarray { name, icon, option }

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:

• DialogAction.KEEP_OPEN
• DialogAction.AUTO_CLOSE
• DialogAction.SET_CANCEL

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:

• A subarray { action } with an Action
• A subarray { name } with an action name
• A subarray { name, icon } with an action name and icon
• A subarray { action, option }
• A subarray { name, option }
• A subarray { name, icon, option }

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:

• DialogAction.KEEP_OPEN
• DialogAction.AUTO_CLOSE
• DialogAction.SET_CANCEL

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:

• A subarray { action } with an Action
• A subarray { name } with an action name
• A subarray { name, icon } with an action name and icon
• A subarray { action, option }
• A subarray { name, option }
• A subarray { name, icon, option }

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:

• DialogAction.KEEP_OPEN
• DialogAction.AUTO_CLOSE
• DialogAction.SET_CANCEL

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