clean up, stopwatches

prism/src/explicit/AccumulationProductComplex.java

@@ -68,20 +68,18 @@ public abstract class AccumulationProductComplex<M extends Model,Component> exte
 		for(int trackIdx=0; trackIdx<tracker.getTracks().size(); trackIdx++) {
 			AccumulationTrack<Component> track = tracker.getTracks().get(trackIdx);
 			
-			// Is this an initial
-			if (trackIdx==accState.lastRestartNr) {
-				initStates.get(trackIdx).set(index);
-			}
+			boolean isInitial = trackIdx==accState.lastRestartNr;
+			boolean isRunning = track != null;
+			boolean isGoal    = isGoalTrack(track,accexp,mc);
 			
-			// Is this a running track?
-			if (track != null) {
-				runStates.get(trackIdx).set(index);
-			}
+			// Is this an initial
+			initStates.get(trackIdx).set(index, isInitial);
 			
+			// Is this a running track? (Initial tracks are NOT running)
+			runStates.get(trackIdx).set(index, isRunning && !isInitial);
+						
 			// Is this a goal track?
-			if (isGoalTrack(track, accexp, mc)) {
-				goalStates.get(trackIdx).set(index);
-			}
+			goalStates.get(trackIdx).set(index, isGoal);
 		}
 	}
 	

prism/src/explicit/AccumulationProductComplexCounting.java

@@ -207,7 +207,7 @@ public class AccumulationProductComplexCounting<M extends Model> extends Accumul
 	 * @throws PrismException
 	 */
 	protected void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector<? extends Rewards> rewards, final ProbModelChecker mc) throws PrismException {
-		numberOfTracks  = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+2;
+		numberOfTracks  = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+1;
 		numberOfWeights = rewards.size();
 		
 		for(int i=0; i<numberOfTracks; i++) {

prism/src/explicit/AccumulationProductComplexRegular.java

@@ -240,7 +240,7 @@ public class AccumulationProductComplexRegular<M extends Model> extends Accumula
 			throw new PrismException("Cannot handle cyclic automata!");
 		}
 		
-		numberOfTracks = automaton.getLongestPathLength()+1;
+		numberOfTracks = automaton.getLongestPathLength();
 		numberOfWeights= rewards.size();
 		
 		for(int i=0; i<numberOfTracks; i++) {

prism/src/explicit/AccumulationTransformation.java

@@ -4,6 +4,7 @@ import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.Vector;
 
+import common.StopWatch;
 import explicit.rewards.ConstructRewards;
 import explicit.rewards.Rewards;
 import parser.ast.Expression;
@@ -16,7 +17,7 @@ import parser.visitor.ReplaceAccumulationBox;
 import prism.PrismException;
 import prism.PrismSettings;
 
-public class AccumulationTransformation<M extends Model> implements ModelExpressionTransformation<M, M> {
+public class AccumulationTransformation<M extends ModelExplicit> implements ModelExpressionTransformation<M, M> {
 	final protected Expression originalExpression;
 	final protected M originalModel;
 	final protected BitSet statesOfInterest;
@@ -66,10 +67,16 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 	}
 	
 	protected void doTransformation() throws PrismException {
+		mc.getLog().println("Handling maximal state formulas...");
+		transformedExpression = mc.handleMaximalStateFormulas(originalModel, originalExpression);
+		
 		mc.getLog().println("Performing accumulation transformation...");
-		// We work on a copy
-		transformedExpression = originalExpression.deepCopy();
+		
+		// Is this whole thing an ExpressionAccumulation?
+		//if(transformedExpression.isAccumulationExpression()) { System.out.println("HEYOOOO!!! " + transformedExpression); }
 
+		// TODO: WHILE getFirstAccumulationExpression
+		
 		// Get the first ExpressionAccumulation
 		ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression();
 	    mc.getLog().println(" [AT] for " + accexp);
@@ -116,7 +123,11 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 
 	@SuppressWarnings("unchecked")
 	protected void doTransformationComplex(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
+		StopWatch clock = new StopWatch(mc.getLog());
+		
 		// Build the product
+		clock.start("accumulation product construction");
+		
 		if(accexp.hasRegularExpression()) {
 			product = (AccumulationProductComplexRegular<M>) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
 		} else if (accexp.hasBoundExpression()) {
@@ -125,6 +136,8 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 			throw new PrismException("Accumulation Expression has no valid monitor!");
 		}
 		
+		clock.stop(product.getTransformedModel().getNumStates() + " states");
+		
 		mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates());
 		
 		// Transform the model
@@ -147,11 +160,16 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 			goalLabels.add(goalLabel);
 		}
 		// Transform the expression
+		clock.start("transforming expresssion");
+		
 		mc.getLog().println(" [AT] replacing the formula...");
 		ReplaceAccumulationExpressionComplex replace = new ReplaceAccumulationExpressionComplex(accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1);
 		transformedExpression = (Expression)transformedExpression.accept(replace);
 		mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" +
 							"   -> " + transformedExpression.toString());
+		
+		clock.stop();
+		
 		if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) {
 		product.exportToDotFile("DEBUG-product.dot");
 		}
@@ -159,7 +177,11 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 	
 	@SuppressWarnings("unchecked")
 	protected void doTransformationSimple(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
+		StopWatch clock = new StopWatch(mc.getLog());
+
 		// Build the product
+		clock.start("accumulation product construction");
+
 		if(accexp.hasRegularExpression()) {
 			//throw new PrismException("I don't know how to do regular things...");
 			product = (AccumulationProductSimpleRegular<M>) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
@@ -169,6 +191,8 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 			throw new PrismException("Accumulation Expression has no valid monitor!");
 		}
 		
+		clock.stop(product.getTransformedModel().getNumStates() + " states");
+		
 		mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates());
 		
 		// Transform the model
@@ -176,12 +200,18 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		
 		BitSet goodStates = ((AccumulationProductSimple<M,?>)product).getGoodStates();
 		String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels());
+		
 		// Transform the expression
+		clock.start("transforming expresssion");
+		
 		mc.getLog().println(" [AT] replacing the formula...");
 		ReplaceAccumulationExpressionSimple replace = new ReplaceAccumulationExpressionSimple(accexp, goodLabel, product.getNumberOfTracks()-2);
 		transformedExpression = (Expression)transformedExpression.accept(replace);
 		mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" +
 							"   -> " + transformedExpression.toString());
+		
+		clock.stop();
+		
 		if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) {
 		product.exportToDotFile("DEBUG-product.dot");
 		}

prism/src/explicit/DTMCModelChecker.java

@@ -83,7 +83,7 @@ public class DTMCModelChecker extends ProbModelChecker
 	protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
 	{
 		// Do a transformation and a projection
-		AccumulationTransformation<DTMC> accTrans = new AccumulationTransformation<DTMC>(this, (DTMC)model, expr, statesOfInterest);
+		AccumulationTransformation<DTMCExplicit> accTrans = new AccumulationTransformation<DTMCExplicit>(this, (DTMCExplicit)model, expr, statesOfInterest);
 		StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), MinMax.blank(), accTrans.getTransformedStatesOfInterest());
 		//this.getLog().println("TransValues");
 		//transValues.print(this.getLog());

prism/src/explicit/MDPModelChecker.java

@@ -93,7 +93,7 @@ public class MDPModelChecker extends ProbModelChecker
 	protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
 		// Do a transformation and a projection
-		AccumulationTransformation<MDP> accTrans = new AccumulationTransformation<MDP>(this, (MDP)model, expr, statesOfInterest);
+		AccumulationTransformation<MDPExplicit> accTrans = new AccumulationTransformation<MDPExplicit>(this, (MDPExplicit)model, expr, statesOfInterest);
 		StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), minMax, accTrans.getTransformedStatesOfInterest());
 		StateValues projectedValues = accTrans.projectToOriginalModel(transValues);
 		return projectedValues;

prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java

@@ -40,19 +40,22 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 			Expression goal = new ExpressionLabel(goalLabels.get(i));
 			
 			// if this is until:
-			// append first  operand to run
+			// append first  operand to init and run
 			// append second operand to goal
 			if(accexp.getOperand1() != null) {
-				run  = new ExpressionBinaryOp(ExpressionBinaryOp.AND, run, accexp.getOperand1());
+				run  = new ExpressionBinaryOp(ExpressionBinaryOp.AND, run,  accexp.getOperand1());
+				init = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, accexp.getOperand1());
 			}
 			if(accexp.getOperand2() != null) {
 				goal = new ExpressionBinaryOp(ExpressionBinaryOp.AND, goal, accexp.getOperand2());
 			}
 			
 			// until: (run_i UNTIL goal_i)
-			ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, run, goal);
+			ExpressionTemporal until  = new ExpressionTemporal(ExpressionTemporal.P_U, run, goal);
+			// xuntil:(X until)
+			ExpressionTemporal xuntil = new ExpressionTemporal(ExpressionTemporal.P_X, null, Expression.Parenth(until));
 			// and:   (init_i AND until)
-			ExpressionBinaryOp  and  = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, Expression.Parenth(until));
+			ExpressionBinaryOp and    = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, xuntil);
 			
 			clauses.add(and);
 			if(i==0) {