From b2ca743422d292b1ff3d7b168bbeb69f320fbf11 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Tue, 13 Sep 2016 14:18:36 +0200
Subject: [PATCH] ProgramGraph->Jani (only locations & variables)

Former-commit-id: 70324d2df406ac2857bde83e4024144be2440f80 [formerly e17bc3cffd9bb57c9791a7bfbd7cdfeaab46bc07]
Former-commit-id: bafb2e72add590fef3134aaac69344c060fa7c39
---
 src/builder/JaniProgramGraphBuilder.cpp |  7 +++
 src/builder/JaniProgramGraphBuilder.h   | 66 +++++++++++++++++++++++++
 src/storage/IntegerInterval.cpp         |  2 +
 src/storage/IntegerInterval.h           | 42 ++++++++++++++++
 4 files changed, 117 insertions(+)
 create mode 100644 src/builder/JaniProgramGraphBuilder.cpp
 create mode 100644 src/builder/JaniProgramGraphBuilder.h
 create mode 100644 src/storage/IntegerInterval.cpp
 create mode 100644 src/storage/IntegerInterval.h

diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp
new file mode 100644
index 000000000..7ec2e1fb5
--- /dev/null
+++ b/src/builder/JaniProgramGraphBuilder.cpp
@@ -0,0 +1,7 @@
+#include "JaniProgramGraphBuilder.h"
+
+namespace storm {
+    namespace builder {
+        unsigned JaniProgramGraphBuilder::janiVersion = 1;
+    }
+}
\ No newline at end of file
diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h
new file mode 100644
index 000000000..01f392e47
--- /dev/null
+++ b/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;
+            
+        };
+    }
+}
\ No newline at end of file
diff --git a/src/storage/IntegerInterval.cpp b/src/storage/IntegerInterval.cpp
new file mode 100644
index 000000000..7722d359b
--- /dev/null
+++ b/src/storage/IntegerInterval.cpp
@@ -0,0 +1,2 @@
+#include "IntegerInterval.h"
+
diff --git a/src/storage/IntegerInterval.h b/src/storage/IntegerInterval.h
new file mode 100644
index 000000000..6f59be238
--- /dev/null
+++ b/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);
+    }
+}
\ No newline at end of file