From 256137b0809b504dd54e991793a2e39daf919d0c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 5 Apr 2019 19:10:14 +0200 Subject: [PATCH] Some refactoring --- src/storm-dft-cli/storm-dft.cpp | 34 ++++++++++++++++++--------------- src/storm-dft/api/storm-dft.h | 19 +++++++----------- 2 files changed, 26 insertions(+), 27 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 0514e63d0..a804a798d 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -1,17 +1,17 @@ +#include #include "storm-dft/api/storm-dft.h" #include "storm-dft/settings/DftSettings.h" +#include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" -#include "storm-dft/settings/modules/DftGspnSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/ResourceSettings.h" -#include "storm/settings/modules/GeneralSettings.h" - - -#include "storm-parsers/api/storm-parsers.h" #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" +#include "storm-parsers/api/storm-parsers.h" + /*! * Process commandline options and start computations. @@ -28,7 +28,7 @@ void processOptions() { if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); } // Build DFT from given file @@ -48,13 +48,12 @@ void processOptions() { if (dftIOSettings.isExportToJson()) { // Export to json storm::api::exportDFTToJsonFile(*dft, dftIOSettings.getExportJsonFilename()); - return; } // Check well-formedness of DFT std::stringstream stream; if (!dft->checkWellFormedness(stream)) { - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "DFT is not well-formed: " << stream.str()); + STORM_LOG_THROW(false, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << stream.str()); } if (dftGspnSettings.isTransformToGspn()) { @@ -82,14 +81,16 @@ void processOptions() { } #endif + // From now on we analyse DFT via model checking + // Set min or max std::string optimizationDirection = "min"; if (dftIOSettings.isComputeMaximalValue()) { - STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); optimizationDirection = "max"; } - // Construct properties to analyse + // Construct properties to analyse. + // We allow multiple properties to be checked at once. std::vector properties; if (ioSettings.isPropertySet()) { properties.push_back(ioSettings.getProperty()); @@ -114,10 +115,13 @@ void processOptions() { } // Build properties - STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidSettingsException, "No property given."); - std::string propString = properties[0]; - for (size_t i = 1; i < properties.size(); ++i) { - propString += ";" + properties[i]; + STORM_LOG_WARN_COND(!properties.empty(), "No property given."); + std::string propString; + for (size_t i = 0; i < properties.size(); ++i) { + if (i + 1 < properties.size()) { + propString += ";"; + } + propString += properties[i]; } std::vector> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString)); @@ -159,7 +163,7 @@ void processOptions() { * * @param argc The argc argument of main(). * @param argv The argv argument of main(). - * @return Return code, 0 if successfull, not 0 otherwise. + * @return Return code, 0 if successful, > 0 otherwise. */ int main(const int argc, const char** argv) { try { diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index f36bfc3ca..f801b0eda 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -5,11 +5,10 @@ #include "storm-dft/parser/DFTGalileoParser.h" #include "storm-dft/parser/DFTJsonParser.h" #include "storm-dft/storage/dft/DftJsonExporter.h" - #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" - #include "storm-dft/transformations/DftToGspnTransformator.h" + #include "storm-gspn/api/storm-gspn.h" namespace storm { @@ -19,38 +18,35 @@ namespace storm { * Load DFT from Galileo file. * * @param file File containing DFT description in Galileo format. - * * @return DFT. */ template std::shared_ptr> loadDFTGalileoFile(std::string const& file) { - return std::make_shared>(storm::parser::DFTGalileoParser::parseDFT(file)); + return std::make_shared>(storm::parser::DFTGalileoParser::parseDFT(file)); } /*! * Load DFT from JSON string. * * @param jsonString String containing DFT description in JSON format. - * * @return DFT. */ template std::shared_ptr> loadDFTJsonString(std::string const& jsonString) { - storm::parser::DFTJsonParser parser; - return std::make_shared>(parser.parseJsonFromString(jsonString)); + storm::parser::DFTJsonParser parser; + return std::make_shared>(parser.parseJsonFromString(jsonString)); } /*! * Load DFT from JSON file. * * @param file File containing DFT description in JSON format. - * * @return DFT. */ template std::shared_ptr> loadDFTJsonFile(std::string const& file) { - storm::parser::DFTJsonParser parser; - return std::make_shared>(parser.parseJsonFromFile(file)); + storm::parser::DFTJsonParser parser; + return std::make_shared>(parser.parseJsonFromFile(file)); } /*! @@ -107,6 +103,7 @@ namespace storm { * Export DFT to JSON string. * * @param dft DFT. + * @return DFT in JSON format. */ template std::string exportDFTToJsonString(storm::storage::DFT const& dft); @@ -124,7 +121,6 @@ namespace storm { * Transform DFT to GSPN. * * @param dft DFT. - * * @return Pair of GSPN and id of failed place corresponding to the top level element. */ template @@ -135,7 +131,6 @@ namespace storm { * * @param gspn GSPN. * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT. - * * @return JANI model. */ std::shared_ptr transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace);