added support for parsing choice labels for explicit MDPs

Former-commit-id: 89bb1817b4

examples/mdp/tiny/tiny.clab

@@ -0,0 +1,4 @@
+0 0 3
+0 1 1
+1 0 2
+2 0 0

src/models/sparse/Model.cpp

@@ -182,7 +182,8 @@ namespace storm {
             void Model<ValueType, RewardModelType>::printModelInformationFooterToStream(std::ostream& out) const {
                 this->printRewardModelsInformationToStream(out);
                 this->getStateLabeling().printLabelingInformationToStream(out);
-                out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
+                out << "choice labels: \t" << (this->hasChoiceLabeling() ? "yes" : "no")  << std::noboolalpha << std::endl;
+                out << "Size in memory: " << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
                 out << "-------------------------------------------------------------- " << std::endl;
             }
             

src/parser/AutoParser.cpp

@@ -21,7 +21,8 @@ namespace storm {
         std::shared_ptr<storm::models::sparse::Model<double>> AutoParser::parseModel(std::string const& transitionsFilename,
                 std::string const& labelingFilename,
                 std::string const& stateRewardFilename,
-																					 std::string const & transitionRewardFilename) {
+                std::string const& transitionRewardFilename,
+                std::string const& choiceLabelingFilename) {
 
             // Find and parse the model type hint.
             storm::models::ModelType type = AutoParser::analyzeHint(transitionsFilename);
@@ -29,19 +30,23 @@ namespace storm {
             // Do the actual parsing.
             std::shared_ptr<storm::models::sparse::Model<double>> model;
             switch (type) {
-                case storm::models::ModelType::Dtmc: {
+                case storm::models::ModelType::Dtmc:
+                {
                     model.reset(new storm::models::sparse::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
                     break;
                 }
-				case storm::models::ModelType::Ctmc: {
+                case storm::models::ModelType::Ctmc:
+                {
                     model.reset(new storm::models::sparse::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
                     break;
                 }
-				case storm::models::ModelType::Mdp: {
-					model.reset(new storm::models::sparse::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))));
+                case storm::models::ModelType::Mdp:
+                {
+                    model.reset(new storm::models::sparse::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))));
                     break;
                 }
-				case storm::models::ModelType::MarkovAutomaton: {
+                case storm::models::ModelType::MarkovAutomaton:
+                {
                     model.reset(new storm::models::sparse::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)));
                     break;
                 }

src/parser/AutoParser.h

@@ -41,12 +41,16 @@ namespace storm {
 			 * @param labelingFilename The path and name of the file containing the labels for the states of the model.
 			 * @param stateRewardFilename The path and name of the file that contains the state reward of the model. This file is optional.
 			 * @param transitionRewardFilename The path and name of the file that contains the transition rewards of the model. This file is optional.
+                         * @param choiceLabelingFilename The path and name of the file that contains the choice labeling of the model. This file is optional.
+                         * Note: this file is only meaningful for certain models (currently only MDPs). If the model is not of a type for which this input
+                         * is meaningful, this file will not be parsed.
 			 * @return A shared_ptr containing the resulting model.
 			 */
             static std::shared_ptr<storm::models::sparse::Model<double>> parseModel(std::string const& transitionsFilename,
                                                                                     std::string const& labelingFilename,
                                                                                     std::string const& stateRewardFilename = "",
-                                                                                    std::string const & transitionRewardFilename = "");
+                                                                                    std::string const& transitionRewardFilename = "",
+                                                                                    std::string const& choiceLabelingFilename = "");
 
 		private:
             // Define the maximal length of a hint in the file.

src/parser/NondeterministicModelParser.cpp

@@ -8,11 +8,12 @@
 #include "src/parser/NondeterministicSparseTransitionParser.h"
 #include "src/parser/AtomicPropositionLabelingParser.h"
 #include "src/parser/SparseStateRewardParser.h"
+#include "src/parser/SparseChoiceLabelingParser.h"
 
 namespace storm {
     namespace parser {
 
-		NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
+        NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename, std::string const& choiceLabelingFilename) {
 
             // Parse the transitions.
             storm::storage::SparseMatrix<double> transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename)));
@@ -24,30 +25,37 @@ namespace storm {
 
             // Only parse state rewards if a file is given.
             boost::optional<std::vector<double>> stateRewards;
-			if (stateRewardFilename != "") {
-				stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename);
+            if (!stateRewardFilename.empty()) {
+                stateRewards = std::move(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename));
             }
 
             // Only parse transition rewards if a file is given.
             boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
-			if (transitionRewardFilename != "") {
-				transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions);
+            if (!transitionRewardFilename.empty()) {
+                transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions));
+            }
+
+            // Only parse choice labeling if a file is given.
+            boost::optional<std::vector < storm::models::sparse::LabelSet>> choiceLabeling;
+            if (!choiceLabelingFilename.empty()) {
+                choiceLabeling = std::move(storm::parser::SparseChoiceLabelingParser::parseChoiceLabeling(transitions.getRowGroupIndices(), choiceLabelingFilename));
             }
 
             // Construct the result.
             Result result(std::move(transitions), std::move(labeling));
-			result.stateRewards = stateRewards;
-			result.transitionRewards = transitionRewards;
+            result.stateRewards = std::move(stateRewards);
+            result.transitionRewards = std::move(transitionRewards);
+            result.choiceLabeling = std::move(choiceLabeling);
 
             return result;
         }
 
-        storm::models::sparse::Mdp<double> NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) {
-            Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename);
+        storm::models::sparse::Mdp<double> NondeterministicModelParser::parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename, std::string const& choiceLabelingFilename) {
+            Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename);
 
             std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<double>> rewardModels;
             rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<double>(parserResult.stateRewards, boost::optional<std::vector<double>>(), parserResult.transitionRewards)));
-            return storm::models::sparse::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+            return storm::models::sparse::Mdp<double>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), std::move(parserResult.choiceLabeling));
         }
 
     } /* namespace parser */

src/parser/NondeterministicModelParser.h

@@ -60,6 +60,11 @@ namespace storm {
 				 * Optional rewards for each transition.
 				 */
 				boost::optional<storm::storage::SparseMatrix<double>> transitionRewards;
+
+                                /*!
+                                 * Optional choice labeling.
+                                 */
+                                boost::optional<std::vector<storm::models::sparse::LabelSet>> choiceLabeling;
 			};
 
 			/*!
@@ -75,9 +80,10 @@ namespace storm {
 			 * @param labelingFilename The path and name of the file containing the labels for the states of the model.
 			 * @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
 			 * @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
+                         * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional.
 			 * @return The parsed Mdp.
 			 */
-            static storm::models::sparse::Mdp<double> parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = "");
+                        static storm::models::sparse::Mdp<double> parseMdp(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = "", std::string const& choiceLabelingFilename = "");
 
 		private:
 
@@ -92,9 +98,10 @@ namespace storm {
 			 * @param labelingFilename The path and name of the file containing the labels for the states of the model.
 			 * @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional.
 			 * @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional.
+                         * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional.
 			 * @return The parsed model encapsulated in a Result structure.
 			 */
-			static Result parseNondeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", std::string const & transitionRewardFilename = "");
+			static Result parseNondeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "", std::string const& choiceLabelingFilename = "");
 
 		};
 

src/parser/SparseStateRewardParser.cpp

@@ -1,9 +1,3 @@
-/*!
- * SparseStateRewardParser.cpp
- *
- *  Created on: 23.12.2012
- *      Author: Christian Dehnert
- */
 #include <iostream>
 #include "src/parser/SparseStateRewardParser.h"
 
@@ -43,7 +37,7 @@ namespace storm {
 			// Iterate over states.
 			while (buf[0] != '\0') {
 
-				// Parse state number and reward value.
+				// Parse state.
 				state = checked_strtol(buf, &buf);
 
 				// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
@@ -58,6 +52,7 @@ namespace storm {
 					throw storm::exceptions::OutOfRangeException() << "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\"";
 				}
 
+                                // Parse reward value.
 				reward = checked_strtod(buf, &buf);
 
 				if (reward < 0.0) {

src/settings/modules/GeneralSettings.cpp

@@ -33,6 +33,7 @@ namespace storm {
             const std::string GeneralSettings::propertyOptionShortName = "prop";
             const std::string GeneralSettings::transitionRewardsOptionName = "transrew";
             const std::string GeneralSettings::stateRewardsOptionName = "staterew";
+            const std::string GeneralSettings::choiceLabelingOptionName = "choicelab";
             const std::string GeneralSettings::counterexampleOptionName = "counterexample";
             const std::string GeneralSettings::counterexampleOptionShortName = "cex";
             const std::string GeneralSettings::dontFixDeadlockOptionName = "nofixdl";
@@ -84,6 +85,8 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
                 
                 std::vector<std::string> engines = {"sparse", "hybrid", "dd"};
@@ -193,6 +196,14 @@ namespace storm {
                 return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString();
             }
             
+            bool GeneralSettings::isChoiceLabelingSet() const {
+                return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet();
+            }
+                
+            std::string GeneralSettings::getChoiceLabelingFilename() const {
+                return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
             bool GeneralSettings::isCounterexampleSet() const {
                 return this->getOption(counterexampleOptionName).getHasOptionBeenSet();
             }

src/settings/modules/GeneralSettings.h

@@ -20,7 +20,10 @@ namespace storm {
             class GeneralSettings : public ModuleSettings {
             public:
                 // An enumeration of all engines.
-                enum class Engine { Sparse, Hybrid, Dd };
+
+                enum class Engine {
+                    Sparse, Hybrid, Dd
+                };
 
                 /*!
                  * Creates a new set of general settings that is managed by the given manager.
@@ -175,6 +178,21 @@ namespace storm {
                  */
                 std::string getStateRewardsFilename() const;
 
+                /*!
+                 * Retrieves whether the choice labeling option was set.
+                 * 
+                 * @return True iff the choice labeling option was set.
+                 */
+                bool isChoiceLabelingSet() const;
+
+                /*!
+                 * Retrieves the name of the file that contains the choice labeling
+                 * if the model was given using the explicit option.
+                 *
+                 * @return The name of the file that contains the choice labeling.
+                 */
+                std::string getChoiceLabelingFilename() const;
+
                 /*!
                  * Retrieves whether the counterexample option was set.
                  *
@@ -347,6 +365,7 @@ namespace storm {
                 static const std::string propertyOptionShortName;
                 static const std::string transitionRewardsOptionName;
                 static const std::string stateRewardsOptionName;
+                static const std::string choiceLabelingOptionName;
                 static const std::string counterexampleOptionName;
                 static const std::string counterexampleOptionShortName;
                 static const std::string dontFixDeadlockOptionName;

src/utility/storm.h

@@ -75,8 +75,8 @@ namespace storm {
     
 
  template<typename ValueType>
-            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>()) {
-                return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "");
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& choiceLabelingFile = boost::optional<std::string>()) {
+                return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
             }
             
             template<typename ValueType>
@@ -380,7 +380,7 @@ namespace storm {
                 storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
                 
                 STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
-                std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
+                std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>(), settings.isChoiceLabelingSet() ? settings.getChoiceLabelingFilename() : boost::optional<std::string>());
                 
                 // Preprocess the model if needed.
                 model = preprocessModel<ValueType>(model, formulas);