From f52076ee848b306ca752ed308d31b9b3a3b3cfc3 Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Fri, 18 Jan 2019 08:55:28 +0100
Subject: [PATCH] accumulation: enable CTL support

---
 .../explicit/AccumulationTransformation.java    | 16 ++++++++++++----
 prism/src/explicit/NonProbModelChecker.java     | 17 +++++++++++++++++
 2 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java
index 3d7433f8..4c13840c 100644
--- a/prism/src/explicit/AccumulationTransformation.java
+++ b/prism/src/explicit/AccumulationTransformation.java
@@ -34,7 +34,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 	public AccumulationTransformation(
 			StateModelChecker mc,
 			M originalModel, Expression expr,
-			BitSet statesOfInterest) throws PrismException{
+			BitSet statesOfInterest, boolean forceComplex) throws PrismException{
 		super();
 		this.originalExpression = expr;
 		this.originalModel = originalModel;
@@ -45,7 +45,15 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		this.runLabels  = new ArrayList<>();
 		this.goalLabels = new ArrayList<>();
 		
-		doTransformation();
+		doTransformation(forceComplex);
+	}
+	
+
+	public AccumulationTransformation(
+			StateModelChecker mc,
+			M originalModel, Expression expr,
+			BitSet statesOfInterest) throws PrismException{
+		this(mc, originalModel, expr, statesOfInterest, false);
 	}
 	
 	@Override
@@ -76,7 +84,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		return product.projectToOriginalModel(svTransformedModel);
 	}
 	
-	protected void doTransformation() throws PrismException {
+	protected void doTransformation(boolean forceComplexFlag) throws PrismException {
 		StopWatch clock = new StopWatch(mc.getLog());
 
 		mc.getLog().println("Handling maximal state formulas...");
@@ -119,7 +127,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		// Figure out if we need a complex or a simple trafo...
 		boolean isSimple     = !accexp.hasFireOn() && accexp.isNullary();
 		boolean isPast       = accexp.getSymbol().isMinus();
-		boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX);
+		boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || forceComplexFlag;
 		boolean forceMulti   = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI);
 		
 		if(forceComplex && isPast) {
diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java
index 7ee9d96d..f75b9fee 100644
--- a/prism/src/explicit/NonProbModelChecker.java
+++ b/prism/src/explicit/NonProbModelChecker.java
@@ -40,6 +40,7 @@ import parser.ast.ExpressionExists;
 import parser.ast.ExpressionForAll;
 import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
+import prism.ModelType;
 import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
@@ -463,6 +464,10 @@ public class NonProbModelChecker extends StateModelChecker
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
 		}
+		
+		if (Expression.containsAccumulationExpression(expr)) {
+			return this.checkAccumulationExpression(model, expr, statesOfInterest);
+		}
 
 		LTLModelChecker ltlMC = new LTLModelChecker(this);
 		Vector<BitSet> labelBS = new Vector<BitSet>();
@@ -538,5 +543,17 @@ public class NonProbModelChecker extends StateModelChecker
 		return result;
 	}
 
+	protected StateValues checkAccumulationExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
+	{
+		// Do a transformation and a projection
+		AccumulationTransformation<?> accTrans = new AccumulationTransformation<ModelExplicit>(this, (ModelExplicit)model, expr, statesOfInterest, true);
+		StateValues transValues = this.checkExistsLTL(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), accTrans.getTransformedStatesOfInterest());
+		//this.getLog().println("TransValues");
+		//transValues.print(this.getLog());
+		StateValues projectedValues = accTrans.projectToOriginalModel(transValues);
+		//this.getLog().println("ProjectedValues");
+		//projectedValues.print(this.getLog());
+		return projectedValues;
+	}
 }