analysis.java

Petri网分析工具PIPE is open-source

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



}