From fd6aa0814dca55d0d94ad58a30150450c557ed36 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 8 Jun 2016 16:51:08 +0000
Subject: [PATCH] NondetModelChecker.checkRewardCoSafeLTL: We have to intersect
 the goal states (AcceptanceReach) with model.getReach()

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11398 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NondetModelChecker.java | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 4b13f856..12673c28 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -1474,6 +1474,8 @@ public class NondetModelChecker extends NonProbModelChecker
 			// For a DFA, just collect the accept states
 			mainLog.println("\nSkipping end component detection since DRA is a DFA...");
 			acc = ((AcceptanceReachDD) acceptance).getGoalStates();
+			JDD.Ref(modelProduct.getReach());
+			acc = JDD.And(acc, modelProduct.getReach());
 		} else {
 			// Usually, we have to detect end components in the product
 			mainLog.println("\nFinding accepting end components...");