From c052da15b987bebe7b20c04346b18243864e2faf Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 14 Sep 2018 16:56:03 +0200 Subject: [PATCH] conversion from prism to jani respects formulaas --- src/storm/storage/jani/Model.cpp | 29 +++++++++++++++++++++ src/storm/storage/jani/Model.h | 6 +++++ src/storm/storage/prism/ToJaniConverter.cpp | 25 +++++++++++++++++- 3 files changed, 59 insertions(+), 1 deletion(-) diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 5b3464ed4..e2b03461b 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -963,6 +963,35 @@ namespace storm { return result; } + void Model::substitute(std::map 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 emptyPropertyVector; substituteFunctions(emptyPropertyVector); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 24faf8d76..445552cf1 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -386,6 +386,12 @@ namespace storm { */ std::map 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 const& substitution); + /*! * Substitutes all function calls with the corresponding function definition * @param properties also eliminates function call expressions in the given properties diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index f8ec3e053..f998e59ad 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/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(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 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> 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 substitution; + for (auto const& formula : program.getFormulas()) { + storm::expressions::Expression functionCallExpr = std::make_shared(*manager, formula.getType(), formula.getName(), std::vector>())->toExpression(); + substitution.emplace(formula.getExpressionVariable(), functionCallExpr); + } + janiModel.substitute(substitution); + } + janiModel.finalize(); return janiModel;