public class JoinPartnerSelectionDialog extends JDialog
JDialog.AccessibleJDialog
Dialog.AccessibleAWTDialog, Dialog.ModalExclusionType, Dialog.ModalityType
Window.AccessibleAWTWindow, Window.Type
Container.AccessibleAWTContainer
Component.AccessibleAWTComponent, Component.BaselineResizeBehavior, Component.BltBufferStrategy, Component.FlipBufferStrategy
accessibleContext, rootPane, rootPaneCheckingEnabled
DEFAULT_MODALITY_TYPE
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
DISPOSE_ON_CLOSE, DO_NOTHING_ON_CLOSE, EXIT_ON_CLOSE, HIDE_ON_CLOSE
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
Modifier | Constructor and Description |
---|---|
private |
JoinPartnerSelectionDialog() |
|
JoinPartnerSelectionDialog(Goal joinGoal,
PosInOccurrence pio,
ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> candidates,
Services services)
Creates a new join partner selection dialog.
|
Modifier and Type | Method and Description |
---|---|
private void |
checkApplicable()
Enables / disables the OK and Choose all button depending on whether or
not the currently chosen join rule instance is applicable.
|
private static boolean |
checkProvability(Sequent seq,
Term formulaToProve,
Services services)
Checks whether the given formula can be proven within the given sequent.
|
ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> |
getChosenCandidates() |
Term |
getChosenDistinguishingFormula() |
JoinProcedure |
getChosenJoinRule() |
private Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>> |
getNthCandidate(int n)
Returns the n-th candidate in the list.
|
private Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>> |
getSelectedCandidate() |
private <T> ImmutableList<T> |
immutableListFromIterabe(Iterable<T> it) |
private boolean |
isApplicableForCandidates(ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> theCandidates)
Checks whether the join rule is applicable for the given set of
candidates.
|
private boolean |
isSuitableDistFormula()
Checks whether the selected distinguishable formula is actually suitable
for this purpose.
|
private void |
loadCandidates()
Loads the join candidates into the combo box, initializes the partner
editor pane with the text of the first candidate.
|
static void |
main(String[] args) |
private void |
setHighlightedSequentForArea(Goal goal,
PosInOccurrence pio,
JEditorPane area)
Adds the given goal to the given editor pane, with the portion that
corresponds to the given position highlighted in bold.
|
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 long serialVersionUID
private static final String CB_SELECT_CANDIDATE_HINT
private static final String CHOOSE_ALL_BTN_TOOLTIP_TXT
private static final String OK_BTN_TOOLTIP_TXT
private static final Dimension INITIAL_SIZE
private static final Font TXT_AREA_FONT
private static final MainWindow MAIN_WINDOW_INSTANCE
private static Comparator<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> GOAL_COMPARATOR
private LinkedList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> candidates
private Services services
private Pair<Goal,PosInOccurrence> joinGoalPio
private SortedSet<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> chosenGoals
private JoinProcedure chosenRule
private Term chosenDistForm
private JEditorPane txtPartner1
private JEditorPane txtPartner2
private JCheckBox cbSelectCandidate
private ButtonGroup bgJoinMethods
private final JTextField txtDistForm
private JScrollPane scrpPartner1
private JScrollPane scrpPartner2
private JButton okButton
private JButton chooseAllButton
private JoinPartnerSelectionDialog()
public JoinPartnerSelectionDialog(Goal joinGoal, PosInOccurrence pio, ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> candidates, Services services)
joinGoal
- The first (already chosen) join partner.pio
- Position of Update-Modality-Postcondition formula in the
joinNode.candidates
- Potential join candidates.services
- The services object.public static void main(String[] args)
public ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> getChosenCandidates()
public JoinProcedure getChosenJoinRule()
public Term getChosenDistinguishingFormula()
private boolean isApplicableForCandidates(ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> theCandidates)
theCandidates
- Candidates to instantiate the join rule application with.private void checkApplicable()
private boolean isSuitableDistFormula()
private static boolean checkProvability(Sequent seq, Term formulaToProve, Services services)
seq
- Sequent in which to check the provability of formulaToProve.formulaToProve
- Formula to prove.private <T> ImmutableList<T> immutableListFromIterabe(Iterable<T> it)
it
- Iterable to convert into an ImmutableList.private Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>> getSelectedCandidate()
private Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>> getNthCandidate(int n)
n
- Index of the join candidate.private void loadCandidates()
private void setHighlightedSequentForArea(Goal goal, PosInOccurrence pio, JEditorPane area)
goal
- Goal to add.pio
- Position indicating subterm to highlight.area
- The editor pane to add the highlighted goal to.