From dfce095d450345ebb8205756acd98a0b4677167f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 29 Apr 2014 19:46:35 +0000 Subject: [PATCH] Make sure that some PrismFileLogs are close()ed after use - spotted as a bug by Bruno. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8168 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 2 ++ prism/src/explicit/STPGModelChecker.java | 1 + prism/src/prism/NondetModelChecker.java | 4 +++- prism/src/prism/ProbModelChecker.java | 4 +++- prism/src/simulator/SimulatorEngine.java | 2 ++ 5 files changed, 11 insertions(+), 2 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 6bacb884..55902975 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -584,6 +584,7 @@ public class MDPModelChecker extends ProbModelChecker // Export PrismLog out = new PrismFileLog(exportAdvFilename); new DTMCFromMDPMemorylessAdversary(mdp, strat).exportToPrismExplicitTra(out); + out.close(); } // Update time taken @@ -1481,6 +1482,7 @@ public class MDPModelChecker extends ProbModelChecker // Export PrismLog out = new PrismFileLog(exportAdvFilename); new DTMCFromMDPMemorylessAdversary(mdp, strat).exportToPrismExplicitTra(out); + out.close(); } // Finished expected reachability diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 8ac7ce33..bda97150 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -644,6 +644,7 @@ public class STPGModelChecker extends ProbModelChecker out.println(i + " " + (adv[i] != -1 ? stpg.getAction(i, adv[i]) : "-")); } out.println(); + out.close(); } // Return results diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 72588c42..4c7b9487 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1495,7 +1495,9 @@ public class NondetModelChecker extends NonProbModelChecker } if (prism.getExportProductStates()) { mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"..."); - modelProduct.exportStates(Prism.EXPORT_PLAIN, new PrismFileLog(prism.getExportProductStatesFilename())); + PrismFileLog out = new PrismFileLog(prism.getExportProductStatesFilename()); + modelProduct.exportStates(Prism.EXPORT_PLAIN, out); + out.close(); } // Find accepting MECs + compute reachability probabilities diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index ffed90ff..e660feed 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -603,7 +603,9 @@ public class ProbModelChecker extends NonProbModelChecker } if (prism.getExportProductStates()) { mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"..."); - modelProduct.exportStates(Prism.EXPORT_PLAIN, new PrismFileLog(prism.getExportProductStatesFilename())); + PrismFileLog out = new PrismFileLog(prism.getExportProductStatesFilename()); + modelProduct.exportStates(Prism.EXPORT_PLAIN, out); + out.close(); } // Find accepting BSCCs + compute reachability probabilities diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 45efadd6..d3b0c534 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -1319,6 +1319,8 @@ public class SimulatorEngine extends PrismComponent log.println(); } ((PathFull) path).exportToLog(log, timeCumul, colSep, vars); + if (file != null) + log.close(); } /**