From 14f804d8f3feb5f949dff4de9a77c344b3d00058 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 30 Jun 2009 11:19:39 +0000
Subject: [PATCH] Bug fix in D/CTMC LTL model checking.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1132 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/LTLModelChecker.java | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index f14e9d29..6181b7c6 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -497,7 +497,7 @@ public class LTLModelChecker
 		SCCComputer sccComputer ;
 		JDDNode acceptingStates, allAcceptingStates;
 		Vector<JDDNode> vectBSCCs, newVectBSCCs;
-		JDDNode tmp;
+		JDDNode tmp, tmp2;
 		int i, j, n;
 		
 		// Compute BSCCs for model
@@ -531,15 +531,22 @@ public class LTLModelChecker
 				}
 			}
 			
-			// Restrict each BSCC to H_i states
+			// Check each BSCC for inclusion in H_i states
+			// i.e. restrict each BSCC to H_i states and test if unchanged
 			n = vectBSCCs.size();
 			newVectBSCCs = new Vector<JDDNode>();
 			for (j = 0; j < n; j++) {
 				tmp = vectBSCCs.get(j);
 				JDD.Ref(tmp);
+				JDD.Ref(tmp);
 				JDD.Ref(acceptanceVector_H);
-				tmp = JDD.And(tmp, acceptanceVector_H);
-				newVectBSCCs.add(tmp);
+				tmp2 = JDD.And(tmp, acceptanceVector_H);
+				if (tmp.equals(tmp2)) {
+					newVectBSCCs.add(tmp);
+				} else {
+					JDD.Deref(tmp);
+				}
+				JDD.Deref(tmp2);
 			}
 			JDD.Deref(acceptanceVector_H);