From d9050380a6f42a518507b0782f496cd3f27c0e5c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 14 Apr 2008 20:36:10 +0000 Subject: [PATCH] Bugfix: Model state lists generated before reach info ready. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@753 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModel.java | 7 ------- prism/src/prism/ProbModel.java | 25 +++---------------------- 2 files changed, 3 insertions(+), 29 deletions(-) diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index 2eef7ed5..68a7660e 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -153,9 +153,6 @@ public class NondetModel extends ProbModel // build odd odd = ODDUtils.BuildODD(reach, allDDRowVars); - - // store reachable states in a StateList - reachStateList = new StateListMTBDD(reach, this); } // remove non-reachable states from various dds @@ -189,9 +186,6 @@ public class NondetModel extends ProbModel // find reachable states with no transitions JDD.Ref(reach); deadlocks = JDD.And(reach, JDD.Not(deadlocks)); - - // store deadlock states in a StateList - deadlockStateList = new StateListMTBDD(deadlocks, this); } // remove deadlocks by adding self-loops @@ -214,7 +208,6 @@ public class NondetModel extends ProbModel JDD.Deref(fixdl); fixdl = deadlocks; deadlocks = JDD.Constant(0); - deadlockStateList = new StateListMTBDD(deadlocks, this); // update mask JDD.Deref(nondetMask); JDD.Ref(trans01); diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 9bfe9cd0..4cda2f83 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -57,12 +57,6 @@ public class ProbModel implements Model protected double numStates; // number of states protected double numTransitions; // number of transitions protected double numStartStates; // number of initial states - // reachable state list - protected StateListMTBDD reachStateList = null; - // deadlock state list - protected StateListMTBDD deadlockStateList = null; - // initial state list - protected StateListMTBDD startStateList = null; // mtbdd stuff @@ -207,17 +201,17 @@ public class ProbModel implements Model // lists of states public StateList getReachableStates() { - return reachStateList; + return new StateListMTBDD(reach, this); } public StateList getDeadlockStates() { - return deadlockStateList; + return new StateListMTBDD(deadlocks, this); } public StateList getStartStates() { - return startStateList; + return new StateListMTBDD(start, this); } // mtbdd stuff @@ -418,9 +412,6 @@ public class ProbModel implements Model // work out number of initial states numStartStates = JDD.GetNumMinterms(start, allDDRowVars.n()); - - // store initial states in a StateList - startStateList = new StateListMTBDD(start, this); } // do reachability @@ -440,9 +431,6 @@ public class ProbModel implements Model // build odd odd = ODDUtils.BuildODD(reach, allDDRowVars); - - // store reachable states in a StateList - reachStateList = new StateListMTBDD(reach, this); } // this method allows you to skip the reachability phase @@ -458,9 +446,6 @@ public class ProbModel implements Model // build odd odd = ODDUtils.BuildODD(reach, allDDRowVars); - - // store reachable states in a StateList - reachStateList = new StateListMTBDD(reach, this); } // remove non-reachable states from various dds @@ -511,9 +496,6 @@ public class ProbModel implements Model // find reachable states with no transitions JDD.Ref(reach); deadlocks = JDD.And(reach, JDD.Not(deadlocks)); - - // store deadlock states in a StateList - deadlockStateList = new StateListMTBDD(deadlocks, this); } // remove deadlocks by adding self-loops @@ -533,7 +515,6 @@ public class ProbModel implements Model JDD.Deref(fixdl); fixdl = deadlocks; deadlocks = JDD.Constant(0); - deadlockStateList = new StateListMTBDD(deadlocks, this); // update model stats numTransitions = JDD.GetNumMinterms(trans01, getNumDDVarsInTrans()); }