From 87e0da357d0f817c34a931850ff1eec3e48c8679 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 22 Dec 2016 13:13:53 +0000 Subject: [PATCH] prism.NondetModel: cody tidy in doReachability, set the result of reachability computation via setReach() git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11937 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModel.java | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index 35923a2a..2b2e03f6 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -207,17 +207,11 @@ public class NondetModel extends ProbModel tmp = JDD.MaxAbstract(trans01, allDDNondetVars); // compute reachable states - reach = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); + JDDNode reachable = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, start); JDD.Deref(tmp); - // work out number of reachable states - numStates = JDD.GetNumMinterms(reach, allDDRowVars.n()); - - // build odd, clear old one - if (odd != null) { - ODDUtils.ClearODD(odd); - } - odd = ODDUtils.BuildODD(reach, allDDRowVars); + // set the reachable states, compute numStates, create the ODD, etc + setReach(reachable); } // remove non-reachable states from various dds