diff --git a/prism/src/automata/DA.java b/prism/src/automata/DA.java index 896f7aee..7b3bc5b4 100644 --- a/prism/src/automata/DA.java +++ b/prism/src/automata/DA.java @@ -323,6 +323,24 @@ public class DA } } + /** + * Print automaton to a PrintStream in a specified format ("dot", "txt" or "hoa"). + */ + public void print(PrintStream out, String type) throws PrismException + { + switch (type) { + case "txt": + out.println(toString()); + break; + case "dot": + printDot(out); + break; + case "hoa": + printHOA(out); + break; + } + } + // Standard methods @Override diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index cca48098..531d1092 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -28,6 +28,7 @@ package explicit; import java.awt.Point; +import java.io.PrintStream; import java.util.ArrayList; import java.util.Arrays; import java.util.BitSet; @@ -49,10 +50,9 @@ import parser.type.TypePathBool; import prism.ModelType; import prism.PrismComponent; import prism.PrismException; -import prism.PrismFileLog; import prism.PrismLangException; -import prism.PrismLog; import prism.PrismNotSupportedException; +import prism.PrismUtils; import acceptance.AcceptanceGenRabin; import acceptance.AcceptanceOmega; import acceptance.AcceptanceRabin; @@ -60,6 +60,7 @@ import acceptance.AcceptanceStreett; import acceptance.AcceptanceType; import automata.DA; import automata.LTL2DA; + import common.IterableStateSet; /** @@ -250,7 +251,7 @@ public class LTLModelChecker extends PrismComponent // If required, export DA if (settings.getExportPropAut()) { mainLog.println("Exporting " + da.getAutomataType() + " to file \"" + settings.getExportPropAutFilename() + "\"..."); - PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); + PrintStream out = PrismUtils.newPrintStream(settings.getExportPropAutFilename()); da.print(out, settings.getExportPropAutType()); out.close(); } diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index 60e12fd4..d4032200 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -29,6 +29,7 @@ package prism; import java.io.FileNotFoundException; +import java.io.PrintStream; import java.util.ArrayList; import java.util.Arrays; import java.util.BitSet; @@ -93,7 +94,7 @@ public class MultiObjModelChecker extends PrismComponent if (prism.getSettings().getExportPropAut()) { String exportPropAutFilename = PrismUtils.addCounterSuffixToFilename(prism.getSettings().getExportPropAutFilename(), i + 1); mainLog.println("Exporting DRA to file \"" + exportPropAutFilename + "\"..."); - PrismLog out = new PrismFileLog(exportPropAutFilename); + PrintStream out = PrismUtils.newPrintStream(exportPropAutFilename); dra[i].print(out, settings.getExportPropAutType()); out.close(); } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index eefb5406..72f5d0de 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -33,6 +33,7 @@ import hybrid.PrismHybrid; import java.io.File; import java.io.FileNotFoundException; +import java.io.PrintStream; import java.util.ArrayList; import java.util.BitSet; import java.util.List; @@ -1180,7 +1181,7 @@ public class NondetModelChecker extends NonProbModelChecker // If required, export DA if (prism.getSettings().getExportPropAut()) { mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); + PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); da.print(out, prism.getSettings().getExportPropAutType()); out.close(); } @@ -1427,7 +1428,7 @@ public class NondetModelChecker extends NonProbModelChecker // If required, export DA if (prism.getSettings().getExportPropAut()) { mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); + PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); da.print(out, prism.getSettings().getExportPropAutType()); out.close(); //da.printDot(new java.io.PrintStream("da.dot")); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index c01b44b6..536c82ac 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -1500,6 +1500,8 @@ public class PrismSettings implements Observer setExportPropAutType("txt"); } else if (option.getKey().equals("dot")) { setExportPropAutType("dot"); + } else if (option.getKey().equals("hoa")) { + setExportPropAutType("hoa"); } else { throw new PrismException("Unknown option \"" + option.getKey() + "\" for -" + sw + " switch"); } diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index b7a5161e..877d7204 100644 --- a/prism/src/prism/PrismUtils.java +++ b/prism/src/prism/PrismUtils.java @@ -26,6 +26,8 @@ package prism; +import java.io.FileNotFoundException; +import java.io.PrintStream; import java.text.DecimalFormat; import java.text.DecimalFormatSymbols; import java.util.List; @@ -336,6 +338,18 @@ public class PrismUtils System.out.println(s + " => " + PrismUtils.convertMemoryStringtoKB(s) * 1024 + " => " + PrismUtils.convertBytesToMemoryString(PrismUtils.convertMemoryStringtoKB(s) * 1024)); }*/ } + + /** + * Utility method to create a new PrintStream for a file, but any errors are converted to PrismExceptions + */ + public static PrintStream newPrintStream(String filename) throws PrismException + { + try { + return new PrintStream(filename); + } catch (FileNotFoundException e) { + throw new PrismException("File \"" + filename + "\" could not opened for output"); + } + } } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index aae22239..19fb8c05 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -30,6 +30,7 @@ import hybrid.PrismHybrid; import java.io.File; import java.io.FileNotFoundException; +import java.io.PrintStream; import java.util.BitSet; import java.util.List; import java.util.Vector; @@ -558,7 +559,7 @@ public class ProbModelChecker extends NonProbModelChecker // If required, export DA if (prism.getSettings().getExportPropAut()) { mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); + PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); da.print(out, prism.getSettings().getExportPropAutType()); out.close(); } @@ -962,7 +963,7 @@ public class ProbModelChecker extends NonProbModelChecker // If required, export DA if (prism.getSettings().getExportPropAut()) { mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename()); + PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); da.print(out, prism.getSettings().getExportPropAutType()); out.close(); //da.printDot(new java.io.PrintStream("da.dot"));