transient variables in program graphs

Former-commit-id: 078d701589 [formerly 362dfa5f41]
Former-commit-id: 593e5f69b1

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()) {

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<std::vector<storm::jani::Edge>, 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<storm::ppg::ProgramVariableIdentifier> transients;
             /// Restrictions on variables
             std::map<uint64_t, storm::storage::IntegerInterval> variableRestrictions;
             /// Locations for variables that would have gone ot o

src/storage/ppg/ProgramGraph.cpp

@@ -4,6 +4,56 @@
 
 namespace storm {
     namespace ppg {
+        
+        std::vector<ProgramVariableIdentifier> ProgramGraph::transientVariables() const {
+            std::vector<ProgramVariableIdentifier> 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<ProgramVariableIdentifier> ProgramGraph::variablesNotInGuards() const {
+            std::vector<ProgramVariableIdentifier> result;
+            std::set<storm::expressions::Variable> 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;
             

src/storage/ppg/ProgramGraph.h

@@ -180,6 +180,8 @@ namespace storm {
                 return expManager;
             }
             
+            std::vector<ProgramVariableIdentifier> 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<ProgramVariableIdentifier> variablesNotInGuards() const;
+            
             ProgramLocation& getLocation(ProgramLocationIdentifier id) {
                 return locations.at(id);
             }