//****************************************************************************
// CLASS NAME:	ReachabilityTree.java
//
// AUTHOR:	Rick Brink
//		    rick@mail.csh.rit.edu
//		    http://www.csh.rit.edu/~rick
//
// VERSION:	1.0
//
// HISTORY:	4/16/96		Initial Version
//
// COPYRIGHT INFORMATION:
//
// This program and the Java source is in the public domain.
// Permission to use, copy, modify, and distribute this software
// and its documentation for NON-COMMERCIAL purposes and
// without fee is hereby granted.
//
//    Copyright 1996
//
//    Rick Brink
//    1266 Brighton-Henrietta Townline Rd.
//    Rochester, NY 14623
//
// DISCLAIMER:
//
// The author claims no responsibility for any damage, direct or indirect,
// to any harware or software as a result of using this program.
//****************************************************************************

import java.lang.Thread;
import java.util.Vector;

/**
  * A class representing a Petri Net Reachability Tree
  *
  * @see java.lang.Thread
  * @see java.util.Vector
  *
  * @version 1.0 July 3, 1996
  *
  * @author  Rick Brink
**/
class ReachabilityTree extends Thread {
    /** Used to access the design and simulation variables **/
    private protected PetriTool petriTool_;

    /** Vector representing the current marking of the Petri Net **/
    private protected Vector currentMarkingVector_;

    /** Indicates if the current design is valid, i.e. no dangling components **/
    private protected boolean validDesign_ = false;

    /** Timer to be used if petriTool_.boundAnalysisTime_ is true **/
    private protected Timer boundTimer_;

    /** Holds all String markings currently in tree **/
    private protected Vector masterMarkingVector_;

    /** Holds Vectors of nodes of the reachability tree **/
    private protected Vector treeVector_;

    /** Vector of nodes to be solved for the Reachability Tree **/
    private protected Vector toBeSolvedVector_;

    /**
      * Vector of Booleans indicating if the number of tokens in
      * a Place reached the maxPlaceCapacity_ and was overflowed
    **/
    private protected Vector overflowVector_;

    /**
      * Construct a new Reachability Tree.
    **/
    public ReachabilityTree(PetriTool app) {
        petriTool_ = app;
        reset();

        if (petriTool_.designPanel_.validDesign()) {
            this.start();
        }
        else {
            // Enable all Image Buttons
            petriTool_.controlPanel_.enableButtons();
        }
    }


    /**
      * Display a status message in the status panel
    **/
    public void StatusMessage(String msg) {
        petriTool_.statusPanel_.StatusMessage(msg);
    }


    /**
      * Reset the design, set up all links for traversals.
    **/
    private void reset() {
        masterMarkingVector_ = new Vector();
        treeVector_ = new Vector();
        toBeSolvedVector_ = new Vector();
        overflowVector_ = new Vector();

        int numPlaces__ = petriTool_.designPanel_.placeVector_.size();

        for (int i__ = 0; i__ < numPlaces__; i__++) {
            overflowVector_.addElement(new Boolean(false));
        }

        initializeTransitionMarkings();
    }

    /**
      * Returns a String representation of a Vector of Integers
      * of the form (1,2,0,1,0) for example.
    **/
    public String integerVectorToString(Vector integerVector) {
        String returnString__ = new String("(");
        Integer tempInt__ = new Integer(0);
        for (int i__ = 0; i__ < integerVector.size(); i__++) {
            tempInt__ = (Integer)integerVector.elementAt(i__);
            returnString__ += tempInt__.intValue();
            if (i__ < integerVector.size()-1) {
                returnString__ += ",";
            }
        }
        returnString__ += ")";
        return (returnString__);
    }

    /**
      * Main routine for creating the reachability tree.  Makes
      * calls to analyze node while there are nodes left to analyze.
      * Also, sets a timer if the boundAnalysisTime_ option is
      * enabled.
    **/
    public void run() {
        petriTool_.analysisRunning_ = true;

        // If a bound is set on analysis time, set the timer
        if (petriTool_.boundAnalysisTime_) {
            boundTimer_ = new Timer (this, petriTool_.boundTime_ * 60);
            StatusMessage("Analysis Timer set for " +
                          petriTool_.boundTime_ + " minute(s).");
        }
        currentMarkingVector_ = petriTool_.designPanel_.getInitialMarking();

        // Start analyzing the initial node
        addOrRemoveNode(currentMarkingVector_, true);

		while (toBeSolvedVector_.size() > 0) {
			Vector nodeToBeSolved__ = addOrRemoveNode(null, false);
            analyzeNode(nodeToBeSolved__);
        }

        // Set flag to indicate analysis is done
        petriTool_.analysisRunning_ = false;

        // Stop timer if one is running
        if (boundTimer_ != null) {
            boundTimer_.stop();
        }

        // Enable all Image Buttons
        petriTool_.controlPanel_.enableButtons();

        // Show the tree
        displayTree();
    }

    /**
      * Determines all Transitions that are enabled for
      * a marking and adds those markings to the Vector
      * of markings to be solved if it is a new marking,
      * otherwise appends an asterisk next to the marking.
    **/
    public void analyzeNode(Vector currentMarkingVector_) {
        Transition transition__;
        Vector booleanVector_ = new Vector();
        String markingString__;
        String transitionString__;
        Boolean enabled__;
        Integer tempInt1__;
        Integer tempInt2__;
        Vector newMarking__;
        int numTokens__;
        int i__;
        int j__;

        String initialMarkingString__ =
            integerVectorToString(currentMarkingVector_);
        if (!duplicateMarking(initialMarkingString__)) {
            Vector leafMarkingVector__ = new Vector();
            booleanVector_ = getTransitionFirings(currentMarkingVector_);
            Vector transitionVector__ = petriTool_.designPanel_.transitionVector_;


            for (i__ = 0; i__ < booleanVector_.size(); i__++) {
                enabled__ = (Boolean) booleanVector_.elementAt(i__);
                if (enabled__.booleanValue()) {
                    newMarking__ = new Vector();
                    transition__ = (Transition) transitionVector__.elementAt(i__);
                    for (j__ = 0; j__ < currentMarkingVector_.size(); j__++) {
                        tempInt1__ = (Integer) currentMarkingVector_.elementAt(j__);
                        tempInt2__ = (Integer) transition__.changeMarking_.elementAt(j__);
                        numTokens__ = tempInt1__.intValue() + tempInt2__.intValue();
                        if (numTokens__ > petriTool_.maxPlaceCapacity_) {
                            try {
                                overflowVector_.setElementAt(new Boolean(true), j__);
                            }
                            catch (ArrayIndexOutOfBoundsException e) {
                                System.out.println("Error - " + e);
                            }
                            numTokens__ = petriTool_.maxPlaceCapacity_;
                        }
                        try {
                            newMarking__.insertElementAt(new Integer(numTokens__), j__);
                        }
                        catch (ArrayIndexOutOfBoundsException e) {
                            System.out.println("Error - " + e);
                        }
                    }
                    markingString__ = integerVectorToString(newMarking__);
                    transitionString__ = new String("T");
                    transitionString__ = transitionString__.concat(String.valueOf(transition__.getLabel()));
                    leafMarkingVector__.addElement(transitionString__);

                    if (!duplicateMarking(markingString__)) {
                        addOrRemoveNode(newMarking__, true);
                    }
                    else {
                        markingString__ = markingString__.concat("*");
                    }

                    leafMarkingVector__.addElement(markingString__);
                }
            }


            try {
                leafMarkingVector__.insertElementAt(initialMarkingString__, 0);
            }
            catch (ArrayIndexOutOfBoundsException e) {
                System.out.println("Error - " + e);
            }

            addNode(leafMarkingVector__);
        }
    }

    /**
      * Given a marking, finds all Transitions that are enabled
      * with that marking, and returns a Vector of booleans,
      * corresponding to each Transition
    **/
    public Vector getTransitionFirings(Vector currentMarkingVector_) {
        Vector transitionVector__ = petriTool_.designPanel_.transitionVector_;
        Transition transition__;
        boolean enabled__;
        Integer tempInt1__;
        Integer tempInt2__;
        Vector booleanVector__ = new Vector();

        for (int i__ = 0; i__ < transitionVector__.size(); i__++) {
            transition__ = (Transition) transitionVector__.elementAt(i__);
            enabled__ = true;
            for (int j__ = 0; j__ < currentMarkingVector_.size(); j__++) {
                tempInt1__ = (Integer) currentMarkingVector_.elementAt(j__);
                tempInt2__ = (Integer) transition__.needMarking_.elementAt(j__);
                if (tempInt1__.intValue() < tempInt2__.intValue()) {
                    enabled__ = false;
                    break;
                }
            }

            try {
                booleanVector__.insertElementAt(new Boolean(enabled__), i__);
            }
            catch (ArrayIndexOutOfBoundsException e) {
                System.out.println("Error - " + e);
            }
        }

        return (booleanVector__);
    }

    /**
      * Adds a node to a pool of nodes that have yet to be solved, so
      * that the run() may dispatch a NodeAnalyzer to solve the node.
      * Otherwise, if allElseRemove is false, remove a Node and return it.
    **/
    public synchronized Vector addOrRemoveNode(Vector newMarking,
											   boolean addElseRemove) {
        Vector returnVector__ = new Vector();
		if (addElseRemove) { //add node
			toBeSolvedVector_.addElement(newMarking);
			return(null);
		}
		else { //remove node
			if (!toBeSolvedVector_.isEmpty()) {
            	try {
                	returnVector__ = (Vector) toBeSolvedVector_.firstElement();
                	toBeSolvedVector_.removeElementAt(0);
            	}
            	catch (Exception e) {
                	System.out.print("Tried to remove node, none available.");
           		}
            	return (returnVector__);
        	}
        	else {
            	return (null);
        	}
		}
    }

    /**
      * Used to stop the analysis while it is still running.
      * This may result in an incomplete reachability tree.
    **/
    public void stopAnalysis() {
        this.stop();
        petriTool_.analysisRunning_ = false;
        if (petriTool_.boundAnalysisTime_) {
            boundTimer_.stop();
        }
        petriTool_.controlPanel_.enableButtons();
        StatusMessage("Analysis was interrupted before completion, reachability tree may be incomplete.");
        displayTree();
    }

    /**
      * Routine called by the Timer in order to indicate that
      * the analysis time has elapsed.
    **/
    public void timerInterrupt() {
        petriTool_.controlPanel_.enableButtons();
        if (petriTool_.analysisRunning_) {
            StatusMessage("Reachability tree could not be constructed " +
                          "in the amount of time specified in Bound Time.");
        }
        else {
            System.out.println("Timer interrupt after analysis done.");
        }
    }

    /**
      * Returns whether or not the String marking is already in
      * the Reachability Tree
    **/
    public synchronized boolean duplicateMarking(String marking) {
        String marking__;
        Vector nodeVector_;

        for (int i__ = 0; i__ < treeVector_.size(); i__++) {
            nodeVector_ = (Vector) treeVector_.elementAt(i__);
            marking__ = (String) nodeVector_.elementAt(0);
            if (marking__.equals(marking)) {
                return (true);
            }
        }
        return (false);
    }

    /**
      * Generate a Vector for each transition, with each position
      * in the Vector corresponding to a Place, and holds the number
      * of Tokens needed in that place to activate the Transition.
      * Also, make a Vector in each Transition to indicate how the
      * marking changes when the Transition is activated.
    **/
    private void initializeTransitionMarkings() {
        Transition tempTransition__;
        Place tempPlace__;
        Arc tempArc__;
        int i__;
        int j__;
        int k__;
        int x__;
        int y__;
        int x1__;
        int y1__;
        int x2__;
        int y2__;
        int x3__;
        int y3__;
        Vector transitionVector__ = petriTool_.designPanel_.transitionVector_;
        Vector placeVector__ = petriTool_.designPanel_.placeVector_;
        Vector arcVector__ = petriTool_.designPanel_.arcVector_;

        // For all transitions, initialize their changeMarkingVector_
        int totalPlaces__ = petriTool_.designPanel_.placeVector_.size();

        for (i__ = 0; i__ < transitionVector__.size(); i__++) {
            tempTransition__ = (Transition) transitionVector__.elementAt(i__);
            tempTransition__.initializeChangeMarking(totalPlaces__);
            tempTransition__.initializeNeedMarking(totalPlaces__);
        }

        // Loop through all places
        for (i__ = 0; i__ < placeVector__.size(); i__++) {
            tempPlace__ = (Place) placeVector__.elementAt(i__);
            x__ = tempPlace__.getXCoordinate() * petriTool_.gridStep_;
            y__ = tempPlace__.getYCoordinate() * petriTool_.gridStep_;

            // Loop through all arcs, looking for those that start
            // at the current Place
            for (j__ = 0; j__ < arcVector__.size(); j__++) {
                tempArc__ = (Arc) arcVector__.elementAt(j__);
                x1__ = tempArc__.getFirstXCoordinate() * petriTool_.gridStep_;
                y1__ = tempArc__.getFirstYCoordinate() * petriTool_.gridStep_;
                x2__ = tempArc__.getLastXCoordinate() * petriTool_.gridStep_;
                y2__ = tempArc__.getLastYCoordinate() * petriTool_.gridStep_;

                // Deduct for incoming arcs
                if ((x__ == x1__) && (y__ == y1__)) {
                    for (k__ = 0; k__ < transitionVector__.size(); k__++) {
                        tempTransition__ = (Transition) transitionVector__.elementAt(k__);
                        x3__ = tempTransition__.getXCoordinate() * petriTool_.gridStep_;
                        y3__ = tempTransition__.getYCoordinate() * petriTool_.gridStep_;
                        if ((x2__ == x3__) && (y2__ == y3__)) {
                            tempTransition__.updateChangeMarking(i__,
                                tempArc__.getTokensToEnable() * -1);
                            tempTransition__.updateNeedMarking(i__,
                                tempArc__.getTokensToEnable());
                            break;
                        }
                    }
                }

                // Add for outgoing arcs
                if ((x__ == x2__) && (y__ == y2__)) {
                    for (k__ = 0; k__ < transitionVector__.size(); k__++) {
                        tempTransition__ = (Transition) transitionVector__.elementAt(k__);
                        x3__ = tempTransition__.getXCoordinate() * petriTool_.gridStep_;
                        y3__ = tempTransition__.getYCoordinate() * petriTool_.gridStep_;
                        if ((x1__ == x3__) && (y1__ == y3__)) {
                            tempTransition__.updateChangeMarking(i__,
                                tempArc__.getTokensToEnable());
                            break;
                        }
                    }
                }
            }
        }
    }



    /**
      * Adds a marking and all of the possible leafs of that marking
      * given a Vector of Strings.  The first element of the Vector
      * is the initial marking, then pairs of Strings denoting
      * a transition then another marking.
    **/
    public synchronized void addNode(Vector nodeVector) {
        treeVector_.addElement(nodeVector);
    }

    /**
      * Create a new ReachabilityDisplay to display the current
      * reachability tree.
    **/
    public void displayTree() {
        new ReachabilityDisplay(treeVector_, false, "");
    }

    /**
      * Create a new ReachabilityDisplay to display the current
      * reachability tree, with any marking matching
      * searchText highlighted.
    **/
    public void displayTree(String searchText) {
        new ReachabilityDisplay(treeVector_, true, searchText);
    }

    /**
      * Using the reachability tree, calculate and show the
      * properties of the Petri Net.
    **/
    public void displayProperties() {
        new PropertiesDisplay(treeVector_, overflowVector_);
    }

}
