[8780cbec] | 1 | package com.algomagic.atn.vis; |
---|
| 2 | import att.grappa.*; |
---|
| 3 | |
---|
| 4 | import java.util.Properties; |
---|
| 5 | import java.util.Enumeration; |
---|
| 6 | import java.io.*; |
---|
| 7 | |
---|
| 8 | import java.awt.*; |
---|
| 9 | import java.awt.event.*; |
---|
| 10 | import java.awt.geom.*; |
---|
| 11 | import javax.swing.*; |
---|
| 12 | import javax.swing.border.*; |
---|
| 13 | |
---|
| 14 | |
---|
| 15 | public class ATNVisualizer extends JFrame |
---|
| 16 | implements ATNVisualizerConstants, GrappaConstants { |
---|
| 17 | |
---|
| 18 | private Properties _properties; |
---|
| 19 | private GrappaPanel _grappaPanel; |
---|
| 20 | private Graph _graph; |
---|
| 21 | |
---|
| 22 | |
---|
| 23 | |
---|
| 24 | public ATNVisualizer( String log1, String log2 ) { |
---|
| 25 | initATNVisualizer( log1, log2 ); |
---|
| 26 | } |
---|
| 27 | |
---|
| 28 | |
---|
| 29 | private void initATNVisualizer( String log1, String log2 ) { |
---|
| 30 | loadProperties( ); |
---|
| 31 | |
---|
| 32 | addWindowListener( new WindowAdapter( ) { |
---|
| 33 | public void windowClosing( WindowEvent we ) { |
---|
| 34 | Window w = we.getWindow( ); |
---|
| 35 | w.setVisible( false ); |
---|
| 36 | w.dispose( ); |
---|
| 37 | System.exit( 0 ); |
---|
| 38 | } |
---|
| 39 | }); |
---|
| 40 | |
---|
| 41 | |
---|
| 42 | SidePanel leftSide = new SidePanel( log1, LEFT_SIDE ); |
---|
| 43 | SidePanel rightSide = null; |
---|
| 44 | |
---|
| 45 | Container contentPane = getContentPane( ); |
---|
| 46 | contentPane.setLayout( new BoxLayout( contentPane, BoxLayout.X_AXIS ) ); |
---|
| 47 | contentPane.add( leftSide ); |
---|
| 48 | |
---|
| 49 | |
---|
| 50 | if( log2 != null ) { |
---|
| 51 | rightSide = new SidePanel( log2, RIGHT_SIDE ); |
---|
| 52 | contentPane.add( rightSide ); |
---|
| 53 | } |
---|
| 54 | |
---|
| 55 | |
---|
| 56 | |
---|
| 57 | setTitle( _properties.getProperty( WINDOW_TITLE_PROP, WINDOW_TITLE_DEFAULT ) ); |
---|
| 58 | setSize( Integer.parseInt( _properties.getProperty( WINDOW_WIDTH_PROP, WINDOW_WIDTH_DEFAULT ) ), |
---|
| 59 | Integer.parseInt( _properties.getProperty( WINDOW_HEIGHT_PROP, WINDOW_HEIGHT_DEFAULT ) ) ); |
---|
| 60 | |
---|
| 61 | show( ); |
---|
| 62 | |
---|
| 63 | leftSide.resetDividerLocations( ); |
---|
| 64 | |
---|
| 65 | if( log2 != null ) { |
---|
| 66 | rightSide.resetDividerLocations( ); |
---|
| 67 | } |
---|
| 68 | |
---|
| 69 | } |
---|
| 70 | |
---|
| 71 | private void hideGraph( Graph g ) { |
---|
| 72 | Enumeration nodes = _graph.nodeElements( ); |
---|
| 73 | Enumeration edges = _graph.edgeElements( ); |
---|
| 74 | |
---|
| 75 | while( nodes.hasMoreElements( ) ) { |
---|
| 76 | Node n = (Node) nodes.nextElement( ); |
---|
| 77 | setInvis( n ); |
---|
| 78 | } |
---|
| 79 | |
---|
| 80 | while( edges.hasMoreElements( ) ) { |
---|
| 81 | Edge e = (Edge) edges.nextElement( ); |
---|
| 82 | setInvis( e ); |
---|
| 83 | } |
---|
| 84 | |
---|
| 85 | } |
---|
| 86 | |
---|
| 87 | private Graph loadGraph( String dotFile ) { |
---|
| 88 | Parser parser = null; |
---|
| 89 | try { |
---|
| 90 | parser = new Parser( new FileInputStream( dotFile ) ); |
---|
| 91 | parser.parse( ); |
---|
| 92 | } catch( Exception e ) { |
---|
| 93 | e.printStackTrace( ); |
---|
| 94 | System.exit( 1 ); |
---|
| 95 | } |
---|
| 96 | |
---|
| 97 | return parser.getGraph( ); |
---|
| 98 | } |
---|
| 99 | |
---|
| 100 | |
---|
| 101 | private void formatGraph( Graph g ) { |
---|
| 102 | try { |
---|
| 103 | Process formater = Runtime.getRuntime( ).exec( "dot" ); |
---|
| 104 | GrappaSupport.filterGraph( g, formater ); |
---|
| 105 | formater.destroy( ); |
---|
| 106 | |
---|
| 107 | g.repaint( ); |
---|
| 108 | } catch( Exception e ) { |
---|
| 109 | e.printStackTrace( ); |
---|
| 110 | } |
---|
| 111 | } |
---|
| 112 | |
---|
| 113 | private void redrawAndPause( int millis ) { |
---|
| 114 | _graph.resync( ); |
---|
| 115 | _graph.repaint( ); |
---|
| 116 | try { Thread.currentThread( ).sleep( millis ); } |
---|
| 117 | catch( Exception e ) { } |
---|
| 118 | } |
---|
| 119 | |
---|
| 120 | |
---|
| 121 | private void setSolid( Element e ) { |
---|
| 122 | e.setAttribute( FONTSTYLE_ATTR, "normal" ); |
---|
| 123 | e.setAttribute( STYLE_ATTR, "solid" ); |
---|
| 124 | } |
---|
| 125 | |
---|
| 126 | |
---|
| 127 | private void setBold( Element e ) { |
---|
| 128 | e.setAttribute( FONTSTYLE_ATTR, "bold" ); |
---|
| 129 | e.setAttribute( STYLE_ATTR, "bold" ); |
---|
| 130 | } |
---|
| 131 | |
---|
| 132 | private void setInvis( Element e ) { |
---|
| 133 | e.setAttribute( FONTSTYLE_ATTR, "normal" ); |
---|
| 134 | e.setAttribute( STYLE_ATTR, "invis" ); |
---|
| 135 | } |
---|
| 136 | |
---|
| 137 | |
---|
| 138 | |
---|
| 139 | private Edge getEdgeBetween( Node head, Node tail ) { |
---|
| 140 | Enumeration edges = _graph.edgeElements( ); |
---|
| 141 | while( edges.hasMoreElements( ) ) { |
---|
| 142 | Edge e = (Edge) edges.nextElement( ); |
---|
| 143 | Node t = e.getHead( ); |
---|
| 144 | Node h = e.getTail( ); |
---|
| 145 | |
---|
| 146 | if( h.getName( ).equals( head.getName( ) ) && t.getName( ).equals( tail.getName( ) ) ) { |
---|
| 147 | return e; |
---|
| 148 | } |
---|
| 149 | } |
---|
| 150 | |
---|
| 151 | return null; |
---|
| 152 | } |
---|
| 153 | |
---|
| 154 | |
---|
| 155 | |
---|
| 156 | |
---|
| 157 | private void loadProperties( ) { |
---|
| 158 | String propsFileName = System.getProperty( CONFIG_FILE_PROP, CONFIG_FILE_DEFAULT ); |
---|
| 159 | File file = new File( propsFileName ); |
---|
| 160 | |
---|
| 161 | if( file.exists( ) ) { |
---|
| 162 | _properties = new Properties( ); |
---|
| 163 | try { |
---|
| 164 | _properties.load( new FileInputStream( file ) ); |
---|
| 165 | } catch( FileNotFoundException fnfe ) { |
---|
| 166 | _properties = getDefaultProperties( ); |
---|
| 167 | } catch( IOException ioe ) { |
---|
| 168 | _properties = getDefaultProperties( ); |
---|
| 169 | } |
---|
| 170 | } else { |
---|
| 171 | _properties = getDefaultProperties( ); |
---|
| 172 | } |
---|
| 173 | } |
---|
| 174 | |
---|
| 175 | |
---|
| 176 | private Properties getDefaultProperties( ) { |
---|
| 177 | Properties p = new Properties( ); |
---|
| 178 | p.setProperty( WINDOW_TITLE_PROP, WINDOW_TITLE_DEFAULT ); |
---|
| 179 | p.setProperty( WINDOW_HEIGHT_PROP, WINDOW_HEIGHT_DEFAULT ); |
---|
| 180 | p.setProperty( WINDOW_WIDTH_PROP, WINDOW_WIDTH_DEFAULT ); |
---|
| 181 | |
---|
| 182 | return p; |
---|
| 183 | } |
---|
| 184 | |
---|
| 185 | |
---|
| 186 | public static void main( String[] args ) { |
---|
| 187 | ATNVisualizer atnVis = null; |
---|
| 188 | |
---|
| 189 | if( args.length == 1 ) { |
---|
| 190 | atnVis = new ATNVisualizer( args[0], null ); |
---|
| 191 | } else if ( args.length == 2 ) { |
---|
| 192 | atnVis = new ATNVisualizer( args[0], args[1] ); |
---|
| 193 | } else { |
---|
| 194 | System.err.println( "usage: ATNVisualizer <log file> [<log file>]" ); |
---|
| 195 | System.exit( 1 ); |
---|
| 196 | } |
---|
| 197 | |
---|
| 198 | } |
---|
| 199 | |
---|
| 200 | |
---|
| 201 | |
---|
| 202 | |
---|
| 203 | private class SidePanel extends JPanel { |
---|
| 204 | GrappaPanel _grappaPanel; |
---|
| 205 | Graph _graph; |
---|
| 206 | |
---|
| 207 | JPanel _listPanel; |
---|
| 208 | JPanel _messagePanel; |
---|
| 209 | JPanel _graphPanel; |
---|
| 210 | JCheckBox _scaleButton; |
---|
| 211 | |
---|
| 212 | JSplitPane _top; |
---|
| 213 | JSplitPane _complete; |
---|
| 214 | |
---|
| 215 | int _side; |
---|
| 216 | boolean _graphScaleToFit; |
---|
| 217 | Dimension _unScaledDim; |
---|
| 218 | |
---|
| 219 | public SidePanel( String transcriptFile, int side ) { |
---|
| 220 | super( ); |
---|
| 221 | |
---|
| 222 | _side = side; |
---|
| 223 | |
---|
| 224 | _listPanel = new JPanel( new BorderLayout( ) ); |
---|
| 225 | _messagePanel = new JPanel( new BorderLayout( ) ); |
---|
| 226 | _graphPanel = new JPanel( new BorderLayout( ) ); |
---|
| 227 | |
---|
| 228 | |
---|
| 229 | _messagePanel.setMaximumSize( new Dimension( 2000, 100 ) ); |
---|
| 230 | |
---|
| 231 | |
---|
| 232 | |
---|
| 233 | // _graphPanel.addComponentListener( new ComponentAdapter( ) { |
---|
| 234 | // public void componentResized( ComponentEvent e ) { |
---|
| 235 | // if( _graphScaleToFit == true ) { |
---|
| 236 | // setGraphToFit( e.getComponent( ).getSize( ) ); |
---|
| 237 | // } |
---|
| 238 | // } |
---|
| 239 | |
---|
| 240 | // }); |
---|
| 241 | |
---|
| 242 | |
---|
| 243 | // _scaleButton = new JCheckBox( "scale graph to fit" ); |
---|
| 244 | // _scaleButton.setSelected( true ); |
---|
| 245 | // _scaleButton.addItemListener( new ItemListener( ) { |
---|
| 246 | // public void itemStateChanged( ItemEvent e ) { |
---|
| 247 | // if( e.getStateChange( ) == ItemEvent.DESELECTED ) { |
---|
| 248 | // setGraphScaleToFit( false ); |
---|
| 249 | // } else { |
---|
| 250 | // setGraphScaleToFit( true ); |
---|
| 251 | // } |
---|
| 252 | // } |
---|
| 253 | // }); |
---|
| 254 | |
---|
| 255 | |
---|
| 256 | |
---|
| 257 | setPanelBorder( _listPanel, "Creds and Policies" ); |
---|
| 258 | setPanelBorder( _messagePanel, "Output Log" ); |
---|
| 259 | setPanelBorder( _graphPanel, "Trust Negotiation Graph" ); |
---|
| 260 | |
---|
| 261 | |
---|
| 262 | if( _side == LEFT_SIDE ) { |
---|
| 263 | _top = new JSplitPane( JSplitPane.HORIZONTAL_SPLIT, |
---|
| 264 | _listPanel, |
---|
| 265 | _graphPanel ); |
---|
| 266 | } else { |
---|
| 267 | _top = new JSplitPane( JSplitPane.HORIZONTAL_SPLIT, |
---|
| 268 | _graphPanel, |
---|
| 269 | _listPanel); |
---|
| 270 | |
---|
| 271 | |
---|
| 272 | _top.setResizeWeight( 1.0 ); |
---|
| 273 | |
---|
| 274 | |
---|
| 275 | } |
---|
| 276 | |
---|
| 277 | _complete = new JSplitPane( JSplitPane.VERTICAL_SPLIT, |
---|
| 278 | _top, |
---|
| 279 | _messagePanel ); |
---|
| 280 | |
---|
| 281 | _complete.setResizeWeight( 1.0 ); |
---|
| 282 | |
---|
| 283 | |
---|
| 284 | _complete.addComponentListener( new ComponentAdapter( ) { |
---|
| 285 | public void componentResized( ComponentEvent e ) { |
---|
| 286 | System.out.println( "resized: " + e.getComponent( ).getSize( ) ); |
---|
| 287 | } |
---|
| 288 | |
---|
| 289 | public void componentMoved( ComponentEvent e ) { |
---|
| 290 | System.out.println( "moved: " + e.getComponent( ).getSize( ) ); |
---|
| 291 | } |
---|
| 292 | |
---|
| 293 | |
---|
| 294 | |
---|
| 295 | }); |
---|
| 296 | |
---|
| 297 | |
---|
| 298 | _graph = loadGraph( transcriptFile ); |
---|
| 299 | formatGraph( _graph ); |
---|
| 300 | |
---|
| 301 | |
---|
| 302 | _grappaPanel = new GrappaPanel( _graph ); |
---|
| 303 | _grappaPanel.setScaleToFit( false ); |
---|
| 304 | |
---|
| 305 | JScrollPane jsp = new JScrollPane( ); |
---|
| 306 | jsp.getViewport( ).setScrollMode( JViewport.BACKINGSTORE_SCROLL_MODE ); |
---|
| 307 | jsp.getViewport( ).setBackground( Color.white ); |
---|
| 308 | jsp.setViewportView( _grappaPanel ); |
---|
| 309 | |
---|
| 310 | _graphPanel.add( jsp, BorderLayout.CENTER ); |
---|
| 311 | |
---|
| 312 | setLayout( new BorderLayout( ) ); |
---|
| 313 | add( _complete, BorderLayout.CENTER ); |
---|
| 314 | |
---|
| 315 | |
---|
| 316 | _top.setOneTouchExpandable( true ); |
---|
| 317 | _complete.setOneTouchExpandable( true ); |
---|
| 318 | } |
---|
| 319 | |
---|
| 320 | |
---|
| 321 | public void resetDividerLocations( ) { |
---|
| 322 | if( _side == LEFT_SIDE ) { |
---|
| 323 | _top.setDividerLocation( 0.25 ); |
---|
| 324 | } else { |
---|
| 325 | _top.setDividerLocation( 0.75 ); |
---|
| 326 | } |
---|
| 327 | _complete.setDividerLocation( 0.75 ); |
---|
| 328 | |
---|
| 329 | } |
---|
| 330 | |
---|
| 331 | public void setGraphScaleToFit( boolean b ) { |
---|
| 332 | _graphScaleToFit = b; |
---|
| 333 | |
---|
| 334 | if( b == false ) { |
---|
| 335 | setGraphToFit( _unScaledDim ); |
---|
| 336 | } else { |
---|
| 337 | setGraphToFit( _graphPanel.getSize( ) ); |
---|
| 338 | } |
---|
| 339 | |
---|
| 340 | } |
---|
| 341 | |
---|
| 342 | |
---|
| 343 | public void setGraphToFit( Dimension d ) { |
---|
| 344 | |
---|
| 345 | d.setSize( d.getWidth( ) - 50, d.getHeight( ) - 50 ); |
---|
| 346 | |
---|
| 347 | _grappaPanel.setScaleToSize( d ); |
---|
| 348 | _graph.resync( ); |
---|
| 349 | _graph.repaint( ); |
---|
| 350 | |
---|
| 351 | } |
---|
| 352 | |
---|
| 353 | |
---|
| 354 | } |
---|
| 355 | |
---|
| 356 | |
---|
| 357 | |
---|
| 358 | private void setPanelBorder( JComponent comp, String label ) { |
---|
| 359 | Border empty = BorderFactory.createEmptyBorder( 0, 0, 0, 0 ); |
---|
| 360 | Border etched = BorderFactory.createEtchedBorder( ); |
---|
| 361 | |
---|
| 362 | TitledBorder title = BorderFactory.createTitledBorder( etched, label ); |
---|
| 363 | title.setTitleJustification( TitledBorder.RIGHT ); |
---|
| 364 | |
---|
| 365 | Border compound = BorderFactory.createCompoundBorder( title, empty ); |
---|
| 366 | comp.setBorder( compound ); |
---|
| 367 | } |
---|
| 368 | |
---|
| 369 | |
---|
| 370 | |
---|
| 371 | |
---|
| 372 | private void printGraph( Graph g ) { |
---|
| 373 | Enumeration nodes = g.nodeElements( ); |
---|
| 374 | Enumeration edges = g.edgeElements( ); |
---|
| 375 | |
---|
| 376 | while( nodes.hasMoreElements( ) ) { |
---|
| 377 | System.out.println( "----------------------------------------------------------------------" ); |
---|
| 378 | |
---|
| 379 | Node n = (Node) nodes.nextElement( ); |
---|
| 380 | n.printAllAttributes = true; |
---|
| 381 | |
---|
| 382 | System.out.println( n.getName( ) ); |
---|
| 383 | |
---|
| 384 | Enumeration e = n.getAttributePairs( ); |
---|
| 385 | while( e.hasMoreElements( ) ) { |
---|
| 386 | System.out.println( e.nextElement( ) ); |
---|
| 387 | } |
---|
| 388 | |
---|
| 389 | } |
---|
| 390 | |
---|
| 391 | while( edges.hasMoreElements( ) ) { |
---|
| 392 | System.out.println( "----------------------------------------------------------------------" ); |
---|
| 393 | |
---|
| 394 | Edge e = (Edge) edges.nextElement( ); |
---|
| 395 | e.printAllAttributes = true; |
---|
| 396 | |
---|
| 397 | System.out.println( e.getName( ) ); |
---|
| 398 | |
---|
| 399 | Enumeration en = e.getAttributePairs( ); |
---|
| 400 | while( en.hasMoreElements( ) ) { |
---|
| 401 | System.out.println( en.nextElement( ) ); |
---|
| 402 | } |
---|
| 403 | } |
---|
| 404 | |
---|
| 405 | System.out.println( "======================================================================" ); |
---|
| 406 | |
---|
| 407 | g.printSubgraph( new PrintWriter( System.err, true ) ); |
---|
| 408 | } |
---|
| 409 | |
---|
| 410 | |
---|
| 411 | |
---|
| 412 | public void animate( ) { |
---|
| 413 | Node a,b,c,d,e,f,g; |
---|
| 414 | |
---|
| 415 | a = _graph.findNodeByName( "A" ); |
---|
| 416 | b = _graph.findNodeByName( "B" ); |
---|
| 417 | c = _graph.findNodeByName( "C" ); |
---|
| 418 | d = _graph.findNodeByName( "D" ); |
---|
| 419 | e = _graph.findNodeByName( "E" ); |
---|
| 420 | f = _graph.findNodeByName( "F" ); |
---|
| 421 | g = _graph.findNodeByName( "G" ); |
---|
| 422 | |
---|
| 423 | |
---|
| 424 | Edge ab, bc, cd, ce, ef, fg; |
---|
| 425 | |
---|
| 426 | ab = getEdgeBetween( a,b ); |
---|
| 427 | bc = getEdgeBetween( b,c ); |
---|
| 428 | cd = getEdgeBetween( c,d ); |
---|
| 429 | ce = getEdgeBetween( c,e ); |
---|
| 430 | ef = getEdgeBetween( e,f ); |
---|
| 431 | fg = getEdgeBetween( f,g ); |
---|
| 432 | |
---|
| 433 | |
---|
| 434 | while (true) { |
---|
| 435 | |
---|
| 436 | // ---------------------------------------------------------------------- |
---|
| 437 | |
---|
| 438 | setBold( a ); |
---|
| 439 | redrawAndPause( 1000 ); |
---|
| 440 | |
---|
| 441 | setBold( b ); |
---|
| 442 | setBold( ab ); |
---|
| 443 | |
---|
| 444 | redrawAndPause( 1000 ); |
---|
| 445 | |
---|
| 446 | // ---------------------------------------------------------------------- |
---|
| 447 | |
---|
| 448 | |
---|
| 449 | setSolid( a ); |
---|
| 450 | setSolid( b ); |
---|
| 451 | setSolid( ab ); |
---|
| 452 | |
---|
| 453 | // ---------------------------------------------------------------------- |
---|
| 454 | |
---|
| 455 | redrawAndPause( 1000 ); |
---|
| 456 | |
---|
| 457 | setBold( c ); |
---|
| 458 | setBold( bc ); |
---|
| 459 | |
---|
| 460 | redrawAndPause( 1000 ); |
---|
| 461 | |
---|
| 462 | setBold( e ); |
---|
| 463 | setBold( ce ); |
---|
| 464 | |
---|
| 465 | redrawAndPause( 1000 ); |
---|
| 466 | |
---|
| 467 | setBold( f ); |
---|
| 468 | setBold( ef ); |
---|
| 469 | |
---|
| 470 | redrawAndPause( 1000 ); |
---|
| 471 | |
---|
| 472 | // ---------------------------------------------------------------------- |
---|
| 473 | |
---|
| 474 | setSolid( c ); |
---|
| 475 | setSolid( bc ); |
---|
| 476 | setSolid( e ); |
---|
| 477 | setSolid( ce ); |
---|
| 478 | setSolid( f ); |
---|
| 479 | setSolid( ef ); |
---|
| 480 | |
---|
| 481 | redrawAndPause( 1000 ); |
---|
| 482 | |
---|
| 483 | // ---------------------------------------------------------------------- |
---|
| 484 | |
---|
| 485 | setBold( g ); |
---|
| 486 | setBold( fg ); |
---|
| 487 | |
---|
| 488 | redrawAndPause( 1000 ); |
---|
| 489 | |
---|
| 490 | // ---------------------------------------------------------------------- |
---|
| 491 | |
---|
| 492 | setSolid( g ); |
---|
| 493 | setSolid( fg ); |
---|
| 494 | |
---|
| 495 | redrawAndPause( 1000 ); |
---|
| 496 | |
---|
| 497 | // ---------------------------------------------------------------------- |
---|
| 498 | |
---|
| 499 | setBold( d ); |
---|
| 500 | setBold( cd ); |
---|
| 501 | |
---|
| 502 | redrawAndPause( 1000 ); |
---|
| 503 | |
---|
| 504 | // ---------------------------------------------------------------------- |
---|
| 505 | |
---|
| 506 | setSolid( d ); |
---|
| 507 | setSolid( cd ); |
---|
| 508 | |
---|
| 509 | redrawAndPause( 2000 ); |
---|
| 510 | |
---|
| 511 | // ---------------------------------------------------------------------- |
---|
| 512 | |
---|
| 513 | hideGraph( _graph ); |
---|
| 514 | |
---|
| 515 | redrawAndPause( 1000 ); |
---|
| 516 | |
---|
| 517 | } |
---|
| 518 | |
---|
| 519 | } |
---|
| 520 | |
---|
| 521 | |
---|
| 522 | |
---|
| 523 | |
---|
| 524 | |
---|
| 525 | } |
---|