From 9fc29a3b252048794d3362846b1333ab1b01ecc3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 May 2015 18:16:32 +0000 Subject: [PATCH] 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 | 2 ++ prism/src/prism/ProbModelChecker.java | 2 ++ 2 files changed, 4 insertions(+) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index eb17f6bc..f0c9dbb0 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index c36b2684..a8f96834 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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);