Improved file handling especially property file (#644)

src/storm-cli-utilities/model-handling.h

@@ -635,20 +635,20 @@ void exportSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>
 
     if (ioSettings.isExportBuildSet()) {
         switch (ioSettings.getExportBuildFormat()) {
-            case storm::exporter::ModelExportFormat::Dot:
+            case storm::io::ModelExportFormat::Dot:
                 storm::api::exportSparseModelAsDot(model, ioSettings.getExportBuildFilename(), ioSettings.getExportDotMaxWidth());
                 break;
-            case storm::exporter::ModelExportFormat::Drn:
+            case storm::io::ModelExportFormat::Drn:
                 storm::api::exportSparseModelAsDrn(model, ioSettings.getExportBuildFilename(),
                                                    input.model ? input.model.get().getParameterNames() : std::vector<std::string>(),
                                                    !ioSettings.isExplicitExportPlaceholdersDisabled());
                 break;
-            case storm::exporter::ModelExportFormat::Json:
+            case storm::io::ModelExportFormat::Json:
                 storm::api::exportSparseModelAsJson(model, ioSettings.getExportBuildFilename());
                 break;
             default:
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
-                                "Exporting sparse models in " << storm::exporter::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
+                                "Exporting sparse models in " << storm::io::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
         }
     }
 
@@ -675,15 +675,15 @@ void exportDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueT
 
     if (ioSettings.isExportBuildSet()) {
         switch (ioSettings.getExportBuildFormat()) {
-            case storm::exporter::ModelExportFormat::Dot:
+            case storm::io::ModelExportFormat::Dot:
                 storm::api::exportSymbolicModelAsDot(model, ioSettings.getExportBuildFilename());
                 break;
-            case storm::exporter::ModelExportFormat::Drdd:
+            case storm::io::ModelExportFormat::Drdd:
                 storm::api::exportSymbolicModelAsDrdd(model, ioSettings.getExportBuildFilename());
                 break;
             default:
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException,
-                                "Exporting symbolic models in " << storm::exporter::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
+                                "Exporting symbolic models in " << storm::io::toString(ioSettings.getExportBuildFormat()) << " format is not supported.");
         }
     }
 

src/storm-conv/api/storm-conv.cpp

@@ -142,17 +142,17 @@ void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani:
 
 void exportPrismToFile(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
     std::ofstream stream;
-    storm::utility::openFile(filename, stream);
+    storm::io::openFile(filename, stream);
     stream << program << '\n';
-    storm::utility::closeFile(stream);
+    storm::io::closeFile(stream);
 
     if (!properties.empty()) {
-        storm::utility::openFile(filename + ".props", stream);
+        storm::io::openFile(filename + ".props", stream);
         for (auto const& prop : properties) {
             stream << prop.asPrismSyntax() << '\n';
             STORM_LOG_WARN_COND(!prop.containsUndefinedConstants(), "A property contains undefined constants. These might not be exported correctly.");
         }
-        storm::utility::closeFile(stream);
+        storm::io::closeFile(stream);
     }
 }
 void printPrismToStream(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::ostream& ostream) {

src/storm-counterexamples/counterexamples/PathCounterexample.cpp

@@ -29,7 +29,7 @@ void PathCounterexample<ValueType>::writeToStream(std::ostream& out) const {
                 out << ": " << model->getStateValuations().getStateInfo(*it);
             }
             out << ": {";
-            storm::utility::outputFixedWidth(out, model->getLabelsOfState(*it), 0);
+            storm::io::outputFixedWidth(out, model->getLabelsOfState(*it), 0);
             out << "}\n";
         }
     }

src/storm-dft/modelchecker/DFTASFChecker.cpp

@@ -503,7 +503,7 @@ void DFTASFChecker::addMarkovianConstraints() {
 
 void DFTASFChecker::toFile(std::string const &filename) {
     std::ofstream stream;
-    storm::utility::openFile(filename, stream);
+    storm::io::openFile(filename, stream);
     stream << "; time point variables\n";
     for (auto const &timeVarEntry : timePointVariables) {
         stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)\n";
@@ -533,7 +533,7 @@ void DFTASFChecker::toFile(std::string const &filename) {
         stream << "(assert " << constraint->toSmtlib2(varNames) << ")\n";
     }
     stream << "(check-sat)\n";
-    storm::utility::closeFile(stream);
+    storm::io::closeFile(stream);
 }
 
 void DFTASFChecker::toSolver() {

src/storm-dft/parser/DFTGalileoParser.cpp

@@ -23,14 +23,14 @@ storm::dft::storage::DFT<ValueType> DFTGalileoParser<ValueType>::parseDFT(const
     const std::regex commentRegex("(/\\*([^*]|(\\*+[^*/]))*\\*+/)|(//.*)");
 
     std::ifstream file;
-    storm::utility::openFile(filename, file);
+    storm::io::openFile(filename, file);
 
     std::string line;
     size_t lineNo = 0;
     std::string toplevelId = "";
     bool comment = false;  // Indicates whether the current line is part of a multiline comment
     try {
-        while (storm::utility::getline(file, line)) {
+        while (storm::io::getline(file, line)) {
             ++lineNo;
             // First consider comments
             if (comment) {
@@ -147,7 +147,7 @@ storm::dft::storage::DFT<ValueType> DFTGalileoParser<ValueType>::parseDFT(const
         STORM_LOG_THROW(false, storm::exceptions::FileIoException, "A parsing exception occurred in line " << lineNo << ": " << exception.what());
     }
     builder.setTopLevel(toplevelId);
-    storm::utility::closeFile(file);
+    storm::io::closeFile(file);
 
     // Build DFT
     storm::dft::storage::DFT<ValueType> dft = builder.build();

src/storm-dft/parser/DFTJsonParser.cpp

@@ -18,10 +18,10 @@ namespace parser {
 template<typename ValueType>
 storm::dft::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJsonFromFile(std::string const& filename) {
     std::ifstream file;
-    storm::utility::openFile(filename, file);
+    storm::io::openFile(filename, file);
     Json jsonInput;
     file >> jsonInput;
-    storm::utility::closeFile(file);
+    storm::io::closeFile(file);
     return parseJson(jsonInput);
 }
 

src/storm-dft/storage/DftJsonExporter.cpp

@@ -14,9 +14,9 @@ namespace storage {
 template<typename ValueType>
 void DftJsonExporter<ValueType>::toFile(storm::dft::storage::DFT<ValueType> const& dft, std::string const& filepath) {
     std::ofstream stream;
-    storm::utility::openFile(filepath, stream);
+    storm::io::openFile(filepath, stream);
     toStream(dft, stream);
-    storm::utility::closeFile(stream);
+    storm::io::closeFile(stream);
 }
 
 template<typename ValueType>

src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp

@@ -75,7 +75,7 @@ template<storm::dd::DdType DdType, typename ValueType>
 void MenuGameAbstractor<DdType, ValueType>::exportToDot(storm::gbar::abstraction::MenuGame<DdType, ValueType> const& currentGame, std::string const& filename,
                                                         storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
     std::ofstream out;
-    storm::utility::openFile(filename, out);
+    storm::io::openFile(filename, out);
     AbstractionInformation<DdType> const& abstractionInformation = this->getAbstractionInformation();
 
     storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame.getTransitionMatrix();
@@ -172,7 +172,7 @@ void MenuGameAbstractor<DdType, ValueType>::exportToDot(storm::gbar::abstraction
     }
 
     out << "}\n";
-    storm::utility::closeFile(out);
+    storm::io::closeFile(out);
 }
 
 template<storm::dd::DdType DdType, typename ValueType>

src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -1,17 +1,32 @@
 #include "storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 
+#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.h"
+#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h"
+#include "storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h"
+#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h"
+#include "storm/environment/Environment.h"
+#include "storm/exceptions/InvalidModelException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/io/file.h"
+#include "storm/logic/FragmentSpecification.h"
 #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
+#include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
-
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Mdp.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
-
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/solver/StandardGameSolver.h"
+#include "storm/solver/SymbolicGameSolver.h"
+#include "storm/storage/ExplicitGameStrategyPair.h"
+#include "storm/storage/dd/DdManager.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/storage/expressions/VariableSetPredicateSplitter.h"
-
-#include "storm/storage/ExplicitGameStrategyPair.h"
 #include "storm/storage/jani/Automaton.h"
 #include "storm/storage/jani/AutomatonComposition.h"
 #include "storm/storage/jani/Edge.h"
@@ -20,37 +35,10 @@
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/visitor/CompositionInformationVisitor.h"
-
-#include "storm/storage/dd/DdManager.h"
-
-#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h"
-#include "storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h"
-#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h"
-
-#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.h"
-#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.h"
-
-#include "storm/logic/FragmentSpecification.h"
-
-#include "storm/environment/Environment.h"
-#include "storm/solver/StandardGameSolver.h"
-#include "storm/solver/SymbolicGameSolver.h"
-
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/modules/CoreSettings.h"
-#include "storm/settings/modules/GeneralSettings.h"
-
 #include "storm/utility/macros.h"
 #include "storm/utility/prism.h"
-
 #include "storm/utility/vector.h"
 
-#include "storm/exceptions/InvalidModelException.h"
-#include "storm/exceptions/InvalidPropertyException.h"
-#include "storm/exceptions/NotSupportedException.h"
-
-#include "storm/modelchecker/results/CheckResult.h"
-
 namespace storm::gbar {
 namespace modelchecker {
 
@@ -989,9 +977,11 @@ class ExplicitGameExporter {
                       ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, storage::ExplicitGameStrategyPair const* minStrategyPair,
                       storage::ExplicitGameStrategyPair const* maxStrategyPair) {
         // Export game as json.
-        std::ofstream outfile(filename);
+        std::ofstream outfile;
+        storm::io::openFile(filename, outfile);
         exportGame(outfile, player1Groups, player2Groups, transitionMatrix, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair,
                    maxStrategyPair);
+        storm::io::closeFile(outfile);
     }
 
     void setShowNonStrategyAlternatives(bool value) {

src/storm-gspn/api/storm-gspn.cpp

@@ -22,30 +22,30 @@ void handleGSPNExportSettings(storm::gspn::GSPN const& gspn,
     storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>();
     if (exportSettings.isWriteToDotSet()) {
         std::ofstream fs;
-        storm::utility::openFile(exportSettings.getWriteToDotFilename(), fs);
+        storm::io::openFile(exportSettings.getWriteToDotFilename(), fs);
         gspn.writeDotToStream(fs);
-        storm::utility::closeFile(fs);
+        storm::io::closeFile(fs);
     }
 
     if (exportSettings.isWriteToPnproSet()) {
         std::ofstream fs;
-        storm::utility::openFile(exportSettings.getWriteToPnproFilename(), fs);
+        storm::io::openFile(exportSettings.getWriteToPnproFilename(), fs);
         gspn.toPnpro(fs);
-        storm::utility::closeFile(fs);
+        storm::io::closeFile(fs);
     }
 
     if (exportSettings.isWriteToPnmlSet()) {
         std::ofstream fs;
-        storm::utility::openFile(exportSettings.getWriteToPnmlFilename(), fs);
+        storm::io::openFile(exportSettings.getWriteToPnmlFilename(), fs);
         gspn.toPnml(fs);
-        storm::utility::closeFile(fs);
+        storm::io::closeFile(fs);
     }
 
     if (exportSettings.isWriteToJsonSet()) {
         std::ofstream fs;
-        storm::utility::openFile(exportSettings.getWriteToJsonFilename(), fs);
+        storm::io::openFile(exportSettings.getWriteToJsonFilename(), fs);
         gspn.toJson(fs);
-        storm::utility::closeFile(fs);
+        storm::io::closeFile(fs);
     }
 
     if (exportSettings.isDisplayStatsSet()) {
@@ -56,9 +56,9 @@ void handleGSPNExportSettings(storm::gspn::GSPN const& gspn,
 
     if (exportSettings.isWriteStatsToFileSet()) {
         std::ofstream fs;
-        storm::utility::openFile(exportSettings.getWriteStatsFilename(), fs);
+        storm::io::openFile(exportSettings.getWriteStatsFilename(), fs);
         gspn.writeStatsToStream(fs);
-        storm::utility::closeFile(fs);
+        storm::io::closeFile(fs);
     }
 
     if (exportSettings.isWriteToJaniSet()) {
@@ -93,10 +93,10 @@ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const&
     std::unordered_map<std::string, uint64_t> map;
 
     std::ifstream stream;
-    storm::utility::openFile(filename, stream);
+    storm::io::openFile(filename, stream);
 
     std::string line;
-    while (storm::utility::getline(stream, line)) {
+    while (storm::io::getline(stream, line)) {
         std::vector<std::string> strs;
         boost::split(strs, line, boost::is_any_of("\t "));
         STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs");
@@ -108,7 +108,7 @@ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const&
                         "The capacity expression '" << strs[1] << "' still contains undefined constants.");
         map[strs[0]] = expr.evaluateAsInt();
     }
-    storm::utility::closeFile(stream);
+    storm::io::closeFile(stream);
     return map;
 }
 }  // namespace api

src/storm-pars-cli/monotonicity.cpp

@@ -37,7 +37,7 @@ void analyzeMonotonicity(std::shared_ptr<storm::models::sparse::Model<ValueType>
     auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
 
     if (monSettings.isExportMonotonicitySet()) {
-        storm::utility::openFile(monSettings.getExportMonotonicityFilename(), outfile);
+        storm::io::openFile(monSettings.getExportMonotonicityFilename(), outfile);
     }
     std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
     storm::utility::Stopwatch monotonicityWatch(true);
@@ -99,7 +99,7 @@ void analyzeMonotonicity(std::shared_ptr<storm::models::sparse::Model<ValueType>
     }
 
     if (monSettings.isExportMonotonicitySet()) {
-        storm::utility::closeFile(outfile);
+        storm::io::closeFile(outfile);
     }
 
     monotonicityWatch.stop();

src/storm-pars/analysis/MonotonicityHelper.cpp

@@ -136,7 +136,7 @@ MonotonicityHelper<ValueType, ConstantType>::checkMonotonicityInBuild(std::ostre
         while (i < 10 && orderItr != monResults.end()) {
             std::ofstream dotOutfile;
             std::string name = dotOutfileName + std::to_string(i);
-            utility::openFile(name, dotOutfile);
+            storm::io::openFile(name, dotOutfile);
             dotOutfile << "Assumptions:\n";
             auto assumptionItr = orderItr->second.second.begin();
             while (assumptionItr != orderItr->second.second.end()) {
@@ -146,7 +146,7 @@ MonotonicityHelper<ValueType, ConstantType>::checkMonotonicityInBuild(std::ostre
             }
             dotOutfile << '\n';
             orderItr->first->dotOutputToFile(dotOutfile);
-            utility::closeFile(dotOutfile);
+            storm::io::closeFile(dotOutfile);
             i++;
             orderItr++;
         }

src/storm-pars/api/export.h

@@ -17,7 +17,7 @@ inline void exportParametricResultToFile(std::optional<storm::RationalFunction>
                                          storm::OptionalRef<storm::analysis::ConstraintCollector<storm::RationalFunction> const> const& constraintCollector,
                                          std::string const& path) {
     std::ofstream filestream;
-    storm::utility::openFile(path, filestream);
+    storm::io::openFile(path, filestream);
     if (constraintCollector.has_value()) {
         filestream << "$Parameters: ";
         auto const& vars = constraintCollector->getVariables();
@@ -48,7 +48,7 @@ inline void exportParametricResultToFile(std::optional<storm::RationalFunction>
                        [](carl::Formula<typename storm::Polynomial::PolyType> const& c) -> std::string { return c.toString(); });
         std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator<std::string>(filestream, "\n"));
     }
-    storm::utility::closeFile(filestream);
+    storm::io::closeFile(filestream);
 }
 }  // namespace api
 }  // namespace storm