General method for adding transient variables in GSPN->Jani conversion

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

@@ -74,6 +74,7 @@ namespace storm {
             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();
+            storm::jani::Variable const& failedVar = builder.addTransientVariable(model.get(), "failed", targetExpression);
             STORM_LOG_TRACE("Target expression: " << targetExpression);
 
             auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);

src/storm-gspn/builder/JaniGSPNBuilder.cpp

@@ -252,15 +252,18 @@ namespace storm {
                     transientValue = transientValue && transitionDisabled;
                 }
             }
-            
+
+            return addTransientVariable(model, name, transientValue);
+        }
+
+        storm::jani::Variable const& JaniGSPNBuilder::addTransientVariable(storm::jani::Model* model, std::string name, storm::expressions::Expression expression) {
             auto exprVar = expressionManager->declareBooleanVariable(name);
             auto const& janiVar = model->addVariable(*storm::jani::makeBooleanVariable(name, exprVar, expressionManager->boolean(false), true));
-            storm::jani::Assignment assignment(janiVar, transientValue);
+            storm::jani::Assignment assignment(janiVar, expression);
             model->getAutomata().front().getLocations().front().addTransientAssignment(assignment);
             return janiVar;
         }
-        
-        
+
         std::string getUniqueVarName(storm::expressions::ExpressionManager const& manager, std::string name) {
             std::string res = name;
             while (manager.hasVariable(res)) {
@@ -300,4 +303,4 @@ namespace storm {
 
         
     }
-}
+}

src/storm-gspn/builder/JaniGSPNBuilder.h

@@ -11,23 +11,26 @@ namespace storm {
         public:
             JaniGSPNBuilder(storm::gspn::GSPN const& gspn)
                     : gspn(gspn), expressionManager(gspn.getExpressionManager()) {
-                
+
             }
-            
+
             virtual ~JaniGSPNBuilder() {
                 // Intentionally left empty.
             }
-            
-            
+
             storm::jani::Model* build(std::string const& automatonName = "gspn_automaton", bool buildStandardProperties = false);
-            
+
             storm::jani::Variable const& getPlaceVariable(uint64_t placeId) const {
                 return *vars.at(placeId);
             }
-            
+
             std::vector<storm::jani::Property> const& getStandardProperties() const;
 
-            
+            /*!
+             * Add transient variable representing given expression.
+             */
+            storm::jani::Variable const& addTransientVariable(storm::jani::Model* model, std::string name, storm::expressions::Expression expression);
+
         private:
             void addVariables(storm::jani::Model* model);
 
@@ -36,15 +39,16 @@ namespace storm {
             void addEdges(storm::jani::Automaton& automaton, uint64_t locId);
 
             storm::jani::Variable const& addDeadlockTransientVariable(storm::jani::Model* model, std::string name, bool ignoreCapacities = false, bool ignoreInhibitorArcs = false, bool ignoreEmptyPlaces = false);
+
             void buildProperties(storm::jani::Model* model);
-            
+
             const uint64_t janiVersion = 1;
             storm::gspn::GSPN const& gspn;
             std::map<uint64_t, storm::jani::Variable const*> vars;
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
-            
+
             std::vector<storm::jani::Property> standardProperties;
-            
+
         };
     }
 }