From 66da4e5463aeac586a420dca7d78af2b22f99d9c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 1 Aug 2017 15:03:41 +0200 Subject: [PATCH] Made expression module part of storage module --- CMakeLists.txt | 1 - lib/stormpy/expressions/__init__.py | 2 -- setup.py | 3 +-- src/logic/formulae.cpp | 8 +++---- src/mod_expressions.cpp | 21 ----------------- src/mod_storage.cpp | 2 ++ src/storage/expressions.cpp | 30 +++++++++++++++++++++++ src/storage/expressions.h | 8 +++++++ tests/expressions/test_expressions.py | 10 -------- tests/logic/test_formulas.py | 20 +++++++++------- tests/storage/test_expressions.py | 34 +++++++++++++++++++++++++++ 11 files changed, 90 insertions(+), 49 deletions(-) delete mode 100644 lib/stormpy/expressions/__init__.py delete mode 100644 src/mod_expressions.cpp create mode 100644 src/storage/expressions.cpp create mode 100644 src/storage/expressions.h delete mode 100644 tests/expressions/test_expressions.py create mode 100644 tests/storage/test_expressions.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 1eab77a..c400ebd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -44,7 +44,6 @@ endfunction(stormpy_module) stormpy_module(core "${STORMPY_LIB_DIR}") stormpy_module(info) -stormpy_module(expressions) stormpy_module(logic) stormpy_module(storage) stormpy_module(utility) diff --git a/lib/stormpy/expressions/__init__.py b/lib/stormpy/expressions/__init__.py deleted file mode 100644 index b185f36..0000000 --- a/lib/stormpy/expressions/__init__.py +++ /dev/null @@ -1,2 +0,0 @@ -from . import expressions -from .expressions import * diff --git a/setup.py b/setup.py index fe28eea..9e0f447 100755 --- a/setup.py +++ b/setup.py @@ -181,13 +181,12 @@ setup( maintainer_email="sebastian.junges@cs.rwth-aachen.de", url="http://moves.rwth-aachen.de", description="stormpy - Python Bindings for Storm", - packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', + packages=['stormpy', 'stormpy.info', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', 'stormpy.pars', 'stormpy.dft'], package_dir={'': 'lib'}, ext_package='stormpy', ext_modules=[CMakeExtension('core', subdir=''), CMakeExtension('info', subdir='info'), - CMakeExtension('expressions', subdir='expressions'), CMakeExtension('logic', subdir='logic'), CMakeExtension('storage', subdir='storage'), CMakeExtension('utility', subdir='utility'), diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 25324be..a73c2fa 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -11,11 +11,6 @@ void define_formulae(py::module& m) { .value("GEQ", storm::logic::ComparisonType::GreaterEqual) ; - /*py::class_>, void, void>("FormulaVec", "Vector of formulas") - .def(vector_indexing_suite>, true>()) - ;*/ - - py::class_> formula(m, "Formula", "Generic Storm Formula"); formula.def("__str__", &storm::logic::Formula::toString) ; @@ -57,6 +52,9 @@ void define_formulae(py::module& m) { return f.getThresholdAs(); } }, "Threshold of bound (currently only applicable to rational expressions)") + .def("set_bound", [](storm::logic::OperatorFormula& f, storm::logic::ComparisonType comparisonType, storm::expressions::Expression const& bound) { + f.setBound(storm::logic::Bound(comparisonType, bound)); + }, "Set bound", py::arg("comparison_type"), py::arg("bound")) // the above method should be sufficient for now; reinstate the following if needed //.def_property("_threshold_expression", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold expression") //.def_property_readonly("_threshold_as_rational", &storm::logic::OperatorFormula::getThresholdAs, "Rational threshold of bound, if applicable") diff --git a/src/mod_expressions.cpp b/src/mod_expressions.cpp deleted file mode 100644 index c379cfc..0000000 --- a/src/mod_expressions.cpp +++ /dev/null @@ -1,21 +0,0 @@ -#include "common.h" -#include "storm/storage/expressions/ExpressionManager.h" - -PYBIND11_MODULE(expressions, m) { - m.doc() = "Storm expressions"; - -#ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); -#endif - - py::class_>(m, "ExpressionManager", "Manages variables for expressions"); - - py::class_(m, "Expression", "Holds an expression") - .def("__str__", &storm::expressions::Expression::toString) - .def_property_readonly("contains_variables", &storm::expressions::Expression::containsVariables) - .def_property_readonly("has_boolean_type", &storm::expressions::Expression::hasBooleanType) - .def_property_readonly("has_integer_type", &storm::expressions::Expression::hasIntegerType) - .def_property_readonly("has_rational_type", &storm::expressions::Expression::hasRationalType) - ; -} diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index fe1d6d9..b507db6 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -5,6 +5,7 @@ #include "storage/matrix.h" #include "storage/state.h" #include "storage/labeling.h" +#include "storage/expressions.h" PYBIND11_MODULE(storage, m) { m.doc() = "Data structures in Storm"; @@ -19,4 +20,5 @@ PYBIND11_MODULE(storage, m) { define_sparse_matrix(m); define_state(m); define_labeling(m); + define_expressions(m); } diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp new file mode 100644 index 0000000..2c1909c --- /dev/null +++ b/src/storage/expressions.cpp @@ -0,0 +1,30 @@ +#include "expressions.h" +#include "src/helpers.h" + +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/Expression.h" + +//Define python bindings +void define_expressions(py::module& m) { + + // ExpressionManager + py::class_>(m, "ExpressionManager", "Manages variables for expressions") + .def(py::init(), "Constructor") + .def("create_boolean", &storm::expressions::ExpressionManager::boolean, py::arg("boolean"), "Create expression from boolean") + .def("create_integer", &storm::expressions::ExpressionManager::integer, py::arg("integer"), "Create expression from integer number") + .def("create_rational", [](storm::expressions::ExpressionManager const& manager, storm::RationalNumber number) { + return manager.rational(number); + }, py::arg("rational"), "Create expression from rational number") + ; + + // Expression + py::class_>(m, "Expression", "Holds an expression") + .def("contains_variables", &storm::expressions::Expression::containsVariables, "Check if the expression contains variables.") + .def("is_literal", &storm::expressions::Expression::isLiteral, "Check if the expression is a literal") + .def("has_boolean_type", &storm::expressions::Expression::hasBooleanType, "Check if the expression is a boolean") + .def("has_integer_type", &storm::expressions::Expression::hasIntegerType, "Check if the expression is an integer") + .def("has_rational_type", &storm::expressions::Expression::hasRationalType, "Check if the expression is a rational") + .def("__str__", &streamToString) + ; + +} \ No newline at end of file diff --git a/src/storage/expressions.h b/src/storage/expressions.h new file mode 100644 index 0000000..698f6a4 --- /dev/null +++ b/src/storage/expressions.h @@ -0,0 +1,8 @@ +#ifndef PYTHON_STORAGE_EXPRESSIONS_H_ +#define PYTHON_STORAGE_EXPRESSIONS_H_ + +#include "common.h" + +void define_expressions(py::module& m); + +#endif /* PYTHON_STORAGE_EXPRESSIONS_H_ */ diff --git a/tests/expressions/test_expressions.py b/tests/expressions/test_expressions.py deleted file mode 100644 index e25c90f..0000000 --- a/tests/expressions/test_expressions.py +++ /dev/null @@ -1,10 +0,0 @@ -import stormpy -from stormpy.expressions import expressions - - -class TestExpressions: - def test_expression_manager(self): - manager = expressions.ExpressionManager - - def test_expression(self): - expression = expressions.Expression diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index 6cc6816..a81846f 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -42,14 +42,18 @@ class TestFormulas: assert formula.comparison_type == stormpy.logic.ComparisonType.LESS # setter not currently implemented (non-trivial due to Expression container) - #def test_set_bounds(self): - # prop = "P<0.4 [F \"one\"]" - # formula = stormpy.parse_properties(prop)[0].raw_formula - # formula.threshold = pycarl.Rational("0.2") - # formula.comparison_type = stormpy.logic.ComparisonType.GEQ - # assert formula.threshold == pycarl.Rational("0.2") - # assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ - # assert str(formula) == "P>=1/5 [F \"one\"]" + def test_set_bounds(self): + import pycarl + import pycarl.gmp + prop = "P<0.4 [F \"one\"]" + formula = stormpy.parse_properties(prop)[0].raw_formula + expression_manager = stormpy.ExpressionManager() + rational = pycarl.gmp.Rational("0.2") + expression = expression_manager.create_rational(rational) + formula.set_bound(stormpy.logic.ComparisonType.GEQ, expression) + assert formula.threshold == pycarl.gmp.Rational("0.2") + assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ + assert str(formula) == "P>=1/5 [F \"one\"]" def test_subformula(self): prop = "P=? [F \"one\"]" diff --git a/tests/storage/test_expressions.py b/tests/storage/test_expressions.py new file mode 100644 index 0000000..9aed379 --- /dev/null +++ b/tests/storage/test_expressions.py @@ -0,0 +1,34 @@ +import stormpy + + +class TestExpressions: + def test_expression_manager(self): + manager = stormpy.ExpressionManager() + + def test_boolean_expression(self): + manager = stormpy.ExpressionManager() + expression = manager.create_boolean(True) + assert expression.is_literal() + assert not expression.contains_variables() + assert expression.has_boolean_type() + assert not expression.has_integer_type() + assert not expression.has_rational_type() + + def test_integer_expression(self): + manager = stormpy.ExpressionManager() + expression = manager.create_integer(2) + assert expression.is_literal() + assert not expression.contains_variables() + assert not expression.has_boolean_type() + assert expression.has_integer_type() + assert not expression.has_rational_type() + + def test_rational_expression(self): + import pycarl.gmp + manager = stormpy.ExpressionManager() + expression = manager.create_rational(pycarl.gmp.Rational(0.2)) + assert expression.is_literal() + assert not expression.contains_variables() + assert not expression.has_boolean_type() + assert not expression.has_integer_type() + assert expression.has_rational_type()