conversion from prism to jani respects formulaas

src/storm/storage/jani/Model.cpp

@@ -963,6 +963,35 @@ namespace storm {
             return result;
         }
         
+        void Model::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
+            // substitute in all defining expressions of constants
+            for (auto& constant : this->getConstants()) {
+                if (constant.isDefined()) {
+                    constant.define(substituteJaniExpression(constant.getExpression(), substitution));
+                }
+            }
+            
+            for (auto& functionDefinition : this->getGlobalFunctionDefinitions()) {
+                functionDefinition.second.substitute(substitution);
+            }
+            
+            // Substitute in all global variables.
+            for (auto& variable : this->getGlobalVariables().getBoundedIntegerVariables()) {
+                variable.substitute(substitution);
+            }
+            for (auto& variable : this->getGlobalVariables().getArrayVariables()) {
+                variable.substitute(substitution);
+            }
+            
+            // Substitute in initial states expression.
+            this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution));
+            
+            // Substitute in variables of automata and their edges.
+            for (auto& automaton : this->getAutomata()) {
+                automaton.substitute(substitution);
+            }
+        }
+        
         void Model::substituteFunctions() {
             std::vector<Property> emptyPropertyVector;
             substituteFunctions(emptyPropertyVector);

src/storm/storage/jani/Model.h

@@ -386,6 +386,12 @@ namespace storm {
              */
             std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
             
+            /*!
+             * Substitutes all expression variables in all expressions of the model. The original model is not modified, but
+             * instead a new model is created.
+             */
+            void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
             /*!
              * Substitutes all function calls with the corresponding function definition
              * @param properties also eliminates function call expressions in the given properties

src/storm/storage/prism/ToJaniConverter.cpp

@@ -6,6 +6,7 @@
 #include "storm/storage/prism/CompositionToJaniVisitor.h"
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/TemplateEdge.h"
+#include "storm/storage/jani/expressions/FunctionCallExpression.h"
 
 #include "storm/settings/SettingsManager.h"
 
@@ -37,11 +38,22 @@ namespace storm {
             }
             storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager);
             
+            janiModel.getModelFeatures().add(storm::jani::ModelFeature::DerivedOperators);
+            
             // Add all constants of the PRISM program to the JANI model.
             for (auto const& constant : program.getConstants()) {
                 janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional<storm::expressions::Expression>(constant.getExpression()) : boost::none));
             }
             
+            // Add all formulas of the PRISM program to the JANI model.
+            // Also collect a set of variables that occurr in a formula expressions as these need to be made global.
+            std::set<storm::expressions::Variable> formulaExpressionVariables;
+            for (auto const& formula : program.getFormulas()) {
+                storm::jani::FunctionDefinition funDef(formula.getName(), formula.getType(), {}, formula.getExpression());
+                janiModel.addFunctionDefinition(funDef);
+                formula.getExpression().getBaseExpression().gatherVariables(formulaExpressionVariables);
+            }
+            
             // Maintain a mapping from expression variables to JANI variables so we can fill in the correct objects when
             // creating assignments.
             std::map<storm::expressions::Variable, std::reference_wrapper<storm::jani::Variable const>> variableToVariableMap;
@@ -104,7 +116,7 @@ namespace storm {
             for (auto const& varMods : variablesToAccessingModuleIndices) {
                 assert(!varMods.second.empty());
                 // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
-                variablesToMakeGlobal[varMods.first] = allVariablesGlobal || (varMods.second.size() > 1);
+                variablesToMakeGlobal[varMods.first] = allVariablesGlobal || (varMods.second.size() > 1) || formulaExpressionVariables.count(varMods.first) > 0;
             }
             
             // Go through the labels and construct assignments to transient variables that are added to the locations.
@@ -343,6 +355,17 @@ namespace storm {
                 janiModel.setSystemComposition(janiModel.getStandardSystemComposition());
             }
             
+            // if there are formulas, replace the placeholder variables by actual function calls in all expressions
+            if (program.getNumberOfFormulas() > 0) {
+                janiModel.getModelFeatures().add(storm::jani::ModelFeature::Functions);
+                std::map<storm::expressions::Variable, storm::expressions::Expression> substitution;
+                for (auto const& formula : program.getFormulas()) {
+                    storm::expressions::Expression functionCallExpr = std::make_shared<storm::expressions::FunctionCallExpression>(*manager, formula.getType(), formula.getName(), std::vector<std::shared_ptr<storm::expressions::BaseExpression const>>())->toExpression();
+                    substitution.emplace(formula.getExpressionVariable(), functionCallExpr);
+                }
+                janiModel.substitute(substitution);
+            }
+            
             janiModel.finalize();
             
             return janiModel;