From 6e548627ee4bf6f1366418f6e2462fbfd11dff28 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 10 Sep 2017 09:11:26 +0200 Subject: [PATCH 1/6] adding storm-pgcl as a dependency to target binaries --- src/storm-pgcl-cli/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storm-pgcl-cli/CMakeLists.txt b/src/storm-pgcl-cli/CMakeLists.txt index 4778d1e93..4f2799d4d 100644 --- a/src/storm-pgcl-cli/CMakeLists.txt +++ b/src/storm-pgcl-cli/CMakeLists.txt @@ -2,5 +2,7 @@ add_executable(storm-pgcl-cli ${PROJECT_SOURCE_DIR}/src/storm-pgcl-cli/storm-pgc target_link_libraries(storm-pgcl-cli storm-pgcl storm-cli-utilities) set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl") +add_dependencies(binaries storm-pgcl-cli) + # installation install(TARGETS storm-pgcl-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file From 2d99ff312615c19a06d4c2bc48a31acf8d7a7c38 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 14 Sep 2017 10:47:14 +0200 Subject: [PATCH 2/6] preserving action knowledge from first to second PRISM parser pass --- src/storm/parser/PrismParser.cpp | 25 +++++++++++++------------ src/storm/parser/PrismParser.h | 26 ++++++++++++++++++++++++-- 2 files changed, 37 insertions(+), 14 deletions(-) diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 0230fbaca..38ed0cb12 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -216,19 +216,19 @@ namespace storm { moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)]; moduleDefinitionList.name("module list"); - start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), qi::_a)] - > *(modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), qi::_a, qi::_1)] - | definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] - | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] - | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)] - | globalVariableDefinition(qi::_a) - | (moduleRenaming(qi::_a) | moduleDefinition(qi::_a))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_a), qi::_1)] - | initialStatesConstruct(qi::_a) - | rewardModelDefinition(qi::_a)[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] - | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] - | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)] + start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))] + > *(modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)] + | definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] + | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] + | globalVariableDefinition(phoenix::ref(globalProgramInformation)) + | (moduleRenaming(phoenix::ref(globalProgramInformation)) | moduleDefinition(phoenix::ref(globalProgramInformation)))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, phoenix::ref(globalProgramInformation)), qi::_1)] + | initialStatesConstruct(phoenix::ref(globalProgramInformation)) + | rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] + | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] ) - > -(systemCompositionConstruct(qi::_a)) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)]; + > -(systemCompositionConstruct(phoenix::ref(globalProgramInformation))) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), phoenix::ref(globalProgramInformation))]; start.name("probabilistic program"); // Enable location tracking for important entities. @@ -267,6 +267,7 @@ namespace storm { this->secondRun = true; this->expressionParser->setIdentifierMapping(&this->identifiers_); + this->globalProgramInformation.moveToSecondRun(); } void PrismParser::allowDoubleLiterals(bool flag) { diff --git a/src/storm/parser/PrismParser.h b/src/storm/parser/PrismParser.h index f285c5cc9..129cd7b43 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm/parser/PrismParser.h @@ -30,6 +30,25 @@ namespace storm { actionIndices.emplace("", 0); } + void moveToSecondRun() { + // Clear all data except the action to indices mapping. + modelType = storm::prism::Program::ModelType::UNDEFINED; + constants.clear(); + formulas.clear(); + globalBooleanVariables.clear(); + globalIntegerVariables.clear(); + moduleToIndexMap.clear(); + modules.clear(); + rewardModels.clear(); + labels.clear(); + hasInitialConstruct = false; + initialConstruct = storm::prism::InitialConstruct(); + systemCompositionConstruct = boost::none; + + currentCommandIndex = 0; + currentUpdateIndex = 0; + } + // Members for all essential information that needs to be collected. storm::prism::Program::ModelType modelType; std::vector constants; @@ -50,7 +69,7 @@ namespace storm { uint_fast64_t currentUpdateIndex; }; - class PrismParser : public qi::grammar, Skipper> { + class PrismParser : public qi::grammar { public: /*! * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax. @@ -161,8 +180,11 @@ namespace storm { // A function used for annotating the entities with their position. phoenix::function annotate; + // An object gathering information about the program while parsing. + GlobalProgramInformation globalProgramInformation; + // The starting point of the grammar. - qi::rule, Skipper> start; + qi::rule start; // Rules for model type. qi::rule modelTypeDefinition; From bac50a32ab39a89f7d1dfada1dfa693cb06bea76 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 14 Sep 2017 13:35:46 +0200 Subject: [PATCH 3/6] warkaround for gcc 7.2.0: make modernjson compile again --- resources/3rdparty/modernjson/src/json.hpp | 3 ++- src/storm/storage/jani/JSONExporter.h | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/resources/3rdparty/modernjson/src/json.hpp b/resources/3rdparty/modernjson/src/json.hpp index 596095aff..1b279a804 100755 --- a/resources/3rdparty/modernjson/src/json.hpp +++ b/resources/3rdparty/modernjson/src/json.hpp @@ -5650,7 +5650,8 @@ Format](http://rfc7159.net/rfc7159) { case value_t::array: { - return *lhs.m_value.array < *rhs.m_value.array; + // Workaround for gcc 7.2.0, which parses array< as a template. + return (*lhs.m_value.array) < *rhs.m_value.array; } case value_t::object: { diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index e26cf287f..17fa97ad6 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -9,7 +9,7 @@ // JSON parser #include "json.hpp" namespace modernjson { - using json = nlohmann::basic_json; + using json = nlohmann::json; } namespace storm { From fcd277c42a9c61fae03aa60fb4ce954d46242a2f Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Sep 2017 10:12:31 +0200 Subject: [PATCH 4/6] added an option that enables building of state valuations. Also include the state valuations when the model is exported to .dot format --- src/storm-cli-utilities/model-handling.h | 1 + src/storm/models/sparse/Model.cpp | 10 +++++++--- src/storm/settings/modules/IOSettings.cpp | 8 +++++++- src/storm/settings/modules/IOSettings.h | 7 +++++++ 4 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 588d0d330..22b91af71 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -179,6 +179,7 @@ namespace storm { auto counterexampleGeneratorSettings = storm::settings::getModule(); storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); options.setBuildChoiceLabels(ioSettings.isBuildChoiceLabelsSet()); + options.setBuildStateValuations(ioSettings.isBuildStateValuationsSet()); options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); options.setBuildAllLabels(ioSettings.isBuildFullModelSet()); options.setBuildAllRewardModels(ioSettings.isBuildFullModelSet()); diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 062a7fca6..288b46a1a 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -317,12 +317,16 @@ namespace storm { for (uint_fast64_t state = 0, highestStateIndex = this->getNumberOfStates() - 1; state <= highestStateIndex; ++state) { if (subsystem == nullptr || subsystem->get(state)) { outStream << "\t" << state; - if (includeLabeling || firstValue != nullptr || secondValue != nullptr || stateColoring != nullptr) { + if (includeLabeling || firstValue != nullptr || secondValue != nullptr || stateColoring != nullptr || hasStateValuations()) { outStream << " [ "; // If we need to print some extra information, do so now. - if (includeLabeling || firstValue != nullptr || secondValue != nullptr) { - outStream << "label = \"" << state << ": "; + if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) { + outStream << "label = \"" << state; + if (hasStateValuations()) { + outStream << " " << getStateValuations().getStateInfo(state); + } + outStream << ": "; // Now print the state labeling to the stream if requested. if (includeLabeling) { diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 7d26b54ac..6227570ea 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -46,6 +46,7 @@ namespace storm { const std::string IOSettings::noBuildOptionName = "nobuild"; const std::string IOSettings::fullModelBuildOptionName = "buildfull"; const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab"; + const std::string IOSettings::buildStateValuationsOptionName = "buildstateval"; const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; const std::string IOSettings::propertyOptionName = "prop"; @@ -76,7 +77,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, include choice labels").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build()) @@ -266,6 +268,10 @@ namespace storm { return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); } + bool IOSettings::isBuildStateValuationsSet() const { + return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); + } + bool IOSettings::isPropertySet() const { return this->getOption(propertyOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index e68c6b515..7bf0422cc 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -325,6 +325,12 @@ namespace storm { */ bool isBuildChoiceLabelsSet() const; + /*! + * Retrieves whether the choice labels should be build + * @return + */ + bool isBuildStateValuationsSet() const; + bool check() const override; void finalize() override; @@ -362,6 +368,7 @@ namespace storm { static const std::string fullModelBuildOptionName; static const std::string noBuildOptionName; static const std::string buildChoiceLabelOptionName; + static const std::string buildStateValuationsOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; From 904e49dab30369b63d16d8502dadae545e682a76 Mon Sep 17 00:00:00 2001 From: hbruintjes Date: Fri, 22 Sep 2017 11:48:37 +0200 Subject: [PATCH 5/6] Fix wrong type --- src/storm-dft/transformations/DftToGspnTransformator.cpp | 2 +- src/storm/storage/dd/DdManager.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 8c3ef0448..975d01f4a 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -416,7 +416,7 @@ namespace storm { cucNodes.push_back(nodeCUC); builder.setPlaceLayoutInfo(nodeCUC, storm::gspn::LayoutInfo(xcenter-9.0+j*14.0, ycenter+5.0)); if (j > 0) { - uint64 tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name()); + uint64_t tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name()); builder.setTransitionLayoutInfo(tclaim, storm::gspn::LayoutInfo(xcenter-9.0+j*14.0, ycenter)); builder.addInhibitionArc(unavailableNodes.at(child->id()), tclaim); builder.addInputArc(considerNodes.back(), tclaim); diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index 6a00b4cbf..5cce07412 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -265,7 +265,7 @@ namespace storm { std::stringstream tmp1; std::vector result; - for (uint64 layer = 0; layer < numberOfLayers; ++layer) { + for (uint64_t layer = 0; layer < numberOfLayers; ++layer) { if (type == MetaVariableType::Int) { result.emplace_back(manager->declareIntegerVariable(name + tmp1.str())); } else if (type == MetaVariableType::Bool) { @@ -279,7 +279,7 @@ namespace storm { std::vector>> variables(numberOfLayers); for (std::size_t i = 0; i < numberOfDdVariables; ++i) { std::vector> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level); - for (uint64 layer = 0; layer < numberOfLayers; ++layer) { + for (uint64_t layer = 0; layer < numberOfLayers; ++layer) { variables[layer].emplace_back(Bdd(*this, ddVariables[layer], {result[layer]})); } From 142d0347659f25c5c2dcd63abeb1bb3dcbbf7d19 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 22 Sep 2017 16:47:26 +0200 Subject: [PATCH 6/6] New methods for the SparseMatrix: SetRowGroupIndices and filterEntries --- src/storm/storage/SparseMatrix.cpp | 62 ++++++++++++++++++++++-------- src/storm/storage/SparseMatrix.h | 43 ++++++++++++++------- 2 files changed, 76 insertions(+), 29 deletions(-) diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 49d0cddad..c0ef84d19 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -584,6 +584,27 @@ namespace storm { return rowGroupIndices.get(); } + template + void SparseMatrix::setRowGroupIndices(std::vector const& newRowGroupIndices) { + trivialRowGrouping = false; + rowGroupIndices = newRowGroupIndices; + } + + template + bool SparseMatrix::hasTrivialRowGrouping() const { + return trivialRowGrouping; + } + + template + void SparseMatrix::makeRowGroupingTrivial() { + if (trivialRowGrouping) { + STORM_LOG_ASSERT(!rowGroupIndices || rowGroupIndices.get() == storm::utility::vector::buildVectorForRange(0, this->getRowGroupCount() + 1), "Row grouping is supposed to be trivial but actually it is not."); + } else { + trivialRowGrouping = true; + rowGroupIndices = boost::none; + } + } + template storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint) const { storm::storage::BitVector res(this->getRowCount(), false); @@ -984,6 +1005,30 @@ namespace storm { return res; } + template + SparseMatrix SparseMatrix::filterEntries(storm::storage::BitVector const& rowFilter) const { + // Count the number of entries in the resulting matrix. + index_type entryCount = 0; + for (auto const& row : rowFilter) { + entryCount += getRow(row).getNumberOfEntries(); + } + + // Build the resulting matrix. + SparseMatrixBuilder builder(getRowCount(), getColumnCount(), entryCount); + for (auto const& row : rowFilter) { + for (auto const& entry : getRow(row)) { + builder.addNextValue(row, entry.getColumn(), entry.getValue()); + } + } + SparseMatrix result = builder.build(); + + // Add a row grouping if necessary. + if (!hasTrivialRowGrouping()) { + result.setRowGroupIndices(getRowGroupIndices()); + } + return result; + } + template SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const { // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for @@ -1547,22 +1592,7 @@ namespace storm { typename SparseMatrix::iterator SparseMatrix::end() { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } - - template - bool SparseMatrix::hasTrivialRowGrouping() const { - return trivialRowGrouping; - } - - template - void SparseMatrix::makeRowGroupingTrivial() { - if (trivialRowGrouping) { - STORM_LOG_ASSERT(!rowGroupIndices || rowGroupIndices.get() == storm::utility::vector::buildVectorForRange(0, this->getRowGroupCount() + 1), "Row grouping is supposed to be trivial but actually it is not."); - } else { - trivialRowGrouping = true; - rowGroupIndices = boost::none; - } - } - + template ValueType SparseMatrix::getRowSum(index_type row) const { ValueType sum = storm::utility::zero(); diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 6f4dba96f..b6b9a9622 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -563,6 +563,27 @@ namespace storm { */ std::vector const& getRowGroupIndices() const; + /*! + * Sets the row grouping to the given one. + * @note It is assumed that the new row grouping is non-trivial. + * + * @param newRowGroupIndices The new row group indices. + */ + void setRowGroupIndices(std::vector const& newRowGroupIndices); + + /*! + * Retrieves whether the matrix has a trivial row grouping. + * + * @return True iff the matrix has a trivial row grouping. + */ + bool hasTrivialRowGrouping() const; + + /*! + * Makes the row grouping of this matrix trivial. + * Has no effect when the row grouping is already trivial. + */ + void makeRowGroupingTrivial(); + /*! * Returns the indices of the rows that belong to one of the selected row groups. * @@ -665,6 +686,15 @@ namespace storm { */ SparseMatrix restrictRows(storm::storage::BitVector const& rowsToKeep, bool allowEmptyRowGroups = false) const; + /*! + * Returns a copy of this matrix that only considers entries in the selected rows. + * Non-selected rows will not have any entries + * + * @note does not change the dimensions (row-, column-, and rowGroup count) of this matrix + * @param rowFilter the selected rows + */ + SparseMatrix filterEntries(storm::storage::BitVector const& rowFilter) const; + /** * Compares two rows. * @param i1 Index of first row @@ -1004,19 +1034,6 @@ namespace storm { */ iterator end(); - /*! - * Retrieves whether the matrix has a trivial row grouping. - * - * @return True iff the matrix has a trivial row grouping. - */ - bool hasTrivialRowGrouping() const; - - /*! - * Makes the row grouping of this matrix trivial. - * Has no effect when the row grouping is already trivial. - */ - void makeRowGroupingTrivial(); - /*! * Returns a copy of the matrix with the chosen internal data type */