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