From b7f3871fd70489796646e6fcf122e6876c920aca Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 1 Sep 2015 20:18:33 +0000
Subject: [PATCH] Fix for SCC export on MDPs (and new underlying methods for
 computing/storing transition relation).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10604 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Model.java       |  6 ++++++
 prism/src/prism/NondetModel.java | 28 +++++++++++++++++++++++++++-
 prism/src/prism/ProbModel.java   |  6 ++++++
 prism/src/prism/SCCComputer.java |  2 +-
 4 files changed, 40 insertions(+), 2 deletions(-)

diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java
index d9f1ba90..b54ab0bb 100644
--- a/prism/src/prism/Model.java
+++ b/prism/src/prism/Model.java
@@ -78,6 +78,12 @@ public interface Model
 	JDDNode getStart();
 	JDDNode getReach();
 	
+	/**
+	 * Get a BDD storing the underlying transition relation of the model.
+	 * If it is not stored already, it will be computed.
+	 */
+	JDDNode getTransReln();
+	
 	/**
 	 * Get a BDD storing the set of states that are/were deadlocks.
 	 * (Such states may have been fixed at build-time by adding self-loops)
diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java
index 1fa26bfb..51736cf1 100644
--- a/prism/src/prism/NondetModel.java
+++ b/prism/src/prism/NondetModel.java
@@ -51,9 +51,21 @@ public class NondetModel extends ProbModel
 	protected JDDVars allDDNondetVars; // all nondet dd vars (union of two above)
 	protected JDDNode transInd; // BDD for independent part of trans
 	protected JDDNode transSynch[]; // BDD for parts of trans from each action
+	protected JDDNode transReln; // BDD for the transition relation (no action encoding)
 
 	// accessor methods
 
+	@Override
+	public JDDNode getTransReln()
+	{
+		// First, compute the transition relation if it is not there
+		if (transReln == null) {
+			JDD.Ref(trans01);
+			transReln = JDD.ThereExists(trans01, allDDNondetVars);
+		}
+		return transReln;
+	}
+
 	// type
 	public ModelType getModelType()
 	{
@@ -181,6 +193,7 @@ public class NondetModel extends ProbModel
 
 		transInd = null;
 		transSynch = null;
+		transReln = null;
 	}
 
 	// do reachability
@@ -221,7 +234,12 @@ public class NondetModel extends ProbModel
 				transSynch[i] = JDD.Apply(JDD.TIMES, reach, transSynch[i]);
 			}
 		}
-
+		// also filter transReln DD (if necessary)
+		if (transReln != null) {
+			JDD.Ref(reach);
+			transReln = JDD.Apply(JDD.TIMES, reach, transReln);
+		}
+		
 		// build mask for nondeterminstic choices
 		// (and work out number of choices)
 		JDD.Ref(trans01);
@@ -268,6 +286,12 @@ public class NondetModel extends ProbModel
 				transInd = JDD.Or(transInd, JDD.ThereExists(tmp, allDDColVars));
 			}
 			JDD.Deref(tmp);
+			// recompute transReln (if needed)
+			if (transReln != null) {
+				JDD.Deref(transReln);
+				JDD.Ref(trans01);
+				transReln = JDD.ThereExists(trans01, allDDNondetVars);
+			}
 			// update transition count
 			numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans());
 			// re-build mask for nondeterminstic choices
@@ -425,6 +449,8 @@ public class NondetModel extends ProbModel
 			for (int i = 0; i < numSynchs; i++) {
 				JDD.Deref(transSynch[i]);
 			}
+		if (transReln != null)
+			JDD.Deref(transReln);
 	}
 }
 
diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java
index 842b320f..e9633372 100644
--- a/prism/src/prism/ProbModel.java
+++ b/prism/src/prism/ProbModel.java
@@ -244,6 +244,12 @@ public class ProbModel implements Model
 		return reach;
 	}
 
+	@Override
+	public JDDNode getTransReln()
+	{
+		return trans01;
+	}
+
 	@Override
 	public JDDNode getDeadlocks()
 	{
diff --git a/prism/src/prism/SCCComputer.java b/prism/src/prism/SCCComputer.java
index a8c64309..dce8e03b 100644
--- a/prism/src/prism/SCCComputer.java
+++ b/prism/src/prism/SCCComputer.java
@@ -59,7 +59,7 @@ public abstract class SCCComputer extends PrismComponent
 	 */
 	public static SCCComputer createSCCComputer(PrismComponent parent, Model model) throws PrismException
 	{
-		return createSCCComputer(parent, model.getReach(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars());
+		return createSCCComputer(parent, model.getReach(), model.getTransReln(), model.getAllDDRowVars(), model.getAllDDColVars());
 	}
 
 	/**