Index: fedd/abac-src/atnvis/src/vis/ATNVisualizer.java
===================================================================
--- fedd/abac-src/atnvis/src/vis/ATNVisualizer.java	(revision 8780cbecc6db2bdc2b9ef31eec6e5209ad3bff15)
+++ fedd/abac-src/atnvis/src/vis/ATNVisualizer.java	(revision 8780cbecc6db2bdc2b9ef31eec6e5209ad3bff15)
@@ -0,0 +1,1426 @@
+package com.algomagic.atn.vis;
+import att.grappa.*;
+
+import java.util.*;
+import java.io.*;
+
+import java.awt.*;
+import java.awt.event.*;
+import java.awt.geom.*;
+import javax.swing.*;
+import javax.swing.border.*;
+import javax.swing.event.*;
+
+
+public class ATNVisualizer extends JFrame 
+    implements ATNVisualizerConstants, GrappaConstants {
+
+    private Properties _properties;
+    private SidePanel[] _sides;
+
+    private Collection _updates;
+
+    private ControlPanel _controls;
+    private ProgressPanel _progressPanel;
+    private PlayBackManager _playBackManager;
+
+
+    public ATNVisualizer( String log1, String log2 ) {
+	loadProperties( );
+
+	initATNVisualizer( log1, log2 );
+	parseUpdates( log1, log2 );
+
+	_playBackManager = new PlayBackManager( );
+	_controls.addObserver( _playBackManager );
+	_playBackManager.addObserver( _progressPanel );
+
+
+	show( );
+    }
+
+
+    private void initATNVisualizer( String log1, String log2 ) {
+
+	addWindowListener( new WindowAdapter( ) {
+		public void windowClosing( WindowEvent we ) {
+		    Window w = we.getWindow( );
+		    w.setVisible( false );
+		    w.dispose( );
+		    System.exit( 0 );
+		}
+	    });
+
+
+	_sides = new SidePanel[2];
+
+
+
+	_sides[LEFT_SIDE] = new SidePanel( LEFT_SIDE );
+	_sides[RIGHT_SIDE] = null;
+
+	JPanel main = new JPanel( );
+	main.setLayout( new BoxLayout( main, BoxLayout.X_AXIS ) );
+	main.add( _sides[LEFT_SIDE] );
+
+
+	if( log2 != null ) {
+	    _sides[RIGHT_SIDE] = new SidePanel( RIGHT_SIDE );
+	    main.add( Box.createHorizontalStrut( 10 ) );
+	    main.add( _sides[RIGHT_SIDE] );
+	}
+
+
+	JPanel bottom = new JPanel( );
+
+	bottom.setLayout( new BoxLayout( bottom, BoxLayout.X_AXIS ) );
+	bottom.add( _controls = new ControlPanel( ) );
+	bottom.add( _progressPanel = new ProgressPanel( ) );
+	
+
+	Container contentPane = getContentPane( );
+	contentPane.setLayout( new BoxLayout( contentPane, BoxLayout.Y_AXIS ) );
+	contentPane.add( main );
+	contentPane.add( bottom );
+
+
+ 	setTitle( _properties.getProperty( WINDOW_TITLE_PROP, WINDOW_TITLE_DEFAULT ) );
+ 	setSize( Integer.parseInt( _properties.getProperty( WINDOW_WIDTH_PROP, WINDOW_WIDTH_DEFAULT ) ),
+ 		 Integer.parseInt( _properties.getProperty( WINDOW_HEIGHT_PROP, WINDOW_HEIGHT_DEFAULT ) ) );
+
+	show( );
+    }
+
+
+    private void parseUpdates( String log1, String log2 ) {
+	_updates = new ArrayList( );
+
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: MedSup.discount <- Alice",
+				      STANDARD_TARGET, 
+				      NOT_SATISFIED,
+				      OPPONENT_PROC ) );
+
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: ReliefNet.provisioner <- Alice",
+				      STANDARD_TARGET,
+				      NOT_SATISFIED,
+				      VERIFIER_PROC ) );
+
+	_updates.add( new EdgeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: MedSup.discount <- Alice", "MedSup: ReliefNet.provisioner <- Alice",
+				      IMPLICATION_EDGE ) );
+
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: MedSup.discount <- Alice",
+				      STANDARD_TARGET, 
+				      NOT_SATISFIED,
+				      VERIFIER_PROC ) );
+
+
+
+	if( _sides[RIGHT_SIDE] != null ) {
+
+	    _updates.add( new MessageBeginUpdate( _sides[RIGHT_SIDE], "<Message>\n<NodeOp type=\"root\">\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>MedSup.discount</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n<ProcessingState>OpponentProcessed</ProcessingState>\n</NodeOp>\n<EdgeOp type=\"implication\" newChild=\"true\">\n<Parent>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>MedSup.discount</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n</Parent>\n<Child>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>ReliefNet.provisioner</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n</Child>\n<ProcessingState>Verifier Processed</ProcessingState>\n<Credential  definedRole=\"MedSup.discount\" subject=\"ReliefNet.provisioner\"/>\n</Evidence>\n</EdgeOp>\n<NodeOp>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>MedSup.discount</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n<ProcessingState>Verifier Processed</ProcessingState>\n</NodeOp>\n</Message>" ) );
+
+
+	    // 2
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: MedSup.discount <- Alice",
+					  STANDARD_TARGET, 
+					  NOT_SATISFIED,
+					  OPPONENT_PROC ) );
+
+	    
+	    // 3
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: ReliefNet.provisioner <- Alice",
+					  STANDARD_TARGET,
+					  NOT_SATISFIED,
+					  VERIFIER_PROC ) );
+
+	    _updates.add( new EdgeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: MedSup.discount <- Alice", 
+					  "MedSup: ReliefNet.provisioner <- Alice",
+					  IMPLICATION_EDGE ) );
+
+	    
+	    // 4 
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: MedSup.discount <- Alice",
+					  STANDARD_TARGET, 
+					  NOT_SATISFIED,
+					  VERIFIER_PROC ) );
+	    
+
+	    _updates.add( new MessageEndUpdate( _sides[RIGHT_SIDE] ) );
+			  
+
+	    
+	    // 6
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE],
+					  "MedSup: MedixFund.purchasingA <- Alice",
+					  STANDARD_TARGET,
+					  NOT_SATISFIED,
+					  VERIFIER_PROC ) );
+
+	    _updates.add( new EdgeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: ReliefNet.provisioner <- Alice", 
+					  "MedSup: MedixFund.purchasingA <- Alice" ) );
+
+
+	    
+	    // 7
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: ReliefNet.provisioner <- Alice",
+					  STANDARD_TARGET,
+					  NOT_SATISFIED,
+					  OPPONENT_PROC ) );
+
+
+	    // 8
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: MedixFund.cPartner <- MedSup",
+					  STANDARD_TARGET,
+					  NOT_SATISFIED,
+					  OPPONENT_PROC ) );
+
+	    _updates.add( new EdgeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: MedixFund.purchasingA <- Alice", 
+					  "Alice: MedixFund.cPartner <- MedSup" ) );
+
+
+
+	    // 9
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: ReliefNet.member <- MedSup",
+					  STANDARD_TARGET,
+					  NOT_SATISFIED,
+					  VERIFIER_PROC ) );
+
+	    _updates.add( new EdgeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: MedixFund.cPartner <- MedSup", 
+					  "Alice: ReliefNet.member <- MedSup" ) );
+
+
+	    // 10
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: MedixFund.cPartner <- MedSup",
+					  STANDARD_TARGET,
+					  NOT_SATISFIED,
+					  VERIFIER_PROC ) );
+
+
+
+	}
+
+	_updates.add( new MessageBeginUpdate( _sides[LEFT_SIDE],
+					      "<Message>\n<EdgeOp type=\"implication\" newChild=\"true\">\n<Parent>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>ReliefNet.provisioner</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n</Parent>\n<Child>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>MedixFund.purchasingA</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n</Child>\n<ProcessingState>Verifier Processed</ProcessingState>\n<Evidence count=\"1\">\n<Credential  definedRole=\"ReliefNet.provisioner\" subject=\"MedixFund.purchasingA\"/>\n</Evidence>\n</EdgeOp>\n<NodeOp>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>ReliefNet.provisioner</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n<ProcessingState>OpponentProcessed</ProcessingState>\n</NodeOp>\n<EdgeOp type=\"control\" newChild=\"true\">\n<Parent>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>MedixFund.purchasingA</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n</Parent>\n<Child>\n<TrustTarget>\n	<Verifier>Alice</Verifier>\n	<Target>MedixFund.cPartner</Target>\n	<Subject>MedSup</Subject>\n</TrustTarget>\n</Child>\n<ProcessingState>OpponentProcessed</ProcessingState>\n</EdgeOp>\n<EdgeOp type=\"implication\" newChild=\"true\">\n<Parent>\n<TrustTarget>\n	<Verifier>Alice</Verifier>\n	<Target>MedixFund.cPartner</Target>\n	<Subject>MedSup</Subject>\n</TrustTarget>\n</Parent>\n<Child>\n<TrustTarget>\n	<Verifier>Alice</Verifier>\n	<Target>ReliefNet.member</Target>\n	<Subject>MedSup</Subject>\n</TrustTarget>\n</Child>\n<ProcessingState>Verifier Processed</ProcessingState>\n<Evidence count=\"1\">\n<Credential  definedRole=\"MedixFund.cPartner\" subject=\"ReliefNet.member\"/>\n</Evidence>\n</EdgeOp>\n<NodeOp>\n<TrustTarget>\n	<Verifier>Alice</Verifier>\n	<Target>MedixFund.cPartner</Target>\n	<Subject>MedSup</Subject>\n</TrustTarget>\n<ProcessingState>Verifier Processed</ProcessingState>\n</NodeOp>\n</Message>" ) );
+
+
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE],
+				      "MedSup: MedixFund.purchasingA <- Alice",
+				      STANDARD_TARGET,
+				      NOT_SATISFIED,
+				      VERIFIER_PROC ) );
+
+	_updates.add( new EdgeUpdate( _sides[LEFT_SIDE], "MedSup: ReliefNet.provisioner <- Alice", "MedSup: MedixFund.purchasingA <- Alice" ) );
+
+
+	// 7
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: ReliefNet.provisioner <- Alice",
+				      STANDARD_TARGET,
+				      NOT_SATISFIED,
+				      OPPONENT_PROC ) );
+
+
+	// 8
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: MedixFund.cPartner <- MedSup",
+				      STANDARD_TARGET,
+				      NOT_SATISFIED,
+				      OPPONENT_PROC ) );
+
+	_updates.add( new EdgeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: MedixFund.purchasingA <- Alice", 
+				      "Alice: MedixFund.cPartner <- MedSup" ) );
+
+
+	// 9
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: ReliefNet.member <- MedSup",
+				      STANDARD_TARGET,
+				      NOT_SATISFIED,
+				      VERIFIER_PROC ) );
+
+	_updates.add( new EdgeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: MedixFund.cPartner <- MedSup", 
+				      "Alice: ReliefNet.member <- MedSup" ) );
+
+
+	// 10
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: MedixFund.cPartner <- MedSup",
+				      STANDARD_TARGET,
+				      NOT_SATISFIED,
+				      VERIFIER_PROC ) );
+
+
+	_updates.add( new MessageEndUpdate( _sides[LEFT_SIDE] ) );
+
+
+	// 12
+
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: MedSup <- MedSup",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      FULLY_PROC ) );
+
+	_updates.add( new EdgeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: ReliefNet.member <- MedSup",
+				      "Alice: MedSup <- MedSup" ) );
+
+
+	// 13
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: ReliefNet.member <- MedSup",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      VERIFIER_PROC ) );
+
+
+	// 14
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: MedixFund.cPartner <- MedSup",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      FULLY_PROC ) );
+
+	// 15
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "Alice: ReliefNet.member <- MedSup",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      OPPONENT_PROC ) );
+	
+	
+
+	if( _sides[RIGHT_SIDE] != null ) {
+
+	    _updates.add( new MessageBeginUpdate( _sides[RIGHT_SIDE],
+						  "<Message>\n<EdgeOp type=\"implication\" newChild=\"true\">\n<Parent>\n<TrustTarget>\n	<Verifier>Alice</Verifier>\n	<Target>ReliefNet.member</Target>\n	<Subject>MedSup</Subject>\n</TrustTarget>\n</Parent>\n<Child>\n<TrustTarget>\n	<Verifier>Alice</Verifier>\n	<Target>MedSup</Target>\n	<Subject>MedSup</Subject>\n</TrustTarget>\n</Child>\n<ProcessingState>Fully Processed</ProcessingState>\n<Evidence count=\"1\">\n<Credential  definedRole=\"ReliefNet.member\" subject=\"MedSup\"/>\n</Evidence>\n</EdgeOp>\n<NodeOp>\n<TrustTarget>\n	<Verifier>Alice</Verifier>\n	<Target>ReliefNet.member</Target>\n	<Subject>MedSup</Subject>\n</TrustTarget>\n<ProcessingState>OpponentProcessed</ProcessingState>\n</NodeOp>\n</Message>" ) );
+
+
+	    // 13
+
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: MedSup <- MedSup",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  FULLY_PROC ) );
+
+	    _updates.add( new EdgeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: ReliefNet.member <- MedSup",
+					  "Alice: MedSup <- MedSup" ) );
+
+
+	    // 14
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: ReliefNet.member <- MedSup",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  VERIFIER_PROC ) );
+
+
+	    // 15
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: MedixFund.cPartner <- MedSup",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  FULLY_PROC ) );
+
+	    // 16
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "Alice: ReliefNet.member <- MedSup",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  OPPONENT_PROC ) );
+	
+
+
+	    _updates.add( new MessageEndUpdate( _sides[RIGHT_SIDE] ) );
+
+	    
+	    // 18
+
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: Alice <- Alice",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  FULLY_PROC ) );
+
+	    _updates.add( new EdgeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: MedixFund.purchasingA <- Alice", 
+					  "MedSup: Alice <- Alice" ) );
+
+
+
+	    // 19
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE],
+					  "MedSup: MedixFund.purchasingA <- Alice",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  VERIFIER_PROC ) );
+
+
+	    // 20
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: ReliefNet.provisioner <- Alice",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  FULLY_PROC ) );
+
+	
+	    // 21
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE], 
+					  "MedSup: MedSup.discount <- Alice",
+					  STANDARD_TARGET, 
+					  SATISFIED,
+					  FULLY_PROC ) );
+	
+
+	    // 22
+	    _updates.add( new NodeUpdate( _sides[RIGHT_SIDE],
+					  "MedSup: MedixFund.purchasingA <- Alice",
+					  STANDARD_TARGET,
+					  SATISFIED,
+					  OPPONENT_PROC ) );
+
+
+
+	}
+
+
+	_updates.add( new MessageBeginUpdate( _sides[LEFT_SIDE],
+					      "<Message>\n<EdgeOp type=\"implication\" newChild=\"true\">\n<Parent>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>MedixFund.purchasingA</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n</Parent>\n<Child>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>Alice</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n</Child>\n<ProcessingState>Fully Processed</ProcessingState>\n</EdgeOp>\n<NodeOp>\n<TrustTarget>\n	<Verifier>MedSup</Verifier>\n	<Target>MedixFund.purchasingA</Target>\n	<Subject>Alice</Subject>\n</TrustTarget>\n<ProcessingState>OpponentProcessed</ProcessingState>\n</NodeOp>\n</Message>") );
+
+
+
+
+	// 18
+
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: Alice <- Alice",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      FULLY_PROC ) );
+
+	_updates.add( new EdgeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: MedixFund.purchasingA <- Alice", 
+				      "MedSup: Alice <- Alice" ) );
+
+
+
+	// 19
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE],
+				      "MedSup: MedixFund.purchasingA <- Alice",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      VERIFIER_PROC ) );
+
+
+	// 20
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: ReliefNet.provisioner <- Alice",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      FULLY_PROC ) );
+
+	
+	// 21
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE], 
+				      "MedSup: MedSup.discount <- Alice",
+				      STANDARD_TARGET, 
+				      SATISFIED,
+				      FULLY_PROC ) );
+	
+
+	// 22
+	_updates.add( new NodeUpdate( _sides[LEFT_SIDE],
+				      "MedSup: MedixFund.purchasingA <- Alice",
+				      STANDARD_TARGET,
+				      SATISFIED,
+				      OPPONENT_PROC ) );
+
+	_updates.add( new MessageEndUpdate( _sides[LEFT_SIDE] ) );
+
+
+
+ 	formatGraph( _sides[LEFT_SIDE].getGraph( ) );
+
+	if( _sides[RIGHT_SIDE] != null ) {
+ 	    formatGraph( _sides[RIGHT_SIDE].getGraph( ) );
+	}
+
+    }
+
+
+    private void hideGraph( Graph g ) {
+	Enumeration nodes = g.nodeElements( );
+	Enumeration edges = g.edgeElements( );
+
+	while( nodes.hasMoreElements( ) ) {
+	    Node n = (Node) nodes.nextElement( );
+	    setInvis( n );
+	}
+
+	while( edges.hasMoreElements( ) ) {
+	    Edge e = (Edge) edges.nextElement( );
+	    setInvis( e );
+	}
+
+	g.resync( );
+	g.repaint( );
+
+    }
+
+
+    private void formatGraph( Graph g ) {
+	try {
+	    Process formater = Runtime.getRuntime( ).exec( "dot" );
+	    GrappaSupport.filterGraph( g, formater );
+	    formater.destroy( );
+	    
+	    g.repaint( );
+	} catch( Exception e ) {
+	    e.printStackTrace( );
+	}
+    }
+
+
+    
+    private void setNodeProps( Node n, String prefix ) {
+
+	for( int i=0; i < NODE_ATTRS.length; i++ ) {
+	    String strValue = _properties.getProperty( prefix + NODE_ATTRS_PROP[i] );
+	    if( strValue == null ) {
+		continue;
+	    }
+
+	    System.out.print( prefix + NODE_ATTRS_PROP[i] );
+	    System.out.println( ":" + strValue );
+
+// 	    if( NODE_ATTRS_PROP[i].equals( "peripheries" ) ) {
+// 		n.setDefaultAttribute( NODE_ATTRS[i], new Integer( strValue ) );
+// 		continue;
+// 	    }
+	    
+
+	    if( NODE_ATTRS_INT[i] ) {
+		Attribute a = new Attribute( NODE, NODE_ATTRS[i], new Integer( strValue ) );
+		n.setAttribute( a );
+// 		n.setAttribute( NODE_ATTRS[i], new Integer( strValue ) );
+	    } else {
+		Attribute a = new Attribute( NODE, NODE_ATTRS[i], strValue );
+		n.setAttribute( a );
+// 		n.setAttribute( NODE_ATTRS[i], strValue );
+	    }
+	}
+    }
+
+    private void setEdgeProps( Edge e, String prefix ) {
+	for( int i=0; i < EDGE_ATTRS.length; i++ ) {
+	    String strValue = _properties.getProperty( prefix + EDGE_ATTRS_PROP[i] );
+
+	    if( strValue == null ) {
+		continue;
+	    }
+	    
+	    if( EDGE_ATTRS_INT[i] ) {
+		e.setAttribute( EDGE_ATTRS[i], new Integer( strValue ) );
+	    } else {
+		e.setAttribute( EDGE_ATTRS[i], strValue );
+	    }
+	}
+    }
+
+
+
+
+    private void setNodeProperties( Node n, String type, String satisfaction, String process ) {
+	setNodeProps( n, DEFAULT_NODE );
+	setNodeProps( n, SYSTEM_PREFIX + "node." + type + "." );
+	setNodeProps( n, SYSTEM_PREFIX + "node.processed." + process + "." );
+	setNodeProps( n, SYSTEM_PREFIX + "node.satisfied." + satisfaction + "." );
+    }
+
+    private void setEdgeProperties( Edge e, String type ) {
+	setEdgeProps( e, DEFAULT_EDGE );
+	setEdgeProps( e, SYSTEM_PREFIX + "edge." + type + "." );
+    }
+
+
+
+
+    private void setSolid( Element e ) {
+	e.setAttribute( FONTSTYLE_ATTR, "normal" );
+ 	e.setAttribute( STYLE_ATTR, "filled" );
+ 	e.setAttribute( COLOR_ATTR, ".5,.5,.5" );
+	
+	if( e instanceof Node ) {
+	    e.setDefaultAttribute( PERIPHERIES_ATTR, new Integer( 2 ) );
+	}
+    }
+
+    private void setBold( Element e ) {
+	e.setAttribute( FONTSTYLE_ATTR, "bold" );
+	e.setAttribute( STYLE_ATTR, "bold" );
+    }
+
+    private void setInvis( Element e ) {
+	e.setAttribute( FONTSTYLE_ATTR, "normal" );
+ 	e.setAttribute( STYLE_ATTR, "invis" );
+    }
+
+
+    private void loadProperties( ) {
+	String propsFileName = System.getProperty( CONFIG_FILE_PROP, CONFIG_FILE_DEFAULT );
+	File file = new File( propsFileName );
+
+	_properties = new Properties( );
+
+	if( file.exists( ) ) {
+	    try {
+		_properties.load( new FileInputStream( file ) );
+	    } catch( Exception e ) { }
+	}
+
+    }
+
+
+    private class SidePanel extends JPanel {
+	GrappaPanel _grappaPanel;
+	Graph _graph;
+
+	JPanel _listPanel;
+	MessagePanel _messagePanel;
+	JPanel _graphPanel;
+
+	JPanel _tallPanel;
+	JPanel _thinPanel;
+	
+	JPanel _top;
+	JPanel _complete;
+
+	int _side;
+
+	public Graph getGraph( ) {
+	    return _graph;
+	}
+
+
+	public SidePanel( int side ) {
+	    super( );
+	    Class clazz = this.getClass( );
+
+
+	    _side = side;
+
+	    _tallPanel = new JPanel( );
+	    _tallPanel.setLayout( new BoxLayout( _tallPanel, BoxLayout.Y_AXIS ) );
+
+ 	    JButton tall = new JButton( );
+	    tall.setMaximumSize( new Dimension( 10, 2000 ) );
+	    tall.setPreferredSize( new Dimension( 10, 2000 ) );
+	    tall.setMinimumSize( new Dimension( 10, 0 ) );
+
+	    tall.addActionListener( new ActionListener( ) {
+		    boolean removed = false;
+		    
+		    public void actionPerformed( ActionEvent e ) {
+			if( ! removed ) {
+			    _top.remove( _listPanel );
+			    removed = true;
+			} else {
+			    if( _side == LEFT_SIDE ) {
+				_top.add( _listPanel, 0 );
+			    } else {
+				_top.add( _listPanel, 2 );
+			    }
+
+			    removed = false;
+			}
+			
+			validate( );
+			repaint( );
+
+		    }
+
+		} );
+
+
+	    _tallPanel.add( tall );
+
+
+	    _thinPanel = new JPanel( );
+	    _thinPanel.setLayout( new BoxLayout( _thinPanel, BoxLayout.X_AXIS ) );
+
+	    JButton thin = new JButton( );
+	    thin.setMaximumSize( new Dimension( 2000, 10 ) );
+	    thin.setPreferredSize( new Dimension( 2000, 10 ) );
+	    thin.setMinimumSize( new Dimension( 0, 10 ) );
+
+	    thin.addActionListener( new ActionListener( ) {
+		    boolean removed = false;
+		    
+		    public void actionPerformed( ActionEvent e ) {
+			if( ! removed ) {
+			    _complete.remove( _messagePanel );
+			    removed = true;
+			} else {
+			    _complete.add( _messagePanel, 2 );
+			    removed = false;
+			}
+
+			validate( );
+			repaint( );
+		    }
+
+		} );
+
+
+	    _thinPanel.add( thin );
+
+	    _listPanel = new ListPanel( );
+
+	    _messagePanel = new MessagePanel( );
+
+ 	    _graphPanel = new JPanel( new BorderLayout( ) );
+
+	    setPanelBorder( _graphPanel, "Trust Negotiation Graph" );
+
+	    _listPanel.setMaximumSize( new Dimension( 150, 2000 ) );
+	    _listPanel.setPreferredSize( new Dimension( 150, 2000 ) );
+	    _listPanel.setMinimumSize( new Dimension( 150, 0 ) );
+
+	    _messagePanel.setMaximumSize( new Dimension( 2000, 150 ) );
+	    _messagePanel.setPreferredSize( new Dimension( 2000, 150 ) );
+	    _messagePanel.setMinimumSize( new Dimension( 0, 150 ) );
+
+
+	    _top = new JPanel( );
+ 	    _top.setLayout( new BoxLayout( _top, BoxLayout.X_AXIS ) );
+	    
+
+	    if( _side == LEFT_SIDE ) {
+		_top.add( _listPanel );
+		_top.add( _tallPanel );
+		_top.add( _graphPanel );
+	    } else {
+		_top.add( _graphPanel );
+		_top.add( _tallPanel );
+		_top.add( _listPanel );
+	    }
+
+
+	    _complete = new JPanel( );
+	    _complete.setLayout( new BoxLayout( _complete, BoxLayout.Y_AXIS ) );
+
+	    _complete.add( _top );
+ 	    _complete.add( _thinPanel );
+ 	    _complete.add( _messagePanel );
+
+	    _graph = new Graph( "Trust Negotiation Graph: " + _side );
+ 	    _grappaPanel = new GrappaPanel( _graph );
+	    _grappaPanel.setScaleToFit( false );
+
+ 	    JScrollPane jsp = new JScrollPane( );
+ 	    jsp.getViewport( ).setScrollMode( JViewport.BACKINGSTORE_SCROLL_MODE );
+ 	    jsp.getViewport( ).setBackground( Color.white );
+ 	    jsp.setViewportView( _grappaPanel );
+	
+	    _graphPanel.add( jsp, BorderLayout.CENTER );
+
+	    setLayout( new BoxLayout( this, BoxLayout.Y_AXIS ) );
+	    add( _complete );
+
+	}
+
+	public void setMessage( String message ) {
+	    _messagePanel.setMessage( message );
+	}
+
+    }
+
+
+    private class ControlPanel extends JPanel implements ActionListener {
+	JButton play, pause, stepForward, stepBack, rewind, fastForward, stop;
+	InternalObservable _observable;
+
+	public ControlPanel( ) {
+	    super( );
+	    
+	    _observable = new InternalObservable( );
+	    Class clazz = this.getClass( );
+
+	    play = new JButton( new ImageIcon( clazz.getResource( "/resources/Play24.gif" ), "play" ) );
+	    play.setActionCommand( "play" );
+	    play.addActionListener( this );
+	    play.setEnabled( true );
+
+	    pause = new JButton( new ImageIcon( clazz.getResource( "/resources/Pause24.gif" ), "pause" ) );
+	    pause.setActionCommand( "pause" );
+	    pause.addActionListener( this );
+	    pause.setEnabled( false );
+
+
+	    stepForward = new JButton( new ImageIcon( clazz.getResource( "/resources/StepForward24.gif" ), "step forward" ) );
+	    stepForward.setActionCommand( "stepf" );
+	    stepForward.addActionListener( this );
+	    stepForward.setEnabled( true );
+
+	    stepBack = new JButton( new ImageIcon( clazz.getResource( "/resources/StepBack24.gif" ), "step back" ) );
+	    stepBack.setActionCommand( "stepb" );
+	    stepBack.addActionListener( this );
+	    stepBack.setEnabled( true );
+
+	    rewind = new JButton( new ImageIcon( clazz.getResource( "/resources/Rewind24.gif" ), "rewind" ) );
+	    rewind.setActionCommand( "rewind" );
+	    rewind.addActionListener( this );
+	    rewind.setEnabled( true );
+
+	    fastForward = new JButton( new ImageIcon( clazz.getResource( "/resources/FastForward24.gif" ), "fast forward" ) );
+	    fastForward.setActionCommand( "ff" );
+	    fastForward.addActionListener( this );
+	    fastForward.setEnabled( true );
+
+// 	    stop = new JButton( new ImageIcon( clazz.getResource( "/resources/Stop24.gif" ), "stop" ) );
+// 	    stop.setActionCommand( "stop" );
+// 	    stop.addActionListener( this );
+
+
+	    setStyle( play );
+	    setStyle( pause );
+	    setStyle( stepForward );
+	    setStyle( stepBack );
+	    setStyle( rewind );
+	    setStyle( fastForward );
+// 	    setStyle( stop );
+
+	    setLayout( new BoxLayout( this, BoxLayout.X_AXIS ) );
+	    add( rewind );
+	    add( stepBack );
+	    add( play );
+	    add( pause );
+// 	    add( stop );
+	    add( stepForward );
+	    add( fastForward );
+
+	    JCheckBox loop = new JCheckBox( "loop", (new Boolean( _properties.getProperty( LOOP_PROP, LOOP_DEFAULT ) )).booleanValue( ) );
+	    loop.addItemListener( new ItemListener( ) {
+		    public void itemStateChanged( ItemEvent e ) {
+			int s = e.getStateChange( );
+			Boolean state = Boolean.TRUE;
+
+			if( s == ItemEvent.DESELECTED ) {
+			    state = Boolean.FALSE;
+			}
+			
+			_observable.notify( state );
+
+		    }
+
+		} );
+
+
+	    add( Box.createHorizontalStrut( 10 ) );
+	    add( loop );
+
+	    JSpinner spinner = new JSpinner( new SpinnerNumberModel( Integer.parseInt( _properties.getProperty( DELAY_PROP, DELAY_DEFAULT ) ), 
+								     0, 
+								     5000, 
+								     100 ) );
+
+	    JLabel spinnerLabel = new JLabel( "delay (msec)" );
+
+	    spinner.addChangeListener( new ChangeListener( ) {
+		    public void stateChanged( ChangeEvent e ) {
+			_observable.notify( e.getSource( ) );
+		    }
+		} );
+
+
+	    add( spinner );
+	    add( Box.createHorizontalStrut( 5 ) );
+	    add( spinnerLabel );
+
+	    setPanelBorder( this, "Controls" );
+	}
+
+
+	public void addObserver( Observer o ) {
+	    _observable.addObserver( o );
+	}
+
+
+	private void setStyle( JButton b ) {
+	    b.setMinimumSize( new Dimension( 24, 24 ) );
+	    b.setMaximumSize( new Dimension( 24, 24 ) );
+	    b.setPreferredSize( new Dimension( 24, 24 ) );
+	    
+	    b.setBorderPainted( false );
+	}
+
+	public void actionPerformed( ActionEvent e ) {
+	    String cmd = e.getActionCommand( );
+	    if( cmd.equals( "play" ) ) {
+		stepForward.setEnabled( false );
+		stepBack.setEnabled( false );
+		rewind.setEnabled( false );
+		fastForward.setEnabled( false );
+		play.setEnabled( false );
+		pause.setEnabled( true );
+	    }
+
+	    else if( cmd.equals( "pause" ) ) {
+		stepForward.setEnabled( true );
+		stepBack.setEnabled( true );
+		rewind.setEnabled( true );
+		fastForward.setEnabled( true );
+		play.setEnabled( true );
+		pause.setEnabled( false );
+	    }
+
+
+
+
+
+	    _observable.notify( e.getActionCommand( ) );
+	}
+
+
+	private class InternalObservable extends Observable {
+	    public void notify( Object arg ) {
+		setChanged( );
+		notifyObservers( arg );
+	    }
+
+	    
+	}
+
+    }
+
+
+    private class ListPanel extends JPanel implements Observer {
+	public ListPanel( ) {
+	    super( );
+
+	    JList oCreds = new JList( );
+	    JScrollPane oCredsJSP = new JScrollPane( oCreds );
+	    setPanelBorder( oCredsJSP, "Opponent Creds." );
+
+	    JList vCreds = new JList( );
+	    JScrollPane vCredsJSP = new JScrollPane( vCreds );
+	    setPanelBorder( vCredsJSP, "Verifier Creds." );
+
+	    JList acPolicy = new JList( );
+	    JScrollPane acPolicyJSP = new JScrollPane( acPolicy );
+	    setPanelBorder( acPolicyJSP, "AC Policies" );
+
+	    JList ackPolicy = new JList( );
+	    JScrollPane ackPolicyJSP = new JScrollPane( ackPolicy );
+	    setPanelBorder( ackPolicyJSP, "Ack Policies" );
+
+
+	    setLayout( new BoxLayout( this, BoxLayout.Y_AXIS ) );
+
+	    JList list = new JList( );
+	    JScrollPane jsp = new JScrollPane( list );
+	    
+	    add( oCredsJSP );
+	    add( vCredsJSP );
+	    add( acPolicyJSP );
+	    add( ackPolicyJSP );
+
+
+	}
+
+
+	public void update( Observable o, Object arg ) {
+
+
+	}
+
+    }
+
+
+    private class MessagePanel extends JPanel {
+	JTextArea _message;
+
+	public MessagePanel( ) {
+	    super( );
+	    setLayout( new BorderLayout( ) );
+
+	    _message = new JTextArea( );
+	    JScrollPane jsp = new JScrollPane( _message );
+
+	    add( jsp, BorderLayout.CENTER );
+
+	    setPanelBorder( this, "Message" );
+
+	}
+
+	public void setMessage( String message ) {
+	    _message.setText( message );
+	}
+
+
+    }
+
+    
+    private class ProgressPanel extends JPanel implements Observer {
+	JProgressBar _progress;
+
+	public ProgressPanel( ) {
+	    super( );
+	    setLayout( new BorderLayout( ) );
+
+// 	    _progress = new JProgressBar( 0, _updates.size( ) );
+	    _progress = new JProgressBar( 0, 1 );
+	    _progress.setValue( 0 );
+	    _progress.setStringPainted( true );
+
+
+	    add( _progress, BorderLayout.CENTER );
+
+	    setPanelBorder( this, "Negotiation Progress" );
+	}
+
+
+	public void setMax( int n ) {
+	    _progress.setMaximum( n );
+	}
+
+	public void update( Observable o, Object arg ) {
+	    _progress.setValue( ((Integer)arg).intValue( ) );
+
+	}
+
+
+    }
+
+
+    private void setPanelBorder( JComponent comp, String label ) {
+	Border empty = BorderFactory.createEmptyBorder( 0, 0, 0, 0 );
+	Border etched = BorderFactory.createEtchedBorder( );
+	
+	TitledBorder title = BorderFactory.createTitledBorder( etched, label );
+	title.setTitleJustification( TitledBorder.RIGHT );
+
+	Border compound = BorderFactory.createCompoundBorder( title, empty );
+	comp.setBorder( compound );
+    }
+
+
+    private class PlayBackManager extends Observable implements Observer {
+	private int _delay = Integer.parseInt( _properties.getProperty( DELAY_PROP, DELAY_DEFAULT ) );
+	private boolean _loop = (new Boolean( _properties.getProperty( LOOP_PROP, LOOP_DEFAULT ) )).booleanValue( );
+	private Update[] _updateArray = (Update[]) _updates.toArray( new Update[0] );
+	private int _index = 0;
+	private boolean _clear = true;
+
+
+	private boolean _playing = false;
+
+
+	public PlayBackManager( ) {
+	    _progressPanel.setMax( _updateArray.length );
+	}
+
+	public void update( Observable o, Object arg ) {
+	    if( arg instanceof String ) {
+		String cmd = (String)arg;
+
+		if( cmd.equals( "play" ) ) {
+		    _playing = true;
+		    new Thread( new PlayThread( ) ).start( );
+		} else if( cmd.equals( "pause" ) ) {
+		    _playing = false;
+		} else if( cmd.equals( "stepf" ) ) {
+		    stepf( );
+		} else if( cmd.equals( "ff" ) ) {
+		    ff( );
+		} else if( cmd.equals( "rewind" ) ) {
+		    rewind( );
+		}
+
+	    } else if( arg instanceof JSpinner ) {
+		SpinnerNumberModel snm = (SpinnerNumberModel)((JSpinner)arg).getModel( );
+		_delay = snm.getNumber( ).intValue( );
+	    } else if (arg instanceof Boolean ) {
+		_loop = ((Boolean)arg).booleanValue( );
+	    }
+	}
+
+
+	private synchronized void stepf( ) {
+	    if( _index == 0 && _clear == false ) {
+		clearAll( );
+		_clear = true;
+
+		setChanged( );
+		notifyObservers( new Integer( _index ) );
+
+		return;
+	    }
+
+	    _clear = false;
+
+
+	    _updateArray[_index].execute( );
+	    _index++;
+
+	    setChanged( );
+	    notifyObservers( new Integer( _index ) );
+
+	    
+	    if( _index == _updateArray.length ) {
+		_index = 0;
+		if( _playing == true && _loop == false ) {
+		    _playing = false;
+		}
+	    }
+
+
+	}
+
+	private synchronized void stepb( ) {
+	    setChanged( );
+	    notifyObservers( new Integer( _index ) );
+	}
+	
+	private synchronized void ff( ) {
+	    for( int i = _index; i < _updateArray.length; i++ ) {
+		_updateArray[i].execute( );
+	    }
+
+	    _index = 0;
+
+	    setChanged( );
+	    notifyObservers( new Integer( _index ) );
+
+	}
+
+
+	private synchronized void rewind( ) {
+	    clearAll( );
+	    _index = 0;
+
+	    setChanged( );
+	    notifyObservers( new Integer( _index ) );
+	}
+
+
+	private class PlayThread implements Runnable {
+	    public void run( ) {
+		while( _playing ) {
+		    try {
+			stepf( );
+			Thread.currentThread( ).sleep( _delay );
+		    } catch( InterruptedException ie ) {
+			throw new RuntimeException( ie );
+		    }
+		}
+		
+	    }
+	}
+
+
+    }
+
+
+    protected abstract class  Update {
+	public abstract void execute( );
+	public abstract void fixRef( );
+    }
+
+
+    private class TestUpdate extends Update {
+	private int _i;
+
+	public TestUpdate( int i ) {
+	    _i = i;
+	}
+
+	public void execute( ) {
+	    System.out.println( _i );
+	}
+	
+	public void fixRef( ) {
+
+	}
+
+    }
+
+    private class MessageBeginUpdate extends Update {
+	SidePanel _sp;
+	String _message;
+
+	public MessageBeginUpdate( SidePanel sp, String message ) {
+	    _sp = sp;
+	    _message = message;
+	}
+
+
+	public void execute( ) {
+	    _sp.setMessage( _message );
+	}
+	
+	public void fixRef( ) {
+
+	}
+	
+    }
+    
+    private class MessageEndUpdate extends Update {
+	SidePanel _sp;
+
+	public MessageEndUpdate( SidePanel sp ) {
+	    _sp = sp;
+	}
+
+
+	public void execute( ) {
+	    _sp.setMessage( "" );
+	}
+	
+	public void fixRef( ) {
+
+	}
+    }
+    
+	
+
+
+
+
+
+
+    private class NodeUpdate extends Update {
+	SidePanel _sp;
+	String _name;
+	Node _n;
+
+	String _type;
+	String _satisfactionState;
+	String _processingState;
+
+	public NodeUpdate( SidePanel sp, String name ) {
+	    _sp = sp;
+	    _name = name;
+
+	    Graph g = _sp.getGraph( );
+
+	    _n = g.findNodeByName( name );
+	    if( _n == null ) {
+		_n = new Node( g, name );
+		setInvis( _n );
+		g.addNode( _n );
+	    }
+
+	}
+
+	public NodeUpdate( SidePanel sp, 
+			   String name, 
+			   String type,
+			   String satisfactionState, 
+			   String processingState ) {
+	    this( sp, name );
+
+	    _type = type;
+
+
+	    _satisfactionState = satisfactionState;
+	    _processingState = processingState;
+
+
+	}
+
+	public void fixRef( ) {
+	    _n = _sp.getGraph( ).findNodeByName( _name );
+	}
+
+
+	public void execute( ) {
+	    fixRef( );
+
+	    setNodeProperties( _n, _type, _satisfactionState, _processingState );
+
+	    Graph g = _sp.getGraph( );
+
+	    g.resync( );
+	    g.repaint( );
+	}
+    }
+
+    
+    private class EdgeUpdate extends Update {
+	SidePanel _sp;
+	String _headNodeName;
+	String _tailNodeName;
+	Edge _e;
+
+	String _type;
+
+
+	public EdgeUpdate( SidePanel sp, 
+			   String headNodeName, 
+			   String tailNodeName, 
+			   String type ) {
+	    this( sp, headNodeName, tailNodeName );
+	    _type = type;
+	}
+
+
+
+	public EdgeUpdate( SidePanel sp, String headNodeName, String tailNodeName ) {
+	    _sp = sp;
+	    _headNodeName = headNodeName;
+	    _tailNodeName = tailNodeName;
+
+	    Graph g = _sp.getGraph( );
+	    Node head = g.findNodeByName( _headNodeName );
+	    Node tail = g.findNodeByName( _tailNodeName );
+
+
+	    _e = getEdgeBetween( g, head, tail );
+
+	    if( _e == null ) {
+		_e = new Edge( g, head, tail );
+		setInvis( _e );
+		g.addEdge( _e );
+	    }
+
+	}
+
+
+	public void fixRef( ) {
+	    Graph g = _sp.getGraph( );
+	    Node head = g.findNodeByName( _headNodeName );
+	    Node tail = g.findNodeByName( _tailNodeName );
+
+
+	    _e = getEdgeBetween( g, head, tail );
+	}
+
+	public void execute( ) {
+	    fixRef( );
+	    setEdgeProperties( _e, _type );
+
+	    Graph g = _sp.getGraph( );
+
+	    g.resync( );
+	    g.repaint( );
+	}
+    }
+
+
+    private void clearAll( ) {
+	for( int i = 0; i < _sides.length; i++ ) {
+	    if( _sides[i] != null ) {
+		hideGraph( _sides[i].getGraph( ) );
+	    }
+	}
+
+	
+    }
+
+    private Graph loadGraph( String dotFile ) {
+	Parser parser = null;
+	try {
+	    parser = new Parser( new FileInputStream( dotFile ) );
+	    parser.parse( );
+	} catch( Exception e ) {
+	    e.printStackTrace( );
+	    System.exit( 1 );
+	}
+
+	return parser.getGraph( );
+    }
+
+
+
+    public static void main( String[] args ) {
+	ATNVisualizer atnVis = null;
+
+	if( args.length == 1 ) {
+	    atnVis = new ATNVisualizer( args[0], null );
+	} else if ( args.length == 2 ) {
+	    atnVis = new ATNVisualizer( args[0], args[1] );
+	} else {
+	    System.err.println( "usage: ATNVisualizer <log file> [<log file>]" );
+	    System.exit( 1 );
+	}
+
+    }
+
+
+
+    private void printGraph( Graph g ) {
+	Enumeration nodes = g.nodeElements( );
+	Enumeration edges = g.edgeElements( );
+
+	while( nodes.hasMoreElements( ) ) {
+	    System.out.println( "----------------------------------------------------------------------" );
+
+	    Node n = (Node) nodes.nextElement( );
+	    n.printAllAttributes = true;
+
+	    System.out.println( n.getName( ) );
+
+	    Enumeration e = n.getAttributePairs( );
+	    while( e.hasMoreElements( ) ) {
+		System.out.println( e.nextElement( ) );
+	    }
+
+	}
+
+	while( edges.hasMoreElements( ) ) {
+	    System.out.println( "----------------------------------------------------------------------" );
+
+	    Edge e = (Edge) edges.nextElement( );
+	    e.printAllAttributes = true;
+
+	    System.out.println( e.getName( ) );
+
+	    Enumeration en = e.getAttributePairs( );
+	    while( en.hasMoreElements( ) ) {
+		System.out.println( en.nextElement( ) );
+	    }
+	}
+
+	System.out.println( "======================================================================" );
+
+	g.printSubgraph( new PrintWriter( System.err, true ) );
+    }
+
+
+    private Edge getEdgeBetween( Graph g, Node head, Node tail ) {
+	Enumeration edges = g.edgeElements( );
+	while( edges.hasMoreElements( ) ) {
+	    Edge e = (Edge) edges.nextElement( );
+	    Node t = e.getHead( );
+	    Node h = e.getTail( );
+	    
+	    if( h.getName( ).equals( head.getName( ) ) && t.getName( ).equals( tail.getName( ) ) ) {
+		return e;
+	    }
+	}
+
+	return null;
+    }
+
+
+}
Index: fedd/abac-src/atnvis/src/vis/ATNVisualizer.java.tmp
===================================================================
--- fedd/abac-src/atnvis/src/vis/ATNVisualizer.java.tmp	(revision 8780cbecc6db2bdc2b9ef31eec6e5209ad3bff15)
+++ fedd/abac-src/atnvis/src/vis/ATNVisualizer.java.tmp	(revision 8780cbecc6db2bdc2b9ef31eec6e5209ad3bff15)
@@ -0,0 +1,525 @@
+package com.algomagic.atn.vis;
+import att.grappa.*;
+
+import java.util.Properties;
+import java.util.Enumeration;
+import java.io.*;
+
+import java.awt.*;
+import java.awt.event.*;
+import java.awt.geom.*;
+import javax.swing.*;
+import javax.swing.border.*;
+
+
+public class ATNVisualizer extends JFrame 
+    implements ATNVisualizerConstants, GrappaConstants {
+
+    private Properties _properties;
+    private GrappaPanel _grappaPanel;
+    private Graph _graph;
+
+    
+
+    public ATNVisualizer( String log1, String log2 ) {
+	initATNVisualizer( log1, log2 );
+    }
+
+
+    private void initATNVisualizer( String log1, String log2 ) {
+	loadProperties( );
+
+	addWindowListener( new WindowAdapter( ) {
+		public void windowClosing( WindowEvent we ) {
+		    Window w = we.getWindow( );
+		    w.setVisible( false );
+		    w.dispose( );
+		    System.exit( 0 );
+		}
+	    });
+
+
+	SidePanel leftSide = new SidePanel( log1, LEFT_SIDE );
+	SidePanel rightSide = null;
+
+	Container contentPane = getContentPane( );
+	contentPane.setLayout( new BoxLayout( contentPane, BoxLayout.X_AXIS ) );
+  	contentPane.add( leftSide );
+
+
+	if( log2 != null ) {
+	    rightSide = new SidePanel( log2, RIGHT_SIDE );
+	    contentPane.add( rightSide );
+	}
+
+
+
+ 	setTitle( _properties.getProperty( WINDOW_TITLE_PROP, WINDOW_TITLE_DEFAULT ) );
+ 	setSize( Integer.parseInt( _properties.getProperty( WINDOW_WIDTH_PROP, WINDOW_WIDTH_DEFAULT ) ),
+ 		 Integer.parseInt( _properties.getProperty( WINDOW_HEIGHT_PROP, WINDOW_HEIGHT_DEFAULT ) ) );
+
+	show( );
+
+	leftSide.resetDividerLocations( );
+
+	if( log2 != null ) {
+	    rightSide.resetDividerLocations( );
+	}
+
+    }
+
+    private void hideGraph( Graph g ) {
+	Enumeration nodes = _graph.nodeElements( );
+	Enumeration edges = _graph.edgeElements( );
+
+	while( nodes.hasMoreElements( ) ) {
+	    Node n = (Node) nodes.nextElement( );
+	    setInvis( n );
+	}
+
+	while( edges.hasMoreElements( ) ) {
+	    Edge e = (Edge) edges.nextElement( );
+	    setInvis( e );
+	}
+
+    }
+
+    private Graph loadGraph( String dotFile ) {
+	Parser parser = null;
+	try {
+	    parser = new Parser( new FileInputStream( dotFile ) );
+	    parser.parse( );
+	} catch( Exception e ) {
+	    e.printStackTrace( );
+	    System.exit( 1 );
+	}
+
+	return parser.getGraph( );
+    }
+
+
+    private void formatGraph( Graph g ) {
+	try {
+	    Process formater = Runtime.getRuntime( ).exec( "dot" );
+	    GrappaSupport.filterGraph( g, formater );
+	    formater.destroy( );
+	    
+	    g.repaint( );
+	} catch( Exception e ) {
+	    e.printStackTrace( );
+	}
+    }
+
+    private void redrawAndPause( int millis ) {
+	_graph.resync( );
+	_graph.repaint( );
+	try { Thread.currentThread( ).sleep( millis ); }
+	catch( Exception e ) { }
+    }
+
+
+    private void setSolid( Element e ) {
+	e.setAttribute( FONTSTYLE_ATTR, "normal" );
+	e.setAttribute( STYLE_ATTR, "solid" );
+    }
+
+
+    private void setBold( Element e ) {
+	e.setAttribute( FONTSTYLE_ATTR, "bold" );
+	e.setAttribute( STYLE_ATTR, "bold" );
+    }
+
+    private void setInvis( Element e ) {
+	e.setAttribute( FONTSTYLE_ATTR, "normal" );
+	e.setAttribute( STYLE_ATTR, "invis" );
+    }
+
+
+
+    private Edge getEdgeBetween( Node head, Node tail ) {
+	Enumeration edges = _graph.edgeElements( );
+	while( edges.hasMoreElements( ) ) {
+	    Edge e = (Edge) edges.nextElement( );
+	    Node t = e.getHead( );
+	    Node h = e.getTail( );
+	    
+	    if( h.getName( ).equals( head.getName( ) ) && t.getName( ).equals( tail.getName( ) ) ) {
+		return e;
+	    }
+	}
+
+	return null;
+    }
+
+
+
+
+    private void loadProperties( ) {
+	String propsFileName = System.getProperty( CONFIG_FILE_PROP, CONFIG_FILE_DEFAULT );
+	File file = new File( propsFileName );
+
+	if( file.exists( ) ) {
+	    _properties = new Properties( );
+	    try {
+		_properties.load( new FileInputStream( file ) );
+	    } catch( FileNotFoundException fnfe ) {
+		_properties = getDefaultProperties( );
+	    } catch( IOException ioe ) {
+		_properties = getDefaultProperties( );
+	    }
+	} else {
+	    _properties = getDefaultProperties( );
+	}
+    }
+
+
+    private Properties getDefaultProperties( ) {
+	Properties p = new Properties( );
+	p.setProperty( WINDOW_TITLE_PROP, WINDOW_TITLE_DEFAULT );
+	p.setProperty( WINDOW_HEIGHT_PROP, WINDOW_HEIGHT_DEFAULT );
+	p.setProperty( WINDOW_WIDTH_PROP, WINDOW_WIDTH_DEFAULT );
+
+	return p;
+    }
+
+
+    public static void main( String[] args ) {
+	ATNVisualizer atnVis = null;
+
+	if( args.length == 1 ) {
+	    atnVis = new ATNVisualizer( args[0], null );
+	} else if ( args.length == 2 ) {
+	    atnVis = new ATNVisualizer( args[0], args[1] );
+	} else {
+	    System.err.println( "usage: ATNVisualizer <log file> [<log file>]" );
+	    System.exit( 1 );
+	}
+
+    }
+
+
+
+
+    private class SidePanel extends JPanel {
+	GrappaPanel _grappaPanel;
+	Graph _graph;
+
+	JPanel _listPanel;
+	JPanel _messagePanel;
+	JPanel _graphPanel;
+	JCheckBox _scaleButton;
+	
+	JSplitPane _top;
+	JSplitPane _complete;
+
+	int _side;
+	boolean _graphScaleToFit;
+	Dimension _unScaledDim;
+
+	public SidePanel( String transcriptFile, int side ) {
+	    super( );
+
+	    _side = side;
+
+	    _listPanel = new JPanel( new BorderLayout( ) );
+	    _messagePanel = new JPanel( new BorderLayout( ) );
+	    _graphPanel = new JPanel( new BorderLayout( ) );
+
+
+	    _messagePanel.setMaximumSize( new Dimension( 2000, 100 ) );
+
+
+
+// 	    _graphPanel.addComponentListener( new ComponentAdapter( ) {
+// 		    public void componentResized( ComponentEvent e ) {
+// 			if( _graphScaleToFit == true ) {
+// 			    setGraphToFit( e.getComponent( ).getSize( ) );
+// 			}
+// 		    }
+
+// 		});
+
+
+// 	    _scaleButton = new JCheckBox( "scale graph to fit" );
+// 	    _scaleButton.setSelected( true );
+// 	    _scaleButton.addItemListener( new ItemListener( ) {
+// 		    public void itemStateChanged( ItemEvent e ) {
+// 			if( e.getStateChange( ) == ItemEvent.DESELECTED ) {
+// 			    setGraphScaleToFit( false );
+// 			} else {
+// 			    setGraphScaleToFit( true );
+// 			}
+// 		    }
+// 		});
+	    
+
+	    
+	    setPanelBorder( _listPanel, "Creds and Policies" );
+	    setPanelBorder( _messagePanel, "Output Log" );
+	    setPanelBorder( _graphPanel, "Trust Negotiation Graph" );
+
+
+	    if( _side == LEFT_SIDE ) {
+		_top = new JSplitPane( JSplitPane.HORIZONTAL_SPLIT, 
+				       _listPanel, 
+				       _graphPanel );
+	    } else {
+		_top = new JSplitPane( JSplitPane.HORIZONTAL_SPLIT, 
+				       _graphPanel,
+				       _listPanel);
+		
+
+		_top.setResizeWeight( 1.0 );
+
+
+	    }
+
+	    _complete = new JSplitPane( JSplitPane.VERTICAL_SPLIT,
+					_top,
+					_messagePanel );
+
+	    _complete.setResizeWeight( 1.0 );
+
+
+	    _complete.addComponentListener( new ComponentAdapter( ) {
+		    public void componentResized( ComponentEvent e ) {
+			System.out.println( "resized: " + e.getComponent( ).getSize( ) );
+		    }
+
+		    public void componentMoved( ComponentEvent e ) {
+			System.out.println( "moved: " + e.getComponent( ).getSize( ) );
+		    }
+
+
+
+		});
+
+
+ 	    _graph = loadGraph( transcriptFile );
+ 	    formatGraph( _graph );
+
+
+ 	    _grappaPanel = new GrappaPanel( _graph );
+	    _grappaPanel.setScaleToFit( false );
+
+ 	    JScrollPane jsp = new JScrollPane( );
+ 	    jsp.getViewport( ).setScrollMode( JViewport.BACKINGSTORE_SCROLL_MODE );
+ 	    jsp.getViewport( ).setBackground( Color.white );
+ 	    jsp.setViewportView( _grappaPanel );
+	
+	    _graphPanel.add( jsp, BorderLayout.CENTER );
+
+	    setLayout( new BorderLayout( ) );
+	    add( _complete, BorderLayout.CENTER );
+
+
+	    _top.setOneTouchExpandable( true );
+	    _complete.setOneTouchExpandable( true );
+	}
+
+
+	public void resetDividerLocations( ) {
+	    if( _side == LEFT_SIDE ) {
+		_top.setDividerLocation( 0.25 );
+	    } else {
+		_top.setDividerLocation( 0.75 );
+	    }
+	    _complete.setDividerLocation( 0.75 );
+
+	}
+
+	public void setGraphScaleToFit( boolean b ) {
+	    _graphScaleToFit = b;
+
+	    if( b == false ) {
+		setGraphToFit( _unScaledDim );
+	    } else {
+		setGraphToFit( _graphPanel.getSize( ) );
+	    }
+
+	}
+
+
+	public void setGraphToFit( Dimension d ) {
+
+	    d.setSize( d.getWidth( ) - 50, d.getHeight( ) - 50 );
+
+	    _grappaPanel.setScaleToSize( d );
+	    _graph.resync( );
+	    _graph.repaint( );
+
+	}
+
+
+    }
+
+
+
+    private void setPanelBorder( JComponent comp, String label ) {
+	Border empty = BorderFactory.createEmptyBorder( 0, 0, 0, 0 );
+	Border etched = BorderFactory.createEtchedBorder( );
+	
+	TitledBorder title = BorderFactory.createTitledBorder( etched, label );
+	title.setTitleJustification( TitledBorder.RIGHT );
+
+	Border compound = BorderFactory.createCompoundBorder( title, empty );
+	comp.setBorder( compound );
+    }
+
+
+
+
+    private void printGraph( Graph g ) {
+	Enumeration nodes = g.nodeElements( );
+	Enumeration edges = g.edgeElements( );
+
+	while( nodes.hasMoreElements( ) ) {
+	    System.out.println( "----------------------------------------------------------------------" );
+
+	    Node n = (Node) nodes.nextElement( );
+	    n.printAllAttributes = true;
+
+	    System.out.println( n.getName( ) );
+
+	    Enumeration e = n.getAttributePairs( );
+	    while( e.hasMoreElements( ) ) {
+		System.out.println( e.nextElement( ) );
+	    }
+
+	}
+
+	while( edges.hasMoreElements( ) ) {
+	    System.out.println( "----------------------------------------------------------------------" );
+
+	    Edge e = (Edge) edges.nextElement( );
+	    e.printAllAttributes = true;
+
+	    System.out.println( e.getName( ) );
+
+	    Enumeration en = e.getAttributePairs( );
+	    while( en.hasMoreElements( ) ) {
+		System.out.println( en.nextElement( ) );
+	    }
+	}
+
+	System.out.println( "======================================================================" );
+
+	g.printSubgraph( new PrintWriter( System.err, true ) );
+    }
+
+
+
+    public void animate( ) {
+	Node a,b,c,d,e,f,g;
+
+	a = _graph.findNodeByName( "A" );
+	b = _graph.findNodeByName( "B" );
+	c = _graph.findNodeByName( "C" );
+	d = _graph.findNodeByName( "D" );
+	e = _graph.findNodeByName( "E" );
+	f = _graph.findNodeByName( "F" );
+	g = _graph.findNodeByName( "G" );
+
+
+	Edge ab, bc, cd, ce, ef, fg;
+
+	ab = getEdgeBetween( a,b );
+	bc = getEdgeBetween( b,c );
+	cd = getEdgeBetween( c,d );
+	ce = getEdgeBetween( c,e );
+	ef = getEdgeBetween( e,f );
+	fg = getEdgeBetween( f,g );
+	
+
+	while (true) {
+
+	    // ----------------------------------------------------------------------
+
+	    setBold( a );
+	    redrawAndPause( 1000 );
+
+	    setBold( b );
+	    setBold( ab );
+
+	    redrawAndPause( 1000 );
+
+	    // ----------------------------------------------------------------------
+
+
+	    setSolid( a );
+	    setSolid( b );
+	    setSolid( ab );
+
+	    // ----------------------------------------------------------------------
+
+	    redrawAndPause( 1000 );
+
+	    setBold( c );
+	    setBold( bc );
+
+	    redrawAndPause( 1000 );
+
+	    setBold( e );
+	    setBold( ce );
+
+	    redrawAndPause( 1000 );
+
+	    setBold( f );
+	    setBold( ef );
+
+	    redrawAndPause( 1000 );
+
+	    // ----------------------------------------------------------------------
+
+	    setSolid( c );
+	    setSolid( bc );
+	    setSolid( e );
+	    setSolid( ce );
+	    setSolid( f );
+	    setSolid( ef );
+
+	    redrawAndPause( 1000 );
+
+	    // ----------------------------------------------------------------------
+
+	    setBold( g );
+	    setBold( fg );
+
+	    redrawAndPause( 1000 );
+	
+	    // ----------------------------------------------------------------------
+
+	    setSolid( g );
+	    setSolid( fg );
+
+	    redrawAndPause( 1000 );
+
+	    // ----------------------------------------------------------------------
+
+	    setBold( d );
+	    setBold( cd );
+	
+	    redrawAndPause( 1000 );
+
+	    // ----------------------------------------------------------------------
+
+	    setSolid( d );
+	    setSolid( cd );
+
+	    redrawAndPause( 2000 );
+
+	    // ----------------------------------------------------------------------
+
+	    hideGraph( _graph );
+
+	    redrawAndPause( 1000 );
+
+	}
+
+    }
+
+
+
+
+
+}
Index: fedd/abac-src/atnvis/src/vis/ATNVisualizerConstants.java
===================================================================
--- fedd/abac-src/atnvis/src/vis/ATNVisualizerConstants.java	(revision 8780cbecc6db2bdc2b9ef31eec6e5209ad3bff15)
+++ fedd/abac-src/atnvis/src/vis/ATNVisualizerConstants.java	(revision 8780cbecc6db2bdc2b9ef31eec6e5209ad3bff15)
@@ -0,0 +1,120 @@
+package com.algomagic.atn.vis;
+
+import att.grappa.GrappaConstants;
+
+public interface ATNVisualizerConstants extends GrappaConstants {
+    public static final String SYSTEM_PREFIX = "atnvis.";
+
+    public static final String CONFIG_FILE_PROP = SYSTEM_PREFIX + "ConfigFile";
+    public static final String WINDOW_TITLE_PROP = SYSTEM_PREFIX + "window.Title";
+    public static final String WINDOW_HEIGHT_PROP = SYSTEM_PREFIX + "window.Height";
+    public static final String WINDOW_WIDTH_PROP = SYSTEM_PREFIX + "window.Width";
+
+    public static final String DELAY_PROP = SYSTEM_PREFIX + "defaultDelay";
+    public static final String LOOP_PROP = SYSTEM_PREFIX + "loop";
+
+
+    public static final String CONFIG_FILE_DEFAULT = "atnvis.properties";
+    public static final String WINDOW_TITLE_DEFAULT = "ATN Visualization";
+    public static final String WINDOW_HEIGHT_DEFAULT = "800";
+    public static final String WINDOW_WIDTH_DEFAULT = "600";
+
+    public static final String DELAY_DEFAULT = "500";
+    public static final String LOOP_DEFAULT = "true";
+
+    public static final int LEFT_SIDE = 0;
+    public static final int RIGHT_SIDE = 1;
+
+    public static final String OPPONENT_PROC = "Opponent";
+    public static final String VERIFIER_PROC = "Verifier";
+    public static final String FULLY_PROC = "Fully";
+    public static final String NOT_PROC = "Not";
+
+    public static final String SATISFIED = "True";
+    public static final String NOT_SATISFIED = "False";
+
+    public static final String STANDARD_TARGET = "StandardTarget";
+    public static final String INTERSECTION_TARGET = "IntersectionTarget";
+    public static final String LINKING_GOAL = "LinkingGoal";
+
+    public static final String IMPLICATION_EDGE = "Implication";
+    public static final String LINKING_MONITOR_EDGE = "LinkingMonitor";
+    public static final String LINKING_SOLUTION_EDGE = "LinkingSolution";
+    public static final String LINKING_IMPLICATION_EDGE = "LinkingImplication";
+    public static final String INTERSECTION_EDGE = "Intersection";
+    public static final String CONTROL_EDGE = "Control";
+
+    public static final String DEFAULT_NODE = SYSTEM_PREFIX + "node.Default.";
+    public static final String DEFAULT_EDGE = SYSTEM_PREFIX + "edge.Default.";
+
+
+    public static final String[] NODE_ATTRS = {
+	SHAPE_ATTR,
+	SIDES_ATTR,
+	PERIPHERIES_ATTR,
+	STYLE_ATTR,
+	COLOR_ATTR,
+	FONTNAME_ATTR,
+	FONTCOLOR_ATTR,
+	FONTSIZE_ATTR,
+	FONTSTYLE_ATTR };
+
+
+
+    public static final String[] NODE_ATTRS_PROP = {
+	"shape",
+	"sides",
+	"peripheries",
+	"style",
+	"color",
+	"fontname",
+	"fontcolor",
+	"fontsize",
+	"fontstyle" };
+
+    public static final boolean[] NODE_ATTRS_INT = {
+	false,
+	true,
+	true,
+	false,
+	false,
+	false,
+	false,
+	true,
+	false };
+
+
+    public static final String[] EDGE_ATTRS = {
+	STYLE_ATTR,
+	FONTNAME_ATTR,
+	COLOR_ATTR,
+	FONTCOLOR_ATTR,
+	FONTSIZE_ATTR,
+	FONTSTYLE_ATTR,
+	DIR_ATTR };
+
+    public static final String[] EDGE_ATTRS_PROP = {
+	"style",
+	"fontname",
+	"color",
+	"fontcolor",
+	"fontsize",
+	"fontstyle", 
+	"direction"  };
+
+
+    public static final boolean[] EDGE_ATTRS_INT = {
+	false,
+	false,
+	false,
+	false,
+	true,
+	false,
+	false };
+
+    
+
+
+
+
+}
