From 9e42f73015d4bc1e34dcd0f4c2cea0bf420640c0 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Mon, 18 Dec 2017 22:23:45 +0100
Subject: [PATCH] towards support for more info from prism programs

---
 src/core/input.cpp    | 19 -------------------
 src/mod_storage.cpp   |  2 ++
 src/storage/prism.cpp | 33 +++++++++++++++++++++++++++++++++
 src/storage/prism.h   |  5 +++++
 4 files changed, 40 insertions(+), 19 deletions(-)
 create mode 100644 src/storage/prism.cpp
 create mode 100644 src/storage/prism.h

diff --git a/src/core/input.cpp b/src/core/input.cpp
index a87c18a..1ce6a5a 100644
--- a/src/core/input.cpp
+++ b/src/core/input.cpp
@@ -19,25 +19,6 @@ void define_input(py::module& m) {
     // Parse Jani model
     m.def("parse_jani_model", &storm::api::parseJaniModel, "Parse Jani model", py::arg("path"));
 
-    // PrismType
-    py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")
-        .value("DTMC", storm::prism::Program::ModelType::DTMC)
-        .value("CTMC", storm::prism::Program::ModelType::CTMC)
-        .value("MDP", storm::prism::Program::ModelType::MDP)
-        .value("CTMDP", storm::prism::Program::ModelType::CTMDP)
-        .value("MA", storm::prism::Program::ModelType::MA)
-        .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED)
-    ;
-
-    // PrismProgram
-    py::class_<storm::prism::Program>(m, "PrismProgram", "Prism program")
-        .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules")
-        .def_property_readonly("model_type", &storm::prism::Program::getModelType, "Model type")
-        .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants")
-        .def_property_readonly("undefined_constants_are_graph_preserving", &storm::prism::Program::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure")
-        .def("__str__", &streamToString<storm::prism::Program>)
-    ;
-
     // JaniType
     py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model")
         .value("DTMC", storm::jani::ModelType::DTMC)
diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp
index b507db6..62ced7d 100644
--- a/src/mod_storage.cpp
+++ b/src/mod_storage.cpp
@@ -3,6 +3,7 @@
 #include "storage/bitvector.h"
 #include "storage/model.h"
 #include "storage/matrix.h"
+#include "storage/prism.h"
 #include "storage/state.h"
 #include "storage/labeling.h"
 #include "storage/expressions.h"
@@ -19,6 +20,7 @@ PYBIND11_MODULE(storage, m) {
     define_model(m);
     define_sparse_matrix(m);
     define_state(m);
+    define_prism(m);
     define_labeling(m);
     define_expressions(m);
 }
diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp
new file mode 100644
index 0000000..4c97de3
--- /dev/null
+++ b/src/storage/prism.cpp
@@ -0,0 +1,33 @@
+#include "prism.h"
+#include <storm/storage/prism/Program.h>
+#include "src/helpers.h"
+
+using namespace storm::prism;
+
+void define_prism(py::module& m) {
+    py::class_<storm::prism::Program, std::shared_ptr<storm::prism::Program>> program(m, "PrismProgram", "A Prism Program");
+    program.def_property_readonly("constants", &Program::getConstants, "Get Program Constants")
+    .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules")
+            .def_property_readonly("model_type", &storm::prism::Program::getModelType, "Model type")
+            .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants")
+            .def_property_readonly("undefined_constants_are_graph_preserving", &storm::prism::Program::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure")
+            .def("__str__", &streamToString<storm::prism::Program>);
+
+
+    // PrismType
+    py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")
+            .value("DTMC", storm::prism::Program::ModelType::DTMC)
+            .value("CTMC", storm::prism::Program::ModelType::CTMC)
+            .value("MDP", storm::prism::Program::ModelType::MDP)
+            .value("CTMDP", storm::prism::Program::ModelType::CTMDP)
+            .value("MA", storm::prism::Program::ModelType::MA)
+            .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED)
+            ;
+
+
+    py::class_<Constant, std::shared_ptr<Constant>> constant(m, "Constant", "A constant in a Prism program");
+    constant.def_property_readonly("name", &Constant::getName, "Constant name")
+            .def_property_readonly("defined", &Constant::isDefined, "Is the constant defined?")
+            .def_property_readonly("type", &Constant::getType, "The type of the constant");
+
+}
\ No newline at end of file
diff --git a/src/storage/prism.h b/src/storage/prism.h
new file mode 100644
index 0000000..17f3a63
--- /dev/null
+++ b/src/storage/prism.h
@@ -0,0 +1,5 @@
+#pragma  once
+
+#include "common.h"
+
+void define_prism(py::module& m);