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);