From b4f05f3cd051c638b09c11d5b51455c1801a8c06 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 14 Jun 2015 22:51:59 +0000 Subject: [PATCH] Add possibility to specify type to -exportpropaut switch (dot or txt), e.g. -exportpropaut:dot dra.dot. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10018 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 3 +- prism/src/prism/MultiObjModelChecker.java | 3 +- prism/src/prism/NondetModelChecker.java | 3 +- prism/src/prism/PrismSettings.java | 68 ++++++++++++++++++++--- prism/src/prism/ProbModelChecker.java | 3 +- 5 files changed, 65 insertions(+), 15 deletions(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 695c9d47..7216ad06 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -248,9 +248,8 @@ public class LTLModelChecker extends PrismComponent if (settings.getExportPropAut()) { mainLog.println("Exporting " + da.getAutomataType() + " to file \"" + settings.getExportPropAutFilename() + "\"..."); PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); - out.println(da); + da.print(out, settings.getExportPropAutType()); out.close(); - //dra.printDot(new java.io.PrintStream("da.dot")); } return da; diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index b71e1eb1..49b598fa 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -92,9 +92,8 @@ public class MultiObjModelChecker extends PrismComponent String exportPropAutFilename = PrismUtils.addCounterSuffixToFilename(prism.getSettings().getExportPropAutFilename(), i + 1); mainLog.println("Exporting DRA to file \"" + exportPropAutFilename + "\"..."); PrismLog out = new PrismFileLog(exportPropAutFilename); - out.println(dra[i]); + dra[i].print(out, settings.getExportPropAutType()); out.close(); - //dra.printDot(new java.io.PrintStream("dra.dot")); } // Build product of MDP and automaton diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 5cb46635..594337ea 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1017,9 +1017,8 @@ public class NondetModelChecker extends NonProbModelChecker if (prism.getSettings().getExportPropAut()) { mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); - out.println(da); + da.print(out, prism.getSettings().getExportPropAutType()); out.close(); - //da.printDot(new java.io.PrintStream("da.dot")); } // Build product of MDP and automaton diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index fbef2e46..d751b77c 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -31,6 +31,7 @@ package prism; import java.util.*; import java.io.*; import java.awt.*; + import javax.swing.*; import explicit.QuantAbstractRefine; @@ -811,6 +812,7 @@ public class PrismSettings implements Observer // Export property automaton info? protected boolean exportPropAut = false; + protected String exportPropAutType = null; protected String exportPropAutFilename = null; public void setExportPropAut(boolean b) throws PrismException @@ -818,6 +820,11 @@ public class PrismSettings implements Observer exportPropAut = b; } + public void setExportPropAutType(String s) throws PrismException + { + exportPropAutType = s; + } + public void setExportPropAutFilename(String s) throws PrismException { exportPropAutFilename = s; @@ -828,6 +835,11 @@ public class PrismSettings implements Observer return exportPropAut; } + public String getExportPropAutType() + { + return exportPropAutType; + } + public String getExportPropAutFilename() { return exportPropAutFilename; @@ -843,16 +855,15 @@ public class PrismSettings implements Observer */ public synchronized int setFromCommandLineSwitch(String args[], int i) throws PrismException { - String sw, s; + String s; int j; double d; - // Remove "-" - sw = args[i].substring(1); - // Remove optional second "-" (i.e. we allow switches of the form --sw too) - if (sw.charAt(0) == '-') - sw = sw.substring(1); - + // Process string (remove - and extract any options) + Pair> pair = splitSwitch(args[i]); + String sw = pair.first; + Map options = pair.second; + // Note: the order of these switches should match the -help output (just to help keep track of things). // ENGINES/METHODS: @@ -1443,6 +1454,15 @@ public class PrismSettings implements Observer if (i < args.length - 1) { setExportPropAut(true); setExportPropAutFilename(args[++i]); + for (Map.Entry option : options.entrySet()) { + if (option.getKey().equals("txt")) { + setExportPropAutType("txt"); + } else if (option.getKey().equals("dot")) { + setExportPropAutType("dot"); + } else { + throw new PrismException("Unknown option \"" + option.getKey() + "\" for -" + sw + " switch"); + } + } } else { throw new PrismException("No file specified for -" + sw + " switch"); } @@ -1456,6 +1476,40 @@ public class PrismSettings implements Observer return i + 1; } + /** + * Split a switch of the form -switch:options into parts. + * The latter can be empty, in which case the : is optional. + * When present, the options is a comma-separated list of "option" or "option=value" items. + * The switch itself can be prefixed with either 1 or 2 hyphens. + * + * @return a pair containing the switch name and a mapping from options to values. + */ + private static Pair> splitSwitch(String sw) throws PrismException + { + // Remove "-" + sw = sw.substring(1); + // Remove optional second "-" (i.e. we allow switches of the form --sw too) + if (sw.charAt(0) == '-') + sw = sw.substring(1); + // Extract options, if present + int i = sw.indexOf(':'); + Map map = new HashMap(); + if (i != -1) { + String optionsString = sw.substring(i + 1); + sw = sw.substring(0, i); + String options[] = optionsString.split(","); + for (String option : options) { + int j = option.indexOf("="); + if (j == -1) { + map.put(option, null); + } else { + map.put(option.substring(0,j), option.substring(j+1)); + } + } + } + return new Pair>(sw, map); + } + /** * Print a fragment of the -help message, * i.e. a list of the command-line switches handled by this class. diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index a8f96834..8224a6ef 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -551,9 +551,8 @@ public class ProbModelChecker extends NonProbModelChecker if (prism.getSettings().getExportPropAut()) { mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); - out.println(da); + da.print(out, prism.getSettings().getExportPropAutType()); out.close(); - //dra.printDot(new java.io.PrintStream("dra.dot")); } // Build product of Markov chain and automaton