package pipe.modules.predatorInvariantAnalysis;
/**
 * Title:
 * Description:
 * Copyright:    Copyright (c) 2001
 * Company:
 * @author
 * @version 1.0
 */

import java.util.*;
import java.io.*;
import java.awt.*;
import javax.swing.*;

public class Analysis {/*extends JDialog*/// {
  private Vector placeNames;    //contain the place names
  private Vector transitionNames; //contain the transition names
  private Vector arcSources;
  private Vector arcTargets;
  private Vector arcValues;
  private Vector placeMarkings;

  public Vector subnetArcSource;
  public Vector subnetArcTarget;
  public Vector subnetArcWeight;

  private int placeNum; //no of trans (also column number)
  private int tranNum; // no of places (also row number)
  private int c[][];
  private int cplus[][];
  private int cminus[][];
  private int b[][];
  //private int extend[][];
  private int tinvars[][];
  private int extendCols;
  private int extendRows;
  private int currCColNum; //keep track of number of columns currently in C
  private int currCRowNum; //keep track of number of rows currently in C
  private int bRows;
  private int bCols;
  private boolean pCovered;
  private boolean tCovered;

  public int extend[][]; /* = { {-1,0,0,0,0,0,0,0},
               {1,1,-1,0,-1,1,2,-1},
               {0,-1,1,-1,2,0,-3,1},
               {0,0,1,0,-1,-1,0,0},
               {1,0,0,0,0,0,0,0},
               {0,1,0,0,0,0,0,0},
               {0,0,1,0,0,0,0,0},
               {0,0,0,1,0,0,0,0},
               {0,0,0,0,1,0,0,0},
               {0,0,0,0,0,1,0,0},
               {0,0,0,0,0,0,1,0},
               {0,0,0,0,0,0,0,1} }
               ;*/

  public int extendCopy [][];
  public int exCopyRow;
  public int exCopyCol;
  JLabel jLabel1 = new JLabel();
  JFrame frame;

  public InvariantDialog invariantDialog;

  public Analysis() {
    placeNames = new Vector();
    transitionNames = new Vector();
    arcSources = new Vector();
    arcTargets = new Vector();
    placeMarkings = new Vector();
    arcValues = new Vector();
    subnetArcSource = new Vector();
    subnetArcTarget = new Vector();
    subnetArcWeight = new Vector();

    //   try {
    //     jbInit();
    //   }
    //   catch(Exception e) {
    //     e.printStackTrace();
    //   }

  }

  //allocates a 2D array with rows and columns passed
  private void generateArray(int array[][], int rows, int col){

    array = new int [rows][];
    for(int i=0; i<rows;i++){
      array[i] = new int[col];
//      System.out.println(array[i]);
    }
  }
  //End of function///////////

  private int [][] generateInitialiseZeroArray(int array[][], int rows, int col){
    array = new int [rows][];
    for (int i=0; i < array.length;i++)
      array[i] = new int [col];

    for (int i=0; i < array.length; i++){
      for(int j=0; j < array[i].length; j++){
        array[i][j] = 0;
      }
    }
    return array;
  }

  //set array equal to C array(i,j) = c+(i,j) - c-(i,j)
  private void initialiseC(int array[][]){
    for (int i=0; i< placeNum; i++){
      for(int j=0; j < tranNum; j++){
        array[i][j] = cplus[i][j] - cminus[i][j];
      }
    }
  }
  //end of function///////////

  //initialise a matrix to the identiity matrix
  private void identityMatrix(int array[][]){
    for (int i=0; i < array.length; i++){
      for(int j =0; j < array[i].length; j++){
        if (i == j)
          array[i][j] = 1;
        else
          array[i][j] = 0;
      }
    }
  }
  //End of function//////////


  //initialises all the elements in an array to Zero
  private void initialiseZero( int ar[][]){
    //System.out.println("\nArray length is " + ar.length);
    for (int i =0 ; i < ar.length; i++){
      for (int j =0; j < ar[i].length; j++){
        ar[i][j] = 0;
      }
    }
  }
  //End of function/////////

  private void clearAllArrays(){
    extend = null;
    c = null;
    b = null;
    cplus = null;
    cminus = null;
    tranNum =0;
    placeNum =0;
    // transitionNames = new Vector();
    // placeNames = new Vector();
    //extendRows = 0;
    bRows =0;
    bCols =0;
    extendRows = 0;
    extendCols = 0;
    currCColNum =0;
    currCRowNum =0;


  }

  //Copies the ocntents of b array to tinvars array
  private void tinvars(){
    tinvars = new int [bRows][];
    for (int i=0; i < bRows; i ++){
      tinvars[i] = new int[bCols];
    }

    //now copy extend to tinvars
    for (int i=0; i < bRows; i++){
      for (int j=0; j < bCols; j++){
        tinvars[i][j] = b[i][j];
      }
    }


  }

  private void initialiseTranspose(){
    int tempTranNum = tranNum;
    tranNum = placeNum;
    placeNum = tempTranNum;
    //now generate extend so that it is the correct size
    generateExtend();
    placeNum = tranNum;
    tranNum = tempTranNum;
    for (int i =0; i < placeNum; i++){
      for (int j=0; j < tranNum; j++){
        extend[j][i] = cplus[i][j] - cminus[i][j];
      }
    }

    for (int i= tranNum, x=0; i < extend.length; i++, x++){
      for (int j =0, y =0; j < extend[i].length; j++, y++){
        if (x == y)
          extend[i][j] = 1;
        else
          extend[i][j] = 0;
      }
    }
    tranNum = placeNum;
    placeNum = tempTranNum;
  }

  //only copy c part to extendCopy.
  private void initialiseExtend(){
    //initialiseC(extend);  //obtain C
    for (int i=0; i < placeNum; i++){
      for (int j=0; j < tranNum; j++){
        extend[i][j] = cplus[i][j] - cminus[i][j];
        // extendCopy[i][j] = cplus[i][j] - cminus[i][j];
      }
    }

    for (int i= placeNum, x=0; i < extend.length; i++, x++){
      for (int j = 0, y =0; j < extend[i].length; j++, y++){
        if (x == y)
          extend[i][j] = 1;
        else
          extend[i][j] = 0;
      }
    }

  }



  //initialises all elements of an array to the integer passed
  private void initialiseArray(int array[], int value){
    for (int i=0; i<array.length; i++){
      array[i] = value;
    }
  }
  //End of function////////


  //check each row of C to find if there is a row that satisfies if P+ or P-
  //are the empty set
  //if such a row exists its subscript is returned
  //if >1 such rows exist the lowest subscript is returned
  //if there isn't a row that satisfies either of these then return -1;
  private Vector algorithm1_1(){
    boolean positive = false;
    boolean negative = false;
    int zeroCount;
    Vector suitableRows = new Vector();
    //recurse over each row for
    for (int i=0; i < currCRowNum; i++){
      if (currCColNum ==1){
        break;
      }
      positive = false;
      negative = false;
      zeroCount = 0;
      for (int j =0 ; j < currCColNum; j++){
        if (extend[i][j] > 0)
          positive = true;
        if (extend[i][j] < 0)
          negative = true;
        if (extend[i][j] == 0)
          zeroCount++;
      }

      if((!negative || !positive) && (zeroCount != currCColNum) ){
        //System.out.println("The suitable row is " + i);
        suitableRows.addElement(new Integer(i)); //the row that satisfies reqs for P+ or P-
      }
    }
    return suitableRows; //reutrn the vector of rows that satisfy P+ or P-
  }
  //End of function//////////


  //returns true if there are nonZero elements in C
  private boolean nonZero(){
    for (int i=0; i < currCRowNum; i++){
      for (int j =0 ; j < currCColNum; j++){
        if (extend[i][j] != 0)
          return true;
      }
    }

    return false;
  }
  //End of function/////////


  //Deletes a columns from the extended matrix (i.e. from both C and B)
  public void deleteExtendedColumn(int colNum){
    //i.e. copies all subsequent columns onforward and reduces the currCo number
    //System.out.println("deleteExtenedColumn has been called, colNum=" + colNum + " extendCols=" + extendCols);
    if (colNum > extendCols)
      return;

    for (int i = colNum; i < extendCols -1; i++){
      for (int j=0; j < extendRows; j++){
        extend[j][i] = extend[j][i+1];

      }
    }
    if (currCColNum > 0)
      currCColNum--;
    if (extendCols > 0)
      extendCols--;
  }
  //End of function////////



  private boolean modulus1_1b(int pplus[], int pminus[]){
    int ppCount =0;
    int pmCount =0;
    int plusModulusCount;
    int minusModulusCount;
    for (int i=0; i< currCRowNum; i++){
      plusModulusCount =0; //reset the modulus count
      minusModulusCount =0;

      for (int j=0; j< currCColNum; j++){
        if (extend[i][j] < 0)
          minusModulusCount += Math.abs(extend[i][j]);
        else if (extend[i][j] > 0)
          plusModulusCount += Math.abs(extend[i][j]);
      }
      //System.out.println("minusModulusCount= " + minusModulusCount + " plusModCount=" + plusModulusCount);
      if (minusModulusCount == 1){
        //System.out.println("minusModulusCount inside == 1");
        // System.out.println("minusModulusCount is 1");
        pminus[pmCount] = i;
        pmCount++;
      }

      if (plusModulusCount == 1){
        //System.out.println("plusModulusCount is 1");
        pplus[ppCount] = i;
        ppCount++;
      }
      if (pmCount >0 || ppCount > 0){
        //System.out.println("modulus returned true!");
        return true;
      }
    }

    // if (pmCount >0 || ppCount > 0)
    //return true;
    //else
    //System.out.println("modulus returned false!");
    return false;
  }
  //End of function///////


  //linearly combines a column k to column j of 2D Matrix
  private void linearCombination(int j,int k, int alpha, int beta){
    //must add things here
    for (int x=0; x < extendRows; x++)
      extend[x][j] = alpha * extend[x][k] + beta * extend[x][j];
  }
  //End of function//////


  //returns the first nonZero row index of C
  private int firstNonZeroRowC(){
    for (int i=0; i < currCRowNum;i++){
      for (int j=0; j < extendCols; j++){
        if (extend[i][j] != 0){
          return i;
        } //returns the row index
      }
    }
    return -1;
  }
  //End of function//////


  //finsd the first non zero column of row h
  private int firstNonZeroColumn(int h){
    for (int j=0; j < extendCols;j++){
      if (extend[h][j] != 0){
        return j;
      }
    }
    return -1;
  }
  //End of function


  //Initialises the arrays used in calculating the invariants
  private void arrayInitialisation(){
    generateArray(c,placeNum, tranNum);
    generateArray(b, tranNum, tranNum);
  }

  public void executeAlgorithm(){
    executeAlgorithm(false);
  }

  //Runs the algorithm
  public void executeAlgorithm(boolean transpose){
    //allocate all the arrays;
    arrayInitialisation();

    //now initialise C matrix - cplus and cminus must already be initialised
    //initialiseC();
    //initialiseExtend();  //initialise the extended matrix
    if (transpose){
      initialiseTranspose();
    }
    else {
      generateExtend();
      initialiseExtend();
      // System.out.println("\nThe initial extended matrix");
    }
//    System.out.println("extended");
    print2DArray(extend);

    currCColNum = tranNum;
    currCRowNum = placeNum;
    extendRows = tranNum + placeNum;
    extendCols = tranNum;

    //initialise B matrix
    //identityMatrix(b);

    //Phase 1
    while(nonZero()){  //identifythat there are non zero elements in c
      Vector satRows = algorithm1_1();
      if (satRows.size() > 0){
        //System.out.println("The number of suitable row is " +satRows.size());
        //There are rows that satisfy P+ or P-
        //now delete all the columns of the extended matrix that satisfy [1.1]
        // for (int count =0; count < satRows.size(); count++){
        Integer aRow = (Integer)satRows.elementAt(0);
        int aRowValue = aRow.intValue();
        for (int x=0; x < extendCols; x ++){
          if (extend[aRowValue][x] != 0)
            deleteExtendedColumn(x);
        }
        //System.out.println("\n------------------\nA Column has been deleted!");
        // print2DArray(extend, extendRows, extendCols);
        // System.out.println("extendRows =" + extendRows + " extendCols =" + extendCols);

        //}
      }
      else {   //there aren't rows that satisfy P+ or P- are empty
        // System.out.println("Section 1.1.b has been entered");
        int pplus[] = new int[extendCols];
        int pminus[] = new int[extendCols];
        initialiseArray(pplus, -1);
        initialiseArray(pminus, -1);
        if (modulus1_1b(pplus, pminus)){
          int k = -1;//there is a row where mod(P+) = 1 or mod(P-) = 1
          if (pplus[0] != -1 && pminus[0] != -1){
            //i.e there are rows where p+ and p- equal 1
            //Then use the P+
            int rowP = pplus[0];
            k = pPlusCombine(rowP);
            // System.out.println("Program reached position 1");
          }
          else if (pplus[0] != -1){
            int rowP = pplus[0];
            k = pPlusCombine(rowP);
            //print2DArray(extend, extendRows, extendCols);
            //System.out.println("Program reached position 2");
          }
          else if (pminus[0] != -1){
            int rowP = pminus[0];
            //System.out.println("pminus[0]= " + pminus[0]);
            k = pMinusCombine(rowP);
            //System.out.println("Program reached position 3 k=" + k );
          }
          //now delete the row k
          if (k!= -1){
            deleteExtendedColumn(k);
            //System.out.println("Program reached position 4");
            //print2DArray(extend, extendRows, extendCols);
          }
        }
        else {
          //find a nonZeroRow of C
          //k is a column such that Chk != 0
          int h = firstNonZeroRowC();
          if (h != -1){
            int k = firstNonZeroColumn(h);
            //System.out.println("in 1.1.b.2 h=" + h + " k=" + k);
            substituteColumns2(h,k);
            deleteExtendedColumn(k); //now delete the firstNonZeroColumn
            //print2DArray(extend, extendRows, extendCols);
          }
        }



      }//End of 1st else
    } //End of phase1 loop

    //Now in phase2
    phase2(transpose);

  }//End of function


  //phase 2 executes phase2 of the algorithm
  private void phase2(){
    phase2(false);
  }

  private void phase2(boolean transpose){
    //now setup B so that it contains only
    //System.out.println("\nEntering phase 2");
    b = generateInitialiseZeroArray(b, tranNum, tranNum);
    this.b = b;
    //print2DArray(b,2,2);
    //initialiseZero(b);
    this.b = copyB();
    //System.out.println("Printing Array after copyB!");
    // print2DArray(b, bRows, bCols);
    int h = -1;
    while (rowWithNegativeElementB()){
      //System.out.println("Beginning of loop");
      h = rowWithNegativeElementBNumber();
      //  System.out.println("The value of h= " + h);
      int pPlus[] = new int [bCols+2];
      int pMinus[] = new int [bCols+2];
      setPPlusAndPMinus(b,h, pPlus, pMinus); //get P+ and P- sets

      if (pPlus[0] != -1){ //There are elements in the row with +ve values
        //System.out.println("pPlus != -1");
        for (int j=0; pPlus[j] != -1; j++){
          for (int k =0; pMinus[k] != -1; k++){
            //System.out.println("Reached position 1");
            //now perform a linear combination of j and k to form another column
            //first check if there is a spare column in B
            if (b.length == bCols)
              b = addColumnToB();

            int newCol = bCols;
            linearCombToNewColumn(pPlus[j], pMinus[k], h, newCol);
            divideByGCD(b,newCol);  //divide by the columns GCD
            bCols++;

          }
        }

        //now delete from B all columns of index k in P-
        for (int i=0; pMinus[i] != -1; i++){
          deleteColumn(b, pMinus[i], bCols);
          bCols--;
        }
//        System.out.println("2D Array");
        print2DArray(b,bRows, bCols);


      }//endfor
    }//endwhile

    //now delete from B all columns having non-minimal support??
    //see the other paper for details of this!!!!
    //System.out.println("Should now delete all columns with nonminimal support");
    deleteColsWithoutMinimalSupport();
    if (!transpose)
      tinvars();  //
    else {
    }
    //print2DArray(b, bRows, bCols);
  }//End of function

  //deletes a column from an array where colNum is the column to be deleted and
  //totalColNum is the total number of columns used in the array
  private void deleteColumn(int array [][], int colNum , int totalColNum){
    for (int i = colNum; i < totalColNum-1; i++){
      for (int j =0; j < array.length; j++){
        array[j][i] = array[j][i+1];
      }
    }
  }




  private void linearCombToNewColumn(int j, int k,  int h, int newCol){
    int alpha, beta;
    //I'm not sure what alpha and beta should be!
    //Need to see Alaiwan and Memmi
    //In the other implementation alpha is +abs and beta is -abs

    alpha = Math.abs(b[h][j]);
    beta =  Math.abs(b[h][k]);
    // System.out.println("In linearCombTo j= " + j + "k= " + k);
    for (int x =0; x < bRows; x++){
      if (x==h)
        b[x][newCol] = 0;
      else
        b[x][newCol] = beta * b[x][j] + alpha* b[x][k];
    }
    //is this correct???  The other implementation has
    //something strange!!!

  }


  //Divides a column in array[][] by its greatest common denominator
  private void divideByGCD(int array[][], int colNum){
    int gcd = getGCD(array, colNum);
    if (gcd == 0){
      //System.out.println("GCD==0");
      return;
    }
    for (int i=0; i < bRows; i++){
      array[i][colNum]/= gcd;
      //System.out.println("array[" + i + "][" + colNum + "] =" + array[i][colNum]);
    }
  }
  //End of function///////////



  //returns the greatest common denominator of the column
  private int getGCD(int array[][], int colNum){

    int lowestGCD =0;
    for (int i=0; i < bRows; i++){
      for (int j =i; j < bRows; j++){
        int tempGCD = gcd(Math.abs(array[i][colNum]), Math.abs(array[j][colNum]));
        if (lowestGCD ==0)
          lowestGCD = tempGCD;
        else if (tempGCD < lowestGCD && tempGCD != 0)
          lowestGCD = tempGCD;

        //   System.out.println("gcd= " + lowestGCD);
        //  for (int p=0; p < bRows; p++){
        //    System.out.print(" " + array[p][colNum]);
        //  }
      }
    }
    return lowestGCD;
  }
  //End of function///////////

  //returns the greates common denominator of x and y
  private int gcd(int x, int y){
    //System.out.println("x= " +x + "  y=" + y);
    if (x == 0)
      return y;
    if (y ==0)
      return x;
    if (x == y)
      return x;
    if (x < y)
      return gcd(x, (y-x));
    else
      return gcd(y, (x-y));
  }
  //End of Function////////////



  //adds a column to Array B
  private int [][] addColumnToB(){

    int tempA [][] = new int[b.length+1][];
    for (int i=0; i < b.length; i++)
      tempA[i] = new int[bRows];

    //now initialise equal to B
    for (int i=0; i < b.length; i++){
      for (int j=0; j < b[i].length; j++){
        tempA[i][j] = b[i][j];
      }
    }
    b = tempA;  //I hope this works!!!!!
    //bCols++;  //the actual number of Columns that have actual data in them has
    //not changed
    return b;
  }




  //places the indices of columns in row h of -ve nums in pMinus and of pos
  //values in pPlus
  private void setPPlusAndPMinus(int array[][], int h, int pPlus[], int pMinus[]){
    int pPlusPos = 0;
    int pMinusPos = 0;
    for (int j=0; j < bCols; j++){
      //System.out.println("value of j=" + j + "value of h" + h);
      if (array[h][j] < 0){
        pMinus[pMinusPos] = j;
        pMinusPos++;
      }
      else if(array[h][j] > 0){
        pPlus[pPlusPos] = j;
        pPlusPos++;
      }
    }
    pPlus[pPlusPos] = -1;
    pMinus[pMinusPos] = -1;
    //System.out.print("\nPrinting pPlus ");
    //  for (int z=0; pPlus[z] != -1; z++){
    //System.out.print(" " + pPlus[z]);
    //  }
    //System.out.print("\nPrinting pMinus ");
    // for (int z=0; pMinus[z] != -1; z++){
    //System.out.print(" " + pMinus[z]);
    // }

  }
  //End of function//////////////




  //Identifies if there is an a negative element in B[][]
  private boolean rowWithNegativeElementB(){
    //System.out.println("bRows= " + bRows + "  bCols =" + bCols);
    for (int i=0; i < bRows; i++){
      for (int j=0; j< bCols; j++){

        if (b[i][j] < 0){
          //row = i;
          return true;
        }
      }
    }
    return false;
  }

  private int rowWithNegativeElementBNumber(){
    //System.out.println("bRows= " + bRows + "  bCols =" + bCols);
    for (int i=0; i < bRows; i++){
      for (int j=0; j< bCols; j++){
        if (b[i][j] < 0){
          //row = i;
          return i;
        }
      }
    }
    return -1;
  }




  //Copies the extended section corresponding to B to B[][]
  private int[][] copyB(){
    bRows = 0;
    bCols = extendCols;
    // System.out.println ("CRows-" + currCRowNum + " extendRows=" + extendRows + " extendCols=" + extendCols);
    for (int i = currCRowNum, x =0; i < extendRows; i++, x++){
      bRows++;
      for (int j = 0; j < extendCols; j++){
        b[x][j] = extend[i][j];
        // System.out.println("b[x][j]=" + b[x][j] + " extend[x][j]=" + extend[x][j]);
        //System.out.println(b[x][j]);
      }
    }
    //System.out.println("bRows=" + bRows + " extenRows=" + extendRows);
    return b;
  }
  //End of function////////

  private int sign(int x){
    if (x > 0)
      return 1;
    else if (x < 0)
      return -1;
    else
      return 0;
  }

  //finds the element in rowP that is 1 and then calls linearCombination
  //h is the row that satisfies |P+|=1 or |P-|=1
  private int pPlusCombine(int h){
    int k =-1;
    for (int i=0; i < extend[h].length; i++){
      if (extend[h][i] == 1){
        k = i;
        break;
      }
    }
    if (k != -1){
      substituteColumns1(h,k);
    }
    return k;  //returns the index k
  }

  //finds
  //////////////////////////////
  private int pMinusCombine(int h){
    int k =-1;
    //System.out.println("pMinusCombine called for row h=" + h + "length=" + extend[h].length);
    for (int i=0; i < extend[h].length; i++){
      if (extend[h][i] == -1){
        k = i;
        //System.out.println("!!!!!k=" + k);
        break;
      }
    }

    if (k !=-1){
      substituteColumns1(h,k);
    }
    return k; //returns the index k
  }
  //End of function/////////////////


  //
  private void substituteColumns1(int h, int k){
    int j, alpha, beta;
    int position = extend[h][k];
    //  if (position == 0){
    //   System.out.println("In SubstituteColumns1 position is equal to zero");
    //  }
    beta = Math.abs(extend[h][k]); //is this correct?? Should it be [h][k] ???
    if (position < 0){
      for (j=0; j< extendCols; j++){
        if (extend[h][j] > 0){
          alpha = Math.abs(extend[h][j]); //should it be [h][j] ?????
          //int beta = abs(extend[h][k]); //why is beta calculated??
          linearCombination(j,k,alpha, beta);
        }
      }
    }else {
      for (j=0; j < extendCols; j++){
        if (extend[h][j] < 0){
          alpha = Math.abs(extend[h][j]); //should this be the other way round????
          linearCombination(j,k,alpha,beta);
        }
      }
    }
  }
  //End of function


  private void substituteColumns2(int h, int k){
    int j, alpha, beta;

    int position = extend[h][k];
    //if (position == 0){
    //   System.out.println("Position equals zero in substituteColumns2()");
    //}

    beta = Math.abs(extend[h][k]);
    for (j=0; j<extendCols;j++){
      if (j!=k && extend[h][j] != 0){
        if(sign(extend[h][j]) != sign(extend[h][k]))
          alpha = Math.abs(extend[h][j]);
        else
          alpha = - Math.abs(extend[h][j]);

        linearCombination(j,k,alpha,beta);
      }
    }
  }

  public void addTransitionName(String transitionName){
    transitionNames.addElement(transitionName);
    tranNum++;
  }

  public void addPlaceName(String placeName){
    placeNames.addElement(placeName);
    placeNum++;
  }

  public void addArcSourceTarget(String arcSource, String arcTarget){
    arcSources.addElement(arcSource);
    arcTargets.addElement(arcTarget);
  }

  public void addArcValue(int value){
    arcValues.addElement(new Integer(value));
  }

  public void addSubnetArcsToC(){
    int num = subnetArcSource.size();
    String arcSource;
    String arcTarget;
    int theValue;
    Integer integerValue;
    for (int i=0; i < num; i++){
      arcSource = (String)subnetArcSource.elementAt(i);
      arcTarget = (String)subnetArcTarget.elementAt(i);
      integerValue = (Integer)subnetArcWeight.elementAt(i);
      //now get the int value
      theValue = integerValue.intValue();
      addDataToC(arcSource, arcTarget, false, theValue);
    }

  }


  public void addDataToC(String arcSource,
                         String arcTarget,
                         boolean tranTarget,
                         int theValue){

    String thePlace = null;
    String theTran;
    int transitionPosition = -1;
    int placePosition = -1;
    //  if (tranTarget){
    //  thePlace = arcSource;
    //   theTran = arcTarget;
    //}
    //else {
    //thePlace = arcTarget;
    //theTran = arcSource;
    //}

    int num = transitionNames.size();
    for (int i=0; i < num; i++){
      String tempName = (String)transitionNames.elementAt(i);
      if (arcSource.equals(tempName)){
        transitionPosition = i;
        tranTarget = false;
        thePlace = arcTarget;
      }
      else if (arcTarget.equals(tempName)){
        transitionPosition = i;
        tranTarget = true;
        thePlace = arcSource;
      }
    }
    if (thePlace == null){
      //System.out.println("The place equals null Error loading module!!!!");
      return;
    }
    else {
      num = placeNames.size();
      for (int i=0; i < num; i++){
        String tempName = (String)placeNames.elementAt(i);
        if (thePlace.equals(tempName))
          placePosition = i;
      }
      //System.out.println("In addDataToc placeposition=" + placePosition + "transitionPosition=" + transitionPosition);
      if (tranTarget){
        //add to C-
        cminus[placePosition][transitionPosition] = theValue;
      }
      else {
        cplus[placePosition][transitionPosition] = theValue;
        //add to C+
      }
    }
  }

  public String getModuleName(){
    return "Invariant analysis";
  }

  public void clearAllVectors(){
    placeNames.clear();
    transitionNames.clear();
    placeMarkings.clear();
    arcSources.clear();
    arcTargets.clear();
    arcValues.clear();
    subnetArcSource.clear();
    subnetArcTarget.clear();
    subnetArcWeight.clear();
  }

  public void runModule(){
    clearAllArrays();
    clearAllVectors();
    //a new instance has been created by the calling editor
    //System.out.println("Invariant Module runModule has been called");
    //first must read first
    //create a new parser instance
    InvariantXmlFileReader reader= new InvariantXmlFileReader(this);
    //reader.runFileReader();  //Parse the file
    //System.out.println("arcValues: " + arcValues);
    //Now execute the algorithm
    executeAlgorithm(false); //Calculate T invariants
    executeAlgorithm(true); //Calculate P invariants

    String tinvarString = generateTinvarDisplay(false);
    String pinvarEquation =generatePinvarDisplay(true);
    String pinvarString = generatePinvarDisplay(false);
    String covered = generateCoveredString();//"";
    //   showDialog();

//  }

//  private void showDialog(){
    invariantDialog = new InvariantDialog(tinvarString, pinvarString, pinvarEquation, covered);
    invariantDialog.show();
  }
  //Now set up to display the results
   /* frame = new JFrame("Invariant Analysis");
    Container contentPane = frame.getContentPane();
        contentPane.setLayout(new BorderLayout());
        contentPane.add(new InvariantDialog(frame,
                                            tinvarString,
                                            pinvarString,
                                            pinvarEquation,
                                            covered));

  //  frame.addWindowListener(new WindowAdapter());


  ///  public void windowClosing(WindowEvent e) {
  ///     System.exit(0);
  // }
  // });

        frame.pack();
        frame.setVisible(true);
    }*/
    /*
      Container contentPane = frame.getContentPane();
        contentPane.setLayout(new GridLayout(1,1));
        contentPane.add(new DialogDemo(frame));

        frame.addWindowListener(new WindowAdapter() {);

            public void windowClosing(WindowEvent e) {
                System.exit(0);
            }
        });

        frame.pack();
        frame.setVisible(true);

    */

  public void generateCPlusCMinus(){
    //System.out.println("CPlusMinus being generated places= "+ placeNum + " trans=" + tranNum);
    cplus = new int [placeNum][];
    cminus = new int [placeNum][];
    for (int i=0; i < cplus.length; i++){
      cplus[i] = new int[tranNum];
      cminus[i] = new int[tranNum];
    }
  }

  //also generates a copy of extend - extendCopy
  public void generateExtend(){
    //System.out.println("generateExtend has been called");
    extend = new int [placeNum + tranNum][];
    extendCopy = new int [placeNum + tranNum][];
    exCopyRow = placeNum;
    exCopyCol = tranNum;
    for (int i=0 ; i < extend.length; i++){
      extend[i] = new int [tranNum];
      extendCopy[i] = new int[tranNum];
    }
  }

  private void deleteColsWithoutMinimalSupport(){
    //System.out.println("delCols without MinSupp extendCols" + bCols);
    if (bCols < 0)
      return;

    int deleteFlag[] = new int [bCols];
    int i,j,k;
    boolean nonMinimal;

    for (j=0; j < bCols; j++){
      deleteFlag[j] = 0;
    }

    for (j=0; j < bCols; j++){
      for (k=0; k < bCols; k++){
        nonMinimal = false;
        if (k!= j){
          for (i=0; i < bRows; i++)
            if (b[i][k] > 0 && b[i][j] == 0){
          nonMinimal = true;
          break;
            }
            if (!nonMinimal)
              deleteFlag[j] = 1;
        }
      }
    }

    int deleted = 0;
    j =0;

    // System.out.println("Contents of deleteFlag array");
    //Print the deleteFlag array
    //for (int x=0; x < deleteFlag.length; x++){
    //   System.out.println("deleteFlag[" + x +"] = " + deleteFlag[x]);
    // }

    while (j + deleted < bCols){
      // System.out.println("j= " + j + " bCols=" + bCols);
      if (deleteFlag[j+deleted] == 1){
        //delete the column j in extend
        //System.out.println("Column beibg deleted from b, col j=" +j + " bCols=" + bCols);
        deleteColumn(b, j, bCols);
        bCols--;
        // deleted++;
        j++;
      }
      else j++;
    }
  }


  public void addToPlaceMarkings(Integer marking){
    placeMarkings.addElement(marking);
  }


  private void print2DArray(int array[][]){
/*
//    System.out.println("\n\nPrinting Array");
    for (int i=0; i < array.length; i++){
//      System.out.println("");
      //  if (i == 4)
      //System.out.println("--------------------");
      for (int j =0; j < array[i].length; j++){
        if (array[i][j] >= 0)
          System.out.print(" ");
        System.out.print("  " + array[i][j]);
      }
    }
*/
  }

  private void print2DArray(int array[][], int rowNum, int colNum){
/*
    System.out.println("\n\nPrinting Array");
    for (int i=0; i < rowNum; i++){
      System.out.println("");
      if (i == 4)
        System.out.println("-------------------");
      for (int j=0; j < colNum; j++){
        if (array[i][j] >= 0)
          System.out.print(" ");
        System.out.print(" " + array[i][j]);
      }
    }
*/
  }


  public void testAlgorithm(){

    setUpVariables();
    //generate the extendedArray
    generateArray(extend, tranNum + placeNum, tranNum);
    fillC();
    executeAlgorithm();
  }


  public void fillC(){
   /* extend = { {1,0,0,0,0,0,0,0},
               {1,1,-1,0,-1,1,2-1},
               {0,-1,1,-1,2,0,-3,1},
               {0,0,1,0,-1,-1,0,0},
               {1,0,0,0,0,0,0,0},
               {0,1,0,0,0,0,0,0},
               {0,0,1,0,0,0,0,0},
               {0,0,0,1,0,0,0,0},
               {0,0,0,0,1,0,0,0},
               {0,0,0,0,0,1,0,0},
               {0,0,0,0,0,0,1,0},
               {0,0,0,0,0,0,0,1} }
               ;*/
  }

  public void setUpVariables(){
    tranNum = 8;
    placeNum = 4;
    currCRowNum = 4;
    currCColNum =8;
  }


  /*public static void main(String args[]){
    //System.out.println("Starting Program");
    Analysis newAnal = new Analysis();
    // newAnal.print2DArray(array);
    newAnal.testAlgorithm();

  }*/
  // private void jbInit() throws Exception {
  //   jLabel1.setText("Invariant Analysis Module");
  //   jLabel1.setBounds(new Rectangle(118, 4, 158, 38));
  //   this.getContentPane().setLayout(null);
  //  this.getContentPane().add(jLabel1, null);
  // }

  private void generatingDisplay(){
    generateTinvarDisplay(false);
    //generatePinvarDisplay();

  }

  private String generateTinvarDisplay(boolean equation){
    //System.out.println("T invariants are");
    boolean first;
    String results = new String();
    results = "";
    if (tinvars.length == 0 ){
      // System.out.println("there are no T invariants!");
      return null;
    }
    boolean tCoveredArray [] = new boolean[tinvars.length];
    for (int i=0; i < tinvars.length; i++){
      tCoveredArray[i] = false;
    }


    for (int i =0; i < tinvars[0].length; i++){
      first = true;

      for (int j =0; j < tinvars.length; j++){
        if (tinvars[j][i] > 0){
          //get the transition name from the Vector
          tCoveredArray[j] = true;
          String tranName= (String)transitionNames.elementAt(j);
          if (!first && equation){
            results += " + ";
          }
          else if (!first && ! equation){
            results += ",";
          }
          if (tinvars[j][i] > 1){
            results += "" + tinvars[j][i];
          }
          results += tranName;
          first = false;
        }
      }
      results += "\n";
    }

    boolean cov = true;
    for (int j=0; j < tCoveredArray.length && cov; j++){
      if (!tCoveredArray[j])
        cov = false;
    }
    tCovered = cov;
    //System.out.println("T invariants are ");
    // System.out.println(results);
    return results;
  }

  private String generatePinvarDisplay(boolean equation){
    if (bCols == 0 && bRows ==0){
      // System.out.println("There are no P invariants!");
      return null;
    }
    boolean pCoveredArray [] = new boolean[bRows];
    for (int i =0; i < pCoveredArray.length; i++){
      pCoveredArray[i] = false;
    }
    //System.out.println("P invariants are" );
    boolean first;
    String results = "";
    String answer = "";
    for (int i=0; i < bCols; i++){
      //System.out.println("new Column");
      first = true;
      //results += "\n";
      int markingCount =0;
      for (int j=0; j < bRows; j++){
        //System.out.println("new Row");
        if (b[j][i] > 0){
          pCoveredArray[j] = true;
          String placeName = (String)placeNames.elementAt(j);
          if (!first && equation){
            results += " + ";
          }
          else if (!first && !equation){
            results += ",";
          }
          if (b[j][i] > 1){
            results += b[j][i];
          }
          results += placeName;
          first = false;

          if (equation){
            //get the value of the marking
            Integer tempMarking = (Integer)placeMarkings.elementAt(j);
            markingCount += tempMarking.intValue();
            //System.out.println("Temp marking is " + tempMarking.intValue() + "markingCount=" +markingCount);
          }
        }//Enf if
      }//end for j
      if (equation){
        results += " = " + markingCount;
      }
      results += "\n";
    }//end for i

    boolean cov = true;
    for (int j=0; j < pCoveredArray.length && cov; j++){
      if (pCoveredArray[j] == false)
        cov = false;
    }
    pCovered = cov;
    //System.out.println(results);
    return results;
  }

  private String generateCoveredString(){
    String coveredText = "";
    if (pCovered){
      coveredText += "Petri-net is covered by P invariants"
                   + "\nand is therefore bounded\n\n";
    }
    else {
      coveredText += "Petri-net NOT covered by P invariants"
                   + "\nand is therefore not bounded\n\n";
    }

    if (tCovered){
      coveredText += "Petri-net is covered by T invariants";
    }
    else {
      coveredText += "Petri-net NOT covered by T invariants"
                   + "\nand is therefore NOT (live and bounded)";
    }

    return coveredText;
  }



}