From 0a91eccb4b393daa0200c96673137eca3c517c1c Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 19 Dec 2008 14:39:41 +0000 Subject: [PATCH] Tidy-up of (B)SCC computation stuff. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@903 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 2 +- prism/src/prism/Prism.java | 16 +++- prism/src/prism/ProbModelChecker.java | 2 +- prism/src/prism/SCCComputer.java | 103 ++++++++++++++++++++--- prism/src/prism/SCCComputerLockstep.java | 66 ++++++--------- prism/src/prism/SCCComputerSCCFind.java | 88 +++++++++---------- prism/src/prism/SCCComputerXB.java | 84 +++--------------- 7 files changed, 189 insertions(+), 172 deletions(-) diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 1a193eed..84e33e73 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -3,7 +3,7 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) -// * Carlos S. Bederián (Universidad Nacional de Córdoba) +// * Carlos S. Bederian (Universidad Nacional de Cordoba) // //------------------------------------------------------------------------------ // diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index ae5f0ca5..ad5a569d 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -479,6 +479,16 @@ public class Prism implements PrismSettingsListener return theSimulator; } + /** + * Get an SCCComputer object. + * Type (i.e. algorithm) depends on SCCMethod PRISM option. + * @return + */ + public SCCComputer getSCCComputer(Model model) + { + return getSCCComputer(model.getReach(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars()); + } + /** * Get an SCCComputer object. * Type (i.e. algorithm) depends on SCCMethod PRISM option. @@ -1080,6 +1090,7 @@ public class Prism implements PrismSettingsListener public void exportBSCCsToFile(Model model, int exportType, File file) throws FileNotFoundException { int i, n; + long l; // timer PrismLog tmpLog; SCCComputer sccComputer; Vector bsccs; @@ -1092,10 +1103,13 @@ public class Prism implements PrismSettingsListener // Compute BSCCs mainLog.println("\nComputing BSCCs..."); - sccComputer = getSCCComputer(model.getReach(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars()); + sccComputer = getSCCComputer(model); + l = System.currentTimeMillis(); sccComputer.computeBSCCs(); + l = System.currentTimeMillis() - l; bsccs = sccComputer.getVectBSCCs(); not = sccComputer.getNotInBSCCs(); + mainLog.println("\nTime for BSCC computation: " + l/1000.0 + " seconds."); // print message mainLog.print("\nExporting BSCCs "); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 1ea7f89a..603dd91d 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -58,7 +58,7 @@ public class ProbModelChecker extends NonProbModelChecker super(prism, m, pf); // Create SCCComputer object - sccComputer = new SCCComputerXB(prism, reach, trans01, allDDRowVars, allDDColVars); // TODO: generalise? + sccComputer = prism.getSCCComputer(m); // Inherit some options from parent Prism object. // Store locally and/or pass onto engines. diff --git a/prism/src/prism/SCCComputer.java b/prism/src/prism/SCCComputer.java index c1cd691a..ac18df12 100644 --- a/prism/src/prism/SCCComputer.java +++ b/prism/src/prism/SCCComputer.java @@ -3,7 +3,7 @@ // Copyright (c) 2002- // Authors: // * Dave Parker (University of Oxford, formerly University of Birmingham) -// * Carlos S. Bederián (Universidad Nacional de Córdoba) +// * Carlos S. Bederian (Universidad Nacional de Cordoba) // //------------------------------------------------------------------------------ // @@ -33,16 +33,99 @@ import jdd.*; // interface for SCC computing classes -public interface SCCComputer +public abstract class SCCComputer { - // perform maximal SCC search - public void computeBSCCs(); + protected Prism prism; + protected PrismLog mainLog; + + // model info + protected JDDNode trans01; + protected JDDNode reach; + protected JDDVars allDDRowVars; + protected JDDVars allDDColVars; + + // stuff for SCCs + protected Vector vectSCCs; + protected JDDNode notInSCCs; + // stuff for BSCCs + protected Vector vectBSCCs; + protected JDDNode notInBSCCs; + + // Get methods + + // Constructor + public SCCComputer(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) + { + this.prism = prism; + mainLog = prism.getMainLog(); + this.trans01 = trans01; + this.reach = reach; + this.allDDRowVars = allDDRowVars; + this.allDDColVars = allDDColVars; + } - // get vector of maximal SCCs - // note: these BDDs aren't derefed by SCCComputer classes - public Vector getVectBSCCs(); + // Get vector of SCCs + // NB: these BDDs aren't derefed by SCCComputer classes + public Vector getVectSCCs() { return vectSCCs; } - // get states not in any SCCs - // note: this BDD isn't derefed by SCCComputer classes - public JDDNode getNotInBSCCs(); + // Get states not in any SCCs + // NB: this BDD isn't derefed by SCCComputer classes + public JDDNode getNotInSCCs() { return notInSCCs; } + + // Get vector of BSCCs + // NB: these BDDs aren't derefed by SCCComputer classes + public Vector getVectBSCCs() { return vectBSCCs; } + + // Get states not in any BSCCs + // NB: this BDD isn't derefed by SCCComputer classes + public JDDNode getNotInBSCCs() { return notInBSCCs; } + + // Strongly connected components (SCC) computation + // NB: This creates BDDs, obtainable from getVectSCCs() and getNotInSCCs(), + // which the calling code is responsible for dereferencing. + public abstract void computeSCCs(); + + // Bottom strongly connected components (BSCC) computation + // NB: This creates BDDs, obtainable from getVectBSCCs() and getNotInBSCCs(), + // which the calling code is responsible for dereferencing. + public void computeBSCCs() + { + JDDNode scc, out; + int i, n; + + // First compute SCCs + computeSCCs(); + + // Now check which ones are bsccs and keep them + vectBSCCs = new Vector(); + notInBSCCs = notInSCCs; + n = vectSCCs.size(); + for (i = 0; i < n; i++) { + scc = vectSCCs.elementAt(i); + JDD.Ref(trans01); + JDD.Ref(scc); + out = JDD.And(trans01, scc); + JDD.Ref(scc); + out = JDD.And(out, JDD.Not(JDD.PermuteVariables(scc, allDDRowVars, allDDColVars))); + if (out.equals(JDD.ZERO)) { + vectBSCCs.addElement(scc); + } + else { + JDD.Ref(scc); + notInBSCCs = JDD.Or(scc, notInBSCCs); + JDD.Deref(scc); + } + JDD.Deref(out); + } + + // print out some info + mainLog.print("\nSCCs: " + vectSCCs.size()); // note: contents of vectSCCs derefed but array exiists + mainLog.print(", BSCCs: " + vectBSCCs.size()); + mainLog.println(", non-BSCC states: " + JDD.GetNumMintermsString(notInBSCCs, allDDRowVars.n())); + mainLog.print("BSCC sizes:"); + for (i = 0; i < vectBSCCs.size(); i++) { + mainLog.print(" " + (i+1) + ":" + JDD.GetNumMintermsString(vectBSCCs.elementAt(i), allDDRowVars.n())); + } + mainLog.println(); + } } diff --git a/prism/src/prism/SCCComputerLockstep.java b/prism/src/prism/SCCComputerLockstep.java index 153f2315..8af156e9 100644 --- a/prism/src/prism/SCCComputerLockstep.java +++ b/prism/src/prism/SCCComputerLockstep.java @@ -2,7 +2,8 @@ // // Copyright (c) 2002- // Authors: -// * Carlos S. Bederián (Universidad Nacional de Córdoba) +// * Carlos S. Bederian (Universidad Nacional de Cordoba) +// * Dave Parker (University of Oxford, formerly University of Birmingham) // //------------------------------------------------------------------------------ // @@ -34,7 +35,7 @@ import java.util.*; // SCC (strongly connected component) decomposition using lockstep search with trimming // (from Bloem/Gabow/Somenzi 2000) -public class SCCComputerLockstep implements SCCComputer +public class SCCComputerLockstep extends SCCComputer { private class DecompTask { @@ -45,48 +46,31 @@ public class SCCComputerLockstep implements SCCComputer JDDNode getEdges() { return _edges; } } - private Prism prism; - private PrismLog log; - - private JDDNode initialNodes; - private JDDNode initialEdges; - private JDDVars rows; - private JDDVars cols; - private Vector sccs; private JDDNode allSCCs; - private JDDNode notInSCCs; private Stack tasks; - public SCCComputerLockstep(Prism prism, JDDNode nodes, JDDNode edges, JDDVars rows_, JDDVars cols_) + // Constructor + + public SCCComputerLockstep(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) { - this.prism = prism; - log = prism.getMainLog(); - rows = rows_; - cols = cols_; - initialNodes = nodes; - initialEdges = edges; + super(prism, reach, trans01, allDDRowVars, allDDColVars); } - public void computeBSCCs() + public void computeSCCs() { - sccs = new Vector(); + vectSCCs = new Vector(); allSCCs = JDD.Constant(0); tasks = new Stack(); - JDD.Ref(initialNodes); - JDD.Ref(initialEdges); - tasks.push(new DecompTask(initialNodes, initialEdges)); + JDD.Ref(reach); + JDD.Ref(trans01); + tasks.push(new DecompTask(reach, trans01)); while (!tasks.isEmpty()) { lockstep(tasks.pop()); } - JDD.Ref(initialNodes); - notInSCCs = JDD.And(initialNodes, JDD.Not(allSCCs)); - log.print(" BSCCs: " + sccs.size()); - log.println(" Transient states: " + JDD.GetNumMintermsString(notInSCCs, rows.n())); + JDD.Ref(reach); + notInSCCs = JDD.And(reach, JDD.Not(allSCCs)); } - public Vector getVectBSCCs() { return sccs; } - public JDDNode getNotInBSCCs() { return notInSCCs; } - // Return the image of nodes in edges // Refs: result // Derefs: edges, nodes @@ -97,8 +81,8 @@ public class SCCComputerLockstep implements SCCComputer // Get transitions that start at nodes tmp = JDD.Apply(JDD.TIMES, edges, nodes); // Get img(nodes) - tmp = JDD.ThereExists(tmp, rows); - tmp = JDD.PermuteVariables(tmp, cols, rows); + tmp = JDD.ThereExists(tmp, allDDRowVars); + tmp = JDD.PermuteVariables(tmp, allDDColVars, allDDRowVars); return tmp; } @@ -110,10 +94,10 @@ public class SCCComputerLockstep implements SCCComputer JDDNode tmp; // Get transitions that end at nodes - tmp = JDD.PermuteVariables(nodes, rows, cols); + tmp = JDD.PermuteVariables(nodes, allDDRowVars, allDDColVars); tmp = JDD.Apply(JDD.TIMES, edges, tmp); // Get pre(nodes) - tmp = JDD.ThereExists(tmp, cols); + tmp = JDD.ThereExists(tmp, allDDColVars); return tmp; } @@ -125,13 +109,13 @@ public class SCCComputerLockstep implements SCCComputer return; } // Sanity check, partitioning of the state space should prevent this - assert !sccs.contains(nodes); + assert !vectSCCs.contains(nodes); /* if (prism.getVerbose()) { log.println("Found SCC:"); JDD.PrintVector(nodes, rows); } */ - sccs.addElement(nodes); + vectSCCs.addElement(nodes); JDD.Ref(nodes); allSCCs = JDD.Or(allSCCs, nodes); } @@ -196,11 +180,11 @@ public class SCCComputerLockstep implements SCCComputer JDD.Ref(nodes); edges = JDD.Apply(JDD.TIMES, edges, nodes); JDD.Ref(nodes); - edges = JDD.Apply(JDD.TIMES, edges, JDD.PermuteVariables(nodes, rows, cols)); + edges = JDD.Apply(JDD.TIMES, edges, JDD.PermuteVariables(nodes, allDDRowVars, allDDColVars)); // pick a starting node JDD.Ref(nodes); - JDDNode v = JDD.RestrictToFirst(nodes, rows); + JDDNode v = JDD.RestrictToFirst(nodes, allDDRowVars); // mainLog.println("Lockstep - picked node:"); // JDD.PrintVector(v, allDDRowVars); @@ -298,7 +282,7 @@ public class SCCComputerLockstep implements SCCComputer // check if SCC is nontrivial and report JDD.Ref(scc); - tmp = JDD.PermuteVariables(scc, rows, cols); + tmp = JDD.PermuteVariables(scc, allDDRowVars, allDDColVars); JDD.Ref(edges); tmp = JDD.And(tmp, edges); JDD.Ref(scc); @@ -320,7 +304,7 @@ public class SCCComputerLockstep implements SCCComputer JDD.Ref(newNodes1); JDDNode newEdges1 = JDD.Apply(JDD.TIMES, edges, newNodes1); JDD.Ref(newNodes1); - tmp = JDD.PermuteVariables(newNodes1, rows, cols); + tmp = JDD.PermuteVariables(newNodes1, allDDRowVars, allDDColVars); newEdges1 = JDD.Apply(JDD.TIMES, newEdges1, tmp); // newNodes2 = nodes \ convergedSet @@ -332,7 +316,7 @@ public class SCCComputerLockstep implements SCCComputer JDD.Ref(newNodes2); JDDNode newEdges2 = JDD.Apply(JDD.TIMES, edges, newNodes2); JDD.Ref(newNodes2); - tmp = JDD.PermuteVariables(newNodes2, rows, cols); + tmp = JDD.PermuteVariables(newNodes2, allDDRowVars, allDDColVars); newEdges2 = JDD.Apply(JDD.TIMES, newEdges2, tmp); // Queue new sets for search diff --git a/prism/src/prism/SCCComputerSCCFind.java b/prism/src/prism/SCCComputerSCCFind.java index 7beb8d8c..b7682e2e 100644 --- a/prism/src/prism/SCCComputerSCCFind.java +++ b/prism/src/prism/SCCComputerSCCFind.java @@ -1,6 +1,11 @@ //============================================================================== // -// Copyright (c) 2007, Carlos S. Bederián +// Copyright (c) 2002- +// Authors: +// * Carlos S. Bederian (Universidad Nacional de Cordoba) +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ // // This file is part of PRISM. // @@ -30,7 +35,7 @@ import java.util.*; // SCC (strongly connected component) decomposition using SCC-Find search // (from Gentilini/Piazza/Policriti 2003) -public class SCCComputerSCCFind implements SCCComputer +public class SCCComputerSCCFind extends SCCComputer { private class DecompTask { JDDNode nodes; @@ -42,50 +47,37 @@ public class SCCComputerSCCFind implements SCCComputer } } - private Prism prism; - private PrismLog log; - - private JDDNode initialNodes; - private JDDNode initialEdges; - private JDDVars rows; - private JDDVars cols; - private Vector sccs; private JDDNode allSCCs; - private JDDNode notInSCCs; private Stack tasks; - public SCCComputerSCCFind(Prism prism, JDDNode nodes, JDDNode edges, JDDVars rows_, JDDVars cols_) + // Constructor + + public SCCComputerSCCFind(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) { - this.prism = prism; - log = prism.getMainLog(); - rows = rows_; - cols = cols_; - initialNodes = nodes; - initialEdges = edges; + super(prism, reach, trans01, allDDRowVars, allDDColVars); } - public void computeBSCCs() + // Strongly connected components (SCC) computation + // NB: This creates BDDs, obtainable from getVectSCCs() and getNotInSCCs(), + // which the calling code is responsible for dereferencing. + + public void computeSCCs() { - sccs = new Vector(); + vectSCCs = new Vector(); allSCCs = JDD.Constant(0); tasks = new Stack(); - JDD.Ref(initialNodes); - JDD.Ref(initialEdges); - JDDNode trimmedNodes = trim(initialNodes, initialEdges); - JDD.Ref(initialEdges); - tasks.push(new DecompTask(trimmedNodes, initialEdges, JDD.Constant(0), JDD.Constant(0))); + JDD.Ref(reach); + JDD.Ref(trans01); + JDDNode trimmedNodes = trim(reach, trans01); + JDD.Ref(trans01); + tasks.push(new DecompTask(trimmedNodes, trans01, JDD.Constant(0), JDD.Constant(0))); while (!tasks.isEmpty()) { sccFind(tasks.pop()); } - JDD.Ref(initialNodes); - notInSCCs = JDD.And(initialNodes, JDD.Not(allSCCs)); - log.print(" BSCCs: " + sccs.size()); - log.println(" Transient states: " + JDD.GetNumMintermsString(notInSCCs, rows.n())); + JDD.Ref(reach); + notInSCCs = JDD.And(reach, JDD.Not(allSCCs)); } - public Vector getVectBSCCs() { return sccs; } - public JDDNode getNotInBSCCs() { return notInSCCs; } - // Return the image of nodes in edges // Refs: result // Derefs: edges, nodes @@ -95,8 +87,8 @@ public class SCCComputerSCCFind implements SCCComputer // Get transitions that start at nodes tmp = JDD.Apply(JDD.TIMES, edges, nodes); // Get the img(nodes) - tmp = JDD.ThereExists(tmp, rows); - tmp = JDD.PermuteVariables(tmp, cols, rows); + tmp = JDD.ThereExists(tmp, allDDRowVars); + tmp = JDD.PermuteVariables(tmp, allDDColVars, allDDRowVars); return tmp; } @@ -107,10 +99,10 @@ public class SCCComputerSCCFind implements SCCComputer JDDNode tmp; // Get transitions that end at nodes - tmp = JDD.PermuteVariables(nodes, rows, cols); + tmp = JDD.PermuteVariables(nodes, allDDRowVars, allDDColVars); tmp = JDD.Apply(JDD.TIMES, edges, tmp); // Get the pre(nodes) - tmp = JDD.ThereExists(tmp, cols); + tmp = JDD.ThereExists(tmp, allDDColVars); return tmp; } @@ -137,8 +129,8 @@ public class SCCComputerSCCFind implements SCCComputer pre = preimage(current, edges); current = JDD.And(current, JDD.And(img, pre)); if (prism.getVerbose()) { - log.println("Trimming pass " + i + ":"); - JDD.PrintVector(current, rows); + mainLog.println("Trimming pass " + i + ":"); + JDD.PrintVector(current, allDDRowVars); i++; } } while (!current.equals(old)); @@ -156,13 +148,13 @@ public class SCCComputerSCCFind implements SCCComputer return; } // Sanity check, partitioning of the state space should prevent this - assert !sccs.contains(nodes); + assert !vectSCCs.contains(nodes); /* if (prism.getVerbose()) { - log.println("Found SCC:"); + mainLog.println("Found SCC:"); JDD.PrintVector(nodes, rows); } */ - sccs.addElement(nodes); + vectSCCs.addElement(nodes); JDD.Ref(nodes); allSCCs = JDD.Or(allSCCs, nodes); } @@ -198,14 +190,14 @@ public class SCCComputerSCCFind implements SCCComputer JDD.Deref(level); level = stack.pop(); - JDDNode newNode = JDD.RestrictToFirst(level, rows); + JDDNode newNode = JDD.RestrictToFirst(level, allDDRowVars); JDD.Ref(newNode); JDDNode newPath = newNode; while (!stack.isEmpty()) { level = stack.pop(); JDD.Ref(newPath); JDD.Ref(edges); - newPath = JDD.Or(newPath, JDD.RestrictToFirst(JDD.And(preimage(newPath, edges), level), rows)); + newPath = JDD.Or(newPath, JDD.RestrictToFirst(JDD.And(preimage(newPath, edges), level), allDDRowVars)); } return new SkelForwardResult(forwardSet, newPath, newNode); } @@ -230,7 +222,7 @@ public class SCCComputerSCCFind implements SCCComputer } /* if (prism.getVerbose()) { - log.println("SCC-Find pass on nodes: "); + mainLog.println("SCC-Find pass on nodes: "); JDD.PrintVector(nodes, rows); } */ @@ -238,7 +230,7 @@ public class SCCComputerSCCFind implements SCCComputer JDD.Deref(spineSetNode); // Pick a node JDD.Ref(nodes); - spineSetNode = JDD.RestrictToFirst(nodes, rows); + spineSetNode = JDD.RestrictToFirst(nodes, allDDRowVars); } SkelForwardResult skelFw = skelForward(nodes, edges, spineSetNode); @@ -270,7 +262,7 @@ public class SCCComputerSCCFind implements SCCComputer // check if SCC is nontrivial and report JDD.Ref(scc); - tmp = JDD.PermuteVariables(scc, rows, cols); + tmp = JDD.PermuteVariables(scc, allDDRowVars, allDDColVars); JDD.Ref(edges); tmp = JDD.And(tmp, edges); JDD.Ref(scc); @@ -292,7 +284,7 @@ public class SCCComputerSCCFind implements SCCComputer JDD.Ref(newNodes1); JDDNode newEdges1 = JDD.Apply(JDD.TIMES, edges, newNodes1); JDD.Ref(newNodes1); - newEdges1 = JDD.Apply(JDD.TIMES, newEdges1, JDD.PermuteVariables(newNodes1, rows, cols)); + newEdges1 = JDD.Apply(JDD.TIMES, newEdges1, JDD.PermuteVariables(newNodes1, allDDRowVars, allDDColVars)); // newS1 = spineSetPath \ scc JDD.Ref(spineSetPath); JDD.Ref(scc); @@ -313,7 +305,7 @@ public class SCCComputerSCCFind implements SCCComputer JDD.Ref(newNodes2); JDDNode newEdges2 = JDD.Apply(JDD.TIMES, edges, newNodes2); JDD.Ref(newNodes2); - newEdges2 = JDD.Apply(JDD.TIMES, newEdges2, JDD.PermuteVariables(newNodes2, rows, cols)); + newEdges2 = JDD.Apply(JDD.TIMES, newEdges2, JDD.PermuteVariables(newNodes2, allDDRowVars, allDDColVars)); // newS2 = newS \ scc JDD.Ref(scc); JDDNode newSpineSetPath2 = JDD.And(newSpineSetPath, JDD.Not(scc)); diff --git a/prism/src/prism/SCCComputerXB.java b/prism/src/prism/SCCComputerXB.java index d79ae92a..6c625724 100644 --- a/prism/src/prism/SCCComputerXB.java +++ b/prism/src/prism/SCCComputerXB.java @@ -33,46 +33,22 @@ import jdd.*; // SCC (strongly connected component) decomposition // (from Xie/Beerel 1999) -public class SCCComputerXB implements SCCComputer +public class SCCComputerXB extends SCCComputer { - private PrismLog mainLog; - - // model info - private JDDNode trans01; - private JDDNode reach; - private JDDVars allDDRowVars; - private JDDVars allDDColVars; + // Constructor - // stuff for SCCs - private Vector vectSCCs; - private JDDNode notInSCCs; - // stuff for BSCCs - private Vector vectBSCCs; - private JDDNode notInBSCCs; - public SCCComputerXB(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) { - // initialise - mainLog = prism.getMainLog(); - this.trans01 = trans01; - this.reach = reach; - this.allDDRowVars = allDDRowVars; - this.allDDColVars = allDDColVars; + super(prism, reach, trans01, allDDRowVars, allDDColVars); } - - // get methods - - public Vector getVectBSCCs() { return vectBSCCs; } - public JDDNode getNotInBSCCs() { return notInBSCCs; } + // Strongly connected components (SCC) computation + // NB: This creates BDDs, obtainable from getVectSCCs() and getNotInSCCs(), + // which the calling code is responsible for dereferencing. - // bottom strongly connected components (bscc) computation - // (using algorithm of xie/beerel'99) - - public void computeBSCCs() + public void computeSCCs() { - JDDNode v, s, back, scc, out; - int i, n; + JDDNode v, s, back; mainLog.println("\nComputing (B)SCCs..."); @@ -81,7 +57,7 @@ public class SCCComputerXB implements SCCComputer // BDD of non-SCC states (initially zero BDD) notInSCCs = JDD.Constant(0); - // first compute all sccs + // Compute all SCCs // (using algorithm of xie/beerel'99) JDD.Ref(reach); v = reach; @@ -93,43 +69,11 @@ public class SCCComputerXB implements SCCComputer v = JDD.And(v, JDD.And(reach, JDD.Not(JDD.Or(s, back)))); } JDD.Deref(v); - - // now check which ones are bsccs and keep them - vectBSCCs = new Vector(); - notInBSCCs = notInSCCs; - n = vectSCCs.size(); - for (i = 0; i < n; i++) { - scc = vectSCCs.elementAt(i); - JDD.Ref(trans01); - JDD.Ref(scc); - out = JDD.And(trans01, scc); - JDD.Ref(scc); - out = JDD.And(out, JDD.Not(JDD.PermuteVariables(scc, allDDRowVars, allDDColVars))); - if (out.equals(JDD.ZERO)) { - vectBSCCs.addElement(scc); - } - else { - JDD.Ref(scc); - notInBSCCs = JDD.Or(scc, notInBSCCs); - JDD.Deref(scc); - } - JDD.Deref(out); - } - - // 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 < vectBSCCs.size(); 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) - public JDDNode pickRandomState(JDDNode set) + protected JDDNode pickRandomState(JDDNode set) { int i, n; JDDNode tmp, tmp2, res, var; @@ -167,7 +111,7 @@ public class SCCComputerXB implements SCCComputer // find backward set of state s restricted to set v - public JDDNode computeBackwardSet(JDDNode s, JDDNode v) + protected JDDNode computeBackwardSet(JDDNode s, JDDNode v) { JDDNode back, tmp; boolean done = false; @@ -202,7 +146,7 @@ public class SCCComputerXB implements SCCComputer // find forward set of state s restricted to set v - public JDDNode computeForwardSet(JDDNode s, JDDNode v) + protected JDDNode computeForwardSet(JDDNode s, JDDNode v) { JDDNode forw, v2, tmp; boolean done = false; @@ -244,7 +188,7 @@ public class SCCComputerXB implements SCCComputer // compute fmd (finite maximum distance) predecessors of set w - public JDDNode computeFMDPred(JDDNode w, JDDNode u) + protected JDDNode computeFMDPred(JDDNode w, JDDNode u) { JDDNode pred, front, bound, x, y; @@ -281,7 +225,7 @@ public class SCCComputerXB implements SCCComputer // (store SCCs in first vector, // store states not in an SCC in first element of second vector) - public void computeSCCsRec(JDDNode s, JDDNode back) + protected void computeSCCsRec(JDDNode s, JDDNode back) { JDDNode forw, x, r, y, ip, s2, back2, tmp;