sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

additional bindings for expressions and prism programs

refactoring
Kevin Batz 5 years ago
parent
7641c433a9
commit
a762b28b63
3 changed files with 78 additions and 6 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 51
      src/storage/expressions.cpp
  2. 29
      src/storage/prism.cpp
  3. 2
      tests/storage/test_expressions.py

51
src/storage/expressions.cpp
View File

@ -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_<storm::expressions::OperatorType>(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_<storm::expressions::Expression, std::shared_ptr<storm::expressions::Expression>>(m, "Expression", "Holds an expression")
.def(py::init<Expression>(), "other_expression"_a)
py::class_<storm::expressions::Expression, std::shared_ptr<storm::expressions::Expression>> expression(m, "Expression", "Holds an expression");
expression.def(py::init<Expression>(), "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<Variable, Expression> 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_<storm::parser::ExpressionParser>(m, "ExpressionParser", "Parser for storm-expressions")
.def(py::init<storm::expressions::ExpressionManager const&>(), "Expression Manager to use", py::arg("expression_manager"))
.def("set_identifier_mapping", [](storm::parser::ExpressionParser& p, std::unordered_map<std::string, storm::expressions::Expression> const& identifierMapping) {p.setIdentifierMapping(identifierMapping);}, "sets identifiers")

29
src/storage/prism.cpp
View File

@ -20,15 +20,24 @@ 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<storm::jani::Property> 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<storm::prism::Program>);
.def("__str__", &streamToString<storm::prism::Program>)
.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> 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> command(m, "PrismCommand", "A command in a Prism program");
@ -37,7 +46,9 @@ void define_prism(py::module& m) {
.def_property_readonly("updates", &Command::getUpdates, "Updates in the command");
py::class_<Update> 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> 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, 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")
;
py::class_<IntegerVariable, std::shared_ptr<IntegerVariable>> 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_<BooleanVariable, std::shared_ptr<BooleanVariable>> boolean_variable(m, "Prism_Boolean_Variable", variable, "A program boolean variable in a Prism program");
}

2
tests/storage/test_expressions.py
View File

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

Write Preview
Loading…
Cancel
Save