From e3ce1e85eecb08eccc2caa6280bc188861508bcc Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 31 Jan 2015 01:04:26 +0000
Subject: [PATCH] provide LTLModelChecker.constructProductMC(DTMC dtmc,
 Expression ltl), encapsulating DA generation and product construction.
 [Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9593 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/DTMCModelChecker.java | 37 +----------------
 prism/src/explicit/LTLModelChecker.java  | 52 ++++++++++++++++++++++++
 2 files changed, 53 insertions(+), 36 deletions(-)

diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 6c09e4fe..667c8366 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -30,16 +30,11 @@ import java.io.File;
 import java.util.BitSet;
 import java.util.List;
 import java.util.Map;
-import java.util.Vector;
 
-import acceptance.AcceptanceRabin;
 import parser.ast.Expression;
 import parser.type.TypeDouble;
-import prism.DA;
 import prism.PrismComponent;
 import prism.PrismException;
-import prism.PrismFileLog;
-import prism.PrismLog;
 import prism.PrismUtils;
 import explicit.rewards.MCRewards;
 
@@ -63,44 +58,14 @@ public class DTMCModelChecker extends ProbModelChecker
 	{
 		LTLModelChecker mcLtl;
 		StateValues probsProduct, probs;
-		Expression ltl;
-		DA<BitSet,AcceptanceRabin> dra;
 		LTLModelChecker.LTLProduct<DTMC> product;
 		DTMCModelChecker mcProduct;
-		long time;
-
-		// Can't do LTL with time-bounded variants of the temporal operators
-		if (Expression.containsTemporalTimeBounds(expr)) {
-			throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
-		}
 
 		// For LTL model checking routines
 		mcLtl = new LTLModelChecker(this);
 
-		// Model check maximal state formulas
-		Vector<BitSet> labelBS = new Vector<BitSet>();
-		ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelBS);
-
-		// Convert LTL formula to deterministic Rabin automaton (DRA)
-		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
-		time = System.currentTimeMillis();
-		dra = LTLModelChecker.convertLTLFormulaToDRA(ltl);
-		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
-		time = System.currentTimeMillis() - time;
-		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
-		// If required, export DRA 
-		if (settings.getExportPropAut()) {
-			mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"...");
-			PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
-			out.println(dra);
-			out.close();
-			//dra.printDot(new java.io.PrintStream("dra.dot"));
-		}
-
 		// Build product of Markov chain and automaton
-		mainLog.println("\nConstructing MC-DRA product...");
-		product = mcLtl.constructProductMC(dra, (DTMC) model, labelBS, statesOfInterest);
-		mainLog.print("\n" + product.getProductModel().infoStringTable());
+		product = mcLtl.constructProductMC(this, (DTMC)model, expr, statesOfInterest);
 
 		// Find accepting BSCCs + compute reachability probabilities
 		mainLog.println("\nFinding accepting BSCCs...");
diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java
index bcdb119c..4913c5a8 100644
--- a/prism/src/explicit/LTLModelChecker.java
+++ b/prism/src/explicit/LTLModelChecker.java
@@ -52,6 +52,8 @@ import prism.DA;
 import prism.LTL2RabinLibrary;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismFileLog;
+import prism.PrismLog;
 
 /**
  * LTL model checking functionality
@@ -161,6 +163,56 @@ public class LTLModelChecker extends PrismComponent
 		return expr;
 	}
 
+	/**
+	 * Generate the DRA for the given LTL expression and construct the product.
+	 *
+	 * @param mc a ProbModelChecker, used for checking maximal state formulas
+	 * @param dtmc the model
+	 * @param expr a path expression
+ 	 * @param statesOfInterest the set of states for which values should be calculated (null = all states)
+	 * @return the product with the DRA
+	 */
+	public LTLProduct<DTMC> constructProductMC(ProbModelChecker mc, DTMC dtmc, Expression expr, BitSet statesOfInterest) throws PrismException
+	{
+		Expression ltl;
+		DA<BitSet,AcceptanceRabin> dra;
+		LTLProduct<DTMC> product;
+		long time;
+
+		// Can't do LTL with time-bounded variants of the temporal operators
+		if (Expression.containsTemporalTimeBounds(expr)) {
+			throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+		}
+
+		// Model check maximal state formulas
+		Vector<BitSet> labelBS = new Vector<BitSet>();
+		ltl = checkMaximalStateFormulas(mc, dtmc, expr.deepCopy(), labelBS);
+
+		// Convert LTL formula to deterministic Rabin automaton (DRA)
+		mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")...");
+		time = System.currentTimeMillis();
+		dra = convertLTLFormulaToDRA(ltl);
+		mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + ".");
+		time = System.currentTimeMillis() - time;
+		mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds.");
+		// If required, export DRA
+		if (settings.getExportPropAut()) {
+			mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"...");
+			PrismLog out = new PrismFileLog(settings.getExportPropAutFilename());
+			out.println(dra);
+			out.close();
+			//dra.printDot(new java.io.PrintStream("dra.dot"));
+		}
+
+		// Build product of Markov chain and automaton
+		mainLog.println("\nConstructing MC-DRA product...");
+		product = constructProductMC(dra, dtmc, labelBS, statesOfInterest);
+
+		mainLog.print("\n" + product.getProductModel().infoStringTable());
+
+		return product;
+	}
+
 	/**
 	 * Construct the product of a DRA and a DTMC.
 	 * @param dra The DRA