diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index e91f051..f43f8ae 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -8,6 +8,7 @@ //Define python bindings void define_expressions(py::module& m) { using Expression = storm::expressions::Expression; + using Variable = storm::expressions::Variable; @@ -47,6 +48,7 @@ void define_expressions(py::module& m) { .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("__str__", &storm::expressions::Expression::toString, "To string") .def_static("plus", [](Expression const& lhs, Expression const& rhs) {return lhs + rhs;}) diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 10d4d29..d18f766 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -14,11 +14,13 @@ std::string janiToString(Model const& m) { } void define_jani(py::module& m) { + py::class_> md(m, "JaniModel", "A Jani Model"); md.def_property_readonly("name", &Model::getName, "model name") .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type") - .def_property_readonly("automata", [](const Model& model) {return model.getAutomata();}, "get automata") - .def_property_readonly("constants", [](const Model& model) {return model.getConstants();}, "get constants") + .def("set_model_type", &Model::setModelType, "Sets (only) the model type") + .def_property_readonly("automata", [](const Model& model) -> auto& {return model.getAutomata();}, "get automata") + .def_property_readonly("constants", [](const Model& model) -> auto& {return model.getConstants();}, "get constants") .def("restrict_edges", &Model::restrictEdges, "restrict model to edges given by set", py::arg("edge_set")) .def_property_readonly("expression_manager", &Model::getExpressionManager, "get expression manager", pybind11::return_value_policy::reference_internal) .def_property_readonly("has_undefined_constants", &Model::hasUndefinedConstants, "Flag if program has undefined constants") @@ -26,10 +28,12 @@ void define_jani(py::module& m) { .def("__str__", &janiToString) .def("define_constants", &Model::defineUndefinedConstants, "define constants with a mapping from the corresponding expression variables to expressions", py::arg("map")) .def("substitute_constants", &Model::substituteConstants, "substitute constants") + .def("remove_constant", &Model::removeConstant, "remove a constant. Make sure the constant does not appear in the model.", "constant_name"_a) .def("get_automaton_index", &Model::getAutomatonIndex, "name"_a, "get index for automaton name") .def("replace_automaton", &Model::replaceAutomaton, "index"_a, "new_automaton"_a, "replace automaton at index") .def_static("encode_edge_and_automaton_index", &Model::encodeAutomatonAndEdgeIndices, "get edge/automaton-index") .def_static("decode_edge_and_automaton_index", &Model::decodeAutomatonAndEdgeIndices, "get edge and automaton from edge/automaton index") + .def("finalize", &Model::finalize,"finalizes the model. After this action, be careful changing the data structure.") ; py::class_> automaton(m, "JaniAutomaton", "A Jani Automation"); @@ -39,8 +43,8 @@ void define_jani(py::module& m) { }, "get edges") .def_property_readonly("name", &Automaton::getName) .def_property_readonly("location_variable", &Automaton::getLocationExpressionVariable) - .def_property_readonly("variables", [](Automaton& aut) {return aut.getVariables();}) - .def_property_readonly("locations", [](Automaton& aut) {return aut.getLocations();}) + .def_property_readonly("variables", [](Automaton& aut) -> VariableSet& {return aut.getVariables();}, py::return_value_policy::reference_internal) + .def_property_readonly("locations", [](Automaton& aut) -> auto& {return aut.getLocations();}) .def("add_location", &Automaton::addLocation, "location"_a, "adds a new location, returns the index") .def("add_initial_location", [](Automaton& aut, uint64_t index) { aut.addInitialLocation(index); }, "index"_a) .def_property_readonly("initial_location_indices", &Automaton::getInitialLocationIndices) @@ -107,7 +111,9 @@ void define_jani(py::module& m) { .def("__iter__", [](VariableSet &v) { return py::make_iterator(v.begin(), v.end()); }, py::keep_alive<0, 1>()) - .def("add_variable", [](VariableSet& vs, Variable& v) { vs.addVariable(v);} ) + .def("add_variable", [](VariableSet& vs, Variable& v) { vs.addVariable(v); }) + .def("add_bounded_integer_variable", [](VariableSet& vs, BoundedIntegerVariable& v) { return vs.addVariable(v);}, "variable"_a) + .def("empty", &VariableSet::empty, "is there a variable in the set?") ; py::class_> variable(m, "JaniVariable", "A Variable in JANI");