edu.neu.ccs.jpf
Class JPFPane

java.lang.Object
  java.awt.Component
      java.awt.Container
          javax.swing.JComponent
              javax.swing.JPanel
                  edu.neu.ccs.gui.DisplayPanel
                      edu.neu.ccs.jpf.JPFPane

All Implemented Interfaces:

Accessible, AlertListener, Displayable, EventListener, ImageObserver, JPTConstants, MalformedDataListener, MenuContainer, Serializable, SwingConstants

public class JPFPane

extends DisplayPanel

implements JPTConstants

Class JPFPane is an adaption of the earlier JPF class JPFApplication which has been removed as of 2.7.0. The key reason for this change is to create a panel that may be used in multiple ways, for example, in JPF and JPFApplet. This class is now public so it may also be used in creative ways by any applications programmer.

Revised in 2.7.0a to use the changes in JPFHelper. In addition, if an error is encountered or an exception is thrown in the construction of a JPFPane, then an alternate pane with the error information or exception trace will be shown.

Since:

2.7.0

Version:

2.7.0a

See Also:

Serialized Form

Nested Class Summary

Nested classes inherited from class javax.swing.JPanel

JPanel.AccessibleJPanel

Nested classes inherited from class javax.swing.JComponent

JComponent.AccessibleJComponent

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

protected Class	baseClass Base class for the initializer object; the code that recursively extracts JPF methods will stop the search when this base class is reached.
static int	BUFFER_HEIGHT Default buffer height = 400.
static int	BUFFER_WIDTH Default buffer width = 400.
protected VTable	buttonsPanel Buttons panel that combines the three actions panels.
protected Action	clearGraphicsAction Clear graphics action.
private static Color	commonButtonColor Color of the common buttons.
protected ActionsPanel	commonButtonsPanel Actions panel for the common actions.
protected Action	exitAction Default application closing action.
protected JButton	exitButton Exit button.
private static Color	exitButtonColor Color of the exit button.
protected ActionsPanel	exitButtonPanel Actions panel for the exit action.
protected MethodFilter	filter Method filter for extra pruning if any.
protected Object	initializer Initializer object for the JPF methods to be displayed in the automatic GUI.
protected Class	initializerClass Class of the initializer object.
protected DisplayPanel	LHS LHS of main GUI panel.
protected HTable	mainPanel Main GUI panel.
protected Action	makeShapshotAction Make shapshot action.
private static Color	methodButtonColor Color of the method buttons when enabled.
private static Color	methodButtonColorDisabled Color of the method buttons when disabled.
protected JButton[]	methodButtons Method buttons.
protected ActionsPanel	methodButtonsPanel Actions panel for the automatic JPF method buttons.
protected DisplayPanel	RHS RHS of main GUI panel.
static int	SCROLL_HEIGHT Default button scroll panel maximum height = 400.
static int	SCROLL_WIDTH Default button scroll panel maximum width = 400.
protected boolean	showGraphics Whether or not to show the graphics window.
protected BufferedPanel	window Default graphics buffered panel.

Fields inherited from class edu.neu.ccs.gui.DisplayPanel

background, codec, CODEC

Fields inherited from class javax.swing.JPanel

Fields inherited from class javax.swing.JComponent

accessibleContext, listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW

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 edu.neu.ccs.gui.Displayable

DEFAULT_VIEW_STATE, VIEW_STATE

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

JPFPane(Object initializer, Class baseClass)
Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; this constructor shows the graphics window.

JPFPane(Object initializer, Class baseClass, boolean showGraphics)
Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; this constructor shows the graphics window if the given boolean parameter is true.

JPFPane(Object initializer, Class baseClass, MethodFilter filter)
Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; in addition, provides a method filter that will further restrict the methods selected for the GUI; this constructor shows the graphics window.

JPFPane(Object initializer, Class baseClass, MethodFilter filter, boolean showGraphics)
Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; in addition, provides a method filter that will further restrict the methods selected for the GUI; this constructor will show the graphics window if the given boolean parameter is true.

Method Summary

void	addCommonButton(Action action, String tooltip) Allows the user of this class to add a common button by providing its action and tooltip.
protected JButton	addOneButton(ActionsPanel panel, Action action, String tooltip) Adds one button with the given action and tool tip to the given panel and then returns the button.
protected void	buildButtons() Build the buttons and the buttons panel.
protected void	buildGUI() Build the main panel.
void	clearGraphics() Clears the graphics window.
void	exitFramework() Exits the framework by programmatically invoking the doClick() method on the exit button.
Class	getBaseClass() Returns the base class used to limit how deep the recursive search for methods will go.
BufferedPanel	getGraphicsWindow() Returns the graphics window.
Object	getInitializer() Returns the initializer object for this pane.
Class	getInitializerClass() Returns the initializer object class.
MethodFilter	getMethodFilter() Returns the method filter if any.
protected Method[]	getMethodList() Returns a list of the JPF methods, that is, the methods for which we can instantiate buttons in the main GUI.
boolean	isGraphicsVisible() Returns whether or not the graphics window is visible.
protected Action	makeActionFromMethod(Method method) Makes a ThreadedAction from the given method.
void	makeShapshot() Makes a shapshot of the graphics windows and shows this snapshot in a separate frame.
protected void	performAction(Method method) Performs the given method.
protected void	performActionUsingGUI(Method method) Constructs the method GUI.
void	setExitAction(Action action) Sets the action for the exit button.
void	setGraphicsVisible(boolean visible) Sets the visibility of the graphics window.
protected void	setMethodButtonsEnabled(boolean enable) Enable or disable the method buttons.
void	toggleGraphics() Toggles the visibility of the graphics window by adding or removing the graphics panel from the GUI.

Methods inherited from class edu.neu.ccs.gui.DisplayPanel

add, add, add, add, add, addBorder, addObject, addObject, addObject, addObject, bevelBorderLowered, bevelBorderLowered, bevelBorderLowered, bevelBorderLowered, bevelBorderLowered, bevelBorderRaised, bevelBorderRaised, bevelBorderRaised, bevelBorderRaised, bevelBorderRaised, compoundBorder, compoundBorder, dataMalformed, emptyBorder, emptyBorder, emptyBorder, endAlert, etchBorderLowered, etchBorderLowered, etchBorderLowered, etchBorderRaised, etchBorderRaised, etchBorderRaised, frame, frame, frame, frame, frame, frame, generalDialog, generalDialog, generalDialog, generalDialog, getCodec, getDefaultViewState, getDefaultViewStates, getDisplayables, getViewState, getViewStates, lineBorder, lineBorder, lineBorder, lineBorder, makeComponent, matteBorder, matteBorder, matteBorder, matteBorder, matteBorder, matteBorder, OKCancelDialog, OKCancelDialog, OKDialog, OKDialog, refreshComponent, remove, remove, removeAll, removeBorder, reset, sandwichBorder, setCodec, setDeepBackground, setDeepBackground, setDefaultViewState, setDefaultViewStates, setEnabled, setViewState, setViewStates, startAlert, titleBorder, titleBorder, titleBorder, titleBorder, titleBorder, titleBorder, titleBorder, titleBorder, uniformizeHeight, uniformizeSize, uniformizeWidth, YesNoCancelDialog, YesNoCancelDialog

Methods inherited from class javax.swing.JPanel

getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI

Methods inherited from class javax.swing.JComponent

addAncestorListener, addNotify, addPropertyChangeListener, addPropertyChangeListener, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBorder, getBounds, getClientProperty, getComponentGraphics, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getGraphics, getHeight, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPreferredSize, getPropertyChangeListeners, getPropertyChangeListeners, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, isDoubleBuffered, isLightweightComponent, isManagingFocus, isMaximumSizeSet, isMinimumSizeSet, isOpaque, isOptimizedDrawingEnabled, isPaintingTile, isPreferredSizeSet, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removePropertyChangeListener, removePropertyChangeListener, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setFont, setForeground, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update

Methods inherited from class java.awt.Container

addContainerListener, addImpl, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, removeContainerListener, setFocusCycleRoot, setFocusTraversalKeys, setFocusTraversalPolicy, setLayout, 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, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMouseWheelListeners, getName, getParent, getPeer, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, hide, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processFocusEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processMouseEvent, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setFocusable, setFocusTraversalKeysEnabled, setIgnoreRepaint, setLocale, setLocation, setLocation, setName, setSize, setSize, 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

BUFFER_WIDTH

public static final int BUFFER_WIDTH

Default buffer width = 400.

See Also:

Constant Field Values

BUFFER_HEIGHT

public static final int BUFFER_HEIGHT

Default buffer height = 400.

See Also:

Constant Field Values

SCROLL_WIDTH

public static final int SCROLL_WIDTH

Default button scroll panel maximum width = 400.

See Also:

Constant Field Values

SCROLL_HEIGHT

public static final int SCROLL_HEIGHT

Default button scroll panel maximum height = 400.

See Also:

Constant Field Values

commonButtonColor

private static final Color commonButtonColor

Color of the common buttons.

exitButtonColor

private static final Color exitButtonColor

Color of the exit button.

methodButtonColor

private static final Color methodButtonColor

Color of the method buttons when enabled.

methodButtonColorDisabled

private static final Color methodButtonColorDisabled

Color of the method buttons when disabled.

initializer

protected Object initializer

Initializer object for the JPF methods to be displayed in the automatic GUI.

initializerClass

protected Class initializerClass

Class of the initializer object.

baseClass

protected Class baseClass

Base class for the initializer object; the code that recursively extracts JPF methods will stop the search when this base class is reached.

filter

protected MethodFilter filter

Method filter for extra pruning if any.

window

protected BufferedPanel window

Default graphics buffered panel.

showGraphics

protected boolean showGraphics

Whether or not to show the graphics window.

methodButtonsPanel

protected ActionsPanel methodButtonsPanel

Actions panel for the automatic JPF method buttons.

commonButtonsPanel

protected ActionsPanel commonButtonsPanel

Actions panel for the common actions.

exitButtonPanel

protected ActionsPanel exitButtonPanel

Actions panel for the exit action.

buttonsPanel

protected VTable buttonsPanel

Buttons panel that combines the three actions panels.

methodButtons

protected JButton[] methodButtons

Method buttons.

exitButton

protected JButton exitButton

Exit button.

LHS

protected DisplayPanel LHS

LHS of main GUI panel.

RHS

protected DisplayPanel RHS

RHS of main GUI panel.

mainPanel

protected HTable mainPanel

Main GUI panel.

clearGraphicsAction

protected Action clearGraphicsAction

Clear graphics action.

makeShapshotAction

protected Action makeShapshotAction

Make shapshot action.

exitAction

protected Action exitAction

Default application closing action. Calls:

    System.exit(0);

Constructor Detail

JPFPane

public JPFPane(Object initializer,
               Class baseClass)

Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; this constructor shows the graphics window.

If the initializer is null, then the GUI will show an error message and no internal data will be initialized.

If the base class is null, uses Object.class.

Parameters:

initializer - the object initializer for this pane

baseClass - the base class used to limit the method search

JPFPane

public JPFPane(Object initializer,
               Class baseClass,
               boolean showGraphics)

Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; this constructor shows the graphics window if the given boolean parameter is true.

If the initializer is null, then the GUI will show an error message and no internal data will be initialized.

If the base class is null, uses Object.class.

Parameters:

initializer - the object initializer for this pane

baseClass - the base class used to limit the method search

showGraphics - whether or not to show the graphics window

JPFPane

public JPFPane(Object initializer,
               Class baseClass,
               MethodFilter filter)

Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; in addition, provides a method filter that will further restrict the methods selected for the GUI; this constructor shows the graphics window.

If the initializer is null, then the GUI will show an error message and no internal data will be initialized.

If the base class is null, uses Object.class.

Parameters:

initializer - the object initializer for this pane

baseClass - the base class used to limit the method search

filter - the methods filter to further restrict the methods

JPFPane

public JPFPane(Object initializer,
               Class baseClass,
               MethodFilter filter,
               boolean showGraphics)

Constructs the GUI based on the given initializer object that defines the JPF methods used to create the method buttons and the base class that will limit how deep the recursive search for methods will go; in addition, provides a method filter that will further restrict the methods selected for the GUI; this constructor will show the graphics window if the given boolean parameter is true.

If the initializer is null, then the GUI will show an error message and no internal data will be initialized.

If the base class is null, uses Object.class.

Parameters:

initializer - the object initializer for this pane

baseClass - the base class used to limit the method search

filter - the methods filter to further restrict the methods

showGraphics - whether or not to show the graphics window

Method Detail

getInitializer

public final Object getInitializer()

Returns the initializer object for this pane.

getInitializerClass

public final Class getInitializerClass()

Returns the initializer object class.

getBaseClass

public final Class getBaseClass()

Returns the base class used to limit how deep the recursive search for methods will go.

getMethodFilter

public final MethodFilter getMethodFilter()

Returns the method filter if any.

getGraphicsWindow

public final BufferedPanel getGraphicsWindow()

Returns the graphics window.

clearGraphics

public final void clearGraphics()

Clears the graphics window.

isGraphicsVisible

public final boolean isGraphicsVisible()

Returns whether or not the graphics window is visible.

setGraphicsVisible

public final void setGraphicsVisible(boolean visible)

Sets the visibility of the graphics window.

Does nothing if visibility will not change.

Is it the responsibility of the caller to do whatever revalidation or packing is needed to force the enclosing GUI to update.

Parameters:

visible - the desired visibility setting

toggleGraphics

public final void toggleGraphics()

Toggles the visibility of the graphics window by adding or removing the graphics panel from the GUI.

Is it the responsibility of the caller to do whatever revalidation or packing is needed to force the enclosing GUI to update.

makeShapshot

public final void makeShapshot()

Makes a shapshot of the graphics windows 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 external 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();

addCommonButton

public final void addCommonButton(Action action,
                                  String tooltip)

Allows the user of this class to add a common button by providing its action and tooltip.

This method will create the button, make its backgroundcolor commonButtonColor, and install the tooltip assuming it is non-null. The method uniformizeWidth() will then be called on the panel that contains all common buttons.

This method was introduced to permit the class JPF to install buttons that are not appropriate for the class JPFApplet. It is public to allow other possible applications.

Parameters:

action - the action that defines the button

tooltip - the button tooltip

setExitAction

public final void setExitAction(Action action)

Sets the action for the exit button.

By default, the exit behavior in this class is simply:

    System.exit(0)

This method allows a caller to replace the default exit action in order to add additional clean-up behavior to the exit process. It is strongly recommended that any action used to replace the default action end with a call to System.exit(0).

Ignores a null action parameter.

Parameters:

action - the action to use for the exit action

exitFramework

public final void exitFramework()

Exits the framework by programmatically invoking 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.

buildGUI

protected void buildGUI()

Build the main panel.

buildButtons

protected void buildButtons()

Build the buttons and the buttons panel.

addOneButton

protected JButton addOneButton(ActionsPanel panel,
                               Action action,
                               String tooltip)

Adds one button with the given action and tool tip to the given panel and then returns the button.

Returns null if either the given panel or the given action is null.

Ignores the tool tip if it is null.

Parameters:

panel - the actions panel to hold the button

action - the action to define the button

tooltip - the tool tip for the button

setMethodButtonsEnabled

protected void setMethodButtonsEnabled(boolean enable)

Enable or disable the method buttons.

Parameters:

enable - whether or not to enable.

getMethodList

protected Method[] getMethodList()

Returns a list of the JPF methods, that is, the methods for which we can instantiate buttons in the main GUI.

Here is the current implementation.

The first step is to create the list of possible methods using:

    JPFHelper.getPublicMethods(initializerClass, baseClass)

This list is then pruned using:

    JPFHelper.acceptJPFMethods

Duplicate virtual methods are then pruned using:

    JPFHelper.removeDuplicateVirtualMethods

This list is then pruned by the MethodFilter provided in a constructor if that filter is non-null.

The list returned may contain null objects if some methods have indeed been pruned.

makeActionFromMethod

protected Action makeActionFromMethod(Method method)

Makes a ThreadedAction from the given method.

performAction

protected void performAction(Method method)

Performs the given method.

If the method does not require a method GUI, then it is executed directly. In that case, this method is syncronized on the initializer object.

If the method requires a GUI, then the GUI is constructed and further execution is done via that GUI.

performActionUsingGUI

protected void performActionUsingGUI(Method method)

Constructs the method GUI. Further execution is done via that GUI.