diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index efdb54d42..a524de567 100644
--- a/src/storm/cli/cli.cpp
+++ b/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
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index a3883512f..38ed1f551 100644
--- a/src/storm/cli/entrypoints.h
+++ b/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);
diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp
new file mode 100644
index 000000000..d343e4b6c
--- /dev/null
+++ b/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
diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h
new file mode 100644
index 000000000..536f1b209
--- /dev/null
+++ b/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_ */
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index 9f07c0219..1ade861dd 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/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.")
@@ -109,7 +114,15 @@ namespace storm {
std::string IOSettings::getLabelingFilename() const {
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();
}
@@ -230,9 +243,12 @@ namespace storm {
bool IOSettings::check() const {
// 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.");
diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h
index 711ec2d97..0e329b840 100644
--- a/src/storm/settings/modules/IOSettings.h
+++ b/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;
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index ada4ea0d1..75c52d80d 100644
--- a/src/storm/utility/storm.h
+++ b/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);