reachabilitytreenode.java

petrinets小程序

import java.awt.Graphics;
import java.util.Vector;


public class ReachabilityTreeNode {
	
// type of node	
	protected static final int sideNode = 1;
	protected static final int insideNode = 2;
	protected static final int duplicateNode = 3;
	protected static final int terminateNode = 4;
	protected static final int root = 5;
	
	protected int type;
	
	protected marking mark;
	
	protected ReachabilityTreeNode parentNode;
	protected ReachabilityTreeNode nextNode;
	
	protected int level = 0;
	protected int vol = 0;             //how many children it has
	protected int volth = 0;           //ith in one level
	
	
	public ReachabilityTreeNode(){
		this.type = ReachabilityTreeNode.sideNode;
		this.mark = null;
		this.parentNode = null;
		this.nextNode = null;
		level = 0;
		vol = 0;
		volth = 0;
	}
	
	public ReachabilityTreeNode(marking m){
		this.type = ReachabilityTreeNode.sideNode;
		this.mark = m;
		this.parentNode = null;
		this.nextNode = null;
		level = 0;
		vol = 0;
		volth = 0;
	}
	
	public ReachabilityTreeNode(pn PN){
		this.type = ReachabilityTreeNode.sideNode;
		this.mark = new marking(PN);
		this.parentNode = null;
		this.nextNode = null;
		level = 0;
		vol = 0;
		volth = 0;
	
	}
	
	public ReachabilityTreeNode(ReachabilityTreeNode node){
		this.type = node.type;
		this.mark = node.mark;
		this.parentNode = node.parentNode;
		this.nextNode = node.nextNode;
		level = node.level;
		vol = node.vol;
		volth = node.volth;
	}
	
	public void setType(int typ){
		this.type = typ;
	}
	public int getType(){
		return this.type;
	}
	
	public void setMark(marking m){
		this.mark = new marking(m);
	}
	public void setMark(pn PN){
		this.mark = new marking(PN);
	}
	public marking getMark(){
		return this.mark;
	}
	
	public void setParentNode(ReachabilityTreeNode node){
		this.parentNode = new ReachabilityTreeNode(node);
	}
	public ReachabilityTreeNode getParentNode(){
		return this.parentNode;
	}
	
	public void setNextNode(ReachabilityTreeNode node){
		this.nextNode = new ReachabilityTreeNode(node);
	}
	public ReachabilityTreeNode getNextNode(){
		return this.nextNode;
	}
	
	public void setLevel(int l){
		this.level = l;
	}
	public int getLevel(){
		return this.level;
	}
	
	public void setVol(int v){
		this.vol = v;
	}
	public int getVol(){
		return this.vol;
	}
	
	public void setVolth(int vt){
		this.volth = vt;
	}
	public int getVolth(){
		return this.volth;
	}
	
	public void produceNode(ReachabilityTreeNode z, ReachabilityTreeNode x, transition t, pn PN){
		if(x.enable(x, PN, t)){
		z.type = ReachabilityTreeNode.sideNode;
		ReachabilityTreeNode node = new ReachabilityTreeNode();
		node.setMark(x.mark.fire(PN, t));
		node.setParentNode(x);
		x.setNextNode(z);
		node.setLevel(x.getLevel() + 1);
		x.setVol(x.getVol() + 1);
		node.setVolth(this.getMaxVolthInLevel(PN, node.getLevel()) + 1);
		z = new ReachabilityTreeNode(node);
		z.setType(ReachabilityTreeNode.sideNode);
		x.setType(ReachabilityTreeNode.insideNode);
		
		for(int i = 0; i < x.mark.mar.length; i++){
			if(x.mark.mar[i] == marking.w)
				z.mark.mar[i] = marking.w;
		}
		for(int j = 0; j < PN.RTNodes.size(); j++){
			if(z.notSmallOfM((ReachabilityTreeNode)PN.RTNodes.elementAt(j)) && 
					(!z.equalOfM((ReachabilityTreeNode)PN.RTNodes.elementAt(j)))){
				for(int k = 0; k < z.mark.mar.length; k++){
					if(z.mark.mar[k] > ((ReachabilityTreeNode)PN.RTNodes.elementAt(j)).mark.mar[k])
						z.mark.mar[k] = marking.w;
				}
				break;
			}
		}
		}	
	}
/*	
// creatTree from a node x	
	public Vector creatTree(ReachabilityTreeNode x, pn PN){
		int t = 0;
		ReachabilityTreeNode z = new ReachabilityTreeNode();
		Vector v = new Vector();         //transitions enable from node x
		Vector n = new Vector();      //nodes in reverse order
		n.add(x);
		if(x.type == ReachabilityTreeNode.sideNode)
			x.setType(ReachabilityTreeNode.terminateNode);
		for(int j = 0; j < PN.numberOfTransitions(); j++){
			if(x.mark.enable(PN, PN.getTransition(j))){
				x.setType(ReachabilityTreeNode.insideNode);
				return n;
			}
		}
		for(int i = 0; i < PN.RTNodes.size(); i++){
			if(((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).equalOfM(x) && 
					((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).type == ReachabilityTreeNode.insideNode){
				x.setType(ReachabilityTreeNode.duplicateNode);
				return n;
			}
		}
		
		v = this.TransCanFireFromX(x, PN);
		while(t <= v.size()){
			if(x.mark.enable(PN, (transition)v.elementAt(t))){
				x.setType(ReachabilityTreeNode.insideNode);
				this.produceNode(z, x, (transition)v.elementAt(t), PN);
				n.add(z);
				this.creatTree(z, PN);
			}
			t++;
		}
//		n.add(x);              //nodes in n is begin from tree's end to root
		return n;
	}
*/	
//	 creatTree from a node x	
	public Vector creatTree(ReachabilityTreeNode x, pn PN){

		ReachabilityTreeNode z = new ReachabilityTreeNode();
		Vector t = new Vector();         //transitions enable from node x
		Vector n = new Vector();        //node in one level
		Vector e = new Vector();      //nodes in tree
		int level = 0;       //level endNodes in
		boolean can = false;
		
		e.add(x);
		if(this.enable(x, PN))
			can = true;
		while(can){
			level = this.getMAxLevel(PN);
			n = this.NodesCanFireInLevel(PN, level);
			for(int i = 0; i < n.size(); i++){
				t = this.TransCanFireFromX((ReachabilityTreeNode)n.elementAt(i), PN);
				for(int j = 0; j < t.size(); j++){
					((ReachabilityTreeNode)n.elementAt(i)).produceNode(z, (ReachabilityTreeNode)n.elementAt(i), (transition)t.elementAt(j), PN);
					e.add(z);
				}
		    }
			level +=1;
			can = false;
// whether has enable node in new level		
			for(int k = 0; k < PN.RTNodes.size(); k++){
				if(((ReachabilityTreeNode)PN.RTNodes.elementAt(k)).getLevel() == level && 
						((ReachabilityTreeNode)PN.RTNodes.elementAt(k)).enable((ReachabilityTreeNode)PN.RTNodes.elementAt(k), PN)){
					can = true;
					break;
				}
			}
		}
		
		return e;
	}
	
	
	public String toString(ReachabilityTreeNode node){
		int t = 0;
		String str = "( ";
		for(int i = 0; i < node.mark.mar.length; i++){
			t = node.mark.mar[i];
			if(t == marking.w)
				str += "w ";
			else
				str += Integer.toString(t) + " ";
		}
		str +=")";
		if(node.getType() == ReachabilityTreeNode.duplicateNode)
			str += " D";
		if(node.getType() == ReachabilityTreeNode.terminateNode)
			str += " T";
		return str;
	}
	
	public void setTypeInPN(ReachabilityTreeNode node, pn PN){
		if(node.type == ReachabilityTreeNode.sideNode)
			node.setType(ReachabilityTreeNode.terminateNode);
		for(int j = 0; j < PN.numberOfTransitions(); j++){
			if(node.mark.enable(PN, PN.getTransition(j))){
				node.setType(ReachabilityTreeNode.insideNode);
			}
		}
		for(int i = 0; i < PN.RTNodes.size(); i++){
			if(((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).equalOfM(node) && 
					((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).type == ReachabilityTreeNode.insideNode){
				node.setType(ReachabilityTreeNode.duplicateNode);
			}
		}
	}
	
	public boolean enable(ReachabilityTreeNode node, pn PN, transition t){
		if(node.mark.enable(PN, t) && node.getType() != ReachabilityTreeNode.duplicateNode &&
				node.getType() != ReachabilityTreeNode.terminateNode)
			return true;
		else 
			return false;
	}
	public boolean enable(ReachabilityTreeNode node, pn PN){
		boolean boo = false;
		for(int i = 0; i < PN.numberOfTransitions(); i++){
			if(node.enable(node, PN, PN.getTransition(i))){
				boo = true;
				break;
			}
		}
		return boo;
		
	}
	
	public Vector TransCanFireFromX(ReachabilityTreeNode x, pn PN){
		Vector v = new Vector();
		for(int i = 0; i < PN.numberOfTransitions(); i++){
			if(x.mark.enable(PN, PN.getTransition(i)))
				v.add(PN.getTransition(i));
		}
		return v;
	}
	
	public Vector NodesCanFireInLevel(pn PN, int lev){
		Vector v = new Vector();
		for(int i = 0; i < PN.RTNodes.size(); i++){
			if(((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).getLevel() == lev){
				((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).setTypeInPN((ReachabilityTreeNode)PN.RTNodes.elementAt(i), PN);
				if(((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).enable((ReachabilityTreeNode)PN.RTNodes.elementAt(i), PN)){
					v.add((ReachabilityTreeNode)PN.RTNodes.elementAt(i));
				}
			}
		}
		return v;
	}
	
	public boolean equalOfM(ReachabilityTreeNode node){
		boolean equal = true;
		if(this.mark.mar.length == 0 || node.mark.mar.length == 0 || this.mark.mar.length != node.mark.mar.length)
			equal = false;
		for(int i = 0; i < node.mark.mar.length; i++){
			if(this.mark.mar[i] != node.mark.mar[i])
				equal = false;
		}
		return equal;
	}
	
	public boolean notSmallOfM(ReachabilityTreeNode node){
		boolean nosmall = true;
		if(this.mark.mar.length == 0 || node.mark.mar.length == 0 || this.mark.mar.length != node.mark.mar.length)
			nosmall = false;
		for(int i = 0; i < node.mark.mar.length; i++){
			if(this.mark.mar[i] < node.mark.mar[i])
				nosmall = false;
		}
		return nosmall;		
	}
	
	public int getMaxVolthInLevel(pn PN, int lev){
		int max = 0;
		for(int i = 0; i < PN.RTNodes.size(); i++){
			if(((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).getLevel() == lev &&
					((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).getVolth() > max)
				max = ((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).getVolth();
		}
		return max;
	}
	
	public int getMAxLevel(pn PN){
		int max = 0;
		for(int i = 0; i < PN.RTNodes.size(); i++)
			if(((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).getLevel() > max)
				max = ((ReachabilityTreeNode)PN.RTNodes.elementAt(i)).getLevel();
		return max;
	}

}