ProgramGraph->Jani (only locations & variables)

Former-commit-id: 70324d2df4 [formerly e17bc3cffd]
Former-commit-id: bafb2e72ad

src/builder/JaniProgramGraphBuilder.cpp

@@ -0,0 +1,7 @@
+#include "JaniProgramGraphBuilder.h"
+
+namespace storm {
+    namespace builder {
+        unsigned JaniProgramGraphBuilder::janiVersion = 1;
+    }
+}

src/builder/JaniProgramGraphBuilder.h

@@ -0,0 +1,66 @@
+#include "src/storage/ppg/ProgramGraph.h"
+#include "src/storage/jani/Model.h"
+#include "src/storage/jani/Location.h"
+#include "src/storage/IntegerInterval.h"
+
+
+namespace storm {
+    namespace builder {
+        
+        enum class JaniProgramGraphVariableDomainMethod  {
+            Unrestricted, IntervalPropagation
+        };
+        
+        struct JaniProgramGraphBuilderSetting {
+            JaniProgramGraphVariableDomainMethod variableDomainMethod = JaniProgramGraphVariableDomainMethod::Unrestricted;
+        };
+        
+        class JaniProgramGraphBuilder {
+        public:
+            static unsigned janiVersion;
+            
+            JaniProgramGraphBuilder() {
+                
+            }
+            
+            //void addVariableRestriction(storm::expressions::Variable const& var, storm::IntegerInterval const& interval ) {
+                
+            //}
+            
+        
+            
+            storm::jani::Model* build(storm::ppg::ProgramGraph const& pg, std::string const& name = "program_graph") {
+                expManager = pg.getExpressionManager();
+                storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager);
+                storm::jani::Automaton mainAutomaton("main");
+                addProcedureVariables(mainAutomaton, pg);
+                addProcedureLocations(mainAutomaton, pg);
+                model->addAutomaton(mainAutomaton);
+                return model;
+            }
+            
+        private:
+            void addProcedureVariables(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) {
+                for (auto const& v : pg.getVariables()) {
+                    if(variableRestrictions.count(v.getIndex())) {
+                        assert(false);
+                    } else {
+                        storm::jani::UnboundedIntegerVariable janiVar(v.getName(), v, expManager->integer(0), false);
+                        automaton.addUnboundedIntegerVariable(janiVar);
+                    }
+                }
+            }
+            
+            void addProcedureLocations(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) {
+                for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) {
+                    storm::jani::Location janiLoc(std::to_string(it->second.id()));
+                    automaton.addLocation(janiLoc);
+                }
+            }
+            
+            std::map<uint64_t, storm::storage::IntegerInterval> variableRestrictions;
+            std::shared_ptr<storm::expressions::ExpressionManager> expManager;
+            
+        };
+    }
+}

src/storage/IntegerInterval.cpp

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

src/storage/IntegerInterval.h

@@ -0,0 +1,42 @@
+#pragma once 
+
+#include <boost/optional.hpp>
+
+namespace storm {
+    namespace storage {
+        class IntegerInterval {
+            
+        public:
+            explicit IntegerInterval(uint64_t v) : leftBound(v), rightBound(v) {
+                
+            }
+            
+            IntegerInterval(uint64_t lb, uint64_t rb) : leftBound(lb), rightBound(rb) {
+                
+            }
+            
+            bool hasLeftBound() {
+                return leftBound != boost::none;
+            }
+            
+            bool hasRightBound() {
+                return rightBound != boost::none;
+            }
+            
+            boost::optional<uint64_t> getLeftBound() {
+                return leftBound;
+            }
+            
+            boost::optional<uint64_t> getRightBound() {
+                return rightBound;
+            }
+            
+        private:
+            boost::optional<uint64_t> leftBound;
+            boost::optional<uint64_t> rightBound;
+            
+        };
+        
+        std::ostream& operator<<(std::ostream& os, IntegerInterval const& i);
+    }
+}