program graph

Former-commit-id: 34b6394d24 [formerly 99be317a04]
Former-commit-id: 0c78bdf77e

src/storage/ppg/ProgramEdge.cpp

@@ -0,0 +1,9 @@
+//
+//  ProgramEdge.cpp
+//  storm
+//
+//  Created by Sebastian Junges on 09/09/16.
+//
+//
+
+#include "ProgramEdge.h"

src/storage/ppg/ProgramEdge.h

@@ -0,0 +1,34 @@
+#pragma once
+#include "defines.h"
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace ppg {
+        class ProgramEdge {
+        public:
+            ProgramEdge(ProgramEdgeGroup* group, ProgramEdgeIdentifier id, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId)
+            : group(group), edgeId(id), target(targetId), action(action), condition(condition)
+            {
+                // Intentionally left empty.
+            }
+            
+            virtual ~ProgramEdge() {
+                // Intentionally left empty.
+            }
+            
+        private:
+            /// Pointer to the group; not owned
+            ProgramEdgeGroup* group;
+            /// Edge identifier
+            ProgramEdgeIdentifier edgeId;
+            /// Target location identifier
+            ProgramLocationIdentifier target;
+            /// Action identifier
+            ProgramActionIdentifier action;
+            /// Condition
+            storm::expressions::Expression condition;
+            
+        };
+    }
+}

src/storage/ppg/ProgramEdgeGroup.cpp

@@ -0,0 +1,14 @@
+#include "ProgramEdgeGroup.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+    namespace ppg {
+        ProgramEdge* ProgramEdgeGroup::addEdge(ProgramActionIdentifier action, ProgramLocationIdentifier target) {
+            return graph->addProgramEdge(*this, action, target);
+        }
+        ProgramEdge* ProgramEdgeGroup::addEdge(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier target) {
+            return graph->addProgramEdge(*this, action, condition, target);
+        }
+
+    }
+}

src/storage/ppg/ProgramEdgeGroup.h

@@ -0,0 +1,48 @@
+#pragma once
+
+#include "defines.h"
+#include "ProgramEdge.h"
+
+namespace storm {
+    namespace ppg {
+        
+        class ProgramEdgeGroup {
+        public:
+            ProgramEdgeGroup(ProgramGraph* graph, ProgramEdgeGroupIdentifier id, ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability)
+            : graph(graph), groupId(id), sourceId(sourceId), probability(probability)
+            {
+                // Intentionally left empty.
+            }
+            
+            virtual ~ProgramEdgeGroup() {
+                for( auto const& e : edges) {
+                    delete e;
+                }
+            }
+            
+            ProgramEdge* addEdge(ProgramActionIdentifier action, ProgramLocationIdentifier target);
+            ProgramEdge* addEdge(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier target);
+            
+            /**
+             * Constructs an outgoing edge in this edge group.
+             */
+            ProgramEdge* emplaceEdge(ProgramEdgeIdentifier id, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier target) {
+                edges.emplace_back(new ProgramEdge(this, id, action, condition, target));
+                return edges.back();
+            }
+            
+        private:
+            /// Pointer to the graph; not owned.
+            ProgramGraph* graph;
+            /// Own id (persistent over copy)
+            ProgramEdgeGroupIdentifier groupId;
+            /// Id of source location
+            ProgramLocationIdentifier sourceId;
+            /// Probability for this group
+            storm::expressions::Expression probability;
+            /// Outgoing edges
+            std::vector<ProgramEdge*> edges;
+            
+        };
+    }
+}

src/storage/ppg/ProgramGraph.cpp

@@ -0,0 +1,2 @@
+
+#include "ProgramGraph.h"

src/storage/ppg/ProgramGraph.h

@@ -0,0 +1,186 @@
+#pragma once
+
+#include "defines.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+#include "ProgramLocation.h"
+#include "ProgramEdge.h"
+#include "ProgramEdgeGroup.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.
+         */
+        class ProgramGraph {
+        public:
+            using EdgeGroupIterator = ProgramLocation::EdgeGroupIterator;
+            using ConstLocationIterator = std::unordered_map<ProgramLocationIdentifier, ProgramLocation>::const_iterator;
+            
+            ProgramGraph(std::shared_ptr<storm::expressions::ExpressionManager> const& expManager, std::vector<storm::expressions::Variable> const& variables) : expManager(expManager), variables(variables) {
+                
+            }
+            
+            virtual ~ProgramGraph() {
+                std::cout << "remove graph" << std::endl;
+            }
+            
+            ProgramActionIdentifier addAction() {
+                ProgramActionIdentifier newId = freeActionIndex();
+                assert(!hasAction(newId));
+                actions.emplace(newId, ProgramAction(this, newId));
+                return newId;
+            }
+            
+            ProgramLocation* addLocation(bool isInitial = false) {
+                ProgramLocationIdentifier newId = freeLocationIndex();
+                assert(!hasLocation(newId));
+                return &(locations.emplace(newId, ProgramLocation(this, newId, isInitial)).first->second);
+            }
+            
+            
+            ProgramEdgeGroup* addProgramEdgeGroup(ProgramLocation& source, storm::expressions::Expression const& probability) {
+                ProgramEdgeGroupIdentifier newId = freeEdgeGroupIndex();
+                return source.emplaceEdgeGroup(newId, probability);
+            }
+            
+            ProgramEdgeGroup* addProgramEdgeGroup(ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability) {
+                assert(hasLocation(sourceId));
+                return addProgramEdgeGroup(getLocation(sourceId), probability);
+            }
+        
+            ProgramEdge* addProgramEdge(ProgramEdgeGroup& group, ProgramActionIdentifier action, ProgramLocationIdentifier targetId) {
+                return addProgramEdge(group, action, expManager->boolean(true), targetId);
+            }
+            
+            ProgramEdge* addProgramEdge(ProgramEdgeGroup& group, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
+                ProgramEdgeIdentifier newId = freeEdgeIndex();
+                return group.emplaceEdge(newId, action, condition, targetId);
+            }
+            
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramLocation& source, ProgramActionIdentifier action, ProgramLocationIdentifier targetId) {
+                return addProgramEdgeToAllGroups(source, action, expManager->boolean(true), targetId);
+            }
+            
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramLocation& source, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
+                assert(hasLocation(targetId));
+                assert(hasAction(action));
+                
+                if(source.nrOutgoingEdgeGroups() == 0) {
+                    addProgramEdgeGroup(source, expManager->rational(1));
+                }
+                
+                std::vector<ProgramEdge*> res;
+                for(EdgeGroupIterator eg = source.getOutgoingEdgeGroupBegin(); eg != source.getOutgoingEdgeGroupEnd(); ++eg) {
+                    ProgramEdgeIdentifier newId = freeEdgeIndex();
+                    res.push_back((*eg)->emplaceEdge(newId, action, condition, targetId));
+                    
+                }
+                
+                return res;
+                
+            }
+            
+            
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramLocationIdentifier sourceId, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
+                assert(hasLocation(sourceId));
+                return addProgramEdgeToAllGroups(getLocation(sourceId), action, condition, targetId);
+            }
+
+            
+            bool hasLocation(ProgramLocationIdentifier id) const {
+                return locations.count(id) == 1;
+            }
+            
+            bool hasAction(ProgramActionIdentifier id) const {
+                return actions.count(id) == 1;
+            }
+            
+            size_t nrLocations() const {
+                return locations.size();
+            }
+            
+            size_t nrVariables() const {
+                return variables.size();
+            }
+            
+            
+            ConstLocationIterator locationBegin() const {
+                return locations.begin();
+            }
+            
+            ConstLocationIterator locationEnd() const {
+                return locations.end();
+            }
+            
+            std::vector<storm::expressions::Variable> const& getVariables() const {
+                return variables;
+            }
+            
+            std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const {
+                return expManager;
+            }
+            
+            void checkValid() {
+                
+            }
+            
+            void printInfo(std::ostream& os) const {
+                os << "Number of variables: " << nrVariables() << std::endl;
+                os << "Number of locations: " << nrLocations() << std::endl;
+            }
+            
+        protected:
+            
+            ProgramLocation& getLocation(ProgramLocationIdentifier id) {
+                return locations.at(id);
+            }
+            
+            /**
+             * Gets a free location index (based on whatever scheme we are using).
+             */
+            ProgramLocationIdentifier freeLocationIndex() {
+                return newLocationId++;
+            }
+            
+            ProgramActionIdentifier freeActionIndex() {
+                return newActionId++;
+            }
+            
+            ProgramEdgeIdentifier freeEdgeIndex() {
+                return newEdgeId++;
+            }
+            
+            ProgramEdgeGroupIdentifier freeEdgeGroupIndex() {
+                return newEdgeGroupId++;
+            }
+            
+            std::unordered_map<ProgramActionIdentifier, ProgramAction> actions;
+            std::unordered_map<ProgramLocationIdentifier, ProgramLocation> locations;
+            storm::expressions::Expression initialValueRestriction;
+            std::vector<storm::expressions::Variable> variables;
+            
+            std::shared_ptr<storm::expressions::ExpressionManager> expManager;
+        private:
+            // Helper for IDs, may be changed later.
+            ProgramEdgeGroupIdentifier newEdgeGroupId = 0;
+            ProgramLocationIdentifier newLocationId = 0;
+            ProgramEdgeIdentifier newEdgeId = 0;
+            ProgramActionIdentifier newActionId = 0;
+            
+        };
+    }
+}

src/storage/ppg/ProgramLocation.cpp

@@ -0,0 +1,21 @@
+
+#include "ProgramLocation.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+    namespace ppg {
+        
+        std::vector<ProgramEdge*> ProgramLocation::addProgramEdgeToAllGroups(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
+            return graph->addProgramEdgeToAllGroups(*this, action, condition, targetId);
+        }
+        
+        std::vector<ProgramEdge*> ProgramLocation::addProgramEdgeToAllGroups(ProgramActionIdentifier action, ProgramLocationIdentifier targetId) {
+            return graph->addProgramEdgeToAllGroups(*this, action, targetId);
+        }
+        
+        ProgramEdgeGroup* ProgramLocation::addProgramEdgeGroup(storm::expressions::Expression const& probability) {
+            return graph->addProgramEdgeGroup(*this, probability);
+        }
+        
+    }
+}

src/storage/ppg/ProgramLocation.h

@@ -0,0 +1,62 @@
+#pragma once
+
+#include "defines.h"
+#include "ProgramEdgeGroup.h"
+
+namespace storm {
+    namespace ppg {
+        class ProgramLocation {
+        public:
+            using EdgeGroupIterator = std::vector<ProgramEdgeGroup*>::iterator;
+            
+            ProgramLocation(ProgramGraph* graph, ProgramLocationIdentifier id, bool initial) : graph(graph), locId(id), init(initial){
+                // Intentionally left empty
+            }
+            
+            virtual ~ProgramLocation() {
+                for( auto const& e : edgeGroups) {
+                    delete e;
+                }
+            }
+            
+            
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId);
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramActionIdentifier action, ProgramLocationIdentifier targetId);
+            ProgramEdgeGroup* addProgramEdgeGroup(storm::expressions::Expression const& probability);
+            
+            
+            ProgramEdgeGroup* emplaceEdgeGroup(ProgramEdgeGroupIdentifier id, storm::expressions::Expression const& probability) {
+                edgeGroups.emplace_back(new ProgramEdgeGroup(graph, id, locId, probability));
+                return edgeGroups.back();
+            }
+            
+            bool isInitial() const {
+                return init;
+            }
+            
+            size_t nrOutgoingEdgeGroups() const {
+                return edgeGroups.size();
+            }
+            
+            EdgeGroupIterator getOutgoingEdgeGroupBegin() {
+                return edgeGroups.begin();
+            }
+            
+            EdgeGroupIterator getOutgoingEdgeGroupEnd() {
+                return edgeGroups.end();
+            }
+            
+            ProgramLocationIdentifier id() const {
+                return locId;
+            }
+            
+        private:
+            ProgramGraph* graph;
+            ProgramLocationIdentifier locId;
+            bool init;
+            std::vector<ProgramEdgeGroup*> edgeGroups;
+            
+            
+        };
+    }
+}

src/storage/ppg/defines.h

@@ -0,0 +1,15 @@
+#pragma once
+#include <cassert>
+#include <vector>
+namespace storm {
+    namespace ppg {
+        class ProgramGraph;
+        class ProgramEdgeGroup;
+        class ProgramLocation;
+        using ProgramLocationIdentifier = uint64_t;
+        using ProgramActionIdentifier = uint64_t;
+        using ProgramEdgeGroupIdentifier =  uint64_t;
+        using ProgramEdgeIdentifier = uint64_t;
+        
+    }
+}