animator.java

Petri网分析工具PIPE is open-source

package pipe.gui;

import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.util.ArrayList;
import java.util.Iterator;

import javax.swing.JOptionPane;
import javax.swing.Timer;

import pipe.dataLayer.DataLayer;
import pipe.dataLayer.Transition;

public class Animator implements Constants{

  Timer timer;
  int numberSequences;
  
  private ArrayList firedTransitions;
  private static int count= 0;

  public Animator(){
    firedTransitions = new ArrayList();
    
    timer = new Timer(0, new ActionListener() {
      public void actionPerformed(ActionEvent evt) {
        if ((getNumberSequences()<1) ||
            !CreateGui.getView().animationmode) {
          timer.stop();
          CreateGui.getApp().setRandomAnimationMode(false);
          return;
        }
        doRandomFiring();
        setNumberSequences(getNumberSequences()-1);
      }    
    });
  }

  /* highlights enabled transitions*/
  public void highlightEnabledTransitions(){
    Iterator transitionIterator =CreateGui.currentPNMLData().returnTransitions();
    while(transitionIterator.hasNext()){
      Transition tempTransition =(Transition) transitionIterator.next();
      if(tempTransition.isEnabled(true)==true){
      	CreateGui.currentPNMLData().notifyObservers();
        tempTransition.repaint();
      }
    }
  }

    /* called during animation to unhighlight previously highlighted transitions*/
  public void unhighlightDisabledTransitions(){
    Iterator transitionIterator = CreateGui.currentPNMLData().returnTransitions();
    while(transitionIterator.hasNext()){
      Transition tempTransition =(Transition) transitionIterator.next();
      if(tempTransition.isEnabled(true)==false){
      	CreateGui.currentPNMLData().notifyObservers();
        tempTransition.repaint();
      }
    }
  }

    /* called at end of animation and resets all Transitions to false and unhighlighted*/
  public void disableTransitions(){
    Iterator transitionIterator = CreateGui.currentPNMLData().returnTransitions();
    while(transitionIterator.hasNext()){
      Transition tempTransition =(Transition) transitionIterator.next();
      tempTransition.setEnabledFalse();
      CreateGui.currentPNMLData().notifyObservers();
      tempTransition.repaint();
    }
  }

    /* stores model at start of animation*/
  public void storeModel(){
  	CreateGui.currentPNMLData().storeState();
  }

    /*restores model at end of animation and sets all transitions to false and unhighlighted*/
  public void restoreModel(){
  	CreateGui.currentPNMLData().restoreState();
    disableTransitions();
  }

  public void startRandomFiring(){
    if(getNumberSequences()>0) {
      // stop animation
      setNumberSequences(0);
      return;
    } else try {
      String s = JOptionPane.showInputDialog("Enter number of firings to perform", "1");
      this.numberSequences=Integer.parseInt(s);
      s = JOptionPane.showInputDialog("Enter time delay between firing /ms", "500");
      timer.setDelay(Integer.parseInt(s));
      timer.start();
    } catch (NumberFormatException e) {
      CreateGui.getApp().setRandomAnimationMode(false);
    }
  }
  
  public void stopRandomFiring() {
    numberSequences=0;
  }
  
  public void doRandomFiring() {
    DataLayer data=CreateGui.currentPNMLData();
    data.setEnabledTransitions();
    Transition t=data.fireRandomTransition();
    if(t!=null)fireTransition(t);

    data.setEnabledTransitions();
    unhighlightDisabledTransitions();
    highlightEnabledTransitions();
  }
  

  /*steps back through previously fired transitions*/
  public void stepBack(){
    if(count>0){
      Transition lastTransition = (Transition)firedTransitions.get(count-1);
      count--;
      CreateGui.currentPNMLData().fireTransitionBackwards(lastTransition);
      CreateGui.currentPNMLData().setEnabledTransitions();
      unhighlightDisabledTransitions();
      highlightEnabledTransitions();
    }
    else return;
  }

    /* steps forward through previously fired transitions*/
  public void stepForward(){
    if(count < firedTransitions.size()){
      Transition nextTransition = (Transition)firedTransitions.get(count);
      count++;
      CreateGui.currentPNMLData().fireTransition(nextTransition);
    }
    return;
  }

    /* stores transitions that has just been fired in array so that it can be accessed during backwards and forwards stepping*/
  public void fireTransition(Transition transition){
    CreateGui.getAnimationHistory().addHistoryItem(transition.getName());
    CreateGui.currentPNMLData().fireTransition(transition);
    CreateGui.currentPNMLData().setEnabledTransitions();
    CreateGui.getAnimator().highlightEnabledTransitions();
    CreateGui.getAnimator().unhighlightDisabledTransitions();
    firedTransitions.add(transition);
    count++;
  }
  public synchronized int getNumberSequences() {
    return numberSequences;
  }
  public synchronized void setNumberSequences(int numberSequences) {
    this.numberSequences = numberSequences;
  }
}