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

New -exportbsccs option (currently does SCCs though). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@807 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
5bf4f3ca22
commit
3ba831c8cb
4 changed files with 135 additions and 32 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. 20
      prism/src/prism/LTLModelChecker.java
  2. 120
      prism/src/prism/Prism.java
  3. 25
      prism/src/prism/PrismCL.java
  4. 2
      prism/src/prism/SCCComputerXB.java

20
prism/src/prism/LTLModelChecker.java
View File

@ -488,6 +488,7 @@ public class LTLModelChecker
Stack<JDDNode> candidates = new Stack<JDDNode>();
candidates.push(states);
Vector<JDDNode> ecs = new Vector<JDDNode>();
SCCComputer sccComputer;
while (!candidates.isEmpty()) {
JDDNode candidate = candidates.pop();
@ -522,24 +523,7 @@ public class LTLModelChecker
// now find the maximal SCCs in (stableSet, stableSetTrans)
Vector<JDDNode> sccs;
SCCComputer sccComputer;
switch (prism.getSCCMethod()) {
case Prism.LOCKSTEP:
sccComputer = new SCCComputerLockstep(prism, stableSet, stableSetTrans, model.getAllDDRowVars(), model
.getAllDDColVars());
break;
case Prism.SCCFIND:
sccComputer = new SCCComputerSCCFind(prism, stableSet, stableSetTrans, model.getAllDDRowVars(), model
.getAllDDColVars());
break;
case Prism.XIEBEEREL:
sccComputer = new SCCComputerXB(prism, stableSet, stableSetTrans, model.getAllDDRowVars(), model
.getAllDDColVars());
break;
default:
sccComputer = new SCCComputerLockstep(prism, stableSet, stableSetTrans, model.getAllDDRowVars(), model
.getAllDDColVars());
}
sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model.getAllDDColVars());
sccComputer.computeBSCCs();
JDD.Deref(stableSet);
JDD.Deref(stableSetTrans);

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

@ -29,6 +29,7 @@ package prism;
import java.io.*;
import java.util.ArrayList;
import java.util.Vector;
import jdd.*;
import dv.*;
@ -477,7 +478,31 @@ public class Prism implements PrismSettingsListener
}
return theSimulator;
}
/**
* Get an SCCComputer object.
* Type (i.e. algorithm) depends on SCCMethod PRISM option.
* @return
*/
public SCCComputer getSCCComputer(JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars)
{
SCCComputer sccComputer;
switch (getSCCMethod()) {
case Prism.LOCKSTEP:
sccComputer = new SCCComputerLockstep(this, reach, trans01, allDDRowVars, allDDColVars);
break;
case Prism.SCCFIND:
sccComputer = new SCCComputerSCCFind(this, reach, trans01, allDDRowVars, allDDColVars);
break;
case Prism.XIEBEEREL:
sccComputer = new SCCComputerXB(this, reach, trans01, allDDRowVars, allDDColVars);
break;
default:
sccComputer = new SCCComputerLockstep(this, reach, trans01, allDDRowVars, allDDColVars);
}
return sccComputer;
}
// Let PrismSettings object notify us things have changed
public void notifySettings(PrismSettings settings)
@ -1052,18 +1077,28 @@ public class Prism implements PrismSettingsListener
// export states list to a file (plain, matlab, ...)
// file == null mean export to log
public void exportStatesToFile(Model model, int exportType, File file) throws FileNotFoundException
public void exportBSCCsToFile(Model model, int exportType, File file) throws FileNotFoundException
{
int i;
int i, n;
PrismLog tmpLog;
SCCComputer sccComputer;
Vector<JDDNode> bsccs;
JDDNode not, bscc;
// no specific states format for MRMC
if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN;
// rows format does not apply to states output
if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN;
// Compute BSCCs
mainLog.println("\nComputing BSCCs...");
sccComputer = getSCCComputer(model.getReach(), model.getTrans01(), model.getAllDDRowVars(), model.getAllDDColVars());
sccComputer.computeBSCCs();
bsccs = sccComputer.getVectBSCCs();
not = sccComputer.getNotInBSCCs();
// print message
mainLog.print("\nExporting list of reachable states ");
mainLog.print("\nExporting BSCCs ");
switch (exportType) {
case EXPORT_PLAIN: mainLog.print("in plain text format "); break;
case EXPORT_MATLAB: mainLog.print("in Matlab format "); break;
@ -1082,22 +1117,30 @@ public class Prism implements PrismSettingsListener
// print header: list of model vars
if (exportType == EXPORT_MATLAB) tmpLog.print("% ");
tmpLog.print("(");
tmpLog.print("Variables: (");
for (i = 0; i < model.getNumVars(); i++) {
tmpLog.print(model.getVarName(i));
if (i < model.getNumVars()-1) tmpLog.print(",");
}
tmpLog.println(")");
if (exportType == EXPORT_MATLAB) tmpLog.println("states=[");
// print states
if (exportType != EXPORT_MATLAB)
model.getReachableStates().print(tmpLog);
else
model.getReachableStates().printMatlab(tmpLog);
// print states for each bscc
n = bsccs.size();
for (i = 0; i < n; i++) {
tmpLog.println();
if (exportType == EXPORT_MATLAB) tmpLog.print("% ");
tmpLog.println("BSCC "+(i+1)+"/"+n+":");
if (exportType == EXPORT_MATLAB) tmpLog.println("bscc"+(i+1)+"=[");
bscc = bsccs.get(i);
if (exportType != EXPORT_MATLAB)
new StateListMTBDD(bscc, model).print(tmpLog);
else
new StateListMTBDD(bscc, model).printMatlab(tmpLog);
if (exportType == EXPORT_MATLAB) tmpLog.println("];");
JDD.Deref(bscc);
}
// print footer
if (exportType == EXPORT_MATLAB) tmpLog.println("];");
JDD.Deref(not);
// tidy up
if (file != null) tmpLog.close();
@ -1161,6 +1204,57 @@ public class Prism implements PrismSettingsListener
}
}
public void exportStatesToFile(Model model, int exportType, File file) throws FileNotFoundException
{
int i;
PrismLog tmpLog;
// no specific states format for MRMC
if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN;
// rows format does not apply to states output
if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN;
// print message
mainLog.print("\nExporting list of reachable states ");
switch (exportType) {
case EXPORT_PLAIN: mainLog.print("in plain text format "); break;
case EXPORT_MATLAB: mainLog.print("in Matlab format "); break;
}
if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:");
// create new file log or use main log
if (file != null) {
tmpLog = new PrismFileLog(file.getPath());
if (!tmpLog.ready()) {
throw new FileNotFoundException();
}
} else {
tmpLog = mainLog;
}
// print header: list of model vars
if (exportType == EXPORT_MATLAB) tmpLog.print("% ");
tmpLog.print("(");
for (i = 0; i < model.getNumVars(); i++) {
tmpLog.print(model.getVarName(i));
if (i < model.getNumVars()-1) tmpLog.print(",");
}
tmpLog.println(")");
if (exportType == EXPORT_MATLAB) tmpLog.println("states=[");
// print states
if (exportType != EXPORT_MATLAB)
model.getReachableStates().print(tmpLog);
else
model.getReachableStates().printMatlab(tmpLog);
// print footer
if (exportType == EXPORT_MATLAB) tmpLog.println("];");
// tidy up
if (file != null) tmpLog.close();
}
// model checking
// returns result or throws an exception in case of error

25
prism/src/prism/PrismCL.java
View File

@ -52,6 +52,7 @@ public class PrismCL
private boolean exportspy = false;
private boolean exportdot = false;
private boolean exporttransdot = false;
private boolean exportbsccs = false;
private boolean exportresults = false;
private boolean exportPlainDeprecated = false;
private int exportType = Prism.EXPORT_PLAIN;
@ -85,6 +86,7 @@ public class PrismCL
private String exportSpyFilename = null;
private String exportDotFilename = null;
private String exportTransDotFilename = null;
private String exportBSCCsFilename = null;
private String exportResultsFilename = null;
private String simpathFilename = null;
@ -676,6 +678,18 @@ public class PrismCL
error("Couldn't open file \"" + exportTransDotFilename + "\" for output");
}
}
// export BSCCs to a file
if (exportbsccs) {
try {
File f = (exportBSCCsFilename.equals("stdout")) ? null : new File(exportBSCCsFilename);
prism.exportBSCCsToFile(model, exportType, f);
}
// in case of error, report it and proceed
catch (FileNotFoundException e) {
error("Couldn't open file \"" + exportBSCCsFilename + "\" for output");
}
}
}
// do steady state computation (if required)
@ -881,6 +895,16 @@ public class PrismCL
errorAndExit("No file specified for -"+sw+" switch");
}
}
// export bsccs to file
else if (sw.equals("exportbsccs")) {
if (i < args.length-1) {
exportbsccs = true;
exportBSCCsFilename = args[++i];
}
else {
errorAndExit("No file specified for -"+sw+" switch");
}
}
// export results
else if (sw.equals("exportresults")) {
if (i < args.length-1) {
@ -1499,6 +1523,7 @@ public class PrismCL
mainLog.println("-exportunordered ............... When exporting matrices, don't order entries");
mainLog.println("-exporttransdot <file> ......... Export the transition matrix graph to a dot file");
mainLog.println("-exportdot <file> .............. Export the transition matrix MTBDD to a dot file");
mainLog.println("-exportbsccs <file> ............ Compute and export all BSCCs of the model");
mainLog.println();
mainLog.println("-mtbdd (or -m) ................. Use the MTBDD engine");
mainLog.println("-sparse (or -s) ................ Use the Sparse engine");

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

@ -50,7 +50,7 @@ public class SCCComputerXB implements SCCComputer
private Vector<JDDNode> vectBSCCs;
private JDDNode notInBSCCs;
public SCCComputerXB(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars) throws PrismException
public SCCComputerXB(Prism prism, JDDNode reach, JDDNode trans01, JDDVars allDDRowVars, JDDVars allDDColVars)
{
// initialise
mainLog = prism.getMainLog();

Write Preview
Loading…
Cancel
Save