de.uka.ilkd.key.gui.mergerule.predicateabstraction

Class AbstractionPredicatesChoiceDialog

java.lang.Object

java.awt.Component

java.awt.Container

java.awt.Window

java.awt.Dialog

javax.swing.JDialog

de.uka.ilkd.key.gui.mergerule.predicateabstraction.AbstractionPredicatesChoiceDialog

All Implemented Interfaces:

java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible, javax.swing.RootPaneContainer, javax.swing.WindowConstants

public class AbstractionPredicatesChoiceDialog
extends javax.swing.JDialog

A Swing reimplementation of the (much nicer) JavaFX abstraction predicates choice dialog -- since JavaFX got removed from Oracle Java.

Author:

Dominic Steinhoefel

See Also:

Serialized Form

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	AbstractionPredicatesChoiceDialog.ChoiceTableModel
(package private) class	AbstractionPredicatesChoiceDialog.DomElemChoiceTable
(package private) class	AbstractionPredicatesChoiceDialog.Result Encapsulates the results supplied by the user.

Nested classes/interfaces inherited from class javax.swing.JDialog

javax.swing.JDialog.AccessibleJDialog

Nested classes/interfaces inherited from class java.awt.Dialog

java.awt.Dialog.AccessibleAWTDialog, java.awt.Dialog.ModalExclusionType, java.awt.Dialog.ModalityType

Nested classes/interfaces inherited from class java.awt.Window

java.awt.Window.AccessibleAWTWindow, java.awt.Window.Type

Nested classes/interfaces inherited from class java.awt.Container

java.awt.Container.AccessibleAWTContainer

Nested classes/interfaces inherited from class java.awt.Component

java.awt.Component.AccessibleAWTComponent, java.awt.Component.BaselineResizeBehavior, java.awt.Component.BltBufferStrategy, java.awt.Component.FlipBufferStrategy

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.ArrayList<AbstractDomainElemChoice>	abstrPredicateChoices
private ObservableArrayList<java.lang.String>	abstrPredProblemsListData
private static java.lang.String	AVAILABLE_PROGRAM_VARIABLES_DESCR
private static java.lang.String	DIALOG_TITLE
private Goal	goal
private static java.awt.Dimension	INITIAL_SIZE The initial size of this dialog.
private java.lang.Class<? extends AbstractPredicateAbstractionLattice>	latticeType
private static MainWindow	MAIN_WINDOW_INSTANCE
private ObservableArrayList<java.lang.String>	placeholdersProblemsListData
private java.util.ArrayList<Pair<Sort,Name>>	registeredPlaceholders
private java.util.ArrayList<AbstractionPredicate>	registeredPredicates
private static long	serialVersionUID

Fields inherited from class javax.swing.JDialog

accessibleContext, rootPane, rootPaneCheckingEnabled

Fields inherited from class java.awt.Dialog

DEFAULT_MODALITY_TYPE

Fields inherited from class java.awt.Component

BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface javax.swing.WindowConstants

DISPOSE_ON_CLOSE, DO_NOTHING_ON_CLOSE, EXIT_ON_CLOSE, HIDE_ON_CLOSE

Fields inherited from interface java.awt.image.ImageObserver

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

Constructor Summary

Constructors

Modifier	Constructor and Description
private	AbstractionPredicatesChoiceDialog() Constructs a new AbstractionPredicatesChoiceDialog.
	AbstractionPredicatesChoiceDialog(Goal goal, java.util.List<LocationVariable> differingLocVars) Constructs a new AbstractionPredicatesChoiceDialog.

Method Summary

Modifier and Type	Method and Description
private java.lang.String	abstrPredToString(AbstractionPredicate pred) Returns a String representation of an abstraction predicate.
private java.lang.String	abstrPredToStringRepr(java.util.Optional<AbstractPredicateAbstractionDomainElement> domElem) A String representation of an abstraction predicate, that is a "pair" expression of the placeholder variable and the predicate term of the form "(PROGVAR,PREDTERM)".
private javax.swing.JPanel	createAbstractionPredicatesPanel()
private javax.swing.JPanel	createChoiceAbstrPredsPanel()
private void	createDialog()
private javax.swing.JPanel	createInfoPanel()
private javax.swing.JPanel	createLatticeTypePanel()
private javax.swing.JPanel	createPlaceholderVariablesPanel()
private javax.swing.JPanel	createProblemsLabelContainer()
private java.lang.Class<? extends AbstractPredicateAbstractionLattice>	getLatticeType()
private java.util.ArrayList<AbstractionPredicate>	getRegisteredPredicates()
AbstractionPredicatesChoiceDialog.Result	getResult()
private static java.net.URL	getURLForResourceFile(java.lang.Class<?> cl, java.lang.String filename)
(package private) static Proof	loadProof(java.lang.String proofFileName) Loads the given proof file.
static void	main(java.lang.String[] args)
private Pair<Sort,Name>	parsePlaceholder(java.lang.String input) Parses a placeholder using MergeRuleUtils.parsePlaceholder(String, Services).
private AbstractionPredicate	parsePredicate(java.lang.String input, NamespaceSet localNamespaces) Parses an abstraction predicate using MergeRuleUtils.parsePredicate(String, ArrayList, NamespaceSet, Services).
private static java.lang.String	readFromResourceFile(java.lang.String filename)
private static java.lang.String	readFromURL(java.net.URL url)

Methods inherited from class javax.swing.JDialog

addImpl, createRootPane, dialogInit, getAccessibleContext, getContentPane, getDefaultCloseOperation, getGlassPane, getGraphics, getJMenuBar, getLayeredPane, getRootPane, getTransferHandler, isDefaultLookAndFeelDecorated, isRootPaneCheckingEnabled, paramString, processWindowEvent, remove, repaint, setContentPane, setDefaultCloseOperation, setDefaultLookAndFeelDecorated, setGlassPane, setJMenuBar, setLayeredPane, setLayout, setRootPane, setRootPaneCheckingEnabled, setTransferHandler, update

Methods inherited from class java.awt.Dialog

addNotify, getModalityType, getTitle, hide, isModal, isResizable, isUndecorated, setBackground, setModal, setModalityType, setOpacity, setResizable, setShape, setTitle, setUndecorated, setVisible, show, toBack

Methods inherited from class java.awt.Window

addPropertyChangeListener, addPropertyChangeListener, addWindowFocusListener, addWindowListener, addWindowStateListener, applyResourceBundle, applyResourceBundle, createBufferStrategy, createBufferStrategy, dispose, getBackground, getBufferStrategy, getFocusableWindowState, getFocusCycleRootAncestor, getFocusOwner, getFocusTraversalKeys, getIconImages, getInputContext, getListeners, getLocale, getModalExclusionType, getMostRecentFocusOwner, getOpacity, getOwnedWindows, getOwner, getOwnerlessWindows, getShape, getToolkit, getType, getWarningString, getWindowFocusListeners, getWindowListeners, getWindows, getWindowStateListeners, isActive, isAlwaysOnTop, isAlwaysOnTopSupported, isAutoRequestFocus, isFocusableWindow, isFocusCycleRoot, isFocused, isLocationByPlatform, isOpaque, isShowing, isValidateRoot, pack, paint, postEvent, processEvent, processWindowFocusEvent, processWindowStateEvent, removeNotify, removeWindowFocusListener, removeWindowListener, removeWindowStateListener, reshape, setAlwaysOnTop, setAutoRequestFocus, setBounds, setBounds, setCursor, setFocusableWindowState, setFocusCycleRoot, setIconImage, setIconImages, setLocation, setLocation, setLocationByPlatform, setLocationRelativeTo, setMinimumSize, setModalExclusionType, setSize, setSize, setType, toFront

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getAlignmentX, getAlignmentY, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalPolicy, getInsets, getLayout, getMaximumSize, getMinimumSize, getMousePosition, getPreferredSize, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, print, printComponents, processContainerEvent, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusTraversalKeys, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setFont, 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, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBaseline, getBaselineResizeBehavior, getBounds, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getHeight, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocation, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getSize, getTreeLock, getWidth, getX, getY, gotFocus, handleEvent, hasFocus, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isDoubleBuffered, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, 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, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resize, resize, revalidate, setComponentOrientation, setDropTarget, setEnabled, setFocusable, setFocusTraversalKeysEnabled, setForeground, setIgnoreRepaint, setLocale, setMaximumSize, setName, setPreferredSize, show, size, toString, transferFocus, transferFocusBackward, transferFocusUpCycle

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

AVAILABLE_PROGRAM_VARIABLES_DESCR

private static final java.lang.String AVAILABLE_PROGRAM_VARIABLES_DESCR

See Also:

Constant Field Values

serialVersionUID

private static final long serialVersionUID

See Also:

Constant Field Values

MAIN_WINDOW_INSTANCE

private static final MainWindow MAIN_WINDOW_INSTANCE

INITIAL_SIZE

private static final java.awt.Dimension INITIAL_SIZE

The initial size of this dialog.

DIALOG_TITLE

private static final java.lang.String DIALOG_TITLE

See Also:

Constant Field Values

goal

private Goal goal

registeredPlaceholders

private java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders

registeredPredicates

private java.util.ArrayList<AbstractionPredicate> registeredPredicates

abstrPredicateChoices

private java.util.ArrayList<AbstractDomainElemChoice> abstrPredicateChoices

latticeType

private java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType

placeholdersProblemsListData

private final ObservableArrayList<java.lang.String> placeholdersProblemsListData

abstrPredProblemsListData

private final ObservableArrayList<java.lang.String> abstrPredProblemsListData

Constructor Detail

AbstractionPredicatesChoiceDialog

public AbstractionPredicatesChoiceDialog(Goal goal,
                                         java.util.List<LocationVariable> differingLocVars)

Constructs a new AbstractionPredicatesChoiceDialog. The given goal is used to get information about the proof.

Parameters:

goal - The goal on which the merge rule is applied.

differingLocVars - Location variables the values of which differ in the merge partner states.

AbstractionPredicatesChoiceDialog

private AbstractionPredicatesChoiceDialog()

Constructs a new AbstractionPredicatesChoiceDialog.

Method Detail

getRegisteredPredicates

private java.util.ArrayList<AbstractionPredicate> getRegisteredPredicates()

Returns:

The abstraction predicates set by the user. Is null iff the user pressed cancel.

getLatticeType

private java.lang.Class<? extends AbstractPredicateAbstractionLattice> getLatticeType()

Returns:

The chosen lattice type (class object for class that is an instance of AbstractPredicateAbstractionLattice).

getResult

public AbstractionPredicatesChoiceDialog.Result getResult()

Returns:

The resulting input supplied by the user.

createDialog

private void createDialog()

createChoiceAbstrPredsPanel

private javax.swing.JPanel createChoiceAbstrPredsPanel()

createProblemsLabelContainer

private javax.swing.JPanel createProblemsLabelContainer()

createPlaceholderVariablesPanel

private javax.swing.JPanel createPlaceholderVariablesPanel()

createAbstractionPredicatesPanel

private javax.swing.JPanel createAbstractionPredicatesPanel()

createLatticeTypePanel

private javax.swing.JPanel createLatticeTypePanel()

createInfoPanel

private javax.swing.JPanel createInfoPanel()

parsePlaceholder

private Pair<Sort,Name> parsePlaceholder(java.lang.String input)

Parses a placeholder using MergeRuleUtils.parsePlaceholder(String, Services).

Parameters:

input - The input to parse.

Returns:

The parsed placeholder (sort and name).

parsePredicate

private AbstractionPredicate parsePredicate(java.lang.String input,
                                            NamespaceSet localNamespaces)
                                     throws ParserException

Parses an abstraction predicate using MergeRuleUtils.parsePredicate(String, ArrayList, NamespaceSet, Services).

Parameters:

input - The input to parse.

localNamespaces - The local NamespaceSet.

Returns:

The parsed abstraction predicate.

Throws:

ParserException - If there is a mistake in the input.

abstrPredToStringRepr

private java.lang.String abstrPredToStringRepr(java.util.Optional<AbstractPredicateAbstractionDomainElement> domElem)

A String representation of an abstraction predicate, that is a "pair" expression of the placeholder variable and the predicate term of the form "(PROGVAR,PREDTERM)".

Parameters:

domElem - The abstraction predicate to convert into a String representation.

Returns:

A String representation of the given abstraction predicate.

abstrPredToString

private java.lang.String abstrPredToString(AbstractionPredicate pred)

Returns a String representation of an abstraction predicate.

Parameters:

pred - Predicate to compute a String representation for.

Returns:

A String representation of an abstraction predicate.

getURLForResourceFile

private static java.net.URL getURLForResourceFile(java.lang.Class<?> cl,
                                                  java.lang.String filename)

readFromURL

private static java.lang.String readFromURL(java.net.URL url)

readFromResourceFile

private static java.lang.String readFromResourceFile(java.lang.String filename)

main

public static void main(java.lang.String[] args)

loadProof

static Proof loadProof(java.lang.String proofFileName)

Loads the given proof file. Checks if the proof file exists and the proof is not null, and fails if the proof could not be loaded.

Parameters:

proofFileName - The file name of the proof file to load.

Returns:

The loaded proof.