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

@@ -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.
 	 */

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);

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()
 	{