From 1536edb99f612e20571388573efc899da63d7387 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 13 Nov 2019 17:53:44 +0100 Subject: [PATCH] Jani: Check if a variable is never used as the lvalue of an assignment. If yes, (and if the variable has a known initial value), we replace the variable by a constant. --- src/storm/storage/jani/Model.cpp | 32 +++++--- src/storm/storage/jani/Model.h | 16 +++- .../jani/VariablesToConstantsTransformer.cpp | 73 +++++++++++++++++++ .../jani/VariablesToConstantsTransformer.h | 24 ++++++ .../jani/traverser/AssignmentsFinder.cpp | 13 ++++ .../jani/traverser/AssignmentsFinder.h | 2 + 6 files changed, 148 insertions(+), 12 deletions(-) create mode 100644 src/storm/storage/jani/VariablesToConstantsTransformer.cpp create mode 100644 src/storm/storage/jani/VariablesToConstantsTransformer.h diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 0db4a183f..c05417ae2 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -18,6 +18,7 @@ #include "storm/storage/jani/JSONExporter.h" #include "storm/storage/jani/ArrayEliminator.h" #include "storm/storage/jani/FunctionEliminator.h" +#include "storm/storage/jani/VariablesToConstantsTransformer.h" #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" @@ -638,7 +639,6 @@ namespace storm { return constantToIndex.find(name) != constantToIndex.end(); } - void Model::removeConstant(std::string const& name) { auto pos = constantToIndex.find(name); if (pos != constantToIndex.end()) { @@ -1025,12 +1025,16 @@ namespace storm { return result; } - Model Model::substituteConstants() const { - Model result(*this); + Model& Model::replaceUnassignedVariablesWithConstants() { + VariablesToConstantsTransformer().transform(*this); + return *this; + } + + Model& Model::substituteConstantsInPlace() { // Gather all defining expressions of constants. std::map constantSubstitution; - for (auto& constant : result.getConstants()) { + for (auto& constant : this->getConstants()) { if (constant.hasConstraint()) { constant.setConstraintExpression(substituteJaniExpression(constant.getConstraintExpression(), constantSubstitution)); } @@ -1040,30 +1044,38 @@ namespace storm { } } - for (auto& functionDefinition : result.getGlobalFunctionDefinitions()) { + for (auto& functionDefinition : this->getGlobalFunctionDefinitions()) { functionDefinition.second.substitute(constantSubstitution); } // Substitute constants in all global variables. - result.getGlobalVariables().substitute(constantSubstitution); + this->getGlobalVariables().substitute(constantSubstitution); // Substitute constants in initial states expression. - result.setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution)); + this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution)); - for (auto& rewMod : result.getNonTrivialRewardExpressions()) { + for (auto& rewMod : this->getNonTrivialRewardExpressions()) { rewMod.second = substituteJaniExpression(rewMod.second, constantSubstitution); } // Substitute constants in variables of automata and their edges. - for (auto& automaton : result.getAutomata()) { + for (auto& automaton : this->getAutomata()) { automaton.substitute(constantSubstitution); } + return *this; + } + + Model Model::substituteConstants() const { + Model result(*this); + result.substituteConstantsInPlace(); return result; } Model Model::substituteConstantsFunctions() const { - auto result = substituteConstants(); + Model result(*this); + result.replaceUnassignedVariablesWithConstants(); + result.substituteConstantsInPlace(); result.substituteFunctions(); return result; } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index e70762ebe..3adbdd51c 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -427,6 +427,16 @@ namespace storm { */ std::vector> getUndefinedConstants() const; + /*! + * Replaces each variable to which we never assign a value with a constant. + */ + Model& replaceUnassignedVariablesWithConstants(); + + /*! + * Substitutes all constants in all expressions of the model. + */ + Model& substituteConstantsInPlace(); + /*! * Substitutes all constants in all expressions of the model. The original model is not modified, but * instead a new model is created. @@ -453,8 +463,10 @@ namespace storm { void substituteFunctions(std::vector& properties); /*! - * Substitutes all constants in all expressions of the model. The original model is not modified, but - * instead a new model is created. Afterwards, all function calls are substituted with the defining expression. + * 1. Tries to replace variables by constants (if possible). + * 2. Substitutes all constants in all expressions of the model. + * 3. Afterwards, all function calls are substituted with the defining expression. + * The original model is not modified, but instead a new model is created. */ Model substituteConstantsFunctions() const; diff --git a/src/storm/storage/jani/VariablesToConstantsTransformer.cpp b/src/storm/storage/jani/VariablesToConstantsTransformer.cpp new file mode 100644 index 000000000..98384dac6 --- /dev/null +++ b/src/storm/storage/jani/VariablesToConstantsTransformer.cpp @@ -0,0 +1,73 @@ +#include "storm/storage/jani/VariablesToConstantsTransformer.h" + +#include "storm/storage/jani/Constant.h" +#include "storm/storage/jani/Variable.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/traverser/AssignmentsFinder.h" + +#include "storm/storage/expressions/Expressions.h" +#include "storm/storage/jani/expressions/JaniExpressions.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + + + + namespace jani { + namespace detail { + storm::jani::Constant createConstantFromVariable(storm::jani::Variable const& variable) { + STORM_LOG_ASSERT(variable.hasInitExpression(), "Trying to convert variable " << variable.getName() << " to a constant, but the variable does not have an initial value."); + // For the name we use the name of the expression variable to assert uniqueness. + return storm::jani::Constant(variable.getExpressionVariable().getName(), variable.getExpressionVariable(), variable.getInitExpression()); + } + + template + bool canTransformVariable(storm::jani::Variable const& variable, JaniStructureType const& janiStructure) { + // It does not make sense to do this for transient variables. + if (variable.isTransient()) { + return false; + } + // The variable should have a known initial value. + if (!variable.hasInitExpression()) { + return false; + } + // Finally, there should be no assignment that assignes a value to this variable. + auto assignmentTypes = storm::jani::AssignmentsFinder().find(janiStructure, variable); + return !assignmentTypes.hasEdgeAssignment && !assignmentTypes.hasEdgeDestinationAssignment && !assignmentTypes.hasLocationAssignment; + } + } // namespace detail + + void VariablesToConstantsTransformer::transform(Model& model) { + // It is dangerous to erase a variable from a set of variables while iterating over the set. + // Therefore, we store the variables and erase them later. + std::vector variablesToErase; + for (auto const& globalVar : model.getGlobalVariables()) { + if (detail::canTransformVariable(globalVar, model)) { + variablesToErase.push_back(globalVar.getExpressionVariable()); + } + } + for (auto const& varToErase : variablesToErase) { + STORM_LOG_INFO("Transformed Variable " << varToErase.getName() << " to a constant since it is not assigned any value."); + auto erasedJaniVariable = model.getGlobalVariables().eraseVariable(varToErase); + auto createdConstant = detail::createConstantFromVariable(*erasedJaniVariable); + model.addConstant(createdConstant); + } + for (auto& aut : model.getAutomata()) { + variablesToErase.clear(); + for (auto const& localVar : aut.getVariables()) { + if (detail::canTransformVariable(localVar, aut)) { + variablesToErase.push_back(localVar.getExpressionVariable()); + } + } + for (auto const& varToErase : variablesToErase) { + STORM_LOG_INFO("Transformed Variable " << varToErase.getName() << " to a constant since it is not assigned any value."); + auto erasedJaniVariable = aut.getVariables().eraseVariable(varToErase); + auto createdConstant = detail::createConstantFromVariable(*erasedJaniVariable); + model.addConstant(createdConstant); + } + } + } + } +} + diff --git a/src/storm/storage/jani/VariablesToConstantsTransformer.h b/src/storm/storage/jani/VariablesToConstantsTransformer.h new file mode 100644 index 000000000..9a979cb4b --- /dev/null +++ b/src/storm/storage/jani/VariablesToConstantsTransformer.h @@ -0,0 +1,24 @@ +#pragma once + + +namespace storm { + namespace expressions { + class Expression; + } + + namespace jani { + class Model; + + class VariablesToConstantsTransformer { + public: + VariablesToConstantsTransformer() = default; + + /*! + * Replaces each variable to which we never assign a value with a constant. + */ + void transform(Model& model); + + }; + } +} + diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp index c232cddd8..1ae75e45f 100644 --- a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp +++ b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp @@ -8,6 +8,10 @@ namespace storm { AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, storm::jani::Variable const& variable) { return find(model, variable.getExpressionVariable()); } + + AssignmentsFinder::ResultType AssignmentsFinder::find(Automaton const& automaton, storm::jani::Variable const& variable) { + return find(automaton, variable.getExpressionVariable()); + } AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, storm::expressions::Variable const& variable) { ResultType res; @@ -18,6 +22,15 @@ namespace storm { return res; } + AssignmentsFinder::ResultType AssignmentsFinder::find(Automaton const& automaton, storm::expressions::Variable const& variable) { + ResultType res; + res.hasLocationAssignment = false; + res.hasEdgeAssignment = false; + res.hasEdgeDestinationAssignment = false; + ConstJaniTraverser::traverse(automaton, std::make_pair(&variable, &res)); + return res; + } + void AssignmentsFinder::traverse(Location const& location, boost::any const& data) { auto resVar = boost::any_cast>(data); if (!resVar.second->hasLocationAssignment) { diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.h b/src/storm/storage/jani/traverser/AssignmentsFinder.h index 5a2f1598f..1c96e3157 100644 --- a/src/storm/storage/jani/traverser/AssignmentsFinder.h +++ b/src/storm/storage/jani/traverser/AssignmentsFinder.h @@ -22,7 +22,9 @@ namespace storm { AssignmentsFinder() = default; ResultType find(Model const& model, storm::jani::Variable const& variable); + ResultType find(Automaton const& automaton, storm::jani::Variable const& variable); ResultType find(Model const& model, storm::expressions::Variable const& variable); + ResultType find(Automaton const& automaton, storm::expressions::Variable const& variable); virtual ~AssignmentsFinder() = default;