symbolic MDP model checker: Use LTL2WDBA construction to obtain DFA for co-safe LTL reward computations

The DFA needed for co-safe LTL reward computation need to have a
specific structure, i.e., all states that satisfy Sigma^omega have
to be already goal states.

The previous approach did not necessarily ensure this.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12067 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/NondetModelChecker.java

@@ -60,15 +60,18 @@ import parser.type.TypeBool;
 import parser.type.TypeDouble;
 import parser.type.TypePathBool;
 import parser.type.TypePathDouble;
+import prism.LTLModelChecker.LTLProduct;
 import sparse.PrismSparse;
 import strat.MDStrategyIV;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceOmegaDD;
 import acceptance.AcceptanceRabin;
+import acceptance.AcceptanceReach;
 import acceptance.AcceptanceReachDD;
 import acceptance.AcceptanceType;
 import automata.DA;
 import automata.LTL2DA;
+import automata.LTL2WDBA;
 import dv.DoubleVector;
 import dv.IntegerVector;
 import explicit.MinMax;
@@ -1455,18 +1458,15 @@ public class NondetModelChecker extends NonProbModelChecker
 	{
 		LTLModelChecker mcLtl;
 		StateValues rewardsProduct = null, rewards = null;
-		Expression ltl;
-		Vector<JDDNode> labelDDs;
-		DA<BitSet, ? extends AcceptanceOmega> da;
-		NondetModel modelProduct;
+		Vector<JDDNode> labelDDs = new Vector<JDDNode>();
+		DA<BitSet, AcceptanceReach> da;
+		LTLProduct<NondetModel> modelProduct;
 		NondetModelChecker mcProduct;
-		JDDNode startMask;
-		JDDVars daDDRowVars, daDDColVars;
-		int i;
 		long l;
 
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
+				JDD.Deref(statesOfInterest);
 				throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
 
@@ -1480,34 +1480,24 @@ public class NondetModelChecker extends NonProbModelChecker
 				// formulas only appear positively
 				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
 			} else {
+				JDD.Deref(statesOfInterest);
 				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}
 
 		// Can't do "dfa" properties yet
 		if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) {
+			JDD.Deref(statesOfInterest);
 			throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
 		}
 
 		// For LTL model checking routines
 		mcLtl = new LTLModelChecker(prism);
 
-		// Model check maximal state formulas
-		labelDDs = new Vector<JDDNode>();
-		ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs);
+		// Model check maximal state formulas and construct DFA, with the special
+		// handling needed for cosafety reward translation
+		da = mcLtl.constructDFAForCosafetyRewardLTL(this, model, expr, labelDDs);
 
-		// Convert LTL formula to deterministic automaton (DA)
-		mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
-		l = System.currentTimeMillis();
-		LTL2DA ltl2da = new LTL2DA(prism);
-		AcceptanceType[] allowedAcceptance = {
-				AcceptanceType.RABIN,
-				AcceptanceType.REACH
-		};
-		da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
-		mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics()+".");
-		l = System.currentTimeMillis() - l;
-		mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds.");
 		// If required, export DA
 		if (prism.getSettings().getExportPropAut()) {
 			mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"...");
@@ -1518,20 +1508,12 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 
 		// Build product of MDP and automaton
-		mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
-		daDDRowVars = new JDDVars();
-		daDDColVars = new JDDVars();
-		l = System.currentTimeMillis();
-		modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest);
-		l = System.currentTimeMillis() - l;
-		mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
-		mainLog.println();
-		modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
+		modelProduct = mcLtl.constructProductMDP(model, da, labelDDs, statesOfInterest);
 		// Output product, if required
 		if (prism.getExportProductTrans()) {
 			try {
 				mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"...");
-				modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename()));
+				modelProduct.getProductModel().exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename()));
 			} catch (FileNotFoundException e) {
 				mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"");
 			}
@@ -1539,58 +1521,37 @@ public class NondetModelChecker extends NonProbModelChecker
 		if (prism.getExportProductStates()) {
 			mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"...");
 			PrismFileLog out = new PrismFileLog(prism.getExportProductStatesFilename());
-			modelProduct.exportStates(Prism.EXPORT_PLAIN, out);
+			modelProduct.getProductModel().exportStates(Prism.EXPORT_PLAIN, out);
 			out.close();
 		}
 
 		// Adapt reward info to product model
-		JDD.Ref(stateRewards);
-		JDD.Ref(modelProduct.getReach());
-		JDDNode stateRewardsProduct = JDD.Apply(JDD.TIMES, stateRewards, modelProduct.getReach());
-		JDD.Ref(transRewards);
-		JDD.Ref(modelProduct.getTrans01());
-		JDDNode transRewardsProduct = JDD.Apply(JDD.TIMES, transRewards, modelProduct.getTrans01());
+		JDDNode stateRewardsProduct = JDD.Apply(JDD.TIMES, stateRewards.copy(), modelProduct.getProductModel().getReach().copy());
+		JDDNode transRewardsProduct = JDD.Apply(JDD.TIMES, transRewards.copy(), modelProduct.getProductModel().getTrans01().copy());
 		
 		// Find accepting states + compute reachability rewards
-		AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars);
-		JDDNode acc = null;
-		if (acceptance instanceof AcceptanceReachDD) {
-			// For a DFA, just collect the accept states
-			mainLog.println("\nSkipping end component detection since DRA is a DFA...");
-			acc = ((AcceptanceReachDD) acceptance).getGoalStates();
-			JDD.Ref(modelProduct.getReach());
-			acc = JDD.And(acc, modelProduct.getReach());
-		} else {
-			// Usually, we have to detect end components in the product
-			mainLog.println("\nFinding accepting end components...");
-			acc = mcLtl.findAcceptingECStates(acceptance, modelProduct, daDDRowVars, daDDColVars, fairness);
-		}
-		acceptance.clear();
+		AcceptanceReachDD acceptance = (AcceptanceReachDD) modelProduct.getProductAcceptance();
+		// acc is already restricted to the product model's reachable states
+		JDDNode acc = acceptance.getGoalStates();
+
 		mainLog.println("\nComputing reachability rewards...");
-		mcProduct = new NondetModelChecker(prism, modelProduct, null);
-		rewardsProduct = mcProduct.computeReachRewards(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getTrans01(), stateRewardsProduct, transRewardsProduct, acc, min);
+		mcProduct = createNewModelChecker(prism, modelProduct.getProductModel(), null);
+		rewardsProduct = mcProduct.computeReachRewards(modelProduct.getProductModel().getTrans(),
+		                                               modelProduct.getProductModel().getTransActions(),
+		                                               modelProduct.getProductModel().getTrans01(),
+		                                               stateRewardsProduct,
+		                                               transRewardsProduct,
+		                                               acc,
+		                                               min);
 
 		// Convert reward vector to original model
-		// First, filter over DRA start states
-		startMask = mcLtl.buildStartMask(da, labelDDs, daDDRowVars);
-		JDD.Ref(model.getReach());
-		startMask = JDD.And(model.getReach(), startMask);
-		rewardsProduct.filter(startMask);
-		// Then sum over DD vars for the DRA state
-		rewards = rewardsProduct.sumOverDDVars(daDDRowVars, model);
+		rewards = modelProduct.projectToOriginalModel(rewardsProduct);
 
 		// Deref, clean up
 		JDD.Deref(stateRewardsProduct);
 		JDD.Deref(transRewardsProduct);
-		rewardsProduct.clear();
 		modelProduct.clear();
-		for (i = 0; i < labelDDs.size(); i++) {
-			JDD.Deref(labelDDs.get(i));
-		}
 		JDD.Deref(acc);
-		JDD.Deref(startMask);
-		daDDRowVars.derefAll();
-		daDDColVars.derefAll();
 
 		return rewards;
 	}