Bug fix in symbolic model checking of co-safe properties (target was not ANDed with reachable states).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9833 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/NondetModelChecker.java

@@ -1051,6 +1051,8 @@ public class NondetModelChecker extends NonProbModelChecker
 		if (acceptance instanceof AcceptanceReachDD) {
 			mainLog.println("\nSkipping accepting MEC computation since acceptance is defined via goal states...");
 			acc = ((AcceptanceReachDD) acceptance).getGoalStates();
+			JDD.Ref(modelProduct.getReach());
+			acc = JDD.And(acc, modelProduct.getReach());
 		} else {
 			mainLog.println("\nFinding accepting end components...");
 			acc = mcLtl.findAcceptingECStates(acceptance, modelProduct, daDDRowVars, daDDColVars, fairness);

prism/src/prism/ProbModelChecker.java

@@ -586,6 +586,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		if (acceptance instanceof AcceptanceReachDD) {
 			mainLog.println("\nSkipping BSCC computation since acceptance is defined via goal states...");
 			acc = ((AcceptanceReachDD) acceptance).getGoalStates();
+			JDD.Ref(modelProduct.getReach());
+			acc = JDD.And(acc, modelProduct.getReach());
 		} else {
 			mainLog.println("\nFinding accepting BSCCs...");
 			acc = mcLtl.findAcceptingBSCCs(acceptance, modelProduct);