several extensions to program graphs

Former-commit-id: 52162888a4 [formerly 5b4787851c]
Former-commit-id: c5b4a7d868

src/storage/ppg/ProgramAction.cpp

@@ -0,0 +1,15 @@
+#include "ProgramAction.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+    namespace ppg {
+        
+        ProbabilisticProgramAction::ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, int64_t from, int64_t to) : ProgramAction(graph, actId) {
+            assert(from <= to);
+            storm::expressions::Expression prob = graph->getExpressionManager()->integer(1) / graph->getExpressionManager()->integer(to - from + 1);
+            for(int64_t i = from; i <= to; ++i) {
+                values.emplace_back(i, prob);
+            }
+        }
+    }
+}

src/storage/ppg/ProgramAction.h

@@ -0,0 +1,158 @@
+#pragma once
+#include "defines.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+    namespace ppg {
+        
+        class ProgramAction {
+        public:
+            ProgramAction(ProgramGraph* graph, ProgramActionIdentifier id) : graph(graph), actId(id) {
+                
+            }
+            
+            ProgramActionIdentifier id() const {
+                return actId;
+            }
+            
+            ProgramGraph const& getProgramGraph() const {
+                return *graph;
+            }
+            
+            virtual bool isProbabilistic() const = 0;
+        private:
+            ProgramGraph* graph;
+            ProgramActionIdentifier actId;
+        };
+        
+        
+        struct ValueProbabilityPair {
+            ValueProbabilityPair(int64_t value, storm::expressions::Expression const& probability) : value(value), probability(probability) {
+                // Intentionally left empty.
+            }
+            
+            int64_t value;
+            storm::expressions::Expression probability;
+        };
+        
+        class ProbabilisticProgramAction : public ProgramAction {
+        public:
+            // TODO in the long run, we probably need own iterators for this.
+            using iterator = std::vector<ValueProbabilityPair>::iterator;
+            using const_iterator = std::vector<ValueProbabilityPair>::const_iterator;
+            
+            
+            
+            /**
+             * Constructs a uniform assignment operation to a variable;
+             * Action assigns a variable according to a uniform distribution [from, to]
+             */
+            ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, int64_t from, int64_t to);
+            
+            bool isProbabilistic() const override{
+                return true;
+            }
+            
+            iterator begin() {
+                return values.begin();
+            }
+            
+            iterator end() {
+                return values.end();
+            }
+            
+            const_iterator begin() const {
+                return values.begin();
+            }
+            
+            const_iterator end() const {
+                return values.end();
+            }
+            
+        private:
+            // TODO not the smartest representation (but at least it is internal!)
+            std::vector<ValueProbabilityPair> values;
+            
+        };
+        
+        
+        struct AssignmentGroup {
+            using iterator = std::unordered_map<uint64_t, storm::expressions::Expression>::iterator;
+            using const_iterator = std::unordered_map<uint64_t, storm::expressions::Expression>::const_iterator;
+            
+            storm::expressions::Expression& operator[](uint64_t varIndex) {
+                return map[varIndex];
+            }
+            
+            bool hasVariable(uint64_t varIndex) const {
+                return map.count(varIndex) > 0;
+            }
+            
+            iterator begin() {
+                return map.begin();
+            }
+            
+            iterator end() {
+                return map.end();
+            }
+            
+            const_iterator begin() const {
+                return map.begin();
+            }
+            
+            const_iterator end() const {
+                return map.end();
+            }
+            
+        private:
+            std::unordered_map<uint64_t, storm::expressions::Expression> map;
+        };
+        
+        class DeterministicProgramAction : public ProgramAction {
+            
+        public:
+            using iterator = std::vector<AssignmentGroup>::iterator;
+            using const_iterator = std::vector<AssignmentGroup>::const_iterator;
+            
+            DeterministicProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId) : ProgramAction(graph, actId) {
+                
+            }
+            
+            
+            
+            void addAssignment(uint64_t varIndex, storm::expressions::Expression const& expr, uint64_t level=0) {
+                if(assignments.size() <= level) {
+                    assignments.resize(level+1);
+                }
+                assert(!assignments[level].hasVariable(varIndex));
+                assignments[level][varIndex] = expr;
+            }
+            
+            iterator begin() {
+                return assignments.begin();
+            }
+            
+            iterator end() {
+                return assignments.end();
+            }
+            
+            const_iterator begin() const {
+                return assignments.begin();
+            }
+            
+            const_iterator end() const {
+                return assignments.end();
+            }
+            
+            bool isProbabilistic() const override{
+                return false;
+            }
+            
+        protected:
+            std::vector<AssignmentGroup> assignments;
+        };
+        
+    }
+}

src/storage/ppg/ProgramEdge.cpp

@@ -1,9 +1,11 @@
-//
-//  ProgramEdge.cpp
-//  storm
-//
-//  Created by Sebastian Junges on 09/09/16.
-//
-//
-
 #include "ProgramEdge.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+    namespace ppg {
+        
+        ProgramAction const& ProgramEdge::getAction() const {
+            return group->getGraph().getAction(action);
+        }
+    }
+}

src/storage/ppg/ProgramEdge.h

@@ -5,6 +5,8 @@
 
 namespace storm {
     namespace ppg {
+        class ProgramAction;
+        
         class ProgramEdge {
         public:
             ProgramEdge(ProgramEdgeGroup* group, ProgramEdgeIdentifier id, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId)
@@ -13,6 +15,17 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            
+            ProgramLocationIdentifier getTargetId() const {
+                return target;
+            }
+            
+            storm::expressions::Expression const& getCondition() const {
+                return condition;
+            }
+            
+            ProgramAction const& getAction() const;
+            
             virtual ~ProgramEdge() {
                 // Intentionally left empty.
             }

src/storage/ppg/ProgramEdgeGroup.h

@@ -8,6 +8,8 @@ namespace storm {
         
         class ProgramEdgeGroup {
         public:
+            using const_iterator = std::vector<ProgramEdge*>::const_iterator;
+            
             ProgramEdgeGroup(ProgramGraph* graph, ProgramEdgeGroupIdentifier id, ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability)
             : graph(graph), groupId(id), sourceId(sourceId), probability(probability)
             {
@@ -31,6 +33,26 @@ namespace storm {
                 return edges.back();
             }
             
+            const_iterator begin() const {
+                return edges.begin();
+            }
+            
+            const_iterator end() const {
+                return edges.end();
+            }
+            
+            size_t nrEdges() const {
+                return edges.size();
+            }
+            
+            storm::expressions::Expression const& getProbability() const {
+                return probability;
+            }
+            
+            ProgramGraph const& getGraph() const {
+                return *graph;
+            }
+            
         private:
             /// Pointer to the graph; not owned.
             ProgramGraph* graph;

src/storage/ppg/ProgramGraph.h

@@ -8,19 +8,10 @@
 #include "ProgramLocation.h"
 #include "ProgramEdge.h"
 #include "ProgramEdgeGroup.h"
+#include "ProgramAction.h"
 
 namespace storm {
     namespace ppg {
-        struct ProgramAction {
-            ProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId) : graph(graph), actId(actId) {
-                
-            }
-            
-            ProgramGraph* graph;
-            ProgramActionIdentifier actId;
-        };
-        
-         
         /**
          *  Program graph as based on Principles of Model Checking, Def 2.13
          *  Action effects are part of the action.
@@ -34,15 +25,15 @@ namespace storm {
                 
             }
             
+            ProgramGraph(ProgramGraph const&) = delete;
+            
             virtual ~ProgramGraph() {
-                std::cout << "remove graph" << std::endl;
             }
             
-            ProgramActionIdentifier addAction() {
+            DeterministicProgramAction* addDeterministicAction() {
                 ProgramActionIdentifier newId = freeActionIndex();
                 assert(!hasAction(newId));
-                actions.emplace(newId, ProgramAction(this, newId));
-                return newId;
+                return &(deterministicActions.emplace(newId, DeterministicProgramAction(this, newId)).first->second);
             }
             
             ProgramLocation* addLocation(bool isInitial = false) {
@@ -101,12 +92,51 @@ namespace storm {
             }
 
             
+            ProgramVariableIdentifier getVariableId(std::string const& varName) const {
+                // TODO consider holding a map for this.
+                uint64_t res = 0;
+                for(auto const& v : variables) {
+                    if(v.getName() == varName) {
+                        return res;
+                    }
+                    ++res;
+                }
+                assert(false);
+            }
+            
+            std::string const& getVariableName(ProgramVariableIdentifier id) const {
+                return variables.at(id).getName();
+            }
+            
+            bool hasVariable(std::string const& varName) const {
+                for(auto const& v : variables) {
+                    if(v.getName() == varName) {
+                        return true;
+                    }
+                }
+                return false;
+            }
+            
             bool hasLocation(ProgramLocationIdentifier id) const {
                 return locations.count(id) == 1;
             }
             
             bool hasAction(ProgramActionIdentifier id) const {
-                return actions.count(id) == 1;
+                return deterministicActions.count(id) == 1 || probabilisticActions.count(id);
+            }
+            
+            ProgramAction const& getAction(ProgramActionIdentifier id) const {
+                assert(hasAction(id));
+                if(isDeterministicAction(id)) {
+                    return deterministicActions.at(id);
+                } else {
+                    return probabilisticActions.at(id);
+                }
+            }
+            
+            bool isDeterministicAction(ProgramActionIdentifier id) const {
+                assert(hasAction(id));
+                return probabilisticActions.count(id) == 0;
             }
             
             size_t nrLocations() const {
@@ -117,6 +147,10 @@ namespace storm {
                 return variables.size();
             }
             
+            size_t nrActions() const {
+                return variables.size();
+            }
+            
             
             ConstLocationIterator locationBegin() const {
                 return locations.begin();
@@ -141,6 +175,7 @@ namespace storm {
             void printInfo(std::ostream& os) const {
                 os << "Number of variables: " << nrVariables() << std::endl;
                 os << "Number of locations: " << nrLocations() << std::endl;
+                os << "Number of actions: " << nrActions() << std::endl;
             }
             
         protected:
@@ -168,7 +203,8 @@ namespace storm {
                 return newEdgeGroupId++;
             }
             
-            std::unordered_map<ProgramActionIdentifier, ProgramAction> actions;
+            std::unordered_map<ProgramActionIdentifier, DeterministicProgramAction> deterministicActions;
+            std::unordered_map<ProgramActionIdentifier, ProbabilisticProgramAction> probabilisticActions;
             std::unordered_map<ProgramLocationIdentifier, ProgramLocation> locations;
             storm::expressions::Expression initialValueRestriction;
             std::vector<storm::expressions::Variable> variables;

src/storage/ppg/ProgramLocation.h

@@ -8,6 +8,7 @@ namespace storm {
         class ProgramLocation {
         public:
             using EdgeGroupIterator = std::vector<ProgramEdgeGroup*>::iterator;
+            using const_iterator = std::vector<ProgramEdgeGroup*>::const_iterator;
             
             ProgramLocation(ProgramGraph* graph, ProgramLocationIdentifier id, bool initial) : graph(graph), locId(id), init(initial){
                 // Intentionally left empty
@@ -38,10 +39,27 @@ namespace storm {
                 return edgeGroups.size();
             }
             
+            bool hasNonDeterminism() const {
+                for(auto const& eg : edgeGroups) {
+                    if(eg->nrEdges() > 1) return true;
+                }
+                return false;
+            }
+            
+            const_iterator begin() const {
+                return edgeGroups.begin();
+            }
+            
+            const_iterator end() const {
+                return edgeGroups.end();
+            }
+            
+            // Todo rename?
             EdgeGroupIterator getOutgoingEdgeGroupBegin() {
                 return edgeGroups.begin();
             }
             
+            // Todo rename?
             EdgeGroupIterator getOutgoingEdgeGroupEnd() {
                 return edgeGroups.end();
             }

src/storage/ppg/defines.h

@@ -10,6 +10,7 @@ namespace storm {
         using ProgramActionIdentifier = uint64_t;
         using ProgramEdgeGroupIdentifier =  uint64_t;
         using ProgramEdgeIdentifier = uint64_t;
+        using ProgramVariableIdentifier = uint64_t;
         
     }
 }