Refactoring for transformation DFT->GSPN->JANI

src/storm-dft-cli/storm-dft.cpp

@@ -52,7 +52,15 @@ void processOptions() {
 
     if (dftGspnSettings.isTransformToGspn()) {
         // Transform to GSPN
-        storm::api::transformToGSPN(*dft);
+        std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> pair = storm::api::transformToGSPN(*dft);
+        std::shared_ptr<storm::gspn::GSPN> gspn = pair.first;
+        uint64_t toplevelFailedPlace = pair.second;
+
+        // Export
+        storm::api::handleGSPNExportSettings(*gspn);
+
+        // Transform to Jani
+        std::shared_ptr<storm::jani::Model> model = storm::api::transformToJani(*gspn, toplevelFailedPlace);
         return;
     }
 

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

@@ -29,7 +29,7 @@ namespace storm {
         }
 
         template<>
-        void transformToGSPN(storm::storage::DFT<double> const& dft) {
+        std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::storage::DFT<double> const& dft) {
             storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
             storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule<storm::settings::modules::DftGspnSettings>();
 
@@ -46,15 +46,15 @@ namespace storm {
             storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
             auto priorities = gspnTransformator.computePriorities();
             gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed());
-            storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
-            uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
+            std::shared_ptr<storm::gspn::GSPN> gspn(gspnTransformator.obtainGSPN());
+            return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId());
+        }
 
-            // Export
-            storm::api::handleGSPNExportSettings(*gspn);
+        std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace) {
+            storm::builder::JaniGSPNBuilder builder(gspn);
+            std::shared_ptr<storm::jani::Model> model(builder.build());
 
-            std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
-            storm::builder::JaniGSPNBuilder builder(*gspn);
-            storm::jani::Model* model = builder.build();
+            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();
@@ -70,12 +70,11 @@ namespace storm {
                 storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename());
             }
 
-            delete model;
-            delete gspn;
+            return model;
         }
 
         template<>
-        void transformToGSPN(storm::storage::DFT<storm::RationalFunction> const& dft) {
+        std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::storage::DFT<storm::RationalFunction> const& dft) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation to GSPN not supported for this data type.");
         }
 

src/storm-dft/api/storm-dft.h

@@ -24,7 +24,7 @@ namespace storm {
          */
         template<typename ValueType>
         std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTGalileo(std::string const& file) {
-             return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTGalileoParser<ValueType>::parseDFT(file));
+            return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTGalileoParser<ValueType>::parseDFT(file));
         }
 
         /*!
@@ -36,8 +36,8 @@ namespace storm {
          */
         template<typename ValueType>
         std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJson(std::string const& file) {
-                storm::parser::DFTJsonParser<ValueType> parser;
-                return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(file));
+            storm::parser::DFTJsonParser<ValueType> parser;
+            return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(file));
         }
 
         /*!
@@ -52,8 +52,10 @@ namespace storm {
          *
          * @return Result.
          */
-        template <typename ValueType>
-        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, bool printOutput) {
+        template<typename ValueType>
+        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
+        analyzeDFT(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation,
+                   bool enableDC, bool printOutput) {
             storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
             typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, 0.0);
             if (printOutput) {
@@ -76,10 +78,13 @@ namespace storm {
          *
          * @return Result.
          */
-        template <typename ValueType>
-        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
+        template<typename ValueType>
+        typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results
+        analyzeDFTApprox(storm::storage::DFT<ValueType> const& dft, std::vector<std::shared_ptr<storm::logic::Formula const>> const& properties, bool symred,
+                         bool allowModularisation, bool enableDC, double approximationError, bool printOutput) {
             storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
-            typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC, approximationError);
+            typename storm::modelchecker::DFTModelChecker<ValueType>::dft_results results = modelChecker.check(dft, properties, symred, allowModularisation, enableDC,
+                                                                                                               approximationError);
             if (printOutput) {
                 modelChecker.printTimings();
                 modelChecker.printResults();
@@ -109,9 +114,21 @@ namespace storm {
          * Transform DFT to GSPN.
          *
          * @param dft DFT.
+         *
+         * @return Pair of GSPN and id of failed place corresponding to the top level element.
          */
         template<typename ValueType>
-        void transformToGSPN(storm::storage::DFT<ValueType> const& dft);
+        std::pair<std::shared_ptr<storm::gspn::GSPN>, uint64_t> transformToGSPN(storm::storage::DFT<ValueType> const& dft);
+
+        /*!
+         * Transform GSPN to Jani model.
+         *
+         * @param gspn GSPN.
+         * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT.
+         *
+         * @return JANI model.
+         */
+        std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace);
 
     }
 }