several fixes in dft->gspn->jani code path: Most notably, mas are closed, successor nodes failed places keep intact and tb property is added

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

@@ -4,6 +4,7 @@
 #include "storm/cli/cli.h"
 #include "storm/exceptions/BaseException.h"
 
+#include "storm/logic/Formula.h"
 
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
@@ -71,20 +72,6 @@ void analyzeWithSMT(std::string filename) {
     //std::cout << "SMT result: " << sat << std::endl;
 }
 
-/*!
- * Load DFT from filename and transform into a GSPN.
- *
- * @param filename Path to DFT file in Galileo format.
- *
- */
-template <typename ValueType>
-storm::gspn::GSPN* transformDFT(std::string filename) {
-    storm::parser::DFTGalileoParser<ValueType> parser;
-    storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
-    storm::transformations::dft::DftToGspnTransformator<ValueType> gspnTransformator(dft);
-    gspnTransformator.transform();
-    return gspnTransformator.obtainGSPN();
-}
 
 /*!
  * Initialize the settings manager.
@@ -140,15 +127,30 @@ int main(const int argc, const char** argv) {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
         }
 
+        
         if (dftSettings.isTransformToGspn()) {
-            storm::gspn::GSPN* gspn = transformDFT<double>(dftSettings.getDftFilename());
+            storm::parser::DFTGalileoParser<double> parser;
+            storm::storage::DFT<double> dft = parser.parseDFT(dftSettings.getDftFilename());
+            storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft);
+            gspnTransformator.transform();
+            storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
+            uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
             storm::handleGSPNExportSettings(*gspn);
             
-            storm::jani::Model* model = storm::buildJani(*gspn);
+            std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
+            storm::builder::JaniGSPNBuilder builder(*gspn, exprManager);
+            storm::jani::Model* model =  builder.build();
+            storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
+            
+            
+            auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression());
+            auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, 0.0, 10.0);
+            auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula);
             
             storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
             if (janiSettings.isJaniFileSet()) {
-                storm::exportJaniModel(*model, {}, janiSettings.getJaniFilename());
+                storm::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil)}, janiSettings.getJaniFilename());
             }
             
             delete model;

src/storm-dft/transformations/DftToGspnTransformator.cpp

@@ -8,7 +8,7 @@ namespace storm {
             
             // Prevent some magic constants
             static constexpr const uint64_t defaultPriority = 0;
-            static constexpr const uint64_t defaultCapacity = 0;
+            static constexpr const uint64_t defaultCapacity = 1;
 
             template <typename ValueType>
             DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft) : mDft(dft) {
@@ -27,6 +27,12 @@ namespace storm {
 				//drawGSPNRestrictions();
             }
             
+            template<typename ValueType>
+            uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() {
+                assert(failedNodes.size() > mDft.getTopLevelIndex());
+                return failedNodes[mDft.getTopLevelIndex()];
+            }
+            
 			template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawGSPNElements() {
                 
@@ -133,6 +139,7 @@ namespace storm {
                 for(auto const& child : dftAnd->children()) {
                     assert(failedNodes.size() > child->id());
                     builder.addInputArc(failedNodes[child->id()], tAndFailed);
+                    builder.addOutputArc(tAndFailed, failedNodes[child->id()]);
                 }
                 
 			}
@@ -157,6 +164,7 @@ namespace storm {
                     }
                     assert(failedNodes.size() > child->id());
                     builder.addInputArc(failedNodes[child->id()], tNodeFailed);
+                    builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
                     ++i;
                 }
 			}
@@ -188,6 +196,7 @@ namespace storm {
                     builder.addOutputArc(tCollect, childInhibPlace);
                     builder.addInhibitionArc(childInhibPlace, tCollect);
                     builder.addInputArc(failedNodes[child->id()], tCollect);
+                    builder.addOutputArc(tCollect, failedNodes[child->id()]);
                     ++i;
                 }
 			}
@@ -212,12 +221,15 @@ namespace storm {
                 }
                 for(auto const& child : dftPand->children()) {
                     builder.addInputArc(failedNodes[child->id()], tNodeFailed);
+                    builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
                 }
                 for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) {
                     uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j));
                     builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs);
+                    builder.addOutputArc(tfs, failedNodes[dftPand->children().at(j)->id()]);
                     builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs);
                     builder.addOutputArc(tfs, nodeFS);
+                    builder.addInhibitionArc(nodeFS, tfs);
 
                 }
             }

src/storm-dft/transformations/DftToGspnTransformator.h

@@ -33,6 +33,9 @@ namespace storm {
                  */
                 gspn::GSPN* obtainGSPN();
                 
+                
+                uint64_t toplevelFailedPlaceId();
+                
             private:
                 /*
 				 * Draw all elements of the GSPN.

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

@@ -66,9 +66,7 @@ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const&
 }
 
 void handleJani(storm::gspn::GSPN const& gspn) {
-    std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
+
-    storm::builder::JaniGSPNBuilder builder(gspn, exprManager);
-    storm::jani::Model* model = builder.build();
     storm::jani::JsonExporter::toFile(*model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
     delete model;
 }

src/storm-gspn/builder/JaniGSPNBuilder.h

@@ -16,10 +16,6 @@ namespace storm {
                 
             }
             
-            void setIgnoreWeights(bool ignore = true)  {
-                //ignoreWeights = ignore;
-            }
-            
             
             storm::jani::Model* build() {
                 storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
@@ -32,6 +28,10 @@ namespace storm {
                 return model;
             }
             
+            storm::jani::Variable const& getPlaceVariable(uint64_t placeId) {
+                return *vars.at(placeId);
+            }
+            
             void addVariables(storm::jani::Model* model) {
                 for (auto const& place : gspn.getPlaces()) {
                     storm::jani::Variable* janiVar = nullptr;
@@ -86,7 +86,7 @@ namespace storm {
                             destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
                         }
                         for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
-                            destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second);
+                            destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
                         }
                         totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
                         
@@ -103,13 +103,13 @@ namespace storm {
                         storm::expressions::Expression destguard = expressionManager->boolean(true);
                         std::vector<storm::jani::Assignment> assignments;
                         for (auto const& inPlaceEntry : trans.getInputPlaces()) {
-                            destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
+                            destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
                             if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
                                 assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
                             }
                         }
                         for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
-                            destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
+                            destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
                         }
                         for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
                             if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
@@ -140,7 +140,7 @@ namespace storm {
                         }
                     }
                     for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
-                        guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second);
+                        guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
                     }
                     for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
                         if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {

src/storm/utility/storm.h

@@ -227,6 +227,7 @@ namespace storm {
     std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
         if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
             std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
+            ma->close();
             if (ma->hasOnlyTrivialNondeterminism()) {
                 // Markov automaton can be converted into CTMC.
                 model = ma->convertToCTMC();