diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f4b009b7e..914a8153d 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -4,6 +4,7 @@ #include "src/utility/storm.h" #include "src/storage/SymbolicModelDescription.h" +#include "src/utility/ExplicitExporter.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidSettingsException.h" @@ -216,6 +217,14 @@ namespace storm { } else { verifySparseModel(sparseModel, formulas, onlyInitialStatesRelevant); } + + // And export if required. + if(storm::settings::getModule().isExportExplicitSet()) { + std::ofstream ofs; + ofs.open(storm::settings::getModule().getExportExplicitFilename(), std::ofstream::out); + storm::exporter::explicitExportSparseModel(ofs, sparseModel, model.getParameterNames()); + ofs.close(); + } } template diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index c174f1f51..cea559f4e 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -14,7 +14,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; - const std::string IOSettings::exportMatOptionName = "exportmat"; + const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::prismInputOptionName = "prism"; @@ -34,7 +34,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportMatOptionName, "", "If given, the loaded model will be written to the specified file in the mat format.") + 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, 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.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) @@ -66,6 +66,14 @@ namespace storm { std::string IOSettings::getExportDotFilename() const { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isExportExplicitSet() const { + return this->getOption(exportExplicitOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportExplicitFilename() const { + return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString(); + } bool IOSettings::isExplicitSet() const { return this->getOption(explicitOptionName).getHasOptionBeenSet(); diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index ae6ce6831..da4238e5c 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -35,6 +35,22 @@ namespace storm { */ std::string getExportDotFilename() const; + + /*! + * Retrieves whether the export-to-explicit option was set + * + * @return True if the export-to-explicit option was set + */ + bool isExportExplicitSet() const; + + + /*! + * Retrieves thename in which to write the model in explicit format, if the option was set. + * + * @return The name of the file in which to write the exported mode. + */ + std::string getExportExplicitFilename() const; + /*! * Retrieves whether the explicit option was set. * @@ -200,7 +216,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string exportDotOptionName; - static const std::string exportMatOptionName; + static const std::string exportExplicitOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; static const std::string prismInputOptionName; diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index 4c144eff8..62440992d 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -57,6 +57,20 @@ namespace storm { return boost::get(modelDescription.get()); } + std::vector SymbolicModelDescription::getParameterNames() const { + std::vector result; + if(isJaniModel()) { + for(auto const& c : asJaniModel().getUndefinedConstants()) { + result.push_back(c.get().getName()); + } + } else { + for(auto const& c : asPrismProgram().getUndefinedConstants()) { + result.push_back(c.get().getName()); + } + } + return result; + } + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { if (this->isJaniModel()) { return *this; diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h index 8b5b85d88..730578ac4 100644 --- a/src/storage/SymbolicModelDescription.h +++ b/src/storage/SymbolicModelDescription.h @@ -27,6 +27,8 @@ namespace storm { storm::jani::Model const& asJaniModel() const; storm::prism::Program const& asPrismProgram() const; + std::vector getParameterNames() const; + SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; diff --git a/src/utility/ExplicitExporter.cpp b/src/utility/ExplicitExporter.cpp new file mode 100644 index 000000000..77ff2aa1f --- /dev/null +++ b/src/utility/ExplicitExporter.cpp @@ -0,0 +1,62 @@ +#include "ExplicitExporter.h" + +#include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" + +#include "src/models/sparse/StandardRewardModel.h" + + +namespace storm { + namespace exporter { + template + void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { + STORM_LOG_THROW(sparseModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); + std::shared_ptr> mdp = sparseModel->template as>(); + + os << "// Exported by Storm" << std::endl; + os << "@type: mdp" << std::endl; + os << "@parameters" << std::endl; + for (auto const& p : parameters) { + os << p << " "; + } + os << std::endl; + os << "@nr_states" << std::endl << mdp->getNumberOfStates() << std::endl; + os << "@model" << std::endl; + storm::storage::SparseMatrix const& matrix = mdp->getTransitionMatrix(); + + for (typename storm::storage::SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { + os << "state " << group; + for(auto const& label : mdp->getStateLabeling().getLabelsOfState(group)) { + os << " " << label; + } + os << std::endl; + typename storm::storage::SparseMatrix::index_type start = matrix.getRowGroupIndices()[group]; + typename storm::storage::SparseMatrix::index_type end = matrix.getRowGroupIndices()[group + 1]; + + for (typename storm::storage::SparseMatrix::index_type i = start; i < end; ++i) { + // Print the actual row. + os << "\taction"; + if(mdp->hasChoiceLabeling()) { + //TODO + } + os << std::endl; + for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { + os << "\t\t" << it->getColumn() << " : " << it->getValue() << std::endl; + } + + } + } + + } + + + + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + } +} \ No newline at end of file diff --git a/src/utility/ExplicitExporter.h b/src/utility/ExplicitExporter.h new file mode 100644 index 000000000..fd158f001 --- /dev/null +++ b/src/utility/ExplicitExporter.h @@ -0,0 +1,15 @@ +#pragma once +#include +#include + +#include "src/models/sparse/Model.h" + +namespace storm { + namespace exporter { + + template + void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + + + } +} \ No newline at end of file