invariantanalysis.java

Petri网分析工具PIPE is open-source

/**
 * Invariant analysis module.
 * @author Manos Papantoniou 
 * @author Michael Camacho
 * @author Maxim (GUI and some cleanup)
 */

package pipe.modules.invariantAnalysis;

import java.awt.Container;
import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.util.Date;

import javax.swing.BoxLayout;
import javax.swing.JDialog;

import pipe.dataLayer.DataLayer;
import pipe.dataLayer.PNMatrix;
import pipe.gui.CreateGui;
import pipe.gui.widgets.ButtonBar;
import pipe.gui.widgets.PetriNetChooserPanel;
import pipe.gui.widgets.ResultsHTMLPane;
import pipe.modules.Module;

public class InvariantAnalysis implements Module {

  private PNMatrix IncidenceMatrix;
  private PNMatrix PInvariants;
  private PNMatrix TInvariants;
  private static final String MODULE_NAME = "Invariant Analysis";

  private PetriNetChooserPanel sourceFilePanel;
  private ResultsHTMLPane results;
  
  public InvariantAnalysis() {}

  /** 
   * @return        The module name
   */
  public String getName() {
    return MODULE_NAME;
  }

  /** 
   * Call the methods that find the net invariants.
   * @param dataObj       A dataLayer type object with all the information about the petri net
   */
  public void run (DataLayer pnmlData) {
    // Build interface
    JDialog guiDialog = new JDialog(CreateGui.getApp(),MODULE_NAME,true);
    
    // 1 Set layout
    Container contentPane=guiDialog.getContentPane();
    contentPane.setLayout(new BoxLayout(contentPane,BoxLayout.PAGE_AXIS));
    
    // 2 Add file browser
    contentPane.add(sourceFilePanel=new PetriNetChooserPanel("Source net",pnmlData));
    
    // 3 Add results pane
    contentPane.add(results=new ResultsHTMLPane());
    
    // 4 Add button
    contentPane.add(new ButtonBar("Analyse",analyseButtonClick));

    // 5 Make window fit contents' preferred size
    guiDialog.pack();
    
    // 6 Move window to the middle of the screen
    guiDialog.setLocationRelativeTo(null);
    
    guiDialog.setVisible(true);

  }
  
  /**
   * Classify button click handler
   */
  ActionListener analyseButtonClick=new ActionListener() {
    public void actionPerformed(ActionEvent arg0) {
      DataLayer sourceDataLayer=sourceFilePanel.getDataLayer();
      String s="<h2>Petri net invariant analysis results</h2>";
      if(sourceDataLayer==null) return;
      if(!sourceDataLayer.getPetriNetObjects().hasNext()) s+="No Petri net objects defined!";
      else s+=analyse(sourceDataLayer);
      results.setText(s);
    }
  };

  private String analyse(DataLayer pnmlData) {
    Date start_time = new Date(); // start timer for program execution
    // extract data from PN object
    int[][] array = pnmlData.getIncidenceMatrix();
    if (array.length == 0) return "";
    IncidenceMatrix = new PNMatrix(array);

    int[] initialMarking = pnmlData.getInitialMarkupMatrix();
    String output = findNetInvariants(initialMarking);

    Date stop_time = new Date();
    double etime = (stop_time.getTime() - start_time.getTime())/1000.;
    return output + "<br>Analysis time: " + etime + "s";
  }

  /** Find the net invariants.
   *
   * @param M0   An array containing the initial marking of the net.
   * @return     A string containing the resulting matrices of P and T Invariants
   * or "None" in place of one of the matrices if it does not exist.
   */

  public String findNetInvariants(int[] M0){
    return reportTInvariants(M0)+reportPInvariants(M0);
  }

  /** Reports on the P invariants.
   *
   * @param M0   An array containing the initial marking of the net.
   * @return     A string containing the resulting matrix of P Invariants, the P equations and some analysis
   */

  public String reportPInvariants(int[] M0){
    PInvariants = findVectors(IncidenceMatrix.transpose());
    String result="<h3>P-Invariants</h3>"+PInvariants.printString(0,0).replaceAll("\n","<br>");

    if (PInvariants.isCovered()) result+="The net is covered by positive P-Invariants, therefore it is bounded.";
    else result+="The net is not covered by positive P-Invariants, therefore we do not know if it is bounded.";

    return result+findPEquations(M0);
  }


  /** 
   * Reports on the T invariants.
   *
   * @param M0   An array containing the initial marking of the net.
   * @return     A string containing the resulting matrix of T Invariants and some analysis of it
   */

  public String reportTInvariants(int[] M0){
    TInvariants = findVectors(IncidenceMatrix);
    String result= "<h3>T-Invariants</h3>"+TInvariants.printString(0,0).replaceAll("\n","<br>");

    if(TInvariants.isCovered()) result+="The net is covered by positive T-Invariants, therefore it might be bounded and live.";
    else result+="The net is not covered by positive T-Invariants, therefore we do not know if it is bounded and live.";
    
    return result;
  }

  /** Find the P equations of the net.
   *
   * @param initialMarking   An array containing the initial marking of the net.
   * @return                 A string containing the resulting P equations,
   *                         empty string if the equations do not exist.
   */

  public String findPEquations(int[] initialMarking){
    String eq = "<h3>P-Invariant equations</h3>";
    int m = PInvariants.getRowDimension(), n = PInvariants.getColumnDimension();
    if (n < 1) // if there are no P-invariants don't return any equations
      return "";

    PNMatrix col = new PNMatrix(m, 1);
    int rhs = 0; // the right hand side of the equations

    // form the column vector of initial marking
    PNMatrix M0 = new PNMatrix(initialMarking, initialMarking.length);
    // for each column c in PInvariants, form one equation of the form
    // a1*p1+a2*p2+...+am*pm = c.transpose*M0 where a1, a2, .., am are the
    // elements of c
    for (int i = 0; i < n; i++){ // column index
      for (int j = 0; j < m; j++){ // row index
        // form left hand side:
        int a = PInvariants.get(j, i);
        if (a > 1)
          eq += Integer.toString(a);
        if (a > 0)
          eq += "M(p" + Integer.toString(j) + ") + ";
      }
      // replace the last occurance of "+ "
      eq = eq.substring(0, (eq.length()-2)) + "= ";

      // form right hand side
      col = PInvariants.getMatrix(0, m-1, i, i);
      rhs = col.transpose().vectorTimes(M0);
      eq += rhs + "<br>"; // and separate the equations
    }
    return eq;
  }

  /** Transform a matrix to obtain the minimal generating set of vectors.
   *
   * @param C    The matrix to transform.
   * @return     A matrix containing the vectors.
   */

  public PNMatrix findVectors(PNMatrix C){
     /*
     | Tests Invariant Analysis Module
     |
     |   C          = incidence matrix.
     |   B          = identity matrix with same number of columns as C.
     |                Becomes the matrix of vectors in the end.
     |   pPlus      = integer array of +ve indices of a row.
     |   pMinus     = integer array of -ve indices of a row.
     |   pPlusMinus = set union of the above integer arrays.
     */

    int m = C.getRowDimension(), n = C.getColumnDimension();

    // generate the nxn identity matrix
    PNMatrix B = PNMatrix.identity(n, n);

    int[] pPlus, pMinus; // arrays containing the indices of +ve and -ve elements in a row vector respectively

    // while there are no zero elements in C do the steps of phase 1
//--------------------------------------------------------------------------------------
    // PHASE 1:
//--------------------------------------------------------------------------------------
    while (!(C.isZeroMatrix())) {
      if (C.checkCase11()){
        // check each row (case 1.1)
        for (int i = 0; i < m; i++){
          pPlus = C.getPositiveIndices(i); // get +ve indices of ith row
          pMinus = C.getNegativeIndices(i); // get -ve indices of ith row
          if (isEmptySet(pPlus) || isEmptySet(pMinus) ){ // case-action 1.1.a
            // this has to be done for all elements in the union pPlus U pMinus
            // so first construct the union
            int [] pPlusMinus = uniteSets(pPlus, pMinus);

            // eliminate each column corresponding to nonzero elements in pPlusMinus union
            for (int j = pPlusMinus.length-1; j >= 0; j--){
              if (pPlusMinus[j] != 0){
                C = C.eliminateCol(pPlusMinus[j]-1);
                B = B.eliminateCol(pPlusMinus[j]-1);
                n--;  // reduce the number of columns since new matrix is smaller
              }
            }
          }
          resetArray(pPlus);   // reset pPlus and pMinus to 0
          resetArray(pMinus);
        }
      }
      else if ( C.cardinalityCondition() >= 0){
        while (C.cardinalityCondition() >= 0){
          // while there is a row in the C matrix that satisfies the cardinality condition
          // do a linear combination of the appropriate columns and eliminate the appropriate column.
          int cardRow = -1; // the row index where cardinality == 1
          cardRow = C.cardinalityCondition();
          // get the column index of the column to be eliminated
          int k = C.cardinalityOne();
          if (k == -1) System.out.println("Error");

          // get the comlumn indices to be changed by linear combination
          int j[] = C.colsToUpdate();

          // update columns with linear combinations in matrices C and B
          // first retrieve the coefficients
          int[] jCoef = new int[n];
          for (int i = 0; i < j.length; i++){
            if (j[i] != 0)
              jCoef[i] = Math.abs(C.get(cardRow, (j[i]-1)));
          }

          // do the linear combination for C and B
          // k is the column to add, j is the array of cols to add to
          C.linearlyCombine(k, Math.abs(C.get(cardRow, k)), j, jCoef);
          B.linearlyCombine(k, Math.abs(C.get(cardRow, k)), j, jCoef);

          // eliminate column of cardinality == 1 in matrices C and B
          C = C.eliminateCol(k);
          B = B.eliminateCol(k);
          n--;       // reduce the number of columns since new matrix is smaller
        }