From bc29c96cbc9693b503d5fd330dee7652591fb1d1 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 7 Jul 2015 22:17:26 +0000
Subject: [PATCH] Cache the embedded DTMC inside CTMCSimple. This preserves the
 cached PredecessorRelation in the DTMC, allowing subsequent properties to be
 checked more efficiently. [from Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10225 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/CTMC.java             | 13 ++++++++++
 prism/src/explicit/CTMCModelChecker.java | 12 +++++-----
 prism/src/explicit/CTMCSimple.java       | 30 ++++++++++++++++++++++--
 3 files changed, 47 insertions(+), 8 deletions(-)

diff --git a/prism/src/explicit/CTMC.java b/prism/src/explicit/CTMC.java
index b425b312..38b769a1 100644
--- a/prism/src/explicit/CTMC.java
+++ b/prism/src/explicit/CTMC.java
@@ -68,6 +68,19 @@ public interface CTMC extends DTMC
 	 */
 	public DTMC buildImplicitEmbeddedDTMC();
 
+	/**
+	 * Get the embedded DTMC for this CTMC, in implicit form
+	 * (i.e. where the details are computed on the fly from this one).
+	 * <p>
+	 * If there is no cached embedded DTMC, build it and cache it.
+	 * Otherwise, return the cached one.
+	 * <p>
+	 * If the underlying CTMC has changed, build a fresh one using
+	 * buildImplicitEmbeddedDTMC, which will update the cached embedded
+	 * DTMC.
+	 */
+	public DTMC getImplicitEmbeddedDTMC();
+
 	/**
 	 * Build (a new) embedded DTMC for this CTMC.
 	 */
diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java
index 99e5562c..4d1201fc 100644
--- a/prism/src/explicit/CTMCModelChecker.java
+++ b/prism/src/explicit/CTMCModelChecker.java
@@ -57,7 +57,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
 		mainLog.println("Building embedded DTMC...");
-		DTMC dtmcEmb = ((CTMC)model).buildImplicitEmbeddedDTMC();
+		DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC();
 		
 		// use superclass (DTMCModelChecker) method on the embedded DTMC
 		return super.checkProbPathFormulaLTL(dtmcEmb, expr, qual, minMax, statesOfInterest);
@@ -226,7 +226,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 	public ModelCheckerResult computeNextProbs(CTMC ctmc, BitSet target) throws PrismException
 	{
 		mainLog.println("Building embedded DTMC...");
-		DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC();
+		DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC();
 		return super.computeNextProbs(dtmcEmb, target);
 	}
 
@@ -239,7 +239,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 	public ModelCheckerResult computeReachProbs(CTMC ctmc, BitSet target) throws PrismException
 	{
 		mainLog.println("Building embedded DTMC...");
-		DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC();
+		DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC();
 		return super.computeReachProbs(dtmcEmb, target);
 	}
 
@@ -254,7 +254,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 	public ModelCheckerResult computeUntilProbs(CTMC ctmc, BitSet remain, BitSet target) throws PrismException
 	{
 		mainLog.println("Building embedded DTMC...");
-		DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC();
+		DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC();
 		return super.computeUntilProbs(dtmcEmb, remain, target);
 	}
 
@@ -272,7 +272,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 	public ModelCheckerResult computeReachProbs(CTMC ctmc, BitSet remain, BitSet target, double init[], BitSet known) throws PrismException
 	{
 		mainLog.println("Building embedded DTMC...");
-		DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC();
+		DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC();
 		return super.computeReachProbs(dtmcEmb, remain, target, init, known);
 	}
 
@@ -662,7 +662,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 		int i, n;
 		// Build embedded DTMC
 		mainLog.println("Building embedded DTMC...");
-		DTMC dtmcEmb = ctmc.buildImplicitEmbeddedDTMC();
+		DTMC dtmcEmb = ctmc.getImplicitEmbeddedDTMC();
 		// Convert rewards
 		n = ctmc.getNumStates();
 		StateRewardsArray rewEmb = new StateRewardsArray(n);
diff --git a/prism/src/explicit/CTMCSimple.java b/prism/src/explicit/CTMCSimple.java
index 9731d2ef..fd9a31dc 100644
--- a/prism/src/explicit/CTMCSimple.java
+++ b/prism/src/explicit/CTMCSimple.java
@@ -36,8 +36,19 @@ import prism.ModelType;
  */
 public class CTMCSimple extends DTMCSimple implements CTMC
 {
+	/**
+	 * The cached embedded DTMC.
+	 * <p>
+	 * Will become invalid if the CTMC is changed. In this case
+	 * construct a new one by calling buildImplicitEmbeddedDTMC()
+	 * <p>
+	 * We cache this so that the PredecessorRelation of the
+	 * embedded DTMC is cached.
+	 */
+	private DTMCEmbeddedSimple cachedEmbeddedDTMC = null;
+
 	// Constructors
-	
+
 	/**
 	 * Constructor: empty CTMC.
 	 */
@@ -130,9 +141,24 @@ public class CTMCSimple extends DTMCSimple implements CTMC
 	@Override
 	public DTMC buildImplicitEmbeddedDTMC()
 	{
-		return new DTMCEmbeddedSimple(this);
+		DTMCEmbeddedSimple dtmc = new DTMCEmbeddedSimple(this);
+		if (cachedEmbeddedDTMC != null) {
+			// replace cached DTMC
+			cachedEmbeddedDTMC = dtmc;
+		}
+		return dtmc;
 	}
 	
+	@Override
+	public DTMC getImplicitEmbeddedDTMC()
+	{
+		if (cachedEmbeddedDTMC == null) {
+			cachedEmbeddedDTMC = new DTMCEmbeddedSimple(this);
+		}
+		return cachedEmbeddedDTMC;
+	}
+
+	
 	@Override
 	public DTMCSimple buildEmbeddedDTMC()
 	{