From 3ba831c8cb85b6e8d15561dbd65dd6c1f3d234bf Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 12 Jul 2008 21:08:05 +0000 Subject: [PATCH] New -exportbsccs option (currently does SCCs though). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@807 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 20 +---- prism/src/prism/Prism.java | 120 ++++++++++++++++++++++++--- prism/src/prism/PrismCL.java | 25 ++++++ prism/src/prism/SCCComputerXB.java | 2 +- 4 files changed, 135 insertions(+), 32 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index c6523986..cb770cf8 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -488,6 +488,7 @@ public class LTLModelChecker Stack candidates = new Stack(); candidates.push(states); Vector ecs = new Vector(); + 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 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); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 956dec2d..c1811c4d 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -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 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 diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 80a4b8b9..bea5e6fd 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -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 ......... Export the transition matrix graph to a dot file"); mainLog.println("-exportdot .............. Export the transition matrix MTBDD to a dot file"); + mainLog.println("-exportbsccs ............ 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"); diff --git a/prism/src/prism/SCCComputerXB.java b/prism/src/prism/SCCComputerXB.java index aa504d42..d79ae92a 100644 --- a/prism/src/prism/SCCComputerXB.java +++ b/prism/src/prism/SCCComputerXB.java @@ -50,7 +50,7 @@ public class SCCComputerXB implements SCCComputer private Vector 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();