From 5d79eff2cd55cdfa4057d2c613fdfabe84363e7e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 14 Feb 2017 18:25:26 +0100 Subject: [PATCH 1/9] Wrapper for file opening --- .../modelchecker/dft/DFTASFChecker.cpp | 23 +++--- src/storm-dft/parser/DFTGalileoParser.cpp | 17 ++-- src/storm-dft/parser/DFTJsonParser.cpp | 14 +--- src/storm-gspn-cli/storm-gspn.cpp | 8 +- src/storm-gspn/storm-gspn.h | 20 ++--- src/storm-pgcl-cli/storm-pgcl.cpp | 11 +-- src/storm-pgcl/parser/PgclParser.cpp | 9 ++- src/storm/abstraction/MenuGameAbstractor.cpp | 5 +- src/storm/cli/entrypoints.h | 8 +- .../modelchecker/region/ParameterRegion.cpp | 5 +- .../AtomicPropositionLabelingParser.cpp | 5 -- .../DeterministicSparseTransitionParser.cpp | 5 -- src/storm/parser/FormulaParser.cpp | 9 ++- src/storm/parser/JaniParser.cpp | 14 +--- src/storm/parser/MappedFile.cpp | 18 ++--- src/storm/parser/MappedFile.h | 8 -- .../MarkovAutomatonSparseTransitionParser.cpp | 5 -- ...NondeterministicSparseTransitionParser.cpp | 5 -- src/storm/parser/PrismParser.cpp | 10 +-- .../parser/SparseChoiceLabelingParser.cpp | 5 -- src/storm/parser/SparseStateRewardParser.cpp | 5 -- src/storm/settings/SettingsManager.cpp | 8 +- src/storm/solver/SmtlibSmtSolver.cpp | 13 +-- src/storm/storage/dd/Odd.cpp | 6 +- src/storm/storage/jani/JSONExporter.cpp | 18 ++--- src/storm/utility/export.h | 15 +--- src/storm/utility/file.h | 81 +++++++++++++++++++ src/storm/utility/storm.h | 13 +-- src/test/parser/MappedFileTest.cpp | 7 +- 29 files changed, 188 insertions(+), 182 deletions(-) create mode 100644 src/storm/utility/file.h diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 0d6cf2e31..55d968a2c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,5 +1,6 @@ #include "DFTASFChecker.h" #include +#include "storm/utility/file.h" namespace storm { @@ -394,24 +395,22 @@ namespace storm { } void DFTASFChecker::toFile(std::string const& filename) { - std::ofstream ofs; - std::cout << "Writing to " << filename << std::endl; - ofs.open(filename); - ofs << "; time point variables" << std::endl; + std::ofstream stream; + storm::utility::openFile(filename, stream); + stream << "; time point variables" << std::endl; for (auto const& timeVarEntry : timePointVariables) { - ofs << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; + stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; } - ofs << "; claim variables" << std::endl; + stream << "; claim variables" << std::endl; for (auto const& claimVarEntry : claimVariables) { - ofs << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; + stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; } for (auto const& constraint : constraints) { - ofs << "; " << constraint->description() << std::endl; - ofs << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; + stream << "; " << constraint->description() << std::endl; + stream << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl; } - ofs << "(check-sat)" << std::endl; - ofs.close(); - + stream << "(check-sat)" << std::endl; + storm::utility::closeFile(stream); } } } diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index f872f4526..c5a88716c 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -10,6 +10,7 @@ #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -49,18 +50,10 @@ namespace storm { std::string parametricToken = "param"; std::ifstream file; - file.exceptions ( std::ifstream::failbit ); - try { - file.open(filename); - } - catch (std::ifstream::failure e) { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << "."); - return; - } - file.exceptions( std::ifstream::goodbit ); - + storm::utility::openFile(filename, file); std::string line; - while(std::getline(file, line)) { + + while (std::getline(file, line)) { bool success = true; STORM_LOG_TRACE("Parsing: " << line); size_t commentstarts = line.find("//"); @@ -143,7 +136,7 @@ namespace storm { if(!builder.setTopLevel(toplevelId)) { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); } - file.close(); + storm::utility::closeFile(file); } template diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 9a5c5d047..faff4a099 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -10,6 +10,7 @@ #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -52,19 +53,10 @@ namespace storm { STORM_LOG_DEBUG("Parsing from JSON"); std::ifstream file; - file.exceptions ( std::ifstream::failbit ); - try { - file.open(filename); - } - catch (std::ifstream::failure e) { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << "."); - return; - } - file.exceptions( std::ifstream::goodbit ); - + storm::utility::openFile(filename, file); json parsedJson; parsedJson << file; - file.close(); + storm::utility::closeFile(file); // Start by building mapping from ids to names std::map nameMapping; diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 2dd98e645..bbff2c9cc 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -56,19 +56,19 @@ void initializeSettings() { std::unordered_map parseCapacitiesList(std::string const& filename) { std::unordered_map map; - std::ifstream ifs; - ifs.open(filename); + std::ifstream stream; + storm::utility::openFile(filename, stream); std::string line; - while( std::getline(ifs, line) ) { + while ( std::getline(stream, line) ) { std::vector strs; boost::split(strs, line, boost::is_any_of("\t ")); STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs"); std::cout << std::stoll(strs[1]) << std::endl; map[strs[0]] = std::stoll(strs[1]); } + storm::utility::closeFile(stream); return map; - } diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h index de3811109..d043ce53d 100644 --- a/src/storm-gspn/storm-gspn.h +++ b/src/storm-gspn/storm-gspn.h @@ -8,6 +8,8 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GSPNExportSettings.h" +#include "storm/utility/file.h" + namespace storm { /** * Builds JANI model from GSPN. @@ -21,23 +23,23 @@ namespace storm { storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule(); if (exportSettings.isWriteToDotSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteToDotFilename()); + storm::utility::openFile(exportSettings.getWriteToDotFilename(), fs); gspn.writeDotToStream(fs); - fs.close(); + storm::utility::closeFile(fs); } if (exportSettings.isWriteToPnproSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteToPnproFilename()); + storm::utility::openFile(exportSettings.getWriteToPnproFilename(), fs); gspn.toPnpro(fs); - fs.close(); + storm::utility::closeFile(fs); } if (exportSettings.isWriteToPnmlSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteToPnmlFilename()); + storm::utility::openFile(exportSettings.getWriteToPnmlFilename(), fs); gspn.toPnml(fs); - fs.close(); + storm::utility::closeFile(fs); } if (exportSettings.isDisplayStatsSet()) { @@ -48,13 +50,13 @@ namespace storm { if (exportSettings.isWriteStatsToFileSet()) { std::ofstream fs; - fs.open(exportSettings.getWriteStatsFilename()); + storm::utility::openFile(exportSettings.getWriteStatsFilename(), fs); gspn.writeStatsToStream(fs); - fs.close(); + storm::utility::closeFile(fs); } } -} \ No newline at end of file +} diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 6a6707177..2fa9385a2 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -47,13 +47,10 @@ void handleJani(storm::jani::Model& model) { void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) { std::string filepath = storm::settings::getModule().getProgramGraphDotOutputFilename(); - std::ofstream ofs; - ofs.open(filepath, std::ofstream::out ); - if (ofs.is_open()) { - prog.printDot(ofs); - } else { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); - } + std::ofstream stream; + storm::utility::openFile(filepath, stream); + prog.printDot(stream); + storm::utility::closeFile(stream); } int main(const int argc, const char** argv) { diff --git a/src/storm-pgcl/parser/PgclParser.cpp b/src/storm-pgcl/parser/PgclParser.cpp index ca264de5f..6ecde3054 100755 --- a/src/storm-pgcl/parser/PgclParser.cpp +++ b/src/storm-pgcl/parser/PgclParser.cpp @@ -1,6 +1,7 @@ #include "PgclParser.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "storm/exceptions/WrongFormatException.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -9,8 +10,8 @@ namespace storm { storm::pgcl::PgclProgram result; // Open file and initialize result. - std::ifstream inputFileStream(filename, std::ios::in); - STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); + std::ifstream inputFileStream; + storm::utility::openFile(filename, inputFileStream); // Now try to parse the contents of the file. try { @@ -18,12 +19,12 @@ namespace storm { result = parseFromString(fileContent, filename); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); throw e; } // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); return result; } diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index 164802c2b..9a0071571 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -7,6 +7,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/utility/dd.h" +#include "storm/utility/file.h" #include "storm-config.h" #include "storm/adapters/CarlAdapter.h" @@ -47,7 +48,8 @@ namespace storm { template void MenuGameAbstractor::exportToDot(storm::abstraction::MenuGame const& currentGame, std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { - std::ofstream out(filename); + std::ofstream out; + storm::utility::openFile(filename, out); AbstractionInformation const& abstractionInformation = this->getAbstractionInformation(); storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame.getTransitionMatrix(); @@ -130,6 +132,7 @@ namespace storm { } out << "}" << std::endl; + storm::utility::closeFile(out); } template class MenuGameAbstractor; diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 3d1a9397e..79b030fb8 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -324,10 +324,10 @@ namespace storm { // And export if required. if(storm::settings::getModule().isExportExplicitSet()) { - std::ofstream ofs; - ofs.open(storm::settings::getModule().getExportExplicitFilename(), std::ofstream::out); - storm::exporter::explicitExportSparseModel(ofs, sparseModel, model.getParameterNames()); - ofs.close(); + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportExplicitFilename(), stream); + storm::exporter::explicitExportSparseModel(stream, sparseModel, model.getParameterNames()); + storm::utility::closeFile(stream); } } diff --git a/src/storm/modelchecker/region/ParameterRegion.cpp b/src/storm/modelchecker/region/ParameterRegion.cpp index 27b683e8b..d328831fc 100644 --- a/src/storm/modelchecker/region/ParameterRegion.cpp +++ b/src/storm/modelchecker/region/ParameterRegion.cpp @@ -7,7 +7,8 @@ #include "storm/settings/modules/RegionSettings.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/InvalidArgumentException.h" -#include "utility/constants.h" +#include "storm/utility/constants.h" +#include "storm/utility/file.h" namespace storm { namespace modelchecker { @@ -283,7 +284,7 @@ namespace storm { } else{ //if we reach this point we can assume that the region is given as a file. - STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::getModule().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid."); + STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(storm::settings::getModule().getRegionFilePath()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid."); storm::parser::MappedFile mf(storm::settings::getModule().getRegionFilePath().c_str()); regionsString = std::string(mf.getData(),mf.getDataSize()); } diff --git a/src/storm/parser/AtomicPropositionLabelingParser.cpp b/src/storm/parser/AtomicPropositionLabelingParser.cpp index bbb555460..4d55b4fe8 100644 --- a/src/storm/parser/AtomicPropositionLabelingParser.cpp +++ b/src/storm/parser/AtomicPropositionLabelingParser.cpp @@ -24,11 +24,6 @@ namespace storm { storm::models::sparse::StateLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const & filename) { // Open the given file. - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."; - } - MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp index 7b53415cb..9aacb7e4c 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp @@ -41,11 +41,6 @@ namespace storm { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; - } - // Open file. MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/FormulaParser.cpp b/src/storm/parser/FormulaParser.cpp index 6bb1687dc..e592f141c 100644 --- a/src/storm/parser/FormulaParser.cpp +++ b/src/storm/parser/FormulaParser.cpp @@ -15,6 +15,7 @@ #include "storm/storage/expressions/ExpressionEvaluator.h" #include "FormulaParserGrammar.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -65,8 +66,8 @@ namespace storm { std::vector FormulaParser::parseFromFile(std::string const& filename) const { // Open file and initialize result. - std::ifstream inputFileStream(filename, std::ios::in); - STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); + std::ifstream inputFileStream; + storm::utility::openFile(filename, inputFileStream); std::vector properties; @@ -76,12 +77,12 @@ namespace storm { properties = parseFromString(fileContent); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); throw e; } // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); return properties; } diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index c8f0c15e8..826c8075b 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -18,6 +18,7 @@ #include #include "storm/utility/macros.h" +#include "storm/utility/file.h" namespace storm { namespace parser { @@ -64,18 +65,9 @@ namespace storm { void JaniParser::readFile(std::string const &path) { std::ifstream file; - file.exceptions ( std::ifstream::failbit ); - try { - file.open(path); - } - catch (std::ifstream::failure e) { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << path << "."); - return; - } - file.exceptions( std::ifstream::goodbit ); - + storm::utility::openFile(path, file); parsedStructure << file; - file.close(); + storm::utility::closeFile(file); } std::pair> JaniParser::parseModel(bool parseProperties) { diff --git a/src/storm/parser/MappedFile.cpp b/src/storm/parser/MappedFile.cpp index e731ebf18..5b9f02714 100644 --- a/src/storm/parser/MappedFile.cpp +++ b/src/storm/parser/MappedFile.cpp @@ -15,10 +15,14 @@ #include "storm/exceptions/FileIoException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" + namespace storm { namespace parser { MappedFile::MappedFile(const char* filename) { + STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(filename), storm::exceptions::FileIoException, "Error while reading " << filename << ": The file does not exist or is not readable."); + #if defined LINUX || defined MACOSX // Do file mapping for reasonable systems. @@ -29,15 +33,11 @@ namespace storm { #else if (stat64(filename, &(this->st)) != 0) { #endif - STORM_LOG_ERROR("Error in stat(" << filename << "): Probably, this file does not exist."); - throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist."; + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Error in stat(" << filename << "): Probably, this file does not exist."); } this->file = open(filename, O_RDONLY); - if (this->file < 0) { - STORM_LOG_ERROR("Error in open(" << filename << "): Probably, we may not read this file."); - throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file."; - } + STORM_LOG_THROW(this->file >= 0, storm::exceptions::FileIoException, "Error in open(" << filename << "): Probably, we may not read this file."); this->data = static_cast(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0)); if (this->data == MAP_FAILED) { @@ -90,12 +90,6 @@ namespace storm { #endif } - bool MappedFile::fileExistsAndIsReadable(const char* filename) { - // Test by opening an input file stream and testing the stream flags. - std::ifstream fin(filename); - return fin.good(); - } - char const* MappedFile::getData() const { return data; } diff --git a/src/storm/parser/MappedFile.h b/src/storm/parser/MappedFile.h index f1be7f83c..aeeb7fa6f 100644 --- a/src/storm/parser/MappedFile.h +++ b/src/storm/parser/MappedFile.h @@ -49,14 +49,6 @@ namespace storm { */ ~MappedFile(); - /*! - * Tests whether the given file exists and is readable. - *qi - * @param filename Path and name of the file to be tested. - * @return True iff the file exists and is readable. - */ - static bool fileExistsAndIsReadable(const char* filename); - /*! * Returns a pointer to the beginning of the mapped file data. * diff --git a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp index 271f22516..25b62a2e2 100644 --- a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -294,11 +294,6 @@ namespace storm { // Set the locale to correctly recognize floating point numbers. setlocale(LC_NUMERIC, "C"); - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - // Open file and prepare pointer to buffer. MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/NondeterministicSparseTransitionParser.cpp b/src/storm/parser/NondeterministicSparseTransitionParser.cpp index a9e1b53b1..f9a1947b9 100644 --- a/src/storm/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/NondeterministicSparseTransitionParser.cpp @@ -39,11 +39,6 @@ namespace storm { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - // Open file. MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 436d27c5d..62ef9eebe 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -7,6 +7,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -17,9 +18,8 @@ namespace storm { namespace parser { storm::prism::Program PrismParser::parse(std::string const& filename) { // Open file and initialize result. - std::ifstream inputFileStream(filename); - STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); - + std::ifstream inputFileStream; + storm::utility::openFile(filename, inputFileStream); storm::prism::Program result; // Now try to parse the contents of the file. @@ -28,12 +28,12 @@ namespace storm { result = parseFromString(fileContent, filename); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); throw e; } // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); + storm::utility::closeFile(inputFileStream); return result; } diff --git a/src/storm/parser/SparseChoiceLabelingParser.cpp b/src/storm/parser/SparseChoiceLabelingParser.cpp index c73d1def4..26395d057 100644 --- a/src/storm/parser/SparseChoiceLabelingParser.cpp +++ b/src/storm/parser/SparseChoiceLabelingParser.cpp @@ -13,11 +13,6 @@ namespace storm { std::vector SparseChoiceLabelingParser::parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename) { // Open file. - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/parser/SparseStateRewardParser.cpp b/src/storm/parser/SparseStateRewardParser.cpp index d010265a8..3df355578 100644 --- a/src/storm/parser/SparseStateRewardParser.cpp +++ b/src/storm/parser/SparseStateRewardParser.cpp @@ -17,11 +17,6 @@ namespace storm { template std::vector SparseStateRewardParser::parseSparseStateReward(uint_fast64_t stateCount, std::string const& filename) { // Open file. - if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable."; - } - MappedFile file(filename.c_str()); char const* buf = file.getData(); diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 8fefca91c..bbd514c57 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -39,6 +39,7 @@ #include "storm/settings/modules/JitBuilderSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/utility/macros.h" +#include "storm/utility/file.h" #include "storm/settings/Option.h" namespace storm { @@ -394,8 +395,8 @@ namespace storm { std::map> SettingsManager::parseConfigFile(std::string const& filename) const { std::map> result; - std::ifstream input(filename); - STORM_LOG_THROW(input.good(), storm::exceptions::OptionParserException, "Could not read from config file '" << filename << "'."); + std::ifstream input; + storm::utility::openFile(filename, input); bool globalScope = true; std::string activeModule = ""; @@ -480,7 +481,8 @@ namespace storm { } } } - + + storm::utility::closeFile(input); return result; } diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index de33d4f0b..a9da13e4e 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -16,9 +16,10 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/IllegalArgumentException.h" #include "storm/exceptions/IllegalFunctionCallException.h" -#include "utility/macros.h" -#include "adapters/CarlAdapter.h" -#include "exceptions/UnexpectedException.h" +#include "storm/utility/macros.h" +#include "storm/utility/file.h" +#include "storm/adapters/CarlAdapter.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace solver { @@ -245,9 +246,9 @@ namespace storm { if (storm::settings::getModule().isExportSmtLibScriptSet()){ STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file"); - commandFile.open(storm::settings::getModule().getExportSmtLibScriptPath(), std::ios::trunc); - isCommandFileOpen=commandFile.is_open(); - STORM_LOG_THROW(isCommandFileOpen, storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened"); + storm::utility::openFile(storm::settings::getModule().getExportSmtLibScriptPath(), commandFile); + isCommandFileOpen = true; + // TODO also close file } //some initial commands diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index 23443a760..469b590b6 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -6,6 +6,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/utility/file.h" namespace storm { namespace dd { @@ -86,7 +87,7 @@ namespace storm { void Odd::exportToDot(std::string const& filename) const { std::ofstream dotFile; - dotFile.open (filename); + storm::utility::openFile(filename, dotFile); // Print header. dotFile << "digraph \"ODD\" {" << std::endl << "center=true;" << std::endl << "edge [dir = none];" << std::endl; @@ -129,8 +130,7 @@ namespace storm { } dotFile << "}" << std::endl; - - dotFile.close(); + storm::utility::closeFile(dotFile); } void Odd::addToLevelToOddNodesMap(std::map>>& levelToOddNodesMap, uint_fast64_t level) const { diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 834ce8623..c39a6b79b 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -5,6 +5,7 @@ #include #include "storm/utility/macros.h" +#include "storm/utility/file.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/NotSupportedException.h" @@ -510,20 +511,11 @@ namespace storm { return modernjson::json(expression.getValueAsDouble()); } - - - - - - void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector const& formulas, std::string const& filepath, bool checkValid) { - std::ofstream ofs; - ofs.open (filepath, std::ofstream::out ); - if(ofs.is_open()) { - toStream(janiModel, formulas, ofs, checkValid); - } else { - STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); - } + std::ofstream stream; + storm::utility::openFile(filepath, stream); + toStream(janiModel, formulas, stream, checkValid); + storm::utility::closeFile(stream); } void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector const& formulas, std::ostream& os, bool checkValid) { diff --git a/src/storm/utility/export.h b/src/storm/utility/export.h index 3a6891780..b4f5020c0 100644 --- a/src/storm/utility/export.h +++ b/src/storm/utility/export.h @@ -12,7 +12,7 @@ #include #include "storm/utility/macros.h" -#include "storm/exceptions/FileIoException.h" +#include "storm/utility/file.h" //#include "storm/storage/parameters.h" //#include "storm/settings/modules/ParametricSettings.h" @@ -40,19 +40,11 @@ namespace storm { filestream.close(); } */ - - inline void exportStringToFile(std::string const& str, std::string filepath) { - std::ofstream filestream; - filestream.open(filepath); - STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << "."); - filestream << str; - } template inline void exportDataToCSVFile(std::string filepath, std::vector> const& data, boost::optional> const& columnHeaders) { std::ofstream filestream; - filestream.open(filepath); - STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << "."); + storm::utility::openFile(filepath, filestream); if(columnHeaders) { for(auto columnIt = columnHeaders->begin(); columnIt != columnHeaders->end(); ++columnIt) { @@ -73,10 +65,9 @@ namespace storm { } filestream << std::endl; } + storm::utility::closeFile(filestream); } } } - - #endif diff --git a/src/storm/utility/file.h b/src/storm/utility/file.h new file mode 100644 index 000000000..4e234dee5 --- /dev/null +++ b/src/storm/utility/file.h @@ -0,0 +1,81 @@ +/** + * @file: file.h + * @author: Sebastian Junges + * + * @since October 7, 2014 + */ + +#ifndef STORM_UTILITY_FILE_H_ +#define STORM_UTILITY_FILE_H_ + +#include + +#include "storm/utility/macros.h" +#include "storm/exceptions/FileIoException.h" + +namespace storm { + namespace utility { + + /*! + * Open the given file for writing. + * + * @param filename Path and name of the file to be tested. + * @param filestream Contains the file handler afterwards. + * @param append If true, the new content is appended instead of clearing the existing content. + */ + inline void openFile(std::string const& filepath, std::ofstream& filestream, bool append = false) { + if (append) { + filestream.open(filepath, std::ios::app); + } else { + filestream.open(filepath); + } + STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << "."); + STORM_PRINT_AND_LOG("Write to file " << filepath << "." << std::endl); + } + + /*! + * Open the given file for reading. + * + * @param filename Path and name of the file to be tested. + * @param filestream Contains the file handler afterwards. + */ + inline void openFile(std::string const& filepath, std::ifstream& filestream) { + filestream.open(filepath); + STORM_LOG_THROW(filestream, storm::exceptions::FileIoException , "Could not open file " << filepath << "."); + } + + /*! + * Close the given file after writing. + * + * @param filestream Contains the file handler to close. + */ + inline void closeFile(std::ofstream& stream) { + stream.close(); + } + + /*! + * Close the given file after reading. + * + * @param filestream Contains the file handler to close. + */ + inline void closeFile(std::ifstream& stream) { + stream.close(); + } + + /*! + * Tests whether the given file exists and is readable. + * + * @param filename Path and name of the file to be tested. + * @return True iff the file exists and is readable. + */ + inline bool fileExistsAndIsReadable(std::string const& filename) { + // Test by opening an input file stream and testing the stream flags. + std::ifstream filestream; + filestream.open(filename); + return filestream.good(); + } + + } +} + +#endif diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index ef4785c1a..3aca0dbe2 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -97,6 +97,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/utility/Stopwatch.h" +#include "storm/utility/file.h" namespace storm { @@ -434,7 +435,7 @@ namespace storm { inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; - filestream.open(path); + storm::utility::openFile(path, filestream); // TODO: add checks. filestream << "!Parameters: "; std::set vars = result.gatherVariables(); @@ -445,7 +446,7 @@ namespace storm { std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator>(filestream, "\n")); filestream << "!Graph-preserving Constraints: " << std::endl; std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); - filestream.close(); + storm::utility::closeFile(filestream); } template<> @@ -623,10 +624,10 @@ namespace storm { template void exportMatrixToFile(std::shared_ptr> model, std::string const& filepath) { STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); - std::ofstream ofs; - ofs.open (filepath, std::ofstream::out); - model->getTransitionMatrix().printAsMatlabMatrix(ofs); - ofs.close(); + std::ofstream stream; + storm::utility::openFile(filepath, stream); + model->getTransitionMatrix().printAsMatlabMatrix(stream); + storm::utility::closeFile(stream); } } diff --git a/src/test/parser/MappedFileTest.cpp b/src/test/parser/MappedFileTest.cpp index 3e8affe52..f33ee3aa2 100644 --- a/src/test/parser/MappedFileTest.cpp +++ b/src/test/parser/MappedFileTest.cpp @@ -11,6 +11,7 @@ #include #include "storm/parser/MappedFile.h" #include "storm/utility/cstring.h" +#include "storm/utility/file.h" #include "storm/exceptions/FileIoException.h" TEST(MappedFileTest, NonExistingFile) { @@ -41,12 +42,12 @@ TEST(MappedFileTest, ExistsAndReadble) { // Test the fileExistsAndIsReadable() method under various circumstances. // File exists and is readable. - ASSERT_TRUE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/txt/testStringFile.txt")); + ASSERT_TRUE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/txt/testStringFile.txt")); // File does not exist. - ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not")); + ASSERT_FALSE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/nonExistingFile.not")); // File exists but is not readable. // TODO: Find portable solution to providing a situation in which a file exists but is not readable. - //ASSERT_FALSE(storm::parser::MappedFile::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/parser/unreadableFile.txt")); + //ASSERT_FALSE(storm::utility::fileExistsAndIsReadable(STORM_TEST_RESOURCES_DIR "/parser/unreadableFile.txt")); } From e847d71e1338a79c8852c0f09369fa93c31749a5 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 15:45:44 +0100 Subject: [PATCH 2/9] SymbolicModel: getRewardModels. --- src/storm/models/symbolic/Model.cpp | 5 +++++ src/storm/models/symbolic/Model.h | 2 ++ 2 files changed, 7 insertions(+) diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 1ebf69f48..483b4337a 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -192,6 +192,11 @@ namespace storm { bool Model::hasRewardModel() const { return !this->rewardModels.empty(); } + + template + std::unordered_map::RewardModelType> const& Model::getRewardModels() const { + return this->rewardModels; + } template void Model::printModelInformationToStream(std::ostream& out) const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 14c4edbc5..eecbdfdd6 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -246,6 +246,8 @@ namespace storm { * @return True iff the model has a reward model. */ bool hasRewardModel() const; + + std::unordered_map const& getRewardModels() const; /*! * Retrieves the number of reward models associated with this model. From 0ead111deac3cf1c92293cd662fee84491d42326 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 15:57:29 +0100 Subject: [PATCH 3/9] SymbolicModel: getLabels --- src/storm/models/symbolic/Model.cpp | 9 +++++++++ src/storm/models/symbolic/Model.h | 2 ++ 2 files changed, 11 insertions(+) diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 483b4337a..38f87d438 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -203,6 +203,15 @@ namespace storm { this->printModelInformationHeaderToStream(out); this->printModelInformationFooterToStream(out); } + + template + std::vector Model::getLabels() const { + std::vector labels; + for(auto const& entry : labelToExpressionMap) { + labels.push_back(entry.first); + } + return labels; + } template void Model::printModelInformationHeaderToStream(std::ostream& out) const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index eecbdfdd6..f3db59f26 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -259,6 +259,8 @@ namespace storm { virtual void printModelInformationToStream(std::ostream& out) const override; virtual bool isSymbolicModel() const override; + + std::vector getLabels() const; protected: From 598dd85972bd063bf59ea96208ee454ddf702418 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 16:22:43 +0100 Subject: [PATCH 4/9] SymbolicModel: getDeadlockStates --- src/storm/models/symbolic/Model.cpp | 5 +++++ src/storm/models/symbolic/Model.h | 7 ++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 38f87d438..e88895560 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -71,6 +71,11 @@ namespace storm { storm::dd::Bdd const& Model::getInitialStates() const { return initialStates; } + + template + storm::dd::Bdd const& Model::getDeadlockStates() const { + return deadlockStates; + } template storm::dd::Bdd Model::getStates(std::string const& label) const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index f3db59f26..4d70fbf1d 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -130,7 +130,12 @@ namespace storm { * @return The initial states of the model. */ storm::dd::Bdd const& getInitialStates() const; - + + /* + * Retrieves the deadlock states of the model. + */ + storm::dd::Bdd const& getDeadlockStates() const; + /*! * Returns the sets of states labeled with the given label. * From e5b526b7aef0974e40b607fac678c16a0d07a904 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 16:23:50 +0100 Subject: [PATCH 5/9] SymbolicToSparseModel: MDPs --- .../SymbolicToSparseTransformer.cpp | 50 +++++++++++++++++++ .../transformer/SymbolicToSparseTransformer.h | 15 ++++++ 2 files changed, 65 insertions(+) create mode 100644 src/storm/transformer/SymbolicToSparseTransformer.cpp create mode 100644 src/storm/transformer/SymbolicToSparseTransformer.h diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp new file mode 100644 index 000000000..4cb266354 --- /dev/null +++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp @@ -0,0 +1,50 @@ +#include "SymbolicToSparseTransformer.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" +#include "storm/models/symbolic/StandardRewardModel.h" + + +#include "storm/models/sparse/StandardRewardModel.h" + +namespace storm { + namespace transformer { + + template + std::shared_ptr> SymbolicMdpToSparseMdpTransformer::translate( + storm::models::symbolic::Mdp const& symbolicMdp) { + storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd(); + storm::storage::SparseMatrix transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd); + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) { + boost::optional> stateRewards; + boost::optional> stateActionRewards; + boost::optional> transitionRewards; + if (rewardModelNameAndModel.second.hasStateRewards()) { + stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd); + } + if (rewardModelNameAndModel.second.hasStateActionRewards()) { + stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd); + } + if (rewardModelNameAndModel.second.hasTransitionRewards()) { + transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd); + } + rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel(stateRewards, stateActionRewards, transitionRewards)); + } + storm::models::sparse::StateLabeling labelling; + + labelling.addLabel("initial", symbolicMdp.getInitialStates().toVector(odd)); + labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd)); + for(auto const& label : symbolicMdp.getLabels()) { + labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd)); + } + return std::make_shared>(transitionMatrix, labelling, rewardModels); + + + } + + template class SymbolicMdpToSparseMdpTransformer; + template class SymbolicMdpToSparseMdpTransformer; + } +} \ No newline at end of file diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h new file mode 100644 index 000000000..7ea46fff4 --- /dev/null +++ b/src/storm/transformer/SymbolicToSparseTransformer.h @@ -0,0 +1,15 @@ +#pragma once + +#include "storm/models/sparse/Mdp.h" +#include "storm/models/symbolic/Mdp.h" + +namespace storm { + namespace transformer { + + template + class SymbolicMdpToSparseMdpTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::Mdp const& symbolicMdp); + }; + } +} From ce9ee672b50f02bd8228a4d5e8e62fb66f40e00d Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 15 Feb 2017 16:38:29 +0100 Subject: [PATCH 6/9] ExportExplicitToDot now added, thanks to Joachim Klein for pointing this out. --- src/storm/cli/entrypoints.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 79b030fb8..8b968e756 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -329,6 +329,14 @@ namespace storm { storm::exporter::explicitExportSparseModel(stream, sparseModel, model.getParameterNames()); storm::utility::closeFile(stream); } + + // And export DOT if required. + if(storm::settings::getModule().isExportDotSet()) { + std::ofstream stream; + storm::utility::openFile(storm::settings::getModule().getExportDotFilename(), stream); + sparseModel->writeDotToStream(stream); + storm::utility::closeFile(stream); + } } template From e6bf0339d34df1002f29c38c8ce9e534b14ae5e9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 Feb 2017 21:21:09 +0100 Subject: [PATCH 7/9] overhaul of JANI model building to allow using actions of automata in several synchronization vectors --- src/storm/builder/DdJaniModelBuilder.cpp | 420 +++++++++++--------- src/storm/storage/jani/Model.cpp | 5 +- src/test/builder/DdJaniModelBuilderTest.cpp | 196 ++++++--- 3 files changed, 383 insertions(+), 238 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 2c308559c..d9cb430ec 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -518,7 +518,7 @@ namespace storm { result.setValue(metaVariableNameToValueMap, 1); return result; } - + template class CombinedEdgesSystemComposer : public SystemComposer { public: @@ -606,9 +606,53 @@ namespace storm { bool inputEnabled; }; + struct ActionIdentification { + ActionIdentification(uint64_t actionIndex) : actionIndex(actionIndex), synchronizationVectorIndex(boost::none) { + // Intentionally left empty. + } + + ActionIdentification(uint64_t actionIndex, uint64_t synchronizationVectorIndex) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex) { + // Intentionally left empty. + } + + ActionIdentification(uint64_t actionIndex, boost::optional synchronizationVectorIndex) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex) { + // Intentionally left empty. + } + + bool operator==(ActionIdentification const& other) const { + bool result = actionIndex == other.actionIndex; + if (synchronizationVectorIndex) { + if (other.synchronizationVectorIndex) { + result &= synchronizationVectorIndex.get() == other.synchronizationVectorIndex.get(); + } else { + result = false; + } + } else { + if (other.synchronizationVectorIndex) { + result = false; + } + } + return result; + } + + uint64_t actionIndex; + boost::optional synchronizationVectorIndex; + }; + + struct ActionIdentificationHash { + std::size_t operator()(ActionIdentification const& identification) const { + std::size_t seed = 0; + boost::hash_combine(seed, identification.actionIndex); + if (identification.synchronizationVectorIndex) { + boost::hash_combine(seed, identification.synchronizationVectorIndex.get()); + } + return seed; + } + }; + // This structure represents a subcomponent of a composition. struct AutomatonDd { - AutomatonDd(storm::dd::Add const& identity, std::map> const& transientLocationAssignments = {}) : actionIndexToAction(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair(0, 0)) { + AutomatonDd(storm::dd::Add const& identity, std::map> const& transientLocationAssignments = {}) : actions(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair(0, 0)) { // Intentionally left empty. } @@ -633,8 +677,8 @@ namespace storm { setHighestLocalNondeterminismVariable(std::max(localNondeterminismVariables.second, getHighestLocalNondeterminismVariable())); } - // A mapping from action indices to the action DDs. - std::map actionIndexToAction; + // A mapping from action identifications to the action DDs. + std::unordered_map actions; // A mapping from transient variables to their location-based transient assignment values. std::map> transientLocationAssignments; @@ -644,7 +688,6 @@ namespace storm { // The local nondeterminism variables used by this action DD, given as the lowest and highest variable index. std::pair localNondeterminismVariables; - }; CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables const& variables, std::vector const& transientVariables) : SystemComposer(model, variables, transientVariables), actionInformation(actionInformation) { @@ -654,208 +697,192 @@ namespace storm { storm::jani::CompositionInformation const& actionInformation; ComposerResult compose() override { - std::map actionIndexToLocalNondeterminismVariableOffset; - for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { - actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0; - } - actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::SILENT_ACTION_INDEX] = 0; - - AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset)); + STORM_LOG_THROW(this->model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions."); + AutomatonDd globalAutomaton = boost::any_cast(this->model.getSystemComposition().accept(*this, boost::any())); return buildSystemFromAutomaton(globalAutomaton); } + struct ActionInstantiation { + ActionInstantiation(uint64_t actionIndex, uint64_t synchronizationVectorIndex, uint64_t localNondeterminismVariableOffset) : actionIndex(actionIndex), synchronizationVectorIndex(synchronizationVectorIndex), localNondeterminismVariableOffset(localNondeterminismVariableOffset) { + // Intentionally left empty. + } + + ActionInstantiation(uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) : actionIndex(actionIndex), localNondeterminismVariableOffset(localNondeterminismVariableOffset) { + // Intentionally left empty. + } + + bool operator==(ActionInstantiation const& other) const { + bool result = actionIndex == other.actionIndex; + result &= localNondeterminismVariableOffset == other.localNondeterminismVariableOffset; + if (synchronizationVectorIndex) { + if (!other.synchronizationVectorIndex) { + result = false; + } else { + result &= synchronizationVectorIndex.get() == other.synchronizationVectorIndex.get(); + } + } else { + if (other.synchronizationVectorIndex) { + result = false; + } + } + return result; + } + + uint64_t actionIndex; + boost::optional synchronizationVectorIndex; + uint64_t localNondeterminismVariableOffset; + }; + + struct ActionInstantiationHash { + std::size_t operator()(ActionInstantiation const& instantiation) const { + std::size_t seed = 0; + boost::hash_combine(seed, instantiation.actionIndex); + boost::hash_combine(seed, instantiation.localNondeterminismVariableOffset); + if (instantiation.synchronizationVectorIndex) { + boost::hash_combine(seed, instantiation.synchronizationVectorIndex.get()); + } + return seed; + } + }; + + typedef std::map> ActionInstantiations; + boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override { - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); + ActionInstantiations actionInstantiations; + if (data.empty()) { + // If no data was provided, this is the top level element in which case we build the full automaton. + for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) { + actionInstantiations[actionIndex].emplace_back(actionIndex, 0); + } + actionInstantiations[storm::jani::Model::SILENT_ACTION_INDEX].emplace_back(storm::jani::Model::SILENT_ACTION_INDEX, 0); + } std::set inputEnabledActionIndices; for (auto const& actionName : composition.getInputEnabledActions()) { inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName)); } - return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset, inputEnabledActionIndices); + return buildAutomatonDd(composition.getAutomatonName(), data.empty() ? actionInstantiations : boost::any_cast(data), inputEnabledActionIndices); } boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override { - std::map const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast const&>(data); - + STORM_LOG_ASSERT(data.empty(), "Expected parallel composition to be on topmost level to be JANI compliant."); + + // Prepare storage for the subautomata of the composition. std::vector subautomata; + + // The outer loop iterates over the indices of the subcomposition, because the first subcomposition needs + // to be built before the second and so on. + uint64_t silentActionIndex = actionInformation.getActionIndex(storm::jani::Model::SILENT_ACTION_NAME); for (uint64_t subcompositionIndex = 0; subcompositionIndex < composition.getNumberOfSubcompositions(); ++subcompositionIndex) { - // Prepare the new offset mapping. - std::map newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset; + // Now build a new set of action instantiations for the current subcomposition index. + ActionInstantiations actionInstantiations; + actionInstantiations[silentActionIndex].emplace_back(silentActionIndex, 0); - if (subcompositionIndex == 0) { - for (auto const& synchVector : composition.getSynchronizationVectors()) { - auto it = actionIndexToLocalNondeterminismVariableOffset.find(actionInformation.getActionIndex(synchVector.getOutput())); - STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action " << synchVector.getOutput() << "."); - if (synchVector.getInput(0) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { - newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(0))] = it->second; - } - } - } else { - // Based on the previous results, we need to update the offsets. - for (auto const& synchVector : composition.getSynchronizationVectors()) { - if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { - boost::optional previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex); - if (previousActionPosition) { - AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()]; + for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchronizationVectorIndex) { + auto const& synchVector = composition.getSynchronizationVector(synchronizationVectorIndex); + + // Determine the first participating subcomposition, because we need to build the corresponding action + // from all local nondeterminism variable offsets that the output action of the synchronization vector + // is required to have. + if (subcompositionIndex == synchVector.getPositionOfFirstParticipatingAction()) { + uint64_t actionIndex = actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex)); + actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, 0); + } else if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { + uint64_t actionIndex = actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex)); - std::string const& previousAction = synchVector.getInput(previousActionPosition.get()); - auto it = previousAutomatonDd.actionIndexToAction.find(actionInformation.getActionIndex(previousAction)); - if (it != previousAutomatonDd.actionIndexToAction.end()) { - newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex))] = it->second.getHighestLocalNondeterminismVariable(); - } else { - STORM_LOG_ASSERT(false, "Subcomposition does not have action that is mentioned in parallel composition."); - } - } - } + // If this subcomposition is participating in the synchronization vector, but it's not the first + // such subcomposition, then we have to retrieve the offset we need for the participating action + // by looking at the maximal offset used by the preceding participating action. + boost::optional previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex); + STORM_LOG_ASSERT(previousActionPosition, "Inconsistent information about synchronization vector."); + AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()]; + auto precedingActionIt = previousAutomatonDd.actions.find(ActionIdentification(actionInformation.getActionIndex(synchVector.getInput(previousActionPosition.get())), synchronizationVectorIndex)); + STORM_LOG_THROW(precedingActionIt != previousAutomatonDd.actions.end(), storm::exceptions::WrongFormatException, "Subcomposition does not have action that is mentioned in parallel composition."); + actionInstantiations[actionIndex].emplace_back(actionIndex, synchronizationVectorIndex, precedingActionIt->second.getHighestLocalNondeterminismVariable()); } } - // Build the DD for the next element of the composition wrt. to the current offset mapping. - subautomata.push_back(boost::any_cast(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap))); + subautomata.push_back(boost::any_cast(composition.getSubcomposition(subcompositionIndex).accept(*this, actionInstantiations))); } - + return composeInParallel(subautomata, composition.getSynchronizationVectors()); } private: AutomatonDd composeInParallel(std::vector const& subautomata, std::vector const& synchronizationVectors) { - typedef storm::dd::Add IdentityAdd; - typedef std::pair ActionAndAutomatonIdentity; - typedef std::vector ActionAndAutomatonIdentities; - typedef std::vector>> SynchronizationVectorActionsAndIdentities; - AutomatonDd result(this->variables.manager->template getAddOne()); - - std::map> nonSynchronizingActions; - SynchronizationVectorActionsAndIdentities synchronizationVectorActions(synchronizationVectors.size(), boost::none); - for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) { - AutomatonDd const& subautomaton = subautomata[automatonIndex]; - - // Add the transient assignments from the new subautomaton. - addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments); - - // Initilize the used local nondeterminism variables appropriately. - if (automatonIndex == 0) { - result.setLowestLocalNondeterminismVariable(subautomaton.getLowestLocalNondeterminismVariable()); - result.setHighestLocalNondeterminismVariable(subautomaton.getHighestLocalNondeterminismVariable()); - } - - // Compose the actions according to the synchronization vectors. - std::set actionsInSynch; - for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) { - auto const& synchVector = synchronizationVectors[synchVectorIndex]; - - if (synchVector.isNoActionInput(synchVector.getInput(automatonIndex))) { - if (automatonIndex == 0) { - // Create a new action that is the identity over the first automaton. - synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(ActionDd(this->variables.manager->template getAddOne(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero()), subautomaton.identity)}, this->variables.manager->template getAddOne()); - } else { - // If there is no action in the output spot, this means that some other subcomposition did - // not provide the action necessary for the synchronization vector to resolve. - if (synchronizationVectorActions[synchVectorIndex]) { - synchronizationVectorActions[synchVectorIndex].get().second *= subautomaton.identity; - } - } - } else { - // Determine the indices of input (at the current automaton position) and the output. - uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex)); - actionsInSynch.insert(inputActionIndex); - - // Either set the action (if it's the first of the ones to compose) or compose the actions directly. - if (automatonIndex == 0) { - // If the action cannot be found, the particular spot in the output will be left empty. - auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); - if (inputActionIt != subautomaton.actionIndexToAction.end()) { - synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(inputActionIt->second, subautomaton.identity)}, this->variables.manager->template getAddOne()); - } - } else { - // If there is no action in the output spot, this means that some other subcomposition did - // not provide the action necessary for the synchronization vector to resolve. - if (synchronizationVectorActions[synchVectorIndex]) { - auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex); - if (inputActionIt != subautomaton.actionIndexToAction.end()) { - synchronizationVectorActions[synchVectorIndex].get().first.push_back(std::make_pair(inputActionIt->second, subautomaton.identity)); - } else { - // If the current subcomposition does not provide the required action for the synchronization - // vector, we clear the action. - synchronizationVectorActions[synchVectorIndex] = boost::none; - } - } - } - } - } - // Now treat all unsynchronizing actions. - if (automatonIndex == 0) { - // Since it's the first automaton, there is nothing to combine. - for (auto const& action : subautomaton.actionIndexToAction) { - if (actionsInSynch.find(action.first) == actionsInSynch.end()) { - nonSynchronizingActions[action.first].push_back(action.second); - } - } - } else { - // Extend all other non-synchronizing actions with the identity of the current subautomaton. - for (auto& actions : nonSynchronizingActions) { - for (auto& action : actions.second) { - STORM_LOG_TRACE("Extending action '" << actionInformation.getActionName(actions.first) << "' with identity of next composition."); - action.transitions *= subautomaton.identity; - } - } - - // Extend the actions of the current subautomaton with the identity of the previous system and - // add it to the overall non-synchronizing action result. - for (auto const& action : subautomaton.actionIndexToAction) { - if (actionsInSynch.find(action.first) == actionsInSynch.end()) { - STORM_LOG_TRACE("Adding action " << actionInformation.getActionName(action.first) << " to non-synchronizing actions and multiply it with system identity."); - nonSynchronizingActions[action.first].push_back(action.second.multiplyTransitions(result.identity)); - } - } - } + // Build the results of the synchronization vectors. + std::map> actions; + for (uint64_t synchronizationVectorIndex = 0; synchronizationVectorIndex < synchronizationVectors.size(); ++synchronizationVectorIndex) { + auto const& synchVector = synchronizationVectors[synchronizationVectorIndex]; - // Finally, construct combined identity. - result.identity *= subautomaton.identity; + boost::optional synchronizingAction = combineSynchronizingActions(subautomata, synchVector, synchronizationVectorIndex); + if (synchronizingAction) { + actions[actionInformation.getActionIndex(synchVector.getOutput())].emplace_back(synchronizingAction.get()); + } } - // Add the results of the synchronization vectors to that of the non-synchronizing actions. - for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) { - auto const& synchVector = synchronizationVectors[synchVectorIndex]; + // Construct the silent action DDs. + std::vector silentActionDds; + for (auto const& automaton : subautomata) { + for (auto& actionDd : silentActionDds) { + STORM_LOG_TRACE("Extending previous silent action by identity of current automaton."); + actionDd = actionDd.multiplyTransitions(automaton.identity); + } - // If there is an action resulting from this combination of actions, add it to the output action. - if (synchronizationVectorActions[synchVectorIndex]) { - uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput()); - nonSynchronizingActions[outputActionIndex].push_back(combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get().first, synchronizationVectorActions[synchVectorIndex].get().second)); + ActionIdentification silentActionIdentification(storm::jani::Model::SILENT_ACTION_INDEX); + auto silentActionIt = automaton.actions.find(silentActionIdentification); + if (silentActionIt != automaton.actions.end()) { + STORM_LOG_TRACE("Extending silent action by running identity."); + silentActionDds.emplace_back(silentActionIt->second.multiplyTransitions(result.identity)); } + + result.identity *= automaton.identity; } - // Now that we have built the individual action DDs for all resulting actions, we need to combine them - // in an unsynchronizing way. - for (auto const& nonSynchronizingActionDds : nonSynchronizingActions) { - std::vector const& actionDds = nonSynchronizingActionDds.second; - if (actionDds.size() > 1) { - ActionDd combinedAction = combineUnsynchronizedActions(actionDds); - result.actionIndexToAction[nonSynchronizingActionDds.first] = combinedAction; - result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables()); - } else { - result.actionIndexToAction[nonSynchronizingActionDds.first] = actionDds.front(); - result.extendLocalNondeterminismVariables(actionDds.front().getLocalNondeterminismVariables()); - } + if (!silentActionDds.empty()) { + auto& allSilentActionDds = actions[storm::jani::Model::SILENT_ACTION_INDEX]; + allSilentActionDds.insert(actions[storm::jani::Model::SILENT_ACTION_INDEX].end(), silentActionDds.begin(), silentActionDds.end()); } + // Finally, combine (potential) multiple action DDs. + for (auto const& actionDds : actions) { + ActionDd combinedAction = actionDds.second.size() > 1 ? combineUnsynchronizedActions(actionDds.second) : actionDds.second.front(); + result.actions[ActionIdentification(actionDds.first)] = combinedAction; + result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables()); + } + + // Construct combined identity. + for (auto const& subautomaton : subautomata) { + result.identity *= subautomaton.identity; + } + return result; } - ActionDd combineSynchronizingActions(std::vector>> const& actionsAndIdentities, storm::dd::Add const& nonSynchronizingAutomataIdentities) { - // If there is just one action, no need to combine anything. - if (actionsAndIdentities.size() == 1) { - return actionsAndIdentities.front().first; + boost::optional combineSynchronizingActions(std::vector const& subautomata, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) { + std::vector>> actions; + storm::dd::Add nonSynchronizingIdentity = this->variables.manager->template getAddOne(); + for (uint64_t subautomatonIndex = 0; subautomatonIndex < subautomata.size(); ++subautomatonIndex) { + auto const& subautomaton = subautomata[subautomatonIndex]; + if (synchronizationVector.getInput(subautomatonIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) { + auto it = subautomaton.actions.find(ActionIdentification(actionInformation.getActionIndex(synchronizationVector.getInput(subautomatonIndex)), synchronizationVectorIndex)); + if (it != subautomaton.actions.end()) { + actions.emplace_back(subautomatonIndex, it->second); + } else { + return boost::none; + } + } else { + nonSynchronizingIdentity *= subautomaton.identity; + } } // If there are only input-enabled actions, we also need to build the disjunction of the guards. bool allActionsInputEnabled = true; - for (auto const& actionIdentityPair : actionsAndIdentities) { - auto const& action = actionIdentityPair.first; - if (!action.isInputEnabled()) { + for (auto const& action : actions) { + if (!action.second.get().isInputEnabled()) { allActionsInputEnabled = false; } } @@ -875,12 +902,13 @@ namespace storm { storm::dd::Add transitions = this->variables.manager->template getAddOne(); std::map> transientEdgeAssignments; - uint64_t lowestNondeterminismVariable = actionsAndIdentities.front().first.getLowestLocalNondeterminismVariable(); - uint64_t highestNondeterminismVariable = actionsAndIdentities.front().first.getHighestLocalNondeterminismVariable(); + uint64_t lowestNondeterminismVariable = actions.front().second.get().getLowestLocalNondeterminismVariable(); + uint64_t highestNondeterminismVariable = actions.front().second.get().getHighestLocalNondeterminismVariable(); storm::dd::Bdd newIllegalFragment = this->variables.manager->getBddZero(); - for (auto const& actionIdentityPair : actionsAndIdentities) { - auto const& action = actionIdentityPair.first; + for (auto const& actionIndexPair : actions) { + auto componentIndex = actionIndexPair.first; + auto const& action = actionIndexPair.second.get(); storm::dd::Bdd actionGuard = action.guard.toBdd(); if (guardDisjunction) { guardDisjunction.get() |= actionGuard; @@ -892,7 +920,7 @@ namespace storm { if (action.isInputEnabled()) { // If the action is input-enabled, we add self-loops to all states. - transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second); + transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * subautomata[componentIndex].identity); } else { transitions *= action.transitions; } @@ -948,7 +976,7 @@ namespace storm { // such a combined transition. illegalFragment &= inputEnabledGuard; - return ActionDd(inputEnabledGuard.template toAdd(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); + return ActionDd(inputEnabledGuard.template toAdd(), transitions * nonSynchronizingIdentity, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); } ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add const& identity1, storm::dd::Add const& identity2) { @@ -1141,7 +1169,7 @@ namespace storm { bool overlappingGuards = false; for (auto const& edge : edgeDds) { - STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::InvalidArgumentException, "Can only combine Markovian edges."); + STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::WrongFormatException, "Can only combine Markovian edges."); if (!overlappingGuards) { overlappingGuards |= !(guard && edge.guard.toBdd()).isZero(); @@ -1197,7 +1225,7 @@ namespace storm { } return combineEdgesToActionNondeterministic(nonMarkovianEdges, markovianEdge, localNondeterminismVariableOffset); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Cannot translate model of this type."); } } else { return ActionDd(this->variables.manager->template getAddZero(), this->variables.manager->template getAddZero(), {}, std::make_pair(0, 0), {}, this->variables.manager->getBddZero()); @@ -1479,23 +1507,30 @@ namespace storm { } } - AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map const& actionIndexToLocalNondeterminismVariableOffset, std::set const& inputEnabledActionIndices) { + AutomatonDd buildAutomatonDd(std::string const& automatonName, ActionInstantiations const& actionInstantiations, std::set const& inputEnabledActionIndices) { + STORM_LOG_TRACE("Building DD for automaton '" << automatonName << "'."); AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName)); storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName); - for (auto const& action : this->model.getActions()) { - uint64_t actionIndex = this->model.getActionIndex(action.getName()); + for (auto const& actionInstantiation : actionInstantiations) { + uint64_t actionIndex = actionInstantiation.first; if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { continue; } - ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex)); + bool inputEnabled = false; if (inputEnabledActionIndices.find(actionIndex) != inputEnabledActionIndices.end()) { - actionDd.setIsInputEnabled(); + inputEnabled = true; + } + for (auto const& instantiationOffset : actionInstantiation.second) { + STORM_LOG_TRACE("Building " << (actionInformation.getActionName(actionIndex).empty() ? "silent " : "") << "action " << (actionInformation.getActionName(actionIndex).empty() ? "" : actionInformation.getActionName(actionIndex) + " ") << "from offset " << instantiationOffset.localNondeterminismVariableOffset << "."); + ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, instantiationOffset.localNondeterminismVariableOffset); + if (inputEnabled) { + actionDd.setIsInputEnabled(); + } + STORM_LOG_TRACE("Used local nondeterminism variables are " << actionDd.getLowestLocalNondeterminismVariable() << " to " << actionDd.getHighestLocalNondeterminismVariable() << "."); + result.actions[ActionIdentification(actionIndex, instantiationOffset.synchronizationVectorIndex)] = actionDd; + result.extendLocalNondeterminismVariables(actionDd.getLocalNondeterminismVariables()); } - - result.actionIndexToAction[actionIndex] = actionDd; - result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable())); - result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable())); } for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) { @@ -1513,7 +1548,7 @@ namespace storm { return result; } - + void addMissingGlobalVariableIdentities(ActionDd& action) { // Build a DD that we can multiply to the transitions and adds all missing global variable identities that way. storm::dd::Add missingIdentities = this->variables.manager->template getAddOne(); @@ -1539,13 +1574,18 @@ namespace storm { // First, determine the highest number of nondeterminism variables that is used in any action and make // all actions use the same amout of nondeterminism variables. uint64_t numberOfUsedNondeterminismVariables = automaton.getHighestLocalNondeterminismVariable(); + STORM_LOG_TRACE("Building system from composed automaton; number of used nondeterminism variables is " << numberOfUsedNondeterminismVariables << "."); // Add missing global variable identities, action and nondeterminism encodings. std::map> transientEdgeAssignments; - for (auto& action : automaton.actionIndexToAction) { + std::unordered_set actionIndices; + for (auto& action : automaton.actions) { + uint64_t actionIndex = action.first.actionIndex; + STORM_LOG_THROW(actionIndices.find(actionIndex) == actionIndices.end(), storm::exceptions::WrongFormatException, "Duplication action " << actionInformation.getActionName(actionIndex)); + actionIndices.insert(action.first.actionIndex); illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); - storm::dd::Add actionEncoding = encodeAction(action.first != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional(action.first) : boost::none, this->variables); + storm::dd::Add actionEncoding = encodeAction(actionIndex != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional(actionIndex) : boost::none, this->variables); storm::dd::Add missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables); storm::dd::Add extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions; for (auto const& transientAssignment : action.second.transientEdgeAssignments) { @@ -1562,7 +1602,10 @@ namespace storm { storm::dd::Add result = this->variables.manager->template getAddZero(); storm::dd::Bdd illegalFragment = this->variables.manager->getBddZero(); std::map> transientEdgeAssignments; - for (auto& action : automaton.actionIndexToAction) { + std::unordered_set actionIndices; + for (auto& action : automaton.actions) { + STORM_LOG_THROW(actionIndices.find(action.first.actionIndex) == actionIndices.end(), storm::exceptions::WrongFormatException, "Duplication action " << actionInformation.getActionName(action.first.actionIndex)); + actionIndices.insert(action.first.actionIndex); illegalFragment |= action.second.illegalFragment; addMissingGlobalVariableIdentities(action.second); addToTransientAssignmentMap(transientEdgeAssignments, action.second.transientEdgeAssignments); @@ -1571,7 +1614,7 @@ namespace storm { return ComposerResult(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, 0); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Illegal model type."); } } }; @@ -1596,7 +1639,7 @@ namespace storm { } else if (modelType == storm::jani::ModelType::MDP) { return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels)); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Invalid model type."); } } @@ -1718,7 +1761,7 @@ namespace storm { transitionMatrix += deadlockStatesAdd * globalIdentity * action; } } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); } } return deadlockStates; @@ -1813,8 +1856,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << "."); } - STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support assignment levels."); - STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support reusing actions in parallel composition"); + STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support assignment levels."); storm::jani::Model preparedModel = model; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 8f6791441..6943c6178 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -758,10 +758,7 @@ namespace storm { ++i; } - // Only add the synchronization vector if there is more than one participating automaton. - if (numberOfParticipatingAutomata > 1) { - synchVectors.push_back(storm::jani::SynchronizationVector(synchVectorInputs, actionName)); - } + synchVectors.push_back(storm::jani::SynchronizationVector(synchVectorInputs, actionName)); } return std::make_shared(subcompositions, synchVectors); diff --git a/src/test/builder/DdJaniModelBuilderTest.cpp b/src/test/builder/DdJaniModelBuilderTest.cpp index 2622662dc..911d49551 100644 --- a/src/test/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/builder/DdJaniModelBuilderTest.cpp @@ -328,9 +328,42 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { automataCompositions.push_back(std::make_shared("one")); automataCompositions.push_back(std::make_shared("two")); automataCompositions.push_back(std::make_shared("three")); - + // First, make all actions non-synchronizing. std::vector synchronizationVectors; + + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("b"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -338,22 +371,50 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { EXPECT_EQ(48ul, model->getNumberOfTransitions()); // Then, make only a, b and c synchronize. - std::vector inputVector; + synchronizationVectors.clear(); + inputVector.clear(); inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); EXPECT_EQ(7ul, model->getNumberOfStates()); EXPECT_EQ(10ul, model->getNumberOfTransitions()); + synchronizationVectors.clear(); + inputVector.clear(); + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -367,7 +428,7 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); - EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException); + EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { @@ -389,6 +450,39 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { // First, make all actions non-synchronizing. std::vector synchronizationVectors; + + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("b"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -396,22 +490,50 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { EXPECT_EQ(48ul, model->getNumberOfTransitions()); // Then, make only a, b and c synchronize. - std::vector inputVector; + synchronizationVectors.clear(); + inputVector.clear(); inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + inputVector.clear(); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back("c"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); EXPECT_EQ(7ul, model->getNumberOfStates()); EXPECT_EQ(10ul, model->getNumberOfTransitions()); + synchronizationVectors.clear(); + inputVector.clear(); + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); model = builder.build(janiModel); @@ -425,7 +547,7 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); - EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException); + EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Sylvan, Composition) { @@ -433,24 +555,11 @@ TEST(DdJaniModelBuilderTest_Sylvan, Composition) { storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder builder; - std::shared_ptr> model = builder.build(janiModel); - - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(21ul, mdp->getNumberOfStates()); - EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition2.nm"); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - model = builder.build(janiModel); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - mdp = model->as>(); - - EXPECT_EQ(8ul, mdp->getNumberOfStates()); - EXPECT_EQ(21ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(21ul, mdp->getNumberOfChoices()); + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Cudd, Composition) { @@ -458,24 +567,11 @@ TEST(DdJaniModelBuilderTest_Cudd, Composition) { storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); storm::builder::DdJaniModelBuilder builder; - std::shared_ptr> model = builder.build(janiModel); - - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - std::shared_ptr> mdp = model->as>(); - - EXPECT_EQ(21ul, mdp->getNumberOfStates()); - EXPECT_EQ(61ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(61ul, mdp->getNumberOfChoices()); - + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); + modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition2.nm"); janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); - model = builder.build(janiModel); - EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); - mdp = model->as>(); - - EXPECT_EQ(8ul, mdp->getNumberOfStates()); - EXPECT_EQ(21ul, mdp->getNumberOfTransitions()); - EXPECT_EQ(21ul, mdp->getNumberOfChoices()); + EXPECT_THROW(std::shared_ptr> model = builder.build(janiModel), storm::exceptions::WrongFormatException); } TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) { @@ -496,12 +592,17 @@ TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) { inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); @@ -528,12 +629,17 @@ TEST(DdJaniModelBuilderTest_Sylvan, InputEnabling) { inputVector.push_back("a"); inputVector.push_back("b"); inputVector.push_back("c"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); inputVector.clear(); inputVector.push_back("c"); inputVector.push_back("c"); inputVector.push_back("a"); - synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + synchronizationVectors.emplace_back(inputVector, "d"); + inputVector.clear(); + inputVector.push_back("d"); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + inputVector.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); + synchronizationVectors.emplace_back(inputVector); std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); janiModel.setSystemComposition(newComposition); From 2567d070373bdf82d09d9da65597be0d6191d0f6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Feb 2017 22:33:00 +0100 Subject: [PATCH 8/9] hybrid multi-objective model checking. --- .../prctl/HybridMdpPrctlModelChecker.cpp | 20 ++++++++++++++++++- .../prctl/HybridMdpPrctlModelChecker.h | 1 + .../SymbolicToSparseTransformer.cpp | 2 +- 3 files changed, 21 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 56aed7679..d42d81251 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -10,10 +10,15 @@ #include "storm/logic/FragmentSpecification.h" +#include "storm/modelchecker/multiobjective/pcaa.h" + #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/transformer/SymbolicToSparseTransformer.h" + #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -32,7 +37,15 @@ namespace storm { template bool HybridMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false)); + if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false))) { + return true; + } else { + // Check whether we consider a multi-objective formula + // For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that all states are considered. + if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; + return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true)); + } + } template @@ -102,6 +115,11 @@ namespace storm { return storm::modelchecker::helper::HybridMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } + template + std::unique_ptr HybridMdpPrctlModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { + auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer::translate(this->getModel()); + return multiobjective::performPcaa(*sparseModel, checkTask.getFormula()); + } template class HybridMdpPrctlModelChecker>; template class HybridMdpPrctlModelChecker>; diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h index 426be343b..e14177363 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -35,6 +35,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr checkMultiObjectiveFormula(CheckTask const& checkTask) override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp index 4cb266354..a8b82133f 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.cpp +++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp @@ -34,7 +34,7 @@ namespace storm { } storm::models::sparse::StateLabeling labelling; - labelling.addLabel("initial", symbolicMdp.getInitialStates().toVector(odd)); + labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd)); labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd)); for(auto const& label : symbolicMdp.getLabels()) { labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd)); From a8b8ef27a3594364a3d47564105accf45a71cc3d Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Feb 2017 22:24:36 +0100 Subject: [PATCH 9/9] fixed is*Expression() methods as they have not been implemented in the corresponding subclasses before. --- .../expressions/BinaryBooleanFunctionExpression.cpp | 6 +++++- .../storage/expressions/BinaryBooleanFunctionExpression.h | 1 + .../expressions/BinaryNumericalFunctionExpression.cpp | 6 +++++- .../expressions/BinaryNumericalFunctionExpression.h | 1 + src/storm/storage/expressions/BinaryRelationExpression.cpp | 6 +++++- src/storm/storage/expressions/BinaryRelationExpression.h | 1 + src/storm/storage/expressions/BooleanLiteralExpression.cpp | 6 +++++- src/storm/storage/expressions/BooleanLiteralExpression.h | 2 +- src/storm/storage/expressions/IfThenElseExpression.cpp | 4 ++++ src/storm/storage/expressions/IfThenElseExpression.h | 3 ++- src/storm/storage/expressions/IntegerLiteralExpression.cpp | 7 ++++++- src/storm/storage/expressions/IntegerLiteralExpression.h | 3 ++- .../storage/expressions/RationalLiteralExpression.cpp | 4 ++++ src/storm/storage/expressions/RationalLiteralExpression.h | 1 + .../storage/expressions/UnaryBooleanFunctionExpression.cpp | 6 +++++- .../storage/expressions/UnaryBooleanFunctionExpression.h | 1 + .../expressions/UnaryNumericalFunctionExpression.cpp | 6 +++++- .../storage/expressions/UnaryNumericalFunctionExpression.h | 3 ++- src/storm/storage/expressions/VariableExpression.cpp | 6 +++++- src/storm/storage/expressions/VariableExpression.h | 1 + 20 files changed, 62 insertions(+), 12 deletions(-) diff --git a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp index ea25593a2..32aed361e 100644 --- a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -122,7 +122,11 @@ namespace storm { boost::any BinaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BinaryBooleanFunctionExpression::isBinaryBooleanFunctionExpression() const { + return true; + } + void BinaryBooleanFunctionExpression::printToStream(std::ostream& stream) const { stream << "(" << *this->getFirstOperand(); switch (this->getOperatorType()) { diff --git a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h index f0dc1ea51..eb1344262 100644 --- a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h @@ -38,6 +38,7 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isBinaryBooleanFunctionExpression() const override; /*! * Retrieves the operator associated with the expression. diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 3d2e09153..0ed3dc746 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -122,7 +122,11 @@ namespace storm { boost::any BinaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BinaryNumericalFunctionExpression::isBinaryNumericalFunctionExpression() const { + return true; + } + void BinaryNumericalFunctionExpression::printToStream(std::ostream& stream) const { stream << "("; switch (this->getOperatorType()) { diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h index 7cc27fda1..b69c3b8c5 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h @@ -39,6 +39,7 @@ namespace storm { virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isBinaryNumericalFunctionExpression() const override; /*! * Retrieves the operator associated with the expression. diff --git a/src/storm/storage/expressions/BinaryRelationExpression.cpp b/src/storm/storage/expressions/BinaryRelationExpression.cpp index a610802e8..331c8b85e 100644 --- a/src/storm/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storm/storage/expressions/BinaryRelationExpression.cpp @@ -85,7 +85,11 @@ namespace storm { boost::any BinaryRelationExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BinaryRelationExpression::isBinaryRelationExpression() const { + return true; + } + BinaryRelationExpression::RelationType BinaryRelationExpression::getRelationType() const { return this->relationType; } diff --git a/src/storm/storage/expressions/BinaryRelationExpression.h b/src/storm/storage/expressions/BinaryRelationExpression.h index dc9c1e080..a9ed11924 100644 --- a/src/storm/storage/expressions/BinaryRelationExpression.h +++ b/src/storm/storage/expressions/BinaryRelationExpression.h @@ -38,6 +38,7 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isBinaryRelationExpression() const override; /*! * Retrieves the relation associated with the expression. diff --git a/src/storm/storage/expressions/BooleanLiteralExpression.cpp b/src/storm/storage/expressions/BooleanLiteralExpression.cpp index 409cd4b19..c09e5c894 100644 --- a/src/storm/storage/expressions/BooleanLiteralExpression.cpp +++ b/src/storm/storage/expressions/BooleanLiteralExpression.cpp @@ -35,7 +35,11 @@ namespace storm { boost::any BooleanLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool BooleanLiteralExpression::isBooleanLiteralExpression() const { + return true; + } + bool BooleanLiteralExpression::getValue() const { return this->value; } diff --git a/src/storm/storage/expressions/BooleanLiteralExpression.h b/src/storm/storage/expressions/BooleanLiteralExpression.h index 944b47708..b989493d0 100644 --- a/src/storm/storage/expressions/BooleanLiteralExpression.h +++ b/src/storm/storage/expressions/BooleanLiteralExpression.h @@ -33,7 +33,7 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isBooleanLiteralExpression() const override; /*! * Retrieves the value of the boolean literal. * diff --git a/src/storm/storage/expressions/IfThenElseExpression.cpp b/src/storm/storage/expressions/IfThenElseExpression.cpp index f965a9d6e..535b828e9 100644 --- a/src/storm/storage/expressions/IfThenElseExpression.cpp +++ b/src/storm/storage/expressions/IfThenElseExpression.cpp @@ -91,6 +91,10 @@ namespace storm { boost::any IfThenElseExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } + + bool IfThenElseExpression::isIfThenElseExpression() const { + return true; + } std::shared_ptr IfThenElseExpression::getCondition() const { return this->condition; diff --git a/src/storm/storage/expressions/IfThenElseExpression.h b/src/storm/storage/expressions/IfThenElseExpression.h index ba9ab9f7b..0d1be1d4b 100644 --- a/src/storm/storage/expressions/IfThenElseExpression.h +++ b/src/storm/storage/expressions/IfThenElseExpression.h @@ -39,7 +39,8 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isIfThenElseExpression() const override; + /*! * Retrieves the condition expression of the if-then-else expression. * diff --git a/src/storm/storage/expressions/IntegerLiteralExpression.cpp b/src/storm/storage/expressions/IntegerLiteralExpression.cpp index 1e8a56f23..6fcecfd80 100644 --- a/src/storm/storage/expressions/IntegerLiteralExpression.cpp +++ b/src/storm/storage/expressions/IntegerLiteralExpression.cpp @@ -32,7 +32,12 @@ namespace storm { boost::any IntegerLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool IntegerLiteralExpression::isIntegerLiteralExpression() const { + return true; + } + + int_fast64_t IntegerLiteralExpression::getValue() const { return this->value; } diff --git a/src/storm/storage/expressions/IntegerLiteralExpression.h b/src/storm/storage/expressions/IntegerLiteralExpression.h index 8d9dfda63..9266ea968 100644 --- a/src/storm/storage/expressions/IntegerLiteralExpression.h +++ b/src/storm/storage/expressions/IntegerLiteralExpression.h @@ -32,7 +32,8 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isIntegerLiteralExpression() const override; + /*! * Retrieves the value of the integer literal. * diff --git a/src/storm/storage/expressions/RationalLiteralExpression.cpp b/src/storm/storage/expressions/RationalLiteralExpression.cpp index 242489c0a..6215a5df5 100644 --- a/src/storm/storage/expressions/RationalLiteralExpression.cpp +++ b/src/storm/storage/expressions/RationalLiteralExpression.cpp @@ -37,6 +37,10 @@ namespace storm { boost::any RationalLiteralExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } + + bool RationalLiteralExpression::isRationalLiteralExpression() const { + return true; + } double RationalLiteralExpression::getValueAsDouble() const { return storm::utility::convertNumber(this->value); diff --git a/src/storm/storage/expressions/RationalLiteralExpression.h b/src/storm/storage/expressions/RationalLiteralExpression.h index 9b4025794..77d8f3703 100644 --- a/src/storm/storage/expressions/RationalLiteralExpression.h +++ b/src/storm/storage/expressions/RationalLiteralExpression.h @@ -49,6 +49,7 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isRationalLiteralExpression() const override; /*! * Retrieves the value of the double literal. diff --git a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp index 40dc3a919..e0afd87e4 100644 --- a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.cpp @@ -52,7 +52,11 @@ namespace storm { boost::any UnaryBooleanFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool UnaryBooleanFunctionExpression::isUnaryBooleanFunctionExpression() const { + return true; + } + void UnaryBooleanFunctionExpression::printToStream(std::ostream& stream) const { stream << "!(" << *this->getOperand() << ")"; } diff --git a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h index 7fc978034..918300d93 100644 --- a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h +++ b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h @@ -37,6 +37,7 @@ namespace storm { virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isUnaryBooleanFunctionExpression() const override; /*! * Retrieves the operator associated with this expression. diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp index 9fc2c5639..9e8290c02 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -103,7 +103,11 @@ namespace storm { boost::any UnaryNumericalFunctionExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool UnaryNumericalFunctionExpression::isUnaryNumericalFunctionExpression() const { + return true; + } + void UnaryNumericalFunctionExpression::printToStream(std::ostream& stream) const { switch (this->getOperatorType()) { case OperatorType::Minus: stream << "-("; break; diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h index bd863abcf..fe8fbaf45 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h @@ -38,7 +38,8 @@ namespace storm { virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; - + virtual bool isUnaryNumericalFunctionExpression() const override; + /*! * Retrieves the operator associated with this expression. * diff --git a/src/storm/storage/expressions/VariableExpression.cpp b/src/storm/storage/expressions/VariableExpression.cpp index 8a94f6194..f68837f2f 100644 --- a/src/storm/storage/expressions/VariableExpression.cpp +++ b/src/storm/storage/expressions/VariableExpression.cpp @@ -66,7 +66,11 @@ namespace storm { boost::any VariableExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { return visitor.visit(*this, data); } - + + bool VariableExpression::isVariableExpression() const { + return true; + } + void VariableExpression::printToStream(std::ostream& stream) const { stream << this->getVariableName(); } diff --git a/src/storm/storage/expressions/VariableExpression.h b/src/storm/storage/expressions/VariableExpression.h index f1a3bf1ce..708ec35fc 100644 --- a/src/storm/storage/expressions/VariableExpression.h +++ b/src/storm/storage/expressions/VariableExpression.h @@ -36,6 +36,7 @@ namespace storm { virtual void gatherVariables(std::set& variables) const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + virtual bool isVariableExpression() const override; /*! * Retrieves the name of the variable associated with this expression.