From 50e8d24c02371a4dd8a982dd039975bc13ea5ad6 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 19 Dec 2014 00:50:11 +0000 Subject: [PATCH] Add -exportpropaut option (hidden) to export DRA(s) in textual form. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9420 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 15 ++++++++-- prism/src/explicit/MDPModelChecker.java | 13 ++++++-- prism/src/prism/NondetModelChecker.java | 30 +++++++++++++------ prism/src/prism/PrismCL.java | 1 - prism/src/prism/PrismSettings.java | 38 ++++++++++++++++++++++++ prism/src/prism/ProbModelChecker.java | 13 ++++++-- 6 files changed, 91 insertions(+), 19 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 94f0a657..94b7d845 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -38,6 +38,8 @@ import prism.DRA; import prism.Pair; import prism.PrismComponent; import prism.PrismException; +import prism.PrismFileLog; +import prism.PrismLog; import prism.PrismUtils; import explicit.rewards.MCRewards; @@ -84,10 +86,17 @@ public class DTMCModelChecker extends ProbModelChecker time = System.currentTimeMillis(); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); int draSize = dra.size(); - mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); - // dra.print(System.out); + mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); time = System.currentTimeMillis() - time; - mainLog.println("\nTime for Rabin translation: " + time / 1000.0 + " seconds."); + mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds."); + // If required, export DRA + if (settings.getExportPropAut()) { + mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"..."); + PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); + out.println(dra); + out.close(); + //dra.printDot(new java.io.PrintStream("dra.dot")); + } // Build product of Markov chain and automaton mainLog.println("\nConstructing MC-DRA product..."); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 9ae60d5c..f77327cb 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -94,10 +94,17 @@ public class MDPModelChecker extends ProbModelChecker time = System.currentTimeMillis(); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); int draSize = dra.size(); - mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); - // dra.print(System.out); + mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); time = System.currentTimeMillis() - time; - mainLog.println("\nTime for Rabin translation: " + time / 1000.0 + " seconds."); + mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds."); + // If required, export DRA + if (settings.getExportPropAut()) { + mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"..."); + PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); + out.println(dra); + out.close(); + //dra.printDot(new java.io.PrintStream("dra.dot")); + } // Build product of MDP and automaton mainLog.println("\nConstructing MDP-DRA product..."); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index b770ebf8..162bd669 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -673,10 +673,18 @@ public class NondetModelChecker extends NonProbModelChecker mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); long l = System.currentTimeMillis(); dra[i] = LTLModelChecker.convertLTLFormulaToDRA(ltl); - mainLog.print("\nDRA has " + dra[i].size() + " states, " + ", " + dra[i].getNumAcceptancePairs() + " pairs."); - //dra[i].print(System.out); + mainLog.print("DRA has " + dra[i].size() + " states, " + ", " + dra[i].getNumAcceptancePairs() + " pairs."); l = System.currentTimeMillis() - l; - mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); + mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); + // If required, export DRA + if (prism.getSettings().getExportPropAut()) { + String exportPropAutFilename = PrismUtils.addCounterSuffixToFilename(prism.getSettings().getExportPropAutFilename(), i); + mainLog.println("Exporting DRA to file \"" + exportPropAutFilename + "\"..."); + PrismLog out = new PrismFileLog(exportPropAutFilename); + out.println(dra); + out.close(); + //dra.printDot(new java.io.PrintStream("dra.dot")); + } // Build product of MDP and automaton mainLog.println("\nConstructing MDP-DRA product..."); @@ -1469,13 +1477,17 @@ public class NondetModelChecker extends NonProbModelChecker mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); l = System.currentTimeMillis(); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); - mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); - /*try { - mainLog.print(dra); - dra.printDot(new java.io.PrintStream("dra.dot")); - } catch(Exception e) {}*/ + mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); l = System.currentTimeMillis() - l; - mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); + mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); + // If required, export DRA + if (prism.getSettings().getExportPropAut()) { + mainLog.println("Exporting DRA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); + PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); + out.println(dra); + out.close(); + //dra.printDot(new java.io.PrintStream("dra.dot")); + } // Build product of MDP and automaton mainLog.println("\nConstructing MDP-DRA product..."); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 0e9cf767..1fb7b7c6 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -31,7 +31,6 @@ import java.io.FileNotFoundException; import java.util.ArrayList; import java.util.List; -import param.ParamModelChecker; import parser.Values; import parser.ast.Expression; import parser.ast.ExpressionReward; diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index aee1edd2..d593fb02 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -803,7 +803,33 @@ public class PrismSettings implements Observer notifySettingsListeners(); } + + // HIDDEN OPTIONS + + // Export property automaton info? + protected boolean exportPropAut = false; + protected String exportPropAutFilename = null; + public void setExportPropAut(boolean b) throws PrismException + { + exportPropAut = b; + } + + public void setExportPropAutFilename(String s) throws PrismException + { + exportPropAutFilename = s; + } + + public boolean getExportPropAut() + { + return exportPropAut; + } + + public String getExportPropAutFilename() + { + return exportPropAutFilename; + } + /** * Set an option by parsing one or more command-line arguments. * Reads the ith argument (assumed to be in the form "-switch") @@ -1403,6 +1429,18 @@ public class PrismSettings implements Observer } } + // HIDDEN OPTIONS + + // export property automaton to file (hidden option) + else if (sw.equals("exportpropaut")) { + if (i < args.length - 1) { + setExportPropAut(true); + setExportPropAutFilename(args[++i]); + } else { + throw new PrismException("No file specified for -" + sw + " switch"); + } + } + // unknown switch - error else { throw new PrismException("Invalid switch -" + sw + " (type \"prism -help\" for full list)"); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index e660feed..ccfeb71e 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -579,10 +579,17 @@ public class ProbModelChecker extends NonProbModelChecker mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); l = System.currentTimeMillis(); dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); - mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); - // dra.print(System.out); + mainLog.println("DRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); l = System.currentTimeMillis() - l; - mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); + mainLog.println("Time for Rabin translation: " + l / 1000.0 + " seconds."); + // If required, export DRA + if (prism.getExportPropAut()) { + mainLog.println("Exporting DRA to file \"" + prism.getExportPropAutFilename() + "\"..."); + PrismLog out = new PrismFileLog(prism.getExportPropAutFilename()); + out.println(dra); + out.close(); + //dra.printDot(new java.io.PrintStream("dra.dot")); + } // Build product of Markov chain and automaton // (note: might be a CTMC - StochModelChecker extends this class)