fixes for storm-dft and storm-gspn

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

@@ -34,7 +34,7 @@ namespace storm {
             storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
             uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
 
-            storm::api::handleGSPNExportSettings(*gspn, [&]std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const& builder) {
+            storm::api::handleGSPNExportSettings(*gspn, [&](storm::builder::JaniGSPNBuilder const& builder) {
                     std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
                     storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
 
@@ -45,11 +45,11 @@ namespace storm {
 
                     auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);
                     auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation);
-                    return {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)};
+                    std::vector<storm::jani::Property> res({storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)});
+                    return res;
                 }
             );
 
-            delete model;
             delete gspn;
         }
 

src/storm-gspn-cli/storm-gspn.cpp

@@ -112,7 +112,7 @@ int main(const int argc, const char **argv) {
             gspn->setCapacities(capacities);
         }
 
-        storm::api::handleGSPNExportSettings(*gspn, [&]std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const&) { return properties });
+        storm::api::handleGSPNExportSettings(*gspn, [&](storm::builder::JaniGSPNBuilder const&) { return properties; });
         
         delete gspn;
         return 0;

src/storm-gspn/api/storm-gspn.cpp

@@ -15,7 +15,7 @@ namespace storm {
             return builder.build();
         }
 
-        void handleGSPNExportSettings(storm::gspn::GSPN const& gspn, std::vector<storm::jani::Property> const& properties) {
+        void handleGSPNExportSettings(storm::gspn::GSPN const& gspn, std::function<std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const&)> const& janiProperyGetter) {
             storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>();
             if (exportSettings.isWriteToDotSet()) {
                 std::ofstream fs;
@@ -62,12 +62,13 @@ namespace storm {
                 auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
                 storm::converter::JaniConversionOptions options(jani);
     
-                storm::jani::Model* model = storm::api::buildJani(gspn);
+                storm::builder::JaniGSPNBuilder builder(gspn);
+                storm::jani::Model* model = builder.build();
+
                 storm::api::postprocessJani(*model, options);
-                storm::api::exportJaniToFile(*model, properties, storm::settings::getModule<storm::settings::modules::GSPNExportSettings>().getWriteToJaniFilename());
+                storm::api::exportJaniToFile(*model, janiProperyGetter(builder), storm::settings::getModule<storm::settings::modules::GSPNExportSettings>().getWriteToJaniFilename());
                 delete model;
             }
         }
-
     }
 }

src/storm-gspn/builder/JaniGSPNBuilder.h

@@ -21,7 +21,7 @@ namespace storm {
             
             storm::jani::Model* build(std::string const& automatonName = "gspn_automaton");
             
-            storm::jani::Variable const& getPlaceVariable(uint64_t placeId) {
+            storm::jani::Variable const& getPlaceVariable(uint64_t placeId) const {
                 return *vars.at(placeId);
             }
 

src/storm-gspn/settings/modules/GSPNSettings.cpp

@@ -16,15 +16,12 @@ namespace storm {
             
             const std::string GSPNSettings::gspnFileOptionName = "gspnfile";
             const std::string GSPNSettings::gspnFileOptionShortName = "gspn";
-            const std::string GSPNSettings::gspnToJaniOptionName = "to-jani";
-            const std::string GSPNSettings::gspnToJaniOptionShortName = "tj";
             const std::string GSPNSettings::capacitiesFileOptionName = "capacitiesfile";
             const std::string GSPNSettings::capacitiesFileOptionShortName = "capacities";
             
             
             GSPNSettings::GSPNSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, gspnFileOptionName, false, "Parses the GSPN.").setShortName(gspnFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, gspnToJaniOptionName, false, "Transform to JANI.").setShortName(gspnToJaniOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, capacitiesFileOptionName, false, "Capacaties as invariants for places.").setShortName(capacitiesFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
             }
             

src/storm-gspn/settings/modules/GSPNSettings.h

@@ -43,8 +43,6 @@ namespace storm {
             private:
                 static const std::string gspnFileOptionName;
                 static const std::string gspnFileOptionShortName;
-                static const std::string gspnToJaniOptionName;
-                static const std::string gspnToJaniOptionShortName;
                 static const std::string capacitiesFileOptionName;
                 static const std::string capacitiesFileOptionShortName;