From aba185d8359b3147b09dfc8ac1cecd79b08bbf07 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 3 Dec 2014 18:26:31 +0000
Subject: [PATCH] Bugfix - explicit-state model checking for LTL on CTMCs (from
 Joachim Klein).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9356 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/CTMCModelChecker.java   | 10 ++++
 prism/src/explicit/DTMCEmbeddedSimple.java | 59 ++++++++++++++++++++--
 2 files changed, 65 insertions(+), 4 deletions(-)

diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java
index 44007984..abe95922 100644
--- a/prism/src/explicit/CTMCModelChecker.java
+++ b/prism/src/explicit/CTMCModelChecker.java
@@ -53,6 +53,16 @@ public class CTMCModelChecker extends DTMCModelChecker
 	
 	// Model checking functions
 
+	@Override
+	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException
+	{
+		mainLog.println("Building embedded DTMC...");
+		DTMC dtmcEmb = ((CTMC)model).buildImplicitEmbeddedDTMC();
+		
+		// use superclass (DTMCModelChecker) method on the embedded DTMC
+		return super.checkProbPathFormulaLTL(dtmcEmb, expr, qual, minMax);
+	}
+	
 	@Override
 	protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException
 	{
diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java
index 0a9ea3be..0009766c 100644
--- a/prism/src/explicit/DTMCEmbeddedSimple.java
+++ b/prism/src/explicit/DTMCEmbeddedSimple.java
@@ -195,14 +195,65 @@ public class DTMCEmbeddedSimple extends DTMCExplicit
 
 	public int getNumTransitions(int s)
 	{
-		// TODO
-		throw new RuntimeException("Not implemented yet");
+		if (exitRates[s] == 0) {
+			return 1;
+		} else {
+			return ctmc.getNumTransitions(s);
+		}
 	}
 
 	public Iterator<Entry<Integer,Double>> getTransitionsIterator(int s)
 	{
-		// TODO
-		throw new RuntimeException("Not implemented yet");
+		if (exitRates[s] == 0) {
+			// return prob-1 self-loop
+			Map<Integer,Double> m = new TreeMap<Integer,Double>();
+			m.put(s, 1.0);
+			return m.entrySet().iterator();
+		} else {
+			final Iterator<Entry<Integer,Double>> ctmcIterator = ctmc.getTransitionsIterator(s);
+			
+			// return iterator over entries, with probabilities divided by exitRates[s]
+			final double er = exitRates[s];
+			return new Iterator<Entry<Integer,Double>>() {
+				@Override
+				public boolean hasNext()
+				{
+					return ctmcIterator.hasNext();
+				}
+
+				@Override
+				public Entry<Integer, Double> next()
+				{
+					final Entry<Integer, Double> ctmcEntry = ctmcIterator.next();
+					
+					return new Entry<Integer, Double>() {
+						@Override
+						public Integer getKey()
+						{
+							return ctmcEntry.getKey();
+						}
+
+						@Override
+						public Double getValue()
+						{
+							return ctmcEntry.getValue() / er;
+						}
+
+						@Override
+						public Double setValue(Double value)
+						{
+							throw new UnsupportedOperationException();
+						}
+					};
+				}
+
+				@Override
+				public void remove()
+				{
+					throw new UnsupportedOperationException();
+				}
+			};
+		}
 	}
 
 	public void prob0step(BitSet subset, BitSet u, BitSet result)