From 92275c396028218717ef01f8cbedcec05bb7986f Mon Sep 17 00:00:00 2001
From: Kevin Batz <kevinbatz@Admins-MacBook-Pro.local>
Date: Tue, 2 Jul 2019 12:38:40 +0200
Subject: [PATCH] tests for prism programs and expressions

---
 src/storage/expressions.cpp       | 3 +++
 src/storage/prism.cpp             | 2 +-
 tests/storage/test_expressions.py | 1 +
 tests/storage/test_prism.py       | 9 ++++++++-
 4 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp
index e2934ef..ab96006 100644
--- a/src/storage/expressions.cpp
+++ b/src/storage/expressions.cpp
@@ -28,6 +28,8 @@ void define_expressions(py::module& m) {
         .def("create_rational_variable", &storm::expressions::ExpressionManager::declareRationalVariable, "create Rational variable", py::arg("name"), py::arg("auxiliary") = false)
             ;
 
+
+
     // Variable
     py::class_<storm::expressions::Variable, std::shared_ptr<storm::expressions::Variable>>(m, "Variable", "Represents a variable")
         .def_property_readonly("name", &storm::expressions::Variable::getName, "Variable name")
@@ -41,6 +43,7 @@ void define_expressions(py::module& m) {
 
 
 
+
     py::enum_<storm::expressions::OperatorType>(m, "OperatorType", "Type of an operator (of any sort)")
             .value("And", storm::expressions::OperatorType::And)
             .value("Or", storm::expressions::OperatorType::Or)
diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp
index 7c51586..6eb7c78 100644
--- a/src/storage/prism.cpp
+++ b/src/storage/prism.cpp
@@ -75,7 +75,7 @@ void define_prism(py::module& m) {
             ;
 
 
-    // Added by Kevin
+
     py::class_<Variable, std::shared_ptr<Variable>> variable(m, "Prism_Variable", "A program variable in a Prism program");
     variable.def_property_readonly("name", &Variable::getName, "Variable Name")
             .def_property_readonly("initial_value_expression", &Variable::getInitialValueExpression, "The expression represented the initial value of the variable")
diff --git a/tests/storage/test_expressions.py b/tests/storage/test_expressions.py
index 92b8ed1..db2f018 100644
--- a/tests/storage/test_expressions.py
+++ b/tests/storage/test_expressions.py
@@ -9,6 +9,7 @@ class TestExpressions:
         manager = stormpy.ExpressionManager()
         expression = manager.create_boolean(True)
         assert expression.is_literal()
+        assert expression.evaluate_as_bool
         assert not expression.contains_variables()
         assert expression.has_boolean_type()
         assert not expression.has_integer_type()
diff --git a/tests/storage/test_prism.py b/tests/storage/test_prism.py
index cbb9788..0c163aa 100644
--- a/tests/storage/test_prism.py
+++ b/tests/storage/test_prism.py
@@ -12,6 +12,7 @@ class TestPrism:
         jani_model, new_properties = program.to_jani(orig_properties)
         assert len(new_properties) == len(orig_properties)
 
+
     def test_prism_to_jani_labels(self):
         program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
         orig_properties = stormpy.parse_properties_for_prism_program("P=? [F \"two\"]", program)
@@ -27,4 +28,10 @@ class TestPrism:
         assert len(new_properties) == len(orig_properties)
         orig_properties = stormpy.parse_properties_for_prism_program("P=? [F s=7]", program)
         jani_model, new_properties = program.to_jani(orig_properties, suffix = "2")
-        assert len(new_properties) == len(orig_properties)
\ No newline at end of file
+        assert len(new_properties) == len(orig_properties)
+
+    def test_prism_variables(selfs):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
+        module = program.modules[0]
+        assert len(module.integer_variables) == 2
+        assert len(module.boolean_variables) == 0