diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index bdba45a30..7310f56c6 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -15,6 +15,7 @@ #include "storm/settings/modules/JaniExportSettings.h" #include "storm/utility/resources.h" +#include "storm/utility/file.h" #include "storm/utility/storm-version.h" @@ -241,6 +242,13 @@ namespace storm { properties.push_back(input.second.at(propName)); } } + + if(ioSettings.isExportJaniDotSet()) { + std::ofstream out; + storm::utility::openFile(ioSettings.getExportJaniDotFilename(), out); + model.asJaniModel().writeDotToStream(out); + storm::utility::closeFile(out); + } } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 1ade861dd..51d7fe512 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; + const std::string IOSettings::exportJaniDotOptionName = "exportjanidot"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::explicitDrnOptionName = "explicit-drn"; @@ -40,6 +41,7 @@ namespace storm { const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; const std::string IOSettings::noBuildOptionName = "nobuild"; const std::string IOSettings::fullModelBuildOptionName = "buildfull"; + const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab"; const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; const std::string IOSettings::propertyOptionName = "prop"; @@ -50,6 +52,8 @@ 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, exportJaniDotOptionName, "", "If given, the loaded jani 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, 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) @@ -65,6 +69,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, include choice labels").build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build()) @@ -94,6 +99,14 @@ namespace storm { std::string IOSettings::getExportDotFilename() const { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isExportJaniDotSet() const { + return this->getOption(exportJaniDotOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportJaniDotFilename() const { + return this->getOption(exportJaniDotOptionName).getArgumentByName("filename").getValueAsString(); + } bool IOSettings::isExportExplicitSet() const { return this->getOption(exportExplicitOptionName).getHasOptionBeenSet(); @@ -225,6 +238,10 @@ namespace storm { return this->getOption(noBuildOptionName).getHasOptionBeenSet(); } + bool IOSettings::isBuildChoiceLabelsSet() const { + return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); + } + bool IOSettings::isPropertySet() const { return this->getOption(propertyOptionName).getHasOptionBeenSet(); } @@ -247,6 +264,8 @@ namespace storm { // Ensure that not two explicit input models were given. STORM_LOG_THROW(!isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "Explicit model "); + STORM_LOG_THROW(!isExportJaniDotSet() || isJaniInputSet(), storm::exceptions::InvalidSettingsException, "Jani-to-dot export is only available for jani models" ); + // Ensure that the model was given either symbolically or explicitly. 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."); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 0e329b840..d7674e9f2 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -35,6 +35,20 @@ namespace storm { */ std::string getExportDotFilename() const; + /*! + * Retrieves whether the export-to-dot option for jani was set. + * + * @return True if the export-to-jani-dot option was set. + */ + bool isExportJaniDotSet() const; + + /*! + * Retrieves the name in which to write the jani model in dot format, if the export-to-jani-dot option was set. + * + * @return The name of the file in which to write the exported model. + */ + std::string getExportJaniDotFilename() const; + /*! * Retrieves whether the export-to-explicit option was set * @@ -277,6 +291,12 @@ namespace storm { */ bool isBuildFullModelSet() const; + /*! + * Retrieves whether the choice labels should be build + * @return + */ + bool isBuildChoiceLabelsSet() const; + bool check() const override; void finalize() override; @@ -286,6 +306,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string exportDotOptionName; + static const std::string exportJaniDotOptionName; static const std::string exportExplicitOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; @@ -308,6 +329,7 @@ namespace storm { static const std::string prismCompatibilityOptionShortName; static const std::string fullModelBuildOptionName; static const std::string noBuildOptionName; + static const std::string buildChoiceLabelOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 88641c318..00e5bf14b 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -528,5 +528,36 @@ namespace storm { return result; } + + void Automaton::writeDotToStream(std::ostream& outStream) const { + outStream << "\tsubgraph " << name << " {" << std::endl; + + // Write all locations to the stream. + uint64_t locIndex = 0; + for (auto const& loc : locations) { + outStream << "\t" << name << "_s" << locIndex << "[ label=\"" << loc.getName() << "\"];" << std::endl; + ++locIndex; + } + // Write for each edge an node to the stream; + uint64_t edgeIndex = 0; + for (auto const& edge : edges) { + outStream << "\t" << name << "_e" << edgeIndex << ";" << std::endl; + ++edgeIndex; + } + + // Connect edges + edgeIndex = 0; + for (auto const& edge : edges) { + outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << ";" << std::endl; + for (auto const& edgeDest : edge.getDestinations()) { + outStream << "\t" << name << "_e" << edgeIndex << " -> " << name << "_s" << edgeDest.getLocationIndex() << ";" << std::endl; + } + ++edgeIndex; + } + + + outStream << "\t}" << std::endl; + + } } } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 6c940d464..cf8c92fd7 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -371,6 +371,8 @@ namespace storm { * Checks the automaton for linearity. */ bool isLinear() const; + + void writeDotToStream(std::ostream& outStream = std::cout) const; private: /// The name of the automaton. diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index e7ea47349..7cd420a65 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1165,5 +1165,16 @@ namespace storm { return newModel; } + + void Model::writeDotToStream(std::ostream& outStream) const { + outStream << "digraph " << name << " {" << std::endl; + + for (auto const& automaton : automata) { + automaton.writeDotToStream(outStream); + outStream << std::endl; + } + + outStream << "}"; + } } } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 201e1ecc5..bb0b48f26 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -448,6 +448,8 @@ namespace storm { * @return */ bool reusesActionsInComposition() const; + + void writeDotToStream(std::ostream& outStream = std::cout) const; /// The name of the silent action. static const std::string SILENT_ACTION_NAME;