From 6d1747ac332825235f987274d9e663d10e95d6da Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 8 Jul 2011 07:40:32 +0000 Subject: [PATCH] Remove debug output + code tidy. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3235 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/ECComputerDefault.java | 59 +++++++------------------- 1 file changed, 15 insertions(+), 44 deletions(-) diff --git a/prism/src/prism/ECComputerDefault.java b/prism/src/prism/ECComputerDefault.java index 8fd3fb3b..8b4fc5c3 100644 --- a/prism/src/prism/ECComputerDefault.java +++ b/prism/src/prism/ECComputerDefault.java @@ -34,9 +34,8 @@ import jdd.JDDNode; import jdd.JDDVars; public class ECComputerDefault extends ECComputer -{ - public ECComputerDefault(Prism prism, JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, - JDDVars allDDNondetVars) +{ + public ECComputerDefault(Prism prism, JDDNode reach, JDDNode trans, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars allDDNondetVars) { super(prism, reach, trans, trans01, allDDRowVars, allDDColVars, allDDNondetVars); } @@ -51,44 +50,31 @@ public class ECComputerDefault extends ECComputer candidates.push(reach); SCCComputer sccComputer; - while (!candidates.isEmpty()) - { - System.out.println("Checking candidate"); - + while (!candidates.isEmpty()) { JDDNode candidate = candidates.pop(); // Compute the stable set JDD.Ref(candidate); JDDNode stableSet = findMaximalStableSet(candidate); - System.out.println("found max stable set"); - // Drop empty sets - if (stableSet.equals(JDD.ZERO)) - { - System.out.println("empty set"); + if (stableSet.equals(JDD.ZERO)) { JDD.Deref(stableSet); JDD.Deref(candidate); continue; } - if (!initialCandidate) - { - System.out.println("not initial"); - + if (!initialCandidate) { // candidate is an SCC, check if it's stable - if (stableSet.equals(candidate)) - { + if (stableSet.equals(candidate)) { vectECs.add(maxStableSetChoices(candidate)); JDD.Deref(stableSet); continue; } - } - else - { + } else { initialCandidate = false; } - + JDD.Deref(candidate); // Filter bad transitions @@ -106,28 +92,19 @@ public class ECComputerDefault extends ECComputer candidates.addAll(sccs); } } - + /** * Returns a stable set of states contained in candidateStates * - * @param candidateStates - * set of candidate states S x H_i (dereferenced after calling this function) + * @param candidateStates set of candidate states S x H_i (dereferenced after calling this function) * @return a referenced BDD with the maximal stable set in c */ private JDDNode findMaximalStableSet(JDDNode candidateStates) { - System.out.println("findMaximalStableSet"); - - - JDDNode old = JDD.Constant(0); JDDNode current = candidateStates; - - if (current.isConstant()) - System.out.println("current = " + current.getValue()); - while (!current.equals(old)) - { + while (!current.equals(old)) { JDD.Deref(old); JDD.Ref(current); old = current; @@ -150,17 +127,15 @@ public class ECComputerDefault extends ECComputer JDD.Deref(old); return current; } - + /** * Returns the transition relation of a stable set * - * @param b - * BDD of a stable set (dereferenced after calling this function) + * @param b BDD of a stable set (dereferenced after calling this function) * @return referenced BDD of the transition relation restricted to the stable set */ private JDDNode maxStableSetTrans(JDDNode b) { - System.out.println("maxStableSetTrans"); JDD.Ref(b); JDD.Ref(trans); // Select transitions starting in b @@ -179,18 +154,15 @@ public class ECComputerDefault extends ECComputer // Abstract over actions return JDD.ThereExists(stableTrans01, allDDNondetVars); } - + /** * Returns the transition relation of a stable set * - * @param b - * BDD of a stable set (dereferenced after calling this function) + * @param b BDD of a stable set (dereferenced after calling this function) * @return referenced BDD of the transition relation restricted to the stable set */ public JDDNode maxStableSetChoices(JDDNode b) { - System.out.println("maxStableSetChoices"); - JDD.Ref(b); JDD.Ref(trans); // Select transitions starting in b @@ -209,5 +181,4 @@ public class ECComputerDefault extends ECComputer // Abstract over actions return JDD.ThereExists(stableTrans01, allDDColVars); } - }