public class AbstractionPredicatesChoiceDialog
extends javax.swing.JDialog
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.
|
javax.swing.JDialog.AccessibleJDialog
java.awt.Dialog.AccessibleAWTDialog, java.awt.Dialog.ModalExclusionType, java.awt.Dialog.ModalityType
java.awt.Window.AccessibleAWTWindow, java.awt.Window.Type
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 |
accessibleContext, rootPane, rootPaneCheckingEnabled
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
Modifier | Constructor and Description |
---|---|
private |
AbstractionPredicatesChoiceDialog()
Constructs a new
AbstractionPredicatesChoiceDialog . |
|
AbstractionPredicatesChoiceDialog(Goal goal,
java.util.List<LocationVariable> differingLocVars)
Constructs a new
AbstractionPredicatesChoiceDialog . |
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) |
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
addNotify, getModalityType, getTitle, hide, isModal, isResizable, isUndecorated, setBackground, setModal, setModalityType, setOpacity, setResizable, setShape, setTitle, setUndecorated, setVisible, show, toBack
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
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
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
private static final java.lang.String AVAILABLE_PROGRAM_VARIABLES_DESCR
private static final long serialVersionUID
private static final MainWindow MAIN_WINDOW_INSTANCE
private static final java.awt.Dimension INITIAL_SIZE
private static final java.lang.String DIALOG_TITLE
private Goal goal
private java.util.ArrayList<AbstractionPredicate> registeredPredicates
private java.util.ArrayList<AbstractDomainElemChoice> abstrPredicateChoices
private java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType
private final ObservableArrayList<java.lang.String> placeholdersProblemsListData
private final ObservableArrayList<java.lang.String> abstrPredProblemsListData
public AbstractionPredicatesChoiceDialog(Goal goal, java.util.List<LocationVariable> differingLocVars)
AbstractionPredicatesChoiceDialog
. The given
goal is used to get information about the proof.goal
- The goal on which the merge rule is applied.differingLocVars
- Location variables the values of which differ in the merge
partner states.private AbstractionPredicatesChoiceDialog()
AbstractionPredicatesChoiceDialog
.private java.util.ArrayList<AbstractionPredicate> getRegisteredPredicates()
private java.lang.Class<? extends AbstractPredicateAbstractionLattice> getLatticeType()
AbstractPredicateAbstractionLattice
).public AbstractionPredicatesChoiceDialog.Result getResult()
private void createDialog()
private javax.swing.JPanel createChoiceAbstrPredsPanel()
private javax.swing.JPanel createProblemsLabelContainer()
private javax.swing.JPanel createPlaceholderVariablesPanel()
private javax.swing.JPanel createAbstractionPredicatesPanel()
private javax.swing.JPanel createLatticeTypePanel()
private javax.swing.JPanel createInfoPanel()
private Pair<Sort,Name> parsePlaceholder(java.lang.String input)
MergeRuleUtils.parsePlaceholder(String, Services)
.input
- The input to parse.private AbstractionPredicate parsePredicate(java.lang.String input, NamespaceSet localNamespaces) throws ParserException
MergeRuleUtils.parsePredicate(String, ArrayList, NamespaceSet, Services)
.input
- The input to parse.localNamespaces
- The local NamespaceSet
.ParserException
- If there is a mistake in the input.private java.lang.String abstrPredToStringRepr(java.util.Optional<AbstractPredicateAbstractionDomainElement> domElem)
domElem
- The abstraction predicate to convert into a String
representation.private java.lang.String abstrPredToString(AbstractionPredicate pred)
pred
- Predicate to compute a String representation for.private static java.net.URL getURLForResourceFile(java.lang.Class<?> cl, java.lang.String filename)
private static java.lang.String readFromURL(java.net.URL url)
private static java.lang.String readFromResourceFile(java.lang.String filename)
public static void main(java.lang.String[] args)
static Proof loadProof(java.lang.String proofFileName)
proofFileName
- The file name of the proof file to load.