verf.mdverif.cg
Class MDVerifCG

java.lang.Object
  extended by java.awt.Component
      extended by java.awt.Container
          extended by javax.swing.JComponent
              extended by javax.swing.JPanel
                  extended by verf.mdverif.cg.MDVerifCG
All Implemented Interfaces:
java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.accessibility.Accessible

public class MDVerifCG
extends javax.swing.JPanel

Computation graph class.

Author:
Bc. Marek Gach
See Also:
Serialized Form

Nested Class Summary
 
Nested classes/interfaces inherited from class javax.swing.JPanel
javax.swing.JPanel.AccessibleJPanel
 
Nested classes/interfaces inherited from class javax.swing.JComponent
javax.swing.JComponent.AccessibleJComponent
 
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 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.Component
BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT
 
Fields inherited from interface java.awt.image.ImageObserver
ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH
 
Constructor Summary
MDVerifCG()
          Default constructor.
 
Method Summary
 void addNode(MDVerifCGNode node)
          Adds node into CG.
 void addTrans(MDVerifCGTrans trans)
          Adds transition into CG.
 java.util.Vector findSameGMode(MDVerifCGNode node)
          Allows to find the same global mode.
 void generateRTL(java.io.File file, java.util.Vector formulas, MDVerifSGManager sgmanager)
          Allows to generate RTL formulas of given specification
 java.util.Vector getConflictingNodes()
          Gets conflicting nodes from CG graph visualisation.
 MDVerifCGNode getReferencePoint(MDVerifTrans trans, MDVerifCGNode cgnode)
          Returns reference point for given transition up from specified node in SG graph.
 java.util.Vector getTempNodes()
          Allows to get temporal CG nodes.
 int getTotalIsomorphicNodes()
          Allows to get isomorphic CG nodes.
 int getTotalNodes()
          Gets total CG nodes count.
 int getTotalTransCount()
          Gets total CG transition count.
 int getTotalTreeNodes()
          Get total sum of tree nodes.
 int getTotalUnreachableNodes()
          Get total sum of unreachable nodes.
 MDVerifCGNode getUnexpandedNode()
          Get total sum of unexpanded nodes.
 void paint(java.awt.Graphics g)
          Paint CG into canvas.
 void printInfo()
          Prints info abou transitions and nodes.
 void reinit()
          Reinits class and removes all nodes and transitions.
 void removeNode(MDVerifCGNode node)
          Removes node from CG graph together with all transitions.
 void removeTransitions(MDVerifCGNode node)
          Removes all transitions containing given CG node as source or destination.
 void setShowIsomorphic(boolean selected)
          Allows to show isomorphic nodes.
 void setShowOrdinal(boolean selected)
          Allows to show ordinal nodes.
 void setShowUnreachable(boolean selected)
          Allows to show unreachable nodes.
 void update(java.awt.Graphics g)
          Update graphics method.
 boolean verifyFormula(MDVerifFormula formula, MDVerifSGManager sg)
          Allows to verify given formula against CG and SEP
 
Methods inherited from class javax.swing.JPanel
getAccessibleContext, getUI, getUIClassID, paramString, setUI, updateUI
 
Methods inherited from class javax.swing.JComponent
addAncestorListener, addNotify, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAncestorListeners, getAutoscrolls, getBaseline, getBaselineResizeBehavior, getBorder, getBounds, getClientProperty, getComponentGraphics, getComponentPopupMenu, getConditionForKeyStroke, getDebugGraphicsOptions, getDefaultLocale, getFontMetrics, getGraphics, getHeight, getInheritsPopupMenu, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPopupLocation, getPreferredSize, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getTransferHandler, getVerifyInputWhenFocusTarget, getVetoableChangeListeners, getVisibleRect, getWidth, getX, getY, grabFocus, isDoubleBuffered, isLightweightComponent, isManagingFocus, isOpaque, isOptimizedDrawingEnabled, isPaintingForPrint, isPaintingTile, isRequestFocusEnabled, isValidateRoot, paintBorder, paintComponent, paintChildren, paintImmediately, paintImmediately, print, printAll, printBorder, printComponent, printChildren, processComponentKeyEvent, processKeyBinding, processKeyEvent, processMouseEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, requestFocus, requestFocusInWindow, requestFocusInWindow, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setComponentPopupMenu, setDebugGraphicsOptions, setDefaultLocale, setDoubleBuffered, setEnabled, setFocusTraversalKeys, setFont, setForeground, setInheritsPopupMenu, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setTransferHandler, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction
 
Methods inherited from class java.awt.Container
add, add, add, add, add, addContainerListener, addImpl, addPropertyChangeListener, addPropertyChangeListener, applyComponentOrientation, areFocusTraversalKeysSet, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getComponentZOrder, getContainerListeners, getFocusTraversalKeys, getFocusTraversalPolicy, getLayout, getMousePosition, insets, invalidate, isAncestorOf, isFocusCycleRoot, isFocusCycleRoot, isFocusTraversalPolicyProvider, isFocusTraversalPolicySet, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setComponentZOrder, setFocusCycleRoot, setFocusTraversalPolicy, setFocusTraversalPolicyProvider, setLayout, transferFocusBackward, transferFocusDownCycle, validate, validateTree
 
Methods inherited from class java.awt.Component
action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, addMouseWheelListener, bounds, coalesceEvents, contains, createImage, createImage, createVolatileImage, createVolatileImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, getBackground, getBounds, getColorModel, getComponentListeners, getComponentOrientation, getCursor, getDropTarget, getFocusCycleRootAncestor, getFocusListeners, getFocusTraversalKeysEnabled, getFont, getForeground, getGraphicsConfiguration, getHierarchyBoundsListeners, getHierarchyListeners, getIgnoreRepaint, getInputContext, getInputMethodListeners, getInputMethodRequests, getKeyListeners, getLocale, getLocation, getLocationOnScreen, getMouseListeners, getMouseMotionListeners, getMousePosition, getMouseWheelListeners, getName, getParent, getPeer, getPropertyChangeListeners, getPropertyChangeListeners, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, hasFocus, hide, checkImage, checkImage, imageUpdate, inside, isBackgroundSet, isCursorSet, isDisplayable, isEnabled, isFocusable, isFocusOwner, isFocusTraversable, isFontSet, isForegroundSet, isLightweight, isMaximumSizeSet, isMinimumSizeSet, isPreferredSizeSet, 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, processMouseWheelEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, removeMouseWheelListener, removePropertyChangeListener, removePropertyChangeListener, 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
 

Constructor Detail

MDVerifCG

public MDVerifCG()
Default constructor.

Method Detail

reinit

public void reinit()
Reinits class and removes all nodes and transitions.


generateRTL

public void generateRTL(java.io.File file,
                        java.util.Vector formulas,
                        MDVerifSGManager sgmanager)
Allows to generate RTL formulas of given specification

Parameters:
file - Filename to save into.
formulas - Vector of SA formulas.
sgmanager - SGManager reference.

getReferencePoint

public MDVerifCGNode getReferencePoint(MDVerifTrans trans,
                                       MDVerifCGNode cgnode)
Returns reference point for given transition up from specified node in SG graph.

Parameters:
trans - Transtion for reference.
cgnode - Base cg node.
Returns:
Reference point for given transition.

getTempNodes

public java.util.Vector getTempNodes()
Allows to get temporal CG nodes.

Returns:
Temporal CG nodes.

getTotalIsomorphicNodes

public int getTotalIsomorphicNodes()
Allows to get isomorphic CG nodes.

Returns:
Isomorphic CG nodes.

getTotalNodes

public int getTotalNodes()
Gets total CG nodes count.

Returns:
Returns total CG nodes count.

getTotalTransCount

public int getTotalTransCount()
Gets total CG transition count.

Returns:
Total CG transition count.

getTotalTreeNodes

public int getTotalTreeNodes()
Get total sum of tree nodes.

Returns:
Total sum of tree nodes.

getTotalUnreachableNodes

public int getTotalUnreachableNodes()
Get total sum of unreachable nodes.

Returns:
Total sum of unreachable nodes.

getUnexpandedNode

public MDVerifCGNode getUnexpandedNode()
Get total sum of unexpanded nodes.

Returns:
Total sum of unexpanded nodes.

printInfo

public void printInfo()
Prints info abou transitions and nodes.


removeNode

public void removeNode(MDVerifCGNode node)
Removes node from CG graph together with all transitions.

Parameters:
node - Node which we are going to remove.

setShowIsomorphic

public void setShowIsomorphic(boolean selected)
Allows to show isomorphic nodes.

Parameters:
selected - Boolean value.

setShowOrdinal

public void setShowOrdinal(boolean selected)
Allows to show ordinal nodes.

Parameters:
selected - Boolean value.

setShowUnreachable

public void setShowUnreachable(boolean selected)
Allows to show unreachable nodes.

Parameters:
selected - Boolean value.

update

public void update(java.awt.Graphics g)
Update graphics method.

Overrides:
update in class javax.swing.JComponent
Parameters:
g - Graphics.

paint

public void paint(java.awt.Graphics g)
Paint CG into canvas.

Overrides:
paint in class javax.swing.JComponent
Parameters:
g - Graphics.

addNode

public void addNode(MDVerifCGNode node)
Adds node into CG.

Parameters:
node - Node reference.

addTrans

public void addTrans(MDVerifCGTrans trans)
Adds transition into CG.

Parameters:
trans - Transition to add.

verifyFormula

public boolean verifyFormula(MDVerifFormula formula,
                             MDVerifSGManager sg)
Allows to verify given formula against CG and SEP

Parameters:
formula - Formula we are going to verify.
sg - Separation graph manager reference.
Returns:
Truth value if formula is satisfied by system model or not.

findSameGMode

public java.util.Vector findSameGMode(MDVerifCGNode node)
Allows to find the same global mode.

Parameters:
node - CG node.
Returns:
Vector of CG nodes with same Global mode.

removeTransitions

public void removeTransitions(MDVerifCGNode node)
Removes all transitions containing given CG node as source or destination.

Parameters:
node - Node which we are going to analyze.

getConflictingNodes

public java.util.Vector getConflictingNodes()
Gets conflicting nodes from CG graph visualisation.

Returns:
Conflicting graphs vector.