diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index 5345cae..e2934ef 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -3,12 +3,15 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/Valuation.h" +#include "storm/storage/expressions/OperatorType.h" #include "storm-parsers/parser/ExpressionParser.h" //Define python bindings void define_expressions(py::module& m) { using Expression = storm::expressions::Expression; using Variable = storm::expressions::Variable; + using Valuation = storm::expressions::Valuation; @@ -23,7 +26,6 @@ void define_expressions(py::module& m) { .def("create_boolean_variable", &storm::expressions::ExpressionManager::declareBooleanVariable, "create Boolean variable", py::arg("name"), py::arg("auxiliary") = false) .def("create_integer_variable", &storm::expressions::ExpressionManager::declareIntegerVariable, "create Integer variable", py::arg("name"), py::arg("auxiliary") = false) .def("create_rational_variable", &storm::expressions::ExpressionManager::declareRationalVariable, "create Rational variable", py::arg("name"), py::arg("auxiliary") = false) - ; // Variable @@ -37,20 +39,62 @@ void define_expressions(py::module& m) { .def("get_expression", &storm::expressions::Variable::getExpression, "Get expression from variable") ; + + + py::enum_(m, "OperatorType", "Type of an operator (of any sort)") + .value("And", storm::expressions::OperatorType::And) + .value("Or", storm::expressions::OperatorType::Or) + .value("Xor", storm::expressions::OperatorType::Xor) + .value("Implies", storm::expressions::OperatorType::Implies) + .value("Iff", storm::expressions::OperatorType::Iff) + .value("Plus", storm::expressions::OperatorType::Plus) + .value("Minus", storm::expressions::OperatorType::Minus) + .value("Times", storm::expressions::OperatorType::Times) + .value("Divide", storm::expressions::OperatorType::Divide) + .value("Min", storm::expressions::OperatorType::Min) + .value("Max", storm::expressions::OperatorType::Max) + .value("Power", storm::expressions::OperatorType::Power) + .value("Modulo", storm::expressions::OperatorType::Modulo) + .value("Equal", storm::expressions::OperatorType::Equal) + .value("NotEqual", storm::expressions::OperatorType::NotEqual) + .value("Less", storm::expressions::OperatorType::Less) + .value("LessOrEqual", storm::expressions::OperatorType::LessOrEqual) + .value("Greater", storm::expressions::OperatorType::Greater) + .value("GreaterOrEqual", storm::expressions::OperatorType::GreaterOrEqual) + .value("Not", storm::expressions::OperatorType::Not) + .value("Floor", storm::expressions::OperatorType::Floor) + .value("Ceil", storm::expressions::OperatorType::Ceil) + .value("Ite", storm::expressions::OperatorType::Ite) + ; + + // Expression - py::class_>(m, "Expression", "Holds an expression") - .def(py::init(), "other_expression"_a) + py::class_> expression(m, "Expression", "Holds an expression"); + expression.def(py::init(), "other_expression"_a) .def("contains_variables", &storm::expressions::Expression::containsVariables, "Check if the expression contains variables.") .def("contains_variable", &storm::expressions::Expression::containsVariable, "Check if the expression contains any of the given variables.", py::arg("variables")) .def("get_variables" , &storm::expressions::Expression::getVariables, "Get the variables") .def("is_literal", &storm::expressions::Expression::isLiteral, "Check if the expression is a literal") + .def("is_variable", &storm::expressions::Expression::isVariable, "Check if the expression is a variable") + .def("identifier", &storm::expressions::Expression::getIdentifier, "Retrieves the identifier associated with this expression if this expression is a variable") .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_property_readonly("type", &storm::expressions::Expression::getType, "Get the Type") .def_property_readonly("manager", &storm::expressions::Expression::getManager, "Get the manager") .def("substitute", [](Expression const& expr, std::map const& map) { return expr.substitute(map);}, "substitution_map"_a) + .def("evaluate_as_int", [](Expression const& expr) + {return expr.evaluateAsInt();}, "Get the integer value this expression evaluates to") + .def("evaluate_as_bool", [](Expression const& expr) + {return expr.evaluateAsBool();}, "Get the boolean value this expression evaluates to") + .def("evaluate_as_double", [](Expression const& expr) + {return expr.evaluateAsDouble();}, "Get the double value this expression evaluates to") .def("__str__", &storm::expressions::Expression::toString, "To string") + .def_property_readonly("is_function_application", &storm::expressions::Expression::isFunctionApplication, "True iff the expression is a function application (of any sort") + .def_property_readonly("operator", &storm::expressions::Expression::getOperator, "The operator of the expression (if it is a function application)") + .def_property_readonly("arity", &storm::expressions::Expression::getArity, "The arity of the expression") + .def("get_operand", &storm::expressions::Expression::getOperand + , "Get the operand at the given index", py::arg("operandIndex")) .def_static("Plus", [](Expression const& lhs, Expression const& rhs) {return lhs + rhs;}) .def_static("Minus", [](Expression const& lhs, Expression const& rhs) {return lhs - rhs;}) @@ -67,6 +111,7 @@ void define_expressions(py::module& m) { .def_static("Iff", [](Expression const& lhs, Expression const& rhs) {return storm::expressions::iff(lhs, rhs);}) ; + py::class_(m, "ExpressionParser", "Parser for storm-expressions") .def(py::init(), "Expression Manager to use", py::arg("expression_manager")) .def("set_identifier_mapping", [](storm::parser::ExpressionParser& p, std::unordered_map const& identifierMapping) {p.setIdentifierMapping(identifierMapping);}, "sets identifiers") diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 57b0b80..7c51586 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -20,16 +20,25 @@ void define_prism(py::module& m) { .def("restrict_commands", &Program::restrictCommands, "Restrict commands") .def("simplify", &Program::simplify, "Simplify") .def("used_constants",&Program::usedConstants, "Compute Used Constants") + .def_property_readonly("hasUndefinedConstants", &Program::hasUndefinedConstants, "Does the program have undefined constants?") + .def_property_readonly("isDeterministicModel", &Program::isDeterministicModel, "Does the program describe a deterministic model?") .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program") .def("to_jani", [](storm::prism::Program const& program, std::vector const& properties, bool allVariablesGlobal, std::string suffix) { return program.toJani(properties, allVariablesGlobal, suffix); }, "Transform to Jani program", py::arg("properties"), py::arg("all_variables_global") = true, py::arg("suffix") = "") - .def("__str__", &streamToString); + .def("__str__", &streamToString) + .def_property_readonly("variables", &Program::getAllExpressionVariables, "Get all Expression Variables used by the program") + .def("get_label_expression", [](storm::prism::Program const& program, std::string const& label){ + return program.getLabelExpression(label); + }, "Get the expression of the given label.", py::arg("label")) + ; py::class_ module(m, "PrismModule", "A module in a Prism program"); module.def_property_readonly("commands", [](Module const& module) {return module.getCommands();}, "Commands in the module") .def_property_readonly("name", &Module::getName, "Name of the module") - ; + .def_property_readonly("integer_variables", &Module::getIntegerVariables, "All integer Variables of this module") + .def_property_readonly("boolean_variables", &Module::getBooleanVariables, "All boolean Variables of this module") + ; py::class_ command(m, "PrismCommand", "A command in a Prism program"); command.def_property_readonly("global_index", &Command::getGlobalIndex, "Get global index") @@ -37,7 +46,9 @@ void define_prism(py::module& m) { .def_property_readonly("updates", &Command::getUpdates, "Updates in the command"); py::class_ update(m, "PrismUpdate", "An update in a Prism command"); - update.def_property_readonly("assignments", &Update::getAssignments, "Assignments in the update"); + update.def_property_readonly("assignments", &Update::getAssignments, "Assignments in the update") + .def_property_readonly("probability_expression", &Update::getLikelihoodExpression, "The probability expression for this update") + ;//Added by Kevin py::class_ assignment(m, "PrismAssignment", "An assignment in prism"); assignment.def_property_readonly("variable", &Assignment::getVariable, "Variable that is updated") @@ -64,4 +75,18 @@ 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") + ; + + py::class_> integer_variable(m, "Prism_Integer_Variable", variable, "A program integer variable in a Prism program"); + integer_variable.def_property_readonly("lower_bound_expression", &IntegerVariable::getLowerBoundExpression, "The the lower bound expression of this integer variable") + .def_property_readonly("upper_bound_expression", &IntegerVariable::getUpperBoundExpression, "The the upper bound expression of this integer variable") + ; + + py::class_> boolean_variable(m, "Prism_Boolean_Variable", variable, "A program boolean variable in a Prism program"); + + } \ No newline at end of file diff --git a/tests/storage/test_expressions.py b/tests/storage/test_expressions.py index 8ba8e4c..92b8ed1 100644 --- a/tests/storage/test_expressions.py +++ b/tests/storage/test_expressions.py @@ -22,6 +22,7 @@ class TestExpressions: assert not expression.has_boolean_type() assert expression.has_integer_type() assert not expression.has_rational_type() + assert expression.evaluate_as_int() == 2 def test_rational_expression(self): manager = stormpy.ExpressionManager() @@ -31,6 +32,7 @@ class TestExpressions: assert not expression.has_boolean_type() assert not expression.has_integer_type() assert expression.has_rational_type() + assert expression.evaluate_as_double() == 0.2 def test_expression_parser(self): manager = stormpy.ExpressionManager()