Framework for DRN parser

src/storm/cli/cli.cpp

@@ -294,7 +294,7 @@ namespace storm {
                 } else {
                     buildAndCheckSymbolicModel<double>(model, properties, true);
                 }
-            } else if (ioSettings.isExplicitSet()) {
+            } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) {
                 STORM_LOG_THROW(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
                 
                 // If the model is given in an explicit format, we parse the properties without allowing expressions

src/storm/cli/entrypoints.h

@@ -385,10 +385,15 @@ namespace storm {
         void buildAndCheckExplicitModel(std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
             storm::settings::modules::IOSettings const& settings = storm::settings::getModule<storm::settings::modules::IOSettings>();
 
-            STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
+            STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
 
             storm::utility::Stopwatch modelBuildingWatch(true);
-            std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional<std::string>(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional<std::string>(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional<std::string>(settings.getChoiceLabelingFilename()) : boost::none);
+            std::shared_ptr<storm::models::ModelBase> model;
+            if (settings.isExplicitSet()) {
+                model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional<std::string>(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional<std::string>(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional<std::string>(settings.getChoiceLabelingFilename()) : boost::none);
+            } else {
+                model = buildExplicitDRNModel<ValueType>(settings.getExplicitDRNFilename());
+            }
             modelBuildingWatch.stop();
             STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl);
             

src/storm/parser/DirectEncodingParser.cpp

@@ -0,0 +1,72 @@
+#include "storm/parser/DirectEncodingParser.h"
+
+#include <cstdio>
+#include <cstring>
+#include <cstdint>
+#include <clocale>
+#include <iostream>
+#include <string>
+
+#include "storm/exceptions/FileIoException.h"
+#include "storm/exceptions/WrongFormatException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/settings/SettingsManager.h"
+
+#include "storm/adapters/CarlAdapter.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/file.h"
+
+namespace storm {
+    namespace parser {
+
+        template<typename ValueType, typename RewardModelType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseModel(std::string const& filename) {
+
+            // Load file
+            STORM_LOG_INFO("Reading from file " << filename);
+            std::ifstream file;
+            storm::utility::openFile(filename, file);
+            std::string line;
+
+            // Initialize
+            storm::models::ModelType type;
+
+            // Iterate over all lines
+            while (std::getline(file, line)) {
+                STORM_LOG_TRACE("Parsing: " << line);
+            }
+
+            // Done parsing
+            storm::utility::closeFile(file);
+
+
+            // Build model
+            switch (type) {
+                case storm::models::ModelType::Dtmc:
+                {
+                    STORM_LOG_THROW(false, storm::exceptions::FileIoException, "DTMC not supported.");
+                }
+                case storm::models::ModelType::Ctmc:
+                {
+                    STORM_LOG_THROW(false, storm::exceptions::FileIoException, "CTMC not supported.");
+                }
+                case storm::models::ModelType::Mdp:
+                {
+                    STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MDP not supported.");
+                }
+                case storm::models::ModelType::MarkovAutomaton:
+                {
+                    STORM_LOG_THROW(false, storm::exceptions::FileIoException, "MA not supported.");
+                }
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Unknown/Unhandled model type " << type << " which cannot be parsed.");
+            }
+        }
+
+        template class DirectEncodingParser<double>;
+
+#ifdef STORM_HAVE_CARL
+        template class DirectEncodingParser<storm::RationalFunction>;
+#endif
+    } // namespace parser
+} // namespace storm

src/storm/parser/DirectEncodingParser.h

@@ -0,0 +1,33 @@
+#ifndef STORM_PARSER_DIRECTENCODINGPARSER_H_
+#define STORM_PARSER_DIRECTENCODINGPARSER_H_
+
+#include "storm/models/sparse/Model.h"
+
+
+namespace storm {
+    namespace parser {
+
+        /*!
+         *	Parser for models in the DRN format with explicit encoding.
+         */
+        template<typename ValueType, typename RewardModelType = models::sparse::StandardRewardModel<ValueType>>
+        class DirectEncodingParser {
+        public:
+
+            /*!
+             * Load a model in DRN format from a file and create the model.
+             *
+             * @param file The DRN file to be parsed.
+             *
+             * @return A sparse model
+             */
+            static std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> parseModel(std::string const& file);
+
+        private:
+
+        };
+
+    } // namespace parser
+} // namespace storm
+
+#endif /* STORM_PARSER_DIRECTENCODINGPARSER_H_ */

src/storm/settings/modules/IOSettings.cpp

@@ -21,6 +21,8 @@ namespace storm {
             const std::string IOSettings::exportExplicitOptionName = "exportexplicit";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
+            const std::string IOSettings::explicitDrnOptionName = "explicit-drn";
+            const std::string IOSettings::explicitDrnOptionShortName = "drn";
             const std::string IOSettings::prismInputOptionName = "prism";
             const std::string IOSettings::janiInputOptionName = "jani";
             const std::string IOSettings::prismToJaniOptionName = "prism2jani";
@@ -53,6 +55,9 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, explicitDrnOptionName, false, "Parses the model given in the DRN format.").setShortName(explicitDrnOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("drn filename", "The name of the DRN file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build())
+                                .build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
@@ -110,6 +115,14 @@ namespace storm {
                 return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString();
             }
 
+            bool IOSettings::isExplicitDRNSet() const {
+                return this->getOption(explicitDrnOptionName).getHasOptionBeenSet();
+            }
+
+            std::string IOSettings::getExplicitDRNFilename() const {
+                return this->getOption(explicitDrnOptionName).getArgumentByName("drn filename").getValueAsString();
+            }
+
             bool IOSettings::isPrismInputSet() const {
                 return this->getOption(prismInputOptionName).getHasOptionBeenSet();
             }
@@ -231,8 +244,11 @@ namespace storm {
                 // Ensure that not two symbolic input models were given.
                 STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet(), storm::exceptions::InvalidSettingsException, "Symbolic model ");
 
+                // Ensure that not two explicit input models were given.
+                STORM_LOG_THROW(!isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "Explicit model ");
+
                 // Ensure that the model was given either symbolically or explicitly.
-                STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both.");
+                STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both.");
                 
                 // Make sure PRISM-to-JANI conversion is only set if the actual input is in PRISM format.
                 STORM_LOG_THROW(!isPrismToJaniSet() || isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the transformation from PRISM to JANI, the input model must be given in the prism format.");

src/storm/settings/modules/IOSettings.h

@@ -72,6 +72,20 @@ namespace storm {
                  */
                 std::string getLabelingFilename() const;
 
+                /*!
+                 * Retrieves whether the explicit option with DRN was set.
+                 *
+                 * @return True if the explicit option with DRN was set.
+                 */
+                bool isExplicitDRNSet() const;
+
+                /*!
+                 * Retrieves the name of the file that contains the model in the DRN format.
+                 *
+                 * @return The name of the DRN file that contains the model.
+                 */
+                std::string getExplicitDRNFilename() const;
+
                 /*!
                  * Retrieves whether the PRISM language option was set.
                  *
@@ -275,6 +289,8 @@ namespace storm {
                 static const std::string exportExplicitOptionName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;
+                static const std::string explicitDrnOptionName;
+                static const std::string explicitDrnOptionShortName;
                 static const std::string prismInputOptionName;
                 static const std::string janiInputOptionName;
                 static const std::string prismToJaniOptionName;

src/storm/utility/storm.h

@@ -41,6 +41,7 @@
 #include "storm/storage/dd/Bdd.h"
 
 #include "storm/parser/AutoParser.h"
+#include "storm/parser/DirectEncodingParser.h"
 
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/Property.h"
@@ -110,6 +111,11 @@ namespace storm {
         return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
     }
 
+    template<typename ValueType>
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(std::string const& drnFile) {
+        return storm::parser::DirectEncodingParser<ValueType>::parseModel(drnFile);
+    }
+
     std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties);
     std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path);
     storm::prism::Program parseProgram(std::string const& path);