From 4b22d2ea8002b979a4e0a787b1d5f9ac92128268 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 1 May 2008 21:55:23 +0000 Subject: [PATCH] Small tidy-up of BSCC computer code. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@782 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ProbModelChecker.java | 53 +++++++++++++-------------- prism/src/prism/SCCComputerXB.java | 43 ++++++++-------------- 2 files changed, 41 insertions(+), 55 deletions(-) diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index c1ea739d..5e8482c1 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -313,7 +313,7 @@ public class ProbModelChecker extends StateModelChecker String relOp; // relational operator // bscc stuff - Vector vectBSCCs; + Vector vectBSCCs; JDDNode notInBSCCs; // mtbdd stuff JDDNode b, bscc, sol, tmp; @@ -350,7 +350,6 @@ public class ProbModelChecker extends StateModelChecker // compute bottom strongly connected components (bsccs) if (bsccComp) { - mainLog.print("\nComputing (B)SCCs..."); sccComputer.computeBSCCs(); vectBSCCs = sccComputer.getVectBSCCs(); notInBSCCs = sccComputer.getNotInBSCCs(); @@ -359,7 +358,7 @@ public class ProbModelChecker extends StateModelChecker // unless we've been told to skip it else { mainLog.println("\nSkipping BSCC computation..."); - vectBSCCs = new Vector(); + vectBSCCs = new Vector(); JDD.Ref(reach); vectBSCCs.add(reach); notInBSCCs = JDD.Constant(0); @@ -373,7 +372,7 @@ public class ProbModelChecker extends StateModelChecker mainLog.println("\nComputing steady state probabilities for BSCC " + (i + 1)); // get bscc - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); // compute steady state probabilities try { @@ -381,7 +380,7 @@ public class ProbModelChecker extends StateModelChecker } catch (PrismException e) { JDD.Deref(b); for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); throw e; @@ -413,7 +412,7 @@ public class ProbModelChecker extends StateModelChecker // necessary tmp = JDD.Constant(0); for (i = 0; i < n; i++) { - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); JDD.Ref(bscc); tmp = JDD.Apply(JDD.PLUS, tmp, JDD.Apply(JDD.TIMES, JDD.Constant(probBSCCs[i]), bscc)); } @@ -445,7 +444,7 @@ public class ProbModelChecker extends StateModelChecker mainLog.println("\nComputing probabilities of reaching BSCC " + (i + 1)); // get bscc - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); // compute probabilities try { @@ -453,7 +452,7 @@ public class ProbModelChecker extends StateModelChecker } catch (PrismException e) { JDD.Deref(b); for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); totalProbs.clear(); @@ -484,7 +483,7 @@ public class ProbModelChecker extends StateModelChecker // derefs JDD.Deref(b); for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); @@ -778,7 +777,7 @@ public class ProbModelChecker extends StateModelChecker throws PrismException { // bscc stuff - Vector vectBSCCs; + Vector vectBSCCs; JDDNode notInBSCCs; // mtbdd stuff JDDNode newStateRewards, bscc, tmp; @@ -796,7 +795,6 @@ public class ProbModelChecker extends StateModelChecker // compute bottom strongly connected components (bsccs) if (bsccComp) { - mainLog.print("\nComputing (B)SCCs..."); sccComputer.computeBSCCs(); vectBSCCs = sccComputer.getVectBSCCs(); notInBSCCs = sccComputer.getNotInBSCCs(); @@ -805,7 +803,7 @@ public class ProbModelChecker extends StateModelChecker // unless we've been told to skip it else { mainLog.println("\nSkipping BSCC computation..."); - vectBSCCs = new Vector(); + vectBSCCs = new Vector(); JDD.Ref(reach); vectBSCCs.add(reach); notInBSCCs = JDD.Constant(0); @@ -819,7 +817,7 @@ public class ProbModelChecker extends StateModelChecker mainLog.println("\nComputing steady state probabilities for BSCC " + (i + 1)); // get bscc - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); // compute steady state probabilities try { @@ -827,7 +825,7 @@ public class ProbModelChecker extends StateModelChecker } catch (PrismException e) { JDD.Deref(newStateRewards); for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); throw e; @@ -860,7 +858,7 @@ public class ProbModelChecker extends StateModelChecker // build the reward vector tmp = JDD.Constant(0); for (i = 0; i < n; i++) { - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); JDD.Ref(bscc); tmp = JDD.Apply(JDD.PLUS, tmp, JDD.Apply(JDD.TIMES, JDD.Constant(rewBSCCs[i]), bscc)); } @@ -892,7 +890,7 @@ public class ProbModelChecker extends StateModelChecker mainLog.println("\nComputing probabilities of reaching BSCC " + (i + 1)); // get bscc - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); // compute probabilities probs = computeUntilProbs(trans, trans01, notInBSCCs, bscc); @@ -915,7 +913,7 @@ public class ProbModelChecker extends StateModelChecker // derefs JDD.Deref(newStateRewards); for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); @@ -931,7 +929,7 @@ public class ProbModelChecker extends StateModelChecker public StateProbs doSteadyState() throws PrismException { // bscc stuff - Vector vectBSCCs; + Vector vectBSCCs; JDDNode notInBSCCs; // mtbdd stuff JDDNode start, bscc, tmp; @@ -942,7 +940,6 @@ public class ProbModelChecker extends StateModelChecker // compute bottom strongly connected components (bsccs) if (bsccComp) { - mainLog.print("\nComputing (B)SCCs..."); sccComputer.computeBSCCs(); vectBSCCs = sccComputer.getVectBSCCs(); notInBSCCs = sccComputer.getNotInBSCCs(); @@ -951,7 +948,7 @@ public class ProbModelChecker extends StateModelChecker // unless we've been told to skip it else { mainLog.println("\nSkipping BSCC computation..."); - vectBSCCs = new Vector(); + vectBSCCs = new Vector(); JDD.Ref(reach); vectBSCCs.add(reach); notInBSCCs = JDD.Constant(0); @@ -965,7 +962,7 @@ public class ProbModelChecker extends StateModelChecker whichBSCC = -1; bsccCount = 0; for (i = 0; i < n; i++) { - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); JDD.Ref(bscc); JDD.Ref(start); tmp = JDD.And(bscc, start); @@ -988,14 +985,14 @@ public class ProbModelChecker extends StateModelChecker mainLog.println("\nInitial states all in one BSCC (so no reachability probabilities computed)"); // get bscc - bscc = (JDDNode) vectBSCCs.elementAt(whichBSCC); + bscc = vectBSCCs.elementAt(whichBSCC); // compute steady-state probabilities for the bscc try { solnProbs = computeSteadyStateProbs(trans, bscc); } catch (PrismException e) { for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); throw e; @@ -1027,14 +1024,14 @@ public class ProbModelChecker extends StateModelChecker mainLog.println("\nComputing probability of reaching BSCC " + (i + 1)); // get bscc - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); // compute probabilities try { probs = computeUntilProbs(trans, trans01, notInBSCCs, bscc); } catch (PrismException e) { for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); solnProbs.clear(); @@ -1060,14 +1057,14 @@ public class ProbModelChecker extends StateModelChecker mainLog.println("\nComputing steady-state probabilities for BSCC " + (i + 1)); // get bscc - bscc = (JDDNode) vectBSCCs.elementAt(i); + bscc = vectBSCCs.elementAt(i); // compute steady-state probabilities for the bscc try { probs = computeSteadyStateProbs(trans, bscc); } catch (PrismException e) { for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); solnProbs.clear(); @@ -1091,7 +1088,7 @@ public class ProbModelChecker extends StateModelChecker // derefs for (i = 0; i < n; i++) { - JDD.Deref((JDDNode) vectBSCCs.elementAt(i)); + JDD.Deref(vectBSCCs.elementAt(i)); } JDD.Deref(notInBSCCs); diff --git a/prism/src/prism/SCCComputerXB.java b/prism/src/prism/SCCComputerXB.java index 4f8d24f7..bfd0b912 100644 --- a/prism/src/prism/SCCComputerXB.java +++ b/prism/src/prism/SCCComputerXB.java @@ -35,7 +35,6 @@ import jdd.*; public class SCCComputerXB implements SCCComputer { - private Prism prism; private PrismLog mainLog; // model info @@ -45,16 +44,15 @@ public class SCCComputerXB implements SCCComputer private JDDVars allDDColVars; // stuff for SCCs - private Vector vectSCCs; + private Vector vectSCCs; private JDDNode notInSCCs; // stuff for BSCCs - private Vector vectBSCCs; + private Vector vectBSCCs; private JDDNode notInBSCCs; public SCCComputerXB(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException { // initialise - this.prism = prism; mainLog = prism.getMainLog(); this.trans01 = trans01; this.reach = reach; @@ -64,7 +62,7 @@ public class SCCComputerXB implements SCCComputer // get methods - public Vector getVectBSCCs() { return vectBSCCs; } + public Vector getVectBSCCs() { return vectBSCCs; } public JDDNode getNotInBSCCs() { return notInBSCCs; } @@ -76,8 +74,10 @@ public class SCCComputerXB implements SCCComputer JDDNode v, s, back, scc, out; int i, n; + mainLog.println("\nComputing (B)SCCs..."); + // vector to be filled with SCCs - vectSCCs = new Vector(); + vectSCCs = new Vector(); // BDD of non-SCC states (initially zero BDD) notInSCCs = JDD.Constant(0); @@ -94,22 +94,12 @@ public class SCCComputerXB implements SCCComputer } JDD.Deref(v); - // print out sccs - n = vectSCCs.size(); - mainLog.print(" SCCs: " + n); -// for (i = 0; i < n; i++) { -// mainLog.print(i + ": "); -// JDD.PrintVector((JDDNode)vectSCCs.elementAt(i), allDDRowVars); -// } -// mainLog.print("States not in SCCs:\nx: "); -// JDD.PrintVector(notInSCCs, allDDRowVars); - // now check which ones are bsccs and keep them - vectBSCCs = new Vector(); + vectBSCCs = new Vector(); notInBSCCs = notInSCCs; n = vectSCCs.size(); for (i = 0; i < n; i++) { - scc = (JDDNode)vectSCCs.elementAt(i); + scc = vectSCCs.elementAt(i); JDD.Ref(trans01); JDD.Ref(scc); out = JDD.And(trans01, scc); @@ -126,16 +116,15 @@ public class SCCComputerXB implements SCCComputer JDD.Deref(out); } - // print out bsccs - n = vectBSCCs.size(); - mainLog.print(" BSCCs: " + n); -// for (i = 0; i < n; i++) { -// mainLog.print(i + ": "); -// JDD.PrintVector((JDDNode)vectBSCCs.elementAt(i), allDDRowVars); -// } -// mainLog.print("States not in BSCCs:\nx: "); -// JDD.PrintVector(notInBSCCs, allDDRowVars); + // print out some info + mainLog.print("\nSCCs: " + vectSCCs.size()); + mainLog.print(" BSCCs: " + vectBSCCs.size()); mainLog.println(" Transient states: " + JDD.GetNumMintermsString(notInBSCCs, allDDRowVars.n())); + mainLog.print("BSCC sizes:"); + for (i = 0; i < n; i++) { + mainLog.print(" " + (i+1) + ": " + JDD.GetNumMintermsString(vectBSCCs.elementAt(i), allDDRowVars.n())); + } + mainLog.println(); } // pick a random (actually the first) state from set (set not empty)