Fixed json export settings

src/storm-dft/CMakeLists.txt

@@ -17,7 +17,7 @@ set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-dft)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-parsers ${STORM_DFT_LINK_LIBRARIES})
+target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers ${STORM_DFT_LINK_LIBRARIES})
 
 # Install storm headers to include directory.
 foreach(HEADER ${STORM_DFT_HEADERS})

src/storm-dft/api/storm-dft.cpp

@@ -2,6 +2,7 @@
 
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
 #include "storm-dft/settings/modules/DftGspnSettings.h"
+#include "storm-conv/api/storm-conv.h"
 
 namespace storm {
     namespace api {
@@ -64,9 +65,12 @@ namespace storm {
         }
 
         std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) {
+
+            // Build Jani model
             storm::builder::JaniGSPNBuilder builder(gspn);
-            std::shared_ptr<storm::jani::Model> model(builder.build());
+            std::shared_ptr<storm::jani::Model> model(builder.build("dft_gspn"));
 
+            // Build properties
             std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn.getExpressionManager();
             storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
             storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
@@ -80,10 +84,12 @@ namespace storm {
 
             auto timeBoundedProperty = storm::jani::Property("time-bounded", tbUntil);
             auto mttfProperty = storm::jani::Property("mttf", rewFormula);
-            storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
-            if (janiSettings.isJaniFileSet()) {
+
+            // Export Jani to file
+            storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule<storm::settings::modules::DftGspnSettings>();
+            if (dftGspnSettings.isWriteToJaniSet()) {
                 // Currently no properties are set
-                storm::api::exportJaniModel(*model, {}, janiSettings.getJaniFilename());
+                storm::api::exportJaniToFile(*model, {}, dftGspnSettings.getWriteToJaniFilename());
             }
 
             return model;

src/storm-dft/settings/modules/DftGspnSettings.cpp

@@ -17,7 +17,7 @@ namespace storm {
             const std::string DftGspnSettings::disableSmartTransformationOptionName = "disable-smart";
             const std::string DftGspnSettings::mergeDCFailedOptionName = "merge-dc-failed";
             const std::string DftGspnSettings::extendPrioritiesOptionName = "extend-priorities";
-
+            const std::string DftGspnSettings::writeToJaniOptionName = "to-jani";
 
             DftGspnSettings::DftGspnSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
@@ -25,6 +25,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, mergeDCFailedOptionName, false, "Enable merging of Don't Care and Failed places into a combined place.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, extendPrioritiesOptionName, false,
                                                                "Enable experimental calculation of transition priorities").build());
+                 this->addOption(storm::settings::OptionBuilder(moduleName, writeToJaniOptionName, false, "Destination for the jani output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file"    ).build()).build());
             }
 
             bool DftGspnSettings::isTransformToGspn() const {
@@ -43,6 +44,14 @@ namespace storm {
                 return this->getOption(extendPrioritiesOptionName).getHasOptionBeenSet();
             }
 
+            bool DftGspnSettings::isWriteToJaniSet() const {
+                return this->getOption(writeToJaniOptionName).getHasOptionBeenSet();
+            }
+
+            std::string DftGspnSettings::getWriteToJaniFilename() const {
+                return this->getOption(writeToJaniOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
             void DftGspnSettings::finalize() {
             }
 

src/storm-dft/settings/modules/DftGspnSettings.h

@@ -41,10 +41,24 @@ namespace storm {
                 /*!
                  * Retrieves whether the experimental setting of priorities should be used
                  *
-                 * @return True if the settig is enabled is enabled.
+                 * @return True if the setting is enabled.
                  */
                 bool isExtendPriorities() const;
 
+                /*!
+                 * Retrieves whether the GSPN should be exported as a Jani file.
+                 *
+                 * @return True if the Jani file should be exported.
+                 */
+                bool isWriteToJaniSet() const;
+
+                /*!
+                 * Retrieves the jani filename for export.
+                 *
+                 * @return Filename.
+                 */
+                std::string getWriteToJaniFilename() const;
+
                 bool check() const override;
 
                 void finalize() override;
@@ -58,6 +72,7 @@ namespace storm {
                 static const std::string disableSmartTransformationOptionName;
                 static const std::string mergeDCFailedOptionName;
                 static const std::string extendPrioritiesOptionName;
+                static const std::string writeToJaniOptionName;
             };
 
         } // namespace modules