tests for prism programs and expressions

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)

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")

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()

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)
@@ -28,3 +29,9 @@ class TestPrism:
         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)
+
+    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