Merge branch 'master' into conditional_optimizations

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:
                     {

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

@@ -179,6 +179,7 @@ namespace storm {
             auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             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());

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)

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) {

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) {

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<storm::prism::Constant> constants;
@@ -50,7 +69,7 @@ namespace storm {
             uint_fast64_t currentUpdateIndex;
         };
 
-        class PrismParser : public qi::grammar<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> {
+        class PrismParser : public qi::grammar<Iterator, storm::prism::Program(), Skipper> {
         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<PositionAnnotation> annotate;
             
+            // An object gathering information about the program while parsing.
+            GlobalProgramInformation globalProgramInformation;
+            
             // The starting point of the grammar.
-            qi::rule<Iterator, storm::prism::Program(), qi::locals<GlobalProgramInformation>, Skipper> start;
+            qi::rule<Iterator, storm::prism::Program(), Skipper> start;
             
             // Rules for model type.
             qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;

src/storm/settings/modules/IOSettings.cpp

@@ -44,6 +44,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";
@@ -74,7 +75,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())
@@ -255,6 +257,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();
             }

src/storm/settings/modules/IOSettings.h

@@ -311,6 +311,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;
 
@@ -346,6 +352,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;

src/storm/storage/SparseMatrix.cpp

@@ -583,6 +583,27 @@ namespace storm {
             return rowGroupIndices.get();
         }
         
+        template<typename ValueType>
+        void SparseMatrix<ValueType>::setRowGroupIndices(std::vector<index_type> const& newRowGroupIndices) {
+            trivialRowGrouping = false;
+            rowGroupIndices = newRowGroupIndices;
+        }
+
+        template<typename ValueType>
+        bool SparseMatrix<ValueType>::hasTrivialRowGrouping() const {
+            return trivialRowGrouping;
+        }
+        
+        template<typename ValueType>
+        void SparseMatrix<ValueType>::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<typename ValueType>
         storm::storage::BitVector SparseMatrix<ValueType>::getRowFilter(storm::storage::BitVector const& groupConstraint) const {
             storm::storage::BitVector res(this->getRowCount(), false);
@@ -995,6 +1016,30 @@ namespace storm {
             return res;
         }
         
+        template<typename ValueType>
+        SparseMatrix<ValueType> SparseMatrix<ValueType>::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<ValueType> builder(getRowCount(), getColumnCount(), entryCount);
+            for (auto const& row : rowFilter) {
+                for (auto const& entry : getRow(row)) {
+                    builder.addNextValue(row, entry.getColumn(), entry.getValue());
+                }
+            }
+            SparseMatrix<ValueType> result = builder.build();
+            
+            // Add a row grouping if necessary.
+            if (!hasTrivialRowGrouping()) {
+                result.setRowGroupIndices(getRowGroupIndices());
+            }
+            return result;
+        }
+        
         template<typename ValueType>
         SparseMatrix<ValueType> SparseMatrix<ValueType>::selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const {
             // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for
@@ -1880,22 +1925,7 @@ namespace storm {
         typename SparseMatrix<ValueType>::iterator SparseMatrix<ValueType>::end()  {
             return this->columnsAndValues.begin() + this->rowIndications[rowCount];
         }
-        
-        template<typename ValueType>
-        bool SparseMatrix<ValueType>::hasTrivialRowGrouping() const {
-            return trivialRowGrouping;
-        }
-        
-        template<typename ValueType>
-        void SparseMatrix<ValueType>::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<typename ValueType>
         ValueType SparseMatrix<ValueType>::getRowSum(index_type row) const {
             ValueType sum = storm::utility::zero<ValueType>();

src/storm/storage/SparseMatrix.h

@@ -566,6 +566,27 @@ namespace storm {
              */
             std::vector<index_type> 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<index_type> 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.
              *
@@ -675,6 +696,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
@@ -1028,19 +1058,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
 			*/

src/storm/storage/jani/JSONExporter.h

@@ -9,7 +9,7 @@
 // JSON parser
 #include "json.hpp"
 namespace modernjson {
-    using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>;
+    using json = nlohmann::json;
 }
 
 namespace storm {