diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 334480cbf..771a0f8ee 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -569,7 +569,7 @@ namespace storm {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
if (ioSettings.isExportExplicitSet()) {
- storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector<std::string>());
+ storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector<std::string>(), !ioSettings.isExplicitExportPlaceholdersDisabled());
}
if (ioSettings.isExportDdSet()) {
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 0e3a43a97..8ca404609 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -364,7 +364,7 @@ namespace storm {
if (ioSettings.isExportExplicitSet()) {
std::vector<std::string> parameterNames;
// TODO fill parameter names
- storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames);
+ storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames, !ioSettings.isExplicitExportPlaceholdersDisabled());
}
// Check lower bounds
@@ -442,7 +442,7 @@ namespace storm {
if (ioSettings.isExportExplicitSet()) {
std::vector<std::string> parameterNames;
// TODO fill parameter names
- storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames);
+ storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), parameterNames, !ioSettings.isExplicitExportPlaceholdersDisabled());
}
if (ioSettings.isExportDotSet()) {
storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename(), ioSettings.getExportDotMaxWidth());
diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index 979f76474..1ccc0cd56 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -333,7 +333,7 @@ namespace storm {
for (auto const& parameter : parameters) {
parameterNames.push_back(parameter.name());
}
- storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames);
+ storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames, !ioSettings.isExplicitExportPlaceholdersDisabled());
STORM_PRINT_AND_LOG(" done." << std::endl);
transformationPerformed = true;
}
diff --git a/src/storm/api/export.h b/src/storm/api/export.h
index 792319f31..e72496c39 100644
--- a/src/storm/api/export.h
+++ b/src/storm/api/export.h
@@ -19,10 +19,12 @@ namespace storm {
void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename);
template <typename ValueType>
- void exportSparseModelAsDrn(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::string const& filename, std::vector<std::string> const& parameterNames = {}) {
+ void exportSparseModelAsDrn(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::string const& filename, std::vector<std::string> const& parameterNames = {}, bool allowPlaceholders=true) {
std::ofstream stream;
storm::utility::openFile(filename, stream);
- storm::exporter::explicitExportSparseModel(stream, model, parameterNames);
+ storm::exporter::DirectEncodingOptions options;
+ options.allowPlaceholders = allowPlaceholders;
+ storm::exporter::explicitExportSparseModel(stream, model, parameterNames, options);
storm::utility::closeFile(stream);
}
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index e2ecdf14b..95c67a19e 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/src/storm/settings/modules/IOSettings.cpp
@@ -50,6 +50,8 @@ namespace storm {
const std::string IOSettings::qvbsInputOptionName = "qvbs";
const std::string IOSettings::qvbsInputOptionShortName = "qvbs";
const std::string IOSettings::qvbsRootOptionName = "qvbsroot";
+
+ std::string preventDRNPlaceholderOptionName = "nodrnplaceholders";
IOSettings::IOSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, false, "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced()
@@ -63,6 +65,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, exportMonotonicityName, false, "Exports the result of monotonicity checking to the given file.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, preventDRNPlaceholderOptionName, true, "If given, the exported DRN contains no placeholders").setIsAdvanced().build());
this->addOption(storm::settings::OptionBuilder(moduleName, exportDdOptionName, "", "If given, the loaded model will be written to the specified file in the drdd format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
@@ -137,6 +140,10 @@ namespace storm {
return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString();
}
+ bool IOSettings::isExplicitExportPlaceholdersDisabled() const {
+ return this->getOption(preventDRNPlaceholderOptionName).getHasOptionBeenSet();
+ }
+
bool IOSettings::isExportDdSet() const {
return this->getOption(exportDdOptionName).getHasOptionBeenSet();
}
diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h
index 2cbdf65bf..3f41bdce7 100644
--- a/src/storm/settings/modules/IOSettings.h
+++ b/src/storm/settings/modules/IOSettings.h
@@ -152,6 +152,12 @@ namespace storm {
* @return The name of the DRN file that contains the model.
*/
std::string getExplicitDRNFilename() const;
+
+ /*!
+ * Retrieves whether we prevent the usage of placeholders in the explicit DRN format
+ * @return
+ */
+ bool isExplicitExportPlaceholdersDisabled() const;
/*!
* Retrieves whether the explicit option with IMCA was set.
diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp
index 2ea83e9d7..b3f6bf63e 100644
--- a/src/storm/utility/DirectEncodingExporter.cpp
+++ b/src/storm/utility/DirectEncodingExporter.cpp
@@ -18,7 +18,7 @@ namespace storm {
namespace exporter {
template<typename ValueType>
- void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters) {
+ void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters, DirectEncodingOptions const& options) {
// Notice that for CTMCs we write the rate matrix instead of probabilities
@@ -49,7 +49,10 @@ namespace storm {
// 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);
+ std::unordered_map<ValueType, std::string> placeholders;
+ if (options.allowPlaceholders) {
+ placeholders = generatePlaceholders(sparseModel, exitRates);
+ }
if (!placeholders.empty()) {
os << "@placeholders" << std::endl;
for (auto const& entry : placeholders) {
@@ -273,8 +276,8 @@ namespace storm {
// 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);
- template void explicitExportSparseModel<storm::RationalFunction>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel, std::vector<std::string> const& parameters);
+ template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters, DirectEncodingOptions const& options);
+ template void explicitExportSparseModel<storm::RationalNumber>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> sparseModel, std::vector<std::string> const& parameters,DirectEncodingOptions const& options);
+ template void explicitExportSparseModel<storm::RationalFunction>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel, std::vector<std::string> const& parameters,DirectEncodingOptions const& options);
}
}
diff --git a/src/storm/utility/DirectEncodingExporter.h b/src/storm/utility/DirectEncodingExporter.h
index c39622bf1..8f309fddf 100644
--- a/src/storm/utility/DirectEncodingExporter.h
+++ b/src/storm/utility/DirectEncodingExporter.h
@@ -8,6 +8,9 @@
namespace storm {
namespace exporter {
+ struct DirectEncodingOptions {
+ bool allowPlaceholders = true;
+ };
/*!
* Exports a sparse model into the explicit DRN format.
*
@@ -16,7 +19,7 @@ namespace storm {
* @param parameters List of parameters
*/
template<typename ValueType>
- void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters);
+ void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters, DirectEncodingOptions const& options=DirectEncodingOptions());
/*!