s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Tidy-up of (B)SCC computation stuff. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@903 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
2cc923719e
commit
0a91eccb4b
7 changed files with 189 additions and 172 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      prism/src/prism/NondetModelChecker.java
  2. 16
      prism/src/prism/Prism.java
  3. 2
      prism/src/prism/ProbModelChecker.java
  4. 103
      prism/src/prism/SCCComputer.java
  5. 66
      prism/src/prism/SCCComputerLockstep.java
  6. 88
      prism/src/prism/SCCComputerSCCFind.java
  7. 84
      prism/src/prism/SCCComputerXB.java

2
prism/src/prism/NondetModelChecker.java
View File

@ -3,7 +3,7 @@
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
// * Carlos S. Bederián (Universidad Nacional de Córdoba)
// * Carlos S. Bederian (Universidad Nacional de Cordoba)
//
//------------------------------------------------------------------------------
//

16
prism/src/prism/Prism.java
View File

@ -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<JDDNode> 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 ");

2
prism/src/prism/ProbModelChecker.java
View File

@ -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.

103
prism/src/prism/SCCComputer.java
View File

@ -3,7 +3,7 @@
// Copyright (c) 2002-
// Authors:
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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<JDDNode> vectSCCs;
protected JDDNode notInSCCs;
// stuff for BSCCs
protected Vector<JDDNode> 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<JDDNode> getVectBSCCs();
// Get vector of SCCs
// NB: these BDDs aren't derefed by SCCComputer classes
public Vector<JDDNode> 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<JDDNode> 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<JDDNode>();
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();
}
}

66
prism/src/prism/SCCComputerLockstep.java
View File

@ -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 <david.parker@comlab.ox.ac.uk> (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<JDDNode> sccs;
private JDDNode allSCCs;
private JDDNode notInSCCs;
private Stack<DecompTask> 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<JDDNode>();
vectSCCs = new Vector<JDDNode>();
allSCCs = JDD.Constant(0);
tasks = new Stack<DecompTask>();
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<JDDNode> 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

88
prism/src/prism/SCCComputerSCCFind.java
View File

@ -1,6 +1,11 @@
//==============================================================================
//
// Copyright (c) 2007, Carlos S. Bederián
// Copyright (c) 2002-
// Authors:
// * Carlos S. Bederian (Universidad Nacional de Cordoba)
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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<JDDNode> sccs;
private JDDNode allSCCs;
private JDDNode notInSCCs;
private Stack<DecompTask> 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<JDDNode>();
vectSCCs = new Vector<JDDNode>();
allSCCs = JDD.Constant(0);
tasks = new Stack<DecompTask>();
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<JDDNode> 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));

84
prism/src/prism/SCCComputerXB.java
View File

@ -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<JDDNode> vectSCCs;
private JDDNode notInSCCs;
// stuff for BSCCs
private Vector<JDDNode> 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<JDDNode> 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<JDDNode>();
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;

Write Preview
Loading…
Cancel
Save