analysis.java

Petri网分析工具PIPE is open-source

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