First version of Jani-to-Dot.

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);
+                    }
                     
                 }
                 

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.");
                 

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;

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;
+
+        }
     }
 }

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.

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 << "}";
+        }
     }
 }

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;