From cec2861a5d1c68941fef0b701ec5ca2cb03f5116 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 29 Nov 2018 12:55:55 +0100 Subject: [PATCH] several extensions and fixes for jani data structures --- src/storage/choiceorigins.cpp | 6 +++-- src/storage/jani.cpp | 42 ++++++++++++++++++++++++----------- tests/storage/test_jani.py | 0 3 files changed, 33 insertions(+), 15 deletions(-) create mode 100644 tests/storage/test_jani.py diff --git a/src/storage/choiceorigins.cpp b/src/storage/choiceorigins.cpp index c41cfe2..01488b6 100644 --- a/src/storage/choiceorigins.cpp +++ b/src/storage/choiceorigins.cpp @@ -5,9 +5,11 @@ void define_origins(py::module& m) { using ChoiceOrigins = storm::storage::sparse::ChoiceOrigins; py::class_> co(m, "ChoiceOrigins", "This class represents the origin of choices of a model in terms of the input model spec."); + co.def("get_identifier_info", &ChoiceOrigins::getIdentifierInfo, "identifier"_a, "human readable string") + .def("get_choice_info", &ChoiceOrigins::getChoiceInfo, "identifier"_a, "human readable string") ; using JaniChoiceOrigins = storm::storage::sparse::JaniChoiceOrigins; - py::class_>(m, "JaniChoiceOrigins", "This class represents for each choice the origin in the jani spec.") + py::class_>(m, "JaniChoiceOrigins", "This class represents for each choice the origin in the jani spec.", co) .def_property_readonly("model", &JaniChoiceOrigins::getModel, "retrieves the associated JANI model") - .def("get_edge_index_set", [](JaniChoiceOrigins const& co, uint64_t choice) { return co.getEdgeIndexSet(choice); }, "returns the set of edges that induced the choice", py::arg("choice_index")) + .def("get_edge_index_set", [](JaniChoiceOrigins const& co, uint64_t choice) -> auto& { return co.getEdgeIndexSet(choice); }, "returns the set of edges that induced the choice", py::arg("choice_index")) ; } \ No newline at end of file diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index e40076a..9ce9771 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -16,31 +16,40 @@ 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") + md.def(py::init(), "other_model"_a) + .def_property_readonly("name", &Model::getName, "model name") .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type") .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("global_variables", [](const Model& model) -> auto& {return model.getGlobalVariables();}) .def_property_readonly("constants", [](const Model& model) -> auto& {return model.getConstants();}, "get constants") + .def("get_constant", &Model::getConstant, "name"_a, "get constant by name") .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") .def_property_readonly("undefined_constants_are_graph_preserving", &Model::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") .def("__str__", &janiToString) + .def_property("initial_states_restriction", &Model::getInitialStatesRestriction, &Model::setInitialStatesRestriction, "initial states restriction") .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("add_automaton", &Model::addAutomaton, "automaton"_a, "add an automaton (with a unique name)") + .def("set_standard_system_composition", &Model::setStandardSystemComposition, "sets the composition to the standard composition") .def("replace_automaton", &Model::replaceAutomaton, "index"_a, "new_automaton"_a, "replace automaton at index") .def("check_valid", &Model::checkValid, "Some basic checks to ensure validity") - .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("substitute_functions", [](Model& model) {model.substituteFunctions();}, "substitute functions") + .def_static("encode_automaton_and_edge_index", &Model::encodeAutomatonAndEdgeIndices, "get edge/automaton-index") + .def_static("decode_automaton_and_edge_index", &Model::decodeAutomatonAndEdgeIndices, "get edge and automaton from edge/automaton index") + .def("make_standard_compliant", &Model::makeStandardJaniCompliant, "make standard JANI compliant") + .def("has_standard_composition", &Model::hasStandardComposition, "is the composition the standard composition") .def("finalize", &Model::finalize,"finalizes the model. After this action, be careful changing the data structure.") .def("to_dot", [](Model& model) {std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }) ; py::class_> automaton(m, "JaniAutomaton", "A Jani Automation"); automaton.def(py::init()) - .def_property_readonly("edges",[](const Automaton& a) { + .def_property_readonly("edges",[](const Automaton& a) -> auto& { return a.getEdges(); }, "get edges") .def_property_readonly("name", &Automaton::getName) @@ -59,7 +68,7 @@ void define_jani(py::module& m) { edge.def(py::init, std::shared_ptr, std::vector>>(), "source_location_index"_a, "action_index"_a, "rate"_a, "template_edge"_a, "destinations_with_probabilities"_a) .def_property_readonly("source_location_index", &Edge::getSourceLocationIndex, "index for source location") - .def_property_readonly("destinations", [](Edge const& e) { + .def_property_readonly("destinations", [](Edge const& e) -> auto& { return e.getDestinations(); }, "edge destinations") .def_property_readonly("action_index", &Edge::getActionIndex, "action index") @@ -67,15 +76,16 @@ void define_jani(py::module& m) { .def_property_readonly("rate", &Edge::getOptionalRate, "edge rate") .def_property_readonly("nr_destinations", &Edge::getNumberOfDestinations, "nr edge destinations") .def_property_readonly("guard", &Edge::getGuard, "edge guard") + .def_property("color", &Edge::getColor, &Edge::setColor, "color for the edge") .def("substitute", &Edge::substitute, py::arg("mapping")) .def("has_silent_action", &Edge::hasSilentAction, "Is the edge labelled with the silent action") ; py::class_> templateEdge(m, "JaniTemplateEdge", "Template edge, internal data structure for edges"); templateEdge.def(py::init()) - .def_property_readonly("assignments", [](TemplateEdge& te) { return te.getAssignments(); }) + .def_property_readonly("assignments", [](TemplateEdge& te) -> auto& { return te.getAssignments(); }) .def_property("guard", &TemplateEdge::getGuard, &TemplateEdge::setGuard) - .def_property_readonly("destinations",[](TemplateEdge& te) { return te.getDestinations(); }) + .def_property_readonly("destinations",[](TemplateEdge& te) -> auto& { return te.getDestinations(); }) .def("add_destination", &TemplateEdge::addDestination) ; @@ -87,7 +97,7 @@ void define_jani(py::module& m) { py::class_> templateEdgeDestination(m, "JaniTemplateEdgeDestination", "Template edge destination, internal data structure for edge destinations"); templateEdgeDestination.def(py::init(), "ordered_assignments"_a) - .def_property_readonly("assignments", [](TemplateEdgeDestination& ted) {return ted.getOrderedAssignments();}); + .def_property_readonly("assignments", [](TemplateEdgeDestination& ted) -> auto& {return ted.getOrderedAssignments();}); py::class_> orderedAssignments(m, "JaniOrderedAssignments", "Set of assignments"); orderedAssignments.def("__iter__", [](OrderedAssignments &v) { @@ -95,11 +105,13 @@ void define_jani(py::module& m) { }, py::keep_alive<0, 1>()) /* Keep vector alive while iterator is used */ .def("__str__", &streamToString) .def("clone", &OrderedAssignments::clone, "clone assignments (performs a deep copy)") + .def("substitute", &OrderedAssignments::substitute, "substitute in rhs according to given substitution map", "substitution_map"_a) .def("add", [](OrderedAssignments& oa, Assignment const& newAssignment, bool addToExisting) {return oa.add(newAssignment, addToExisting); }, "new_assignment"_a, "add_to_existing"_a = false) ; py::class_> assignment(m, "JaniAssignment", "Jani Assignment"); - assignment.def("__str__", &streamToString) + assignment.def(py::init(), "lhs"_a, "rhs"_a, "lvl"_a = 0) + .def("__str__", &streamToString) .def_property("expression", &Assignment::getAssignedExpression, &Assignment::setAssignedExpression) ; @@ -113,9 +125,11 @@ 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_bounded_integer_variable", [](VariableSet& vs, BoundedIntegerVariable& v) { return vs.addVariable(v);}, "variable"_a) + .def("add_variable", [](VariableSet& vs, Variable& v) -> void { vs.addVariable(v); }) + .def("add_bounded_integer_variable", [](VariableSet& vs, BoundedIntegerVariable& v) -> auto& { return vs.addVariable(v); /*return vs.getVariable(v.getExpressionVariable());*/ }, py::return_value_policy::reference_internal, "variable"_a) .def("empty", &VariableSet::empty, "is there a variable in the set?") + .def("get_variable_by_name", [](VariableSet& v, std::string const& name) -> auto& { return v.getVariable(name);}) + .def("get_variable_by_expr_variable", [](VariableSet& v, storm::expressions::Variable const& var) -> auto& { return v.getVariable(var);}) ; py::class_> variable(m, "JaniVariable", "A Variable in JANI"); @@ -123,9 +137,11 @@ void define_jani(py::module& m) { .def_property_readonly("expression_variable", &Variable::getExpressionVariable, "expression variable for this variable") ; - py::class_ bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable); + py::class_> bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable); bivariable.def(py::init(), - "name"_a, "expression_variable"_a, "init_value"_a, "lower_bound"_a, "upper_bound"_a); + "name"_a, "expression_variable"_a, "init_value"_a, "lower_bound"_a, "upper_bound"_a) + .def(py::init(), + "name"_a, "expression_variable"_a, "lower_bound"_a, "upper_bound"_a);; py::class_> constant(m, "JaniConstant", "A Constant in JANI"); constant.def_property_readonly("defined", &Constant::isDefined, "is constant defined by some expression") diff --git a/tests/storage/test_jani.py b/tests/storage/test_jani.py new file mode 100644 index 0000000..e69de29