Added placeholders to DRN format

src/storm-parsers/parser/DirectEncodingParser.cpp

@@ -40,6 +40,7 @@ namespace storm {
             ValueParser<ValueType> valueParser;
             bool sawType = false;
             bool sawParameters = false;
+            std::unordered_map<std::string, ValueType> placeholders;
             size_t nrStates = 0;
             storm::models::ModelType type;
             std::vector<std::string> rewardModelNames;
@@ -56,7 +57,8 @@ namespace storm {
                     STORM_LOG_THROW(!sawType, storm::exceptions::WrongFormatException, "Type declared twice");
                     type = storm::models::getModelType(line.substr(7));
                     STORM_LOG_TRACE("Model type: " << type);
-                    STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported.");
+                    STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException,
+                                    "Stochastic Two Player Games in DRN format are not supported.");
                     sawType = true;
 
                 } else if (line == "@parameters") {
@@ -73,6 +75,23 @@ namespace storm {
                     }
                     sawParameters = true;
 
+                } else if (line == "@placeholders") {
+                    // Parse placeholders
+                    while (std::getline(file, line)) {
+                        size_t posColon = line.find(':');
+                        STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found.");
+                        std::string placeName = line.substr(0, posColon - 1);
+                        STORM_LOG_THROW(placeName.front() == '$', storm::exceptions::WrongFormatException, "Placeholder must start with dollar symbol $.");
+                        std::string valueStr = line.substr(posColon + 2);
+                        ValueType value = parseValue(valueStr, placeholders, valueParser);
+                        STORM_LOG_TRACE("Placeholder " << placeName << " for value " << value);
+                        auto ret = placeholders.insert(std::make_pair(placeName.substr(1), value));
+                        STORM_LOG_THROW(ret.second, storm::exceptions::WrongFormatException, "Placeholder '$" << placeName << "' was already defined before.");
+                        if (file.peek() == '@') {
+                            // Next character is @ -> placeholder definitions ended
+                            break;
+                        }
+                    }
                 } else if (line == "@reward_models") {
                     // Parse reward models
                     STORM_LOG_THROW(rewardModelNames.empty(), storm::exceptions::WrongFormatException, "Reward model names declared twice");
@@ -90,7 +109,7 @@ namespace storm {
                     STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "No. of states has to be declared before model.");
 
                     // Construct model components
-                    modelComponents = parseStates(file, type, nrStates, valueParser, rewardModelNames);
+                    modelComponents = parseStates(file, type, nrStates, placeholders, valueParser, rewardModelNames);
                     break;
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse line '" << line << "'.");
@@ -104,7 +123,10 @@ namespace storm {
         }
 
         template<typename ValueType, typename RewardModelType>
-        std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames) {
+        std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>
+        DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize,
+                                                                      std::unordered_map<std::string, ValueType> const& placeholders, ValueParser<ValueType> const& valueParser,
+                                                                      std::vector<std::string> const& rewardModelNames) {
             // Initialize
             auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
             bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp);
@@ -152,7 +174,7 @@ namespace storm {
                     size_t posEnd = line.find(" ");
                     if (posEnd != std::string::npos) {
                         curString = line.substr(0, posEnd);
-                        line = line.substr(posEnd+1);
+                        line = line.substr(posEnd + 1);
                     } else {
                         line = "";
                     }
@@ -172,11 +194,11 @@ namespace storm {
                         posEnd = line.find(" ");
                         if (posEnd != std::string::npos) {
                             curString = line.substr(0, posEnd);
-                            line = line.substr(posEnd+1);
+                            line = line.substr(posEnd + 1);
                         } else {
                             line = "";
                         }
-                        ValueType exitRate = valueParser.parseValue(curString);
+                        ValueType exitRate = parseValue(curString, placeholders, valueParser);
                         if (type == storm::models::ModelType::MarkovAutomaton && !storm::utility::isZero<ValueType>(exitRate)) {
                             modelComponents->markovianStates.get().set(state);
                         }
@@ -188,7 +210,7 @@ namespace storm {
                         // Parse rewards
                         size_t posEndReward = line.find(']');
                         STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
-                        std::string rewardsStr = line.substr(1, posEndReward-1);
+                        std::string rewardsStr = line.substr(1, posEndReward - 1);
                         STORM_LOG_TRACE("State rewards: " << rewardsStr);
                         std::vector<std::string> rewards;
                         boost::split(rewards, rewardsStr, boost::is_any_of(","));
@@ -197,7 +219,7 @@ namespace storm {
                         }
                         auto stateRewardsIt = stateRewards.begin();
                         for (auto const& rew : rewards) {
-                            auto rewardValue = valueParser.parseValue(rew);
+                            auto rewardValue = parseValue(rew, placeholders, valueParser);
                             if (!storm::utility::isZero(rewardValue)) {
                                 if (stateRewardsIt->empty()) {
                                     stateRewardsIt->resize(stateSize, storm::utility::zero<ValueType>());
@@ -206,17 +228,17 @@ namespace storm {
                             }
                             ++stateRewardsIt;
                         }
-                        line = line.substr(posEndReward+1);
+                        line = line.substr(posEndReward + 1);
                     }
 
 
                     if (type == storm::models::ModelType::Pomdp) {
                         if (boost::starts_with(line, "{")) {
                             size_t posEndObservation = line.find("}");
-                            std::string observation = line.substr(1, posEndObservation-1);
+                            std::string observation = line.substr(1, posEndObservation - 1);
                             STORM_LOG_TRACE("State observation " << observation);
                             modelComponents->observabilityClasses.get()[state] = std::stoi(observation);
-                            line = line.substr(posEndObservation+1);
+                            line = line.substr(posEndObservation + 1);
                         } else {
                             STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Expected an observation for state " << state << ".");
                         }
@@ -270,7 +292,7 @@ namespace storm {
                     size_t posEnd = line.find(" ");
                     if (posEnd != std::string::npos) {
                         curString = line.substr(0, posEnd);
-                        line = line.substr(posEnd+1);
+                        line = line.substr(posEnd + 1);
                     } else {
                         line = "";
                     }
@@ -281,7 +303,7 @@ namespace storm {
                         // Rewards found
                         size_t posEndReward = line.find(']');
                         STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
-                        std::string rewardsStr = line.substr(1, posEndReward-1);
+                        std::string rewardsStr = line.substr(1, posEndReward - 1);
                         STORM_LOG_TRACE("Action rewards: " << rewardsStr);
                         std::vector<std::string> rewards;
                         boost::split(rewards, rewardsStr, boost::is_any_of(","));
@@ -290,7 +312,7 @@ namespace storm {
                         }
                         auto actionRewardsIt = actionRewards.begin();
                         for (auto const& rew : rewards) {
-                            auto rewardValue = valueParser.parseValue(rew);
+                            auto rewardValue = parseValue(rew, placeholders, valueParser);
                             if (!storm::utility::isZero(rewardValue)) {
                                 if (actionRewardsIt->size() <= row) {
                                     actionRewardsIt->resize(std::max(row + 1, stateSize), storm::utility::zero<ValueType>());
@@ -299,7 +321,7 @@ namespace storm {
                             }
                             ++actionRewardsIt;
                         }
-                        line = line.substr(posEndReward+1);
+                        line = line.substr(posEndReward + 1);
                     }
                     // TODO import choice labeling when the export works
 
@@ -307,9 +329,9 @@ namespace storm {
                     // New transition
                     size_t posColon = line.find(':');
                     STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found.");
-                    size_t target = parseNumber<size_t>(line.substr(2, posColon-3));
-                    std::string valueStr = line.substr(posColon+2);
-                    ValueType value = valueParser.parseValue(valueStr);
+                    size_t target = parseNumber<size_t>(line.substr(2, posColon - 3));
+                    std::string valueStr = line.substr(posColon + 2);
+                    ValueType value = parseValue(valueStr, placeholders, valueParser);
                     STORM_LOG_TRACE("Transition " << row << " -> " << target << ": " << value);
                     STORM_LOG_THROW(target < stateSize, storm::exceptions::WrongFormatException, "Target state " << target << " is greater than state size " << stateSize);
                     builder.addNextValue(row, target, value);
@@ -338,12 +360,27 @@ namespace storm {
                     actionRewards[i].resize(row + 1, storm::utility::zero<ValueType>());
                     actionRewardVector = std::move(actionRewards[i]);
                 }
-                modelComponents->rewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewardVector), std::move(actionRewardVector)));
+                modelComponents->rewardModels.emplace(rewardModelName,
+                                                      storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewardVector), std::move(actionRewardVector)));
             }
             STORM_LOG_TRACE("Built reward models");
             return modelComponents;
         }
 
+        template<typename ValueType, typename RewardModelType>
+        ValueType DirectEncodingParser<ValueType, RewardModelType>::parseValue(std::string const& valueStr, std::unordered_map<std::string, ValueType> const& placeholders,
+                                                                               ValueParser<ValueType> const& valueParser) {
+            if (boost::starts_with(valueStr, "$")) {
+                auto it = placeholders.find(valueStr.substr(1));
+                STORM_LOG_THROW(it != placeholders.end(), storm::exceptions::WrongFormatException, "Placeholder " << valueStr << " unknown.");
+                return it->second;
+            } else {
+                // Use default value parser
+                return valueParser.parseValue(valueStr);
+            }
+        }
+
+
         // Template instantiations.
         template class DirectEncodingParser<double>;
         template class DirectEncodingParser<storm::RationalNumber>;

src/storm-parsers/parser/DirectEncodingParser.h

@@ -30,13 +30,27 @@ namespace storm {
             /*!
              * Parse states and return transition matrix.
              *
-             * @param file      Input file stream.
-             * @param type      Model type.
+             * @param file Input file stream.
+             * @param type Model type.
              * @param stateSize No. of states
+             * @param placeholders Placeholders for values.
+             * @param valueParser Value parser.
+             * @param rewardModelNames Names of reward models.
              *
              * @return Transition matrix.
              */
-            static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames);
+            static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>
+            parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, std::unordered_map<std::string, ValueType> const& placeholders,
+                        ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames);
+
+            /*!
+             * Parse value from string while using placeholders.
+             * @param valueStr String.
+             * @param placeholders Placeholders.
+             * @param valueParser Value parser.
+             * @return
+             */
+            static ValueType parseValue(std::string const& valueStr, std::unordered_map<std::string, ValueType> const& placeholders, ValueParser<ValueType> const& valueParser);
         };
 
     } // namespace parser

src/storm/utility/DirectEncodingExporter.cpp

@@ -45,12 +45,24 @@ namespace storm {
                 }
             }
             os << std::endl;
+
+            // Optionally write placeholders which only need to be parsed once
+            // This is used to reduce the parsing effort for rational functions
+            // Placeholders begin with the dollar symbol $
+            std::unordered_map<ValueType, std::string> placeholders = generatePlaceholders(sparseModel, exitRates);
+            if (!placeholders.empty()) {
+                os << "@placeholders" << std::endl;
+                for (auto const& entry : placeholders) {
+                    os << "$" << entry.second << " : " << entry.first << std::endl;
+                }
+            }
+
             os << "@reward_models" << std::endl;
             for (auto const& rewardModel : sparseModel->getRewardModels()) {
                 os << rewardModel.first << " ";
             }
             os << std::endl;
-            os << "@nr_states" << std::endl  << sparseModel->getNumberOfStates() <<  std::endl;
+            os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl;
             os << "@model" << std::endl;
 
             storm::storage::SparseMatrix<ValueType> const& matrix = sparseModel->getTransitionMatrix();
@@ -61,7 +73,8 @@ namespace storm {
 
                 // Write exit rates for CTMCs and MAs
                 if (!exitRates.empty()) {
-                    os << " !" << exitRates.at(group);
+                    os << " !";
+                    writeValue(os, exitRates.at(group), placeholders);
                 }
 
                 // Write state rewards
@@ -74,8 +87,8 @@ namespace storm {
                         os << ", ";
                     }
 
-                    if(rewardModelEntry.second.hasStateRewards()) {
-                        os << storm::utility::to_string(rewardModelEntry.second.getStateRewardVector().at(group));
+                    if (rewardModelEntry.second.hasStateRewards()) {
+                        writeValue(os, rewardModelEntry.second.getStateRewardVector().at(group), placeholders);
                     } else {
                         os << "0";
                     }
@@ -90,10 +103,11 @@ namespace storm {
                 }
 
                 // Write labels. Only labels with a whitespace are put in (double) quotation marks.
-                for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) {
-                    STORM_LOG_THROW(std::count( label.begin(), label.end(), '\"' ) == 0, storm::exceptions::NotSupportedException, "Labels with quotation marks are not supported in the DRN format and therefore may not be exported.");
+                for (auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) {
+                    STORM_LOG_THROW(std::count(label.begin(), label.end(), '\"') == 0, storm::exceptions::NotSupportedException,
+                                    "Labels with quotation marks are not supported in the DRN format and therefore may not be exported.");
                     // TODO consider escaping the quotation marks. Not sure whether that is a good idea.
-                    if (std::count_if( label.begin(), label.end(), isspace ) > 0) {
+                    if (std::count_if(label.begin(), label.end(), isspace) > 0) {
                         os << " \"" << label << "\"";
                     } else {
                         os << " " << label;
@@ -133,7 +147,7 @@ namespace storm {
                         }
 
                         if (rewardModelEntry.second.hasStateActionRewards()) {
-                            os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(row));
+                            writeValue(os, rewardModelEntry.second.getStateActionRewardVector().at(row), placeholders);
                         } else {
                             os << "0";
                         }
@@ -148,7 +162,8 @@ namespace storm {
                     for (auto it = matrix.begin(row); it != matrix.end(row); ++it) {
                         ValueType prob = it->getValue();
                         os << "\t\t" << it->getColumn() << " : ";
-                        os << storm::utility::to_string(prob) << std::endl;
+                        writeValue(os, prob, placeholders);
+                        os << std::endl;
                     }
 
                 }
@@ -179,6 +194,80 @@ namespace storm {
             return parameters;
         }
 
+        template<typename ValueType>
+        std::unordered_map<ValueType, std::string> generatePlaceholders(std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<ValueType>) {
+            return {};
+        }
+
+        /*!
+         * Helper function to create a possible placeholder.
+         * A new placeholder is inserted if the rational function is not constant and the function does not exist yet.
+         * @param placeholders Existing placeholders.
+         * @param value Value.
+         * @param i Counter to enumerate placeholders.
+         */
+
+        void createPlaceholder(std::unordered_map<storm::RationalFunction, std::string>& placeholders, storm::RationalFunction const& value, size_t& i) {
+            if (!storm::utility::isConstant(value)) {
+                auto ret = placeholders.insert(std::make_pair(value, std::to_string(i)));
+                if (ret.second) {
+                    // New element was inserted
+                    ++i;
+                }
+            }
+        }
+
+        template<>
+        std::unordered_map<storm::RationalFunction, std::string>
+        generatePlaceholders(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel, std::vector<storm::RationalFunction> exitRates) {
+            std::unordered_map<storm::RationalFunction, std::string> placeholders;
+            size_t i = 0;
+
+            // Exit rates
+            for (auto const& exitRate : exitRates) {
+                createPlaceholder(placeholders, exitRate, i);
+            }
+
+            // Rewards
+            for (auto const& rewardModelEntry : sparseModel->getRewardModels()) {
+                if (rewardModelEntry.second.hasStateRewards()) {
+                    for (auto const& reward : rewardModelEntry.second.getStateRewardVector()) {
+                        createPlaceholder(placeholders, reward, i);
+                    }
+                }
+                if (rewardModelEntry.second.hasStateActionRewards()) {
+                    for (auto const& reward : rewardModelEntry.second.getStateActionRewardVector()) {
+                        createPlaceholder(placeholders, reward, i);
+                    }
+                }
+            }
+
+            // Transition probabilities
+            for (auto const& entry : sparseModel->getTransitionMatrix()) {
+                createPlaceholder(placeholders, entry.getValue(), i);
+            }
+
+            return placeholders;
+        }
+
+        template<typename ValueType>
+        void writeValue(std::ostream& os, ValueType value, std::unordered_map<ValueType, std::string> const& placeholders) {
+            if (storm::utility::isConstant(value)) {
+                os << value;
+                return;
+            }
+
+            // Try to use placeholder
+            auto it = placeholders.find(value);
+            if (it != placeholders.end()) {
+                // Use placeholder
+                os << "$" << it->second;
+            } else {
+                os << value;
+            }
+        }
+
+
         // Template instantiations
         template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters);
         template void explicitExportSparseModel<storm::RationalNumber>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> sparseModel, std::vector<std::string> const& parameters);

src/storm/utility/DirectEncodingExporter.h

@@ -1,4 +1,5 @@
 #pragma once
+
 #include <iostream>
 #include <memory>
 
@@ -17,6 +18,7 @@ namespace storm {
         template<typename ValueType>
         void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters);
 
+
         /*!
          * Accumulate parameters in the model.
          *
@@ -26,5 +28,23 @@ namespace storm {
         template<typename ValueType>
         std::vector<std::string> getParameters(std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel);
 
+        /*!
+         * Generate placeholders for rational functions in the model.
+         *
+         * @param sparseModel Model.
+         * @param exitRates Exit rates.
+         * @return Mapping of the form:rational function -> placeholder name.
+         */
+        template<typename ValueType>
+        std::unordered_map<ValueType, std::string> generatePlaceholders(std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<ValueType> exitRates);
+
+        /*!
+         * Write value to stream while using the placeholders.
+         * @param os Output stream.
+         * @param value Value.
+         * @param placeholders Placeholders.
+         */
+        template<typename ValueType>
+        void writeValue(std::ostream& os, ValueType value, std::unordered_map<ValueType, std::string> const& placeholders);
     }
 }