Browse Source

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
master
Joachim Klein 9 years ago
parent
commit
87e0da357d
  1. 12
      prism/src/prism/NondetModel.java

12
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

Loading…
Cancel
Save