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;
    }


}