From 9a814f226b153f54e74f893e6e8281bc7bdd1ed2 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Aug 2015 10:09:12 +0000 Subject: [PATCH] symbolic ProbModelChecker: Fix JDDNode reference issues for total reward computation git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10509 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ProbModelChecker.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index e820e94d..aae22239 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -1726,9 +1726,9 @@ public class ProbModelChecker extends NonProbModelChecker // Find states with infinite reward (those reach a non-zero reward BSCC with prob > 0) JDDNode inf = PrismMTBDD.Prob0(tr01, reach, allDDRowVars, allDDColVars, reach, bsccsNonZero); - inf = JDD.And(reach, JDD.Not(inf)); - JDDNode maybe = JDD.And(reach, JDD.Not(inf)); - JDD.Ref(bsccsNonZero); + inf = JDD.And(reach.copy(), JDD.Not(inf)); + JDDNode maybe = JDD.And(reach.copy(), JDD.Not(inf.copy())); + JDD.Deref(bsccsNonZero); // Print out inf/maybe mainLog.print("\ninf = " + JDD.GetNumMintermsString(inf, allDDRowVars.n()));