From eed1e30f3c30c399f40f1673a72b0acc8a6bbe28 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 22 Sep 2016 23:38:43 +0200 Subject: [PATCH] transient variables in program graphs Former-commit-id: 078d701589c9f0294a0cb00cb2ef0c9d8f9b8814 [formerly 362dfa5f419186bf30ce8a2e1251f25135600b4d] Former-commit-id: 593e5f69b1a3c3ec172d09563be0acfa2eeaaeaf --- src/builder/JaniProgramGraphBuilder.cpp | 2 +- src/builder/JaniProgramGraphBuilder.h | 20 +++++++--- src/storage/ppg/ProgramGraph.cpp | 50 +++++++++++++++++++++++++ src/storage/ppg/ProgramGraph.h | 7 ++++ 4 files changed, 73 insertions(+), 6 deletions(-) diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp index 8aa8db08a..9d2abb6bb 100644 --- a/src/builder/JaniProgramGraphBuilder.cpp +++ b/src/builder/JaniProgramGraphBuilder.cpp @@ -53,7 +53,7 @@ namespace storm { STORM_LOG_THROW(act.nrLevels() <= 1, storm::exceptions::NotSupportedException, "Multi-level assignments with user variable bounds not supported"); for(auto const& group : act) { for(auto const& assignment : group) { - if (isUserRestricted(assignment.first)) { + if (isUserRestrictedVariable(assignment.first)) { assert(variableRestrictions.count(assignment.first) == 1); storm::storage::IntegerInterval const& bound = variableRestrictions.at(assignment.first); if (!assignment.second.containsVariables()) { diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h index 5bbce1d15..f3f49f772 100644 --- a/src/builder/JaniProgramGraphBuilder.h +++ b/src/builder/JaniProgramGraphBuilder.h @@ -25,7 +25,7 @@ namespace storm { static unsigned janiVersion; JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) { - + transients = programGraph.transientVariables(); } //void addVariableRestriction(storm::expressions::Variable const& var, storm::IntegerInterval const& interval ) { @@ -71,13 +71,22 @@ namespace storm { std::pair, storm::expressions::Expression> addVariableChecks(storm::ppg::ProgramEdge const& edge); - bool isUserRestricted(storm::ppg::ProgramVariableIdentifier i) { + bool isUserRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) { + return variableRestrictions.count(i) == 1; + } + + bool isRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) { + // Might be different from user restricted in near future. return variableRestrictions.count(i) == 1; } + bool isTransientVariable(storm::ppg::ProgramVariableIdentifier i) { + return std::find(transients.begin(), transients.end(), i) != transients.end(); + } + void addProcedureVariables(storm::jani::Automaton& automaton) { for (auto const& v : programGraph.getVariables()) { - if(variableRestrictions.count(v.first) == 1) { + if(isRestrictedVariable(v.first) && !isTransientVariable(v.first)) { storm::storage::IntegerInterval const& bounds = variableRestrictions.at(v.first); if (bounds.hasLeftBound()) { if (bounds.hasRightBound()) { @@ -92,7 +101,7 @@ namespace storm { assert(false); } } else { - storm::jani::UnboundedIntegerVariable janiVar(v.second.getName(), v.second, expManager->integer(0), false); + storm::jani::UnboundedIntegerVariable janiVar(v.second.getName(), v.second, expManager->integer(0), isTransientVariable(v.first)); automaton.addVariable(janiVar); } } @@ -118,7 +127,8 @@ namespace storm { } } - + /// Transient variables + std::vector transients; /// Restrictions on variables std::map variableRestrictions; /// Locations for variables that would have gone ot o diff --git a/src/storage/ppg/ProgramGraph.cpp b/src/storage/ppg/ProgramGraph.cpp index b6e951aca..169c880f7 100644 --- a/src/storage/ppg/ProgramGraph.cpp +++ b/src/storage/ppg/ProgramGraph.cpp @@ -4,6 +4,56 @@ namespace storm { namespace ppg { + + std::vector ProgramGraph::transientVariables() const { + std::vector transientCandidates = variablesNotInGuards(); + bool removedCandidate = true; // tmp + while(removedCandidate && !transientCandidates.empty()) { + removedCandidate = false; + for (auto const& act : this->deterministicActions) { + for (auto const& group : act.second) { + for (auto const& assignment : group) { + if (std::find(transientCandidates.begin(), transientCandidates.end(), assignment.first) == transientCandidates.end()) { + for (auto const& vars : assignment.second.getVariables()) { + auto it = std::find(transientCandidates.begin(), transientCandidates.end(), vars.getIndex()); + if (it != transientCandidates.end()) { + transientCandidates.erase(it); + removedCandidate = true; + } + } + } + } + } + } + } + return transientCandidates; + } + + std::vector ProgramGraph::variablesNotInGuards() const { + std::vector result; + std::set contained; + for (auto const& loc : locations) { + for (auto const& edgegroup : loc.second) { + for (auto const& edge : *edgegroup) { + auto conditionVars = edge->getCondition().getVariables(); + std::cout << "Guard " << edge->getCondition() << " contains "; + for (auto const& cv : conditionVars) { + std::cout << cv.getName() << ", "; + } + std::cout << std::endl; + contained.insert(conditionVars.begin(), conditionVars.end()); + } + } + } + for (auto const& varEntry : variables) { + if (contained.count(varEntry.second) == 0) { + result.push_back(varEntry.first); + } + } + + return result; + } + void ProgramGraph::printDot(std::ostream& os) const { os << "digraph ppg {" << std::endl; diff --git a/src/storage/ppg/ProgramGraph.h b/src/storage/ppg/ProgramGraph.h index 1b83eac1f..e2028f28c 100644 --- a/src/storage/ppg/ProgramGraph.h +++ b/src/storage/ppg/ProgramGraph.h @@ -180,6 +180,8 @@ namespace storm { return expManager; } + std::vector transientVariables() const; + void checkValid() { } @@ -193,6 +195,11 @@ namespace storm { void printDot(std::ostream& os) const; protected: + /** + * Returns the set of variables which do not occur in guards. + */ + std::vector variablesNotInGuards() const; + ProgramLocation& getLocation(ProgramLocationIdentifier id) { return locations.at(id); }