From cddaf4ca2a8d7b3b21463016d6468ac1c8319f2e Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 27 Jan 2016 11:36:28 +0100
Subject: [PATCH] python for const formulae

Former-commit-id: 06cbf7386a40f2dfe6395c1114f8f43880e107b5
---
 src/python/storm-core.cpp  | 12 ++++++------
 src/python/storm-logic.cpp |  4 +++-
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp
index 60504d93e..7b740bf1a 100644
--- a/src/python/storm-core.cpp
+++ b/src/python/storm-core.cpp
@@ -17,12 +17,12 @@ public:
 };
 
 // Thin wrapper for model building
-std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula> const& formula) {
-    return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<storm::logic::Formula>>(1,formula)).model;
+std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<const storm::logic::Formula> const& formula) {
+    return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<const storm::logic::Formula>>(1,formula)).model;
 }
 
 // Thin wrapper for parametric state elimination
-std::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+std::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
     std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<storm::RationalFunction>(model, formula);
     std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>();
     result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()]);
@@ -98,8 +98,8 @@ BOOST_PYTHON_MODULE(_core)
     defineClass<storm::models::sparse::Dtmc<storm::RationalFunction>,  storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricDtmc", "");
     defineClass<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMdp", "");
 
-    defineClass<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
-        .def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
+    defineClass<std::vector<std::shared_ptr<const storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
+        .def(vector_indexing_suite<std::vector<std::shared_ptr<const storm::logic::Formula>>, true>())
     ;
     
     ////////////////////////////////////////////
@@ -109,7 +109,7 @@ BOOST_PYTHON_MODULE(_core)
         .value("STRONG", storm::storage::BisimulationType::Strong)
         .value("WEAK", storm::storage::BisimulationType::Weak)
     ;
-    def("perform_bisimulation_parametric", static_cast<std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> (*)(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const&, std::shared_ptr<storm::logic::Formula> const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization<storm::models::sparse::Model<storm::RationalFunction>>));
+    def("perform_bisimulation_parametric", static_cast<std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> (*)(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const&, std::shared_ptr<const storm::logic::Formula> const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization<storm::models::sparse::Model<storm::RationalFunction>>));
     
     
 
diff --git a/src/python/storm-logic.cpp b/src/python/storm-logic.cpp
index a6da9725f..bdf4954df 100644
--- a/src/python/storm-logic.cpp
+++ b/src/python/storm-logic.cpp
@@ -72,7 +72,9 @@ BOOST_PYTHON_MODULE(_logic)
     defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula",
     "");
     defineClass<storm::logic::OperatorFormula, storm::logic::UnaryStateFormula, boost::noncopyable>("OperatorFormula",
-    "");
+    "")
+        .add_property("has_bound", &storm::logic::OperatorFormula::hasBound)
+        .add_property("bound", &storm::logic::OperatorFormula::getBound)
     defineClass<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator",
     "The expected time between two events");
     defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator",