From 559cb678130335ec9cc1a1a0d08c939e3dfda12f Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 9 Sep 2015 13:22:02 +0200
Subject: [PATCH] updates to the stormpy core

Former-commit-id: 092d694ade7e556c008cacccd30e9ec5a26417e4
---
 src/python/storm-core.cpp | 30 +++++++++++++++++++++++++-----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp
index bcdd4c994..bca8bf57c 100644
--- a/src/python/storm-core.cpp
+++ b/src/python/storm-core.cpp
@@ -11,26 +11,46 @@ BOOST_PYTHON_MODULE(_core)
 {
     using namespace boost::python;
     def("setUp", storm::utility::setUp);
-    
+
+    ////////////////////////////////////////////
+    // Formula
+    ////////////////////////////////////////////
     class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula>, boost::noncopyable>("Formula", no_init)
         .def("toString", &storm::logic::Formula::toString);
 	class_<std::vector<std::shared_ptr<storm::logic::Formula>>>("FormulaVec")
 			.def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
 			;
+    class_<storm::logic::ProbabilityOperatorFormula, std::shared_ptr<storm::logic::ProbabilityOperatorFormula>, bases<storm::logic::Formula>>("ProbabilityOperatorFormula", no_init)
+        .def("toString", &storm::logic::ProbabilityOperatorFormula::toString);
 
 
-	class_<storm::logic::ProbabilityOperatorFormula, std::shared_ptr<storm::logic::ProbabilityOperatorFormula>, bases<storm::logic::Formula>>("ProbabilityOperatorFormula", no_init)
-        .def("toString", &storm::logic::ProbabilityOperatorFormula::toString);
+    ////////////////////////////////////////////
+    // Program
+    ////////////////////////////////////////////
+
     class_<storm::prism::Program>("Program")
-        .def("getNumberOfModules", &storm::prism::Program::getNumberOfModules)
+        .add_property("nrModules", &storm::prism::Program::getNumberOfModules)
     ;
 
 
+    ////////////////////////////////////////////
+    // Checkresult
+    ////////////////////////////////////////////
+    class_<std::unique_ptr<storm::modelchecker::CheckResult>, boost::noncopyable>("CheckResult", no_init);
+
+
+    ////////////////////////////////////////////
+    // Models
+    ////////////////////////////////////////////
+    class_<storm::models::ModelBase, std::shared_ptr<storm::models::ModelBase>, boost::noncopyable>("ModelBase", no_init)
+            .add_property("nrStates", &storm::models::ModelBase::getNumberOfStates)
+            .add_property("nrTransitions", &storm::models::ModelBase::getNumberOfTransitions);
+    class_<storm::models::sparse::Model<double>, std::shared_ptr<storm::models::sparse::Model<double>>, boost::noncopyable, bases<storm::models::ModelBase>>("SparseModel", no_init);
 
     def("parseFormulae", storm::parseFormulasForProgram);
     def("parseProgram", storm::parseProgram);
 
-    def("buildAndCheck", storm::buildAndCheckSymbolicModel<double>);
+    def("buildModelFromPrismProgram", storm::buildSymbolicModel<double>);