Optimize unless code

src/spins/promela/compiler/automaton/Automaton.java

@@ -155,10 +155,17 @@ public class Automaton implements Iterable<State> {
 	    		Transition n = t.duplicateFrom(s);
 	    		n.setUnlessPriority(priority);
 	    	}
+	    	s.nextUnless();
 	    }
     	escape.delete();
 	}
 
+	public void finalize() {
+	    for (State s : this) {
+	    	s.finalize();
+	    }
+	}
+
 	/**
 	 * @return The number of states that are reachable from the current starting state.
 	 */

src/spins/promela/compiler/automaton/State.java

@@ -167,6 +167,8 @@ public class State {
         }
 	}
 
+	boolean end, accept, progress;
+	
 	/**
 	 * Returns true when this state is an ending state. A {@link State} is an ending state when
 	 * either it has one or more {@link EndTransition} or {@link NeverEndTransition} going out of
@@ -174,12 +176,7 @@ public class State {
 	 * @return true when this state is an ending state.
 	 */
 	public boolean isEndingState() {
-		for (Transition trans : out) {
-			if (trans instanceof EndTransition ||
-				null == trans.getTo())
-				return true;
-		}
-		return hasLabelPrefix(LABEL_END);
+		return end;
 	}
 
 	/**
@@ -188,7 +185,7 @@ public class State {
 	 * @return true when this state is and acceptance state.
 	 */
 	public boolean isAcceptState() {
-		return hasLabelPrefix(LABEL_ACCEPT);
+		return accept;
 	}
 
 	/**
@@ -197,9 +194,32 @@ public class State {
 	 * @return true when this state is and progress state.
 	 */
 	public boolean isProgressState() {
+		return progress;
+	}
+
+	private boolean checkEndingState() {
+		for (Transition trans : out) {
+			if (trans instanceof EndTransition ||
+				null == trans.getTo())
+				return true;
+		}
+		return hasLabelPrefix(LABEL_END);
+	}
+
+	private boolean checkAcceptState() {
+		return hasLabelPrefix(LABEL_ACCEPT);
+	}
+	
+	private boolean checkProgressState() {
 		return hasLabelPrefix(LABEL_PROGRESS);
 	}
 
+	public void finalize() {
+		end = checkEndingState();
+		progress = checkProgressState();
+		accept = checkAcceptState();
+	}
+
 	/**
 	 * @param index
 	 *            The index of the output transition.
@@ -383,4 +403,8 @@ public class State {
     public int nextUnless() {
         return unlesses++;
     }
+
+	public int unlesses() {
+		return unlesses;
+	}
 }

src/spins/promela/compiler/ltsmin/LTSminTreeWalker.java

@@ -210,6 +210,10 @@ public class LTSminTreeWalker {
 		instantiate();
 		bindByReferenceCalls();
 
+		for (ProcInstance p : spec) {
+			p.getAutomaton().finalize();
+		}
+		
         LTSminModel model = new LTSminModel(name, spec);
 		createModelTransitions(model);
 		createModelAssertions(model);
@@ -505,10 +509,9 @@ public class LTSminTreeWalker {
 		instance.setEnabler(e);
 		for (Variable var : p.getVariables()) {
 			Variable newvar = instantiate(var, instance);
-			if (newvar.getName().equals(Promela.C_STATE_PROC_COUNTER))
-				newvar.setAssignedTo(); // Process counter is always assigned to
 			instance.addVariable(newvar, p.getArguments().contains(var));
 		}
+		instance.getPC().setAssignedTo();
 		instance.lastArgument();
 		HashMap<State, State> seen = new HashMap<State, State>();
 		instantiate(p.getStartState(), instance.getStartState(), seen, instance);
@@ -986,9 +989,11 @@ public class LTSminTreeWalker {
 			}
 		}}
 
+		if (state.unlesses() > 0) {  
 	        for (LTSminTransition lt : begin.getOut()) {
 	    		createUnlessGuards (lt);
 	        }
+		}
 
 		// update stack table
 		removeSearchStack (begin);
@@ -1077,11 +1082,11 @@ public class LTSminTreeWalker {
     private List<LTSminTransition> createStateTransition(Transition t,
 	                                                     Transition n) {
 		++debug.say_indent;
-		if(n!=null) {
-			debug.say(MessageKind.DEBUG, "Handling trans: " + t.getClass().getName() + " || " + n.getClass().getName());
-		} else {
-			debug.say(MessageKind.DEBUG, "Handling trans: " + t.getClass().getName());
-		}
+//		if(n!=null) {
+//			debug.say(MessageKind.DEBUG, "Handling trans: " + t.getClass().getName() + " || " + n.getClass().getName());
+//		} else {
+//			debug.say(MessageKind.DEBUG, "Handling trans: " + t.getClass().getName());
+//		}
 		--debug.say_indent;
 
         LinkedList<LTSminTransition> list = new LinkedList<LTSminTransition>();