diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 192f680..877518a 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -2,6 +2,7 @@ #include #include #include +#include #include "src/helpers.h" using namespace storm::jani; @@ -15,53 +16,70 @@ 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("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("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("get_automaton_index", &Model::getAutomatonIndex, "get index for automaton name") - .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_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("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("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("get_automaton_index", &Model::getAutomatonIndex, "get index for automaton name") + .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") + ; + py::class_> automaton(m, "JaniAutomaton", "A Jani Automation"); automaton.def_property_readonly("edges",[](const Automaton& a) {return a.getEdges();}, "get edges") - .def_property_readonly("name", &Automaton::getName); + .def_property_readonly("name", &Automaton::getName) + ; + py::class_> edge(m, "JaniEdge", "A Jani Edge"); edge.def_property_readonly("source_location_index", &Edge::getSourceLocationIndex, "index for source location") - .def_property_readonly("destinations", &Edge::getDestinations, "edge destinations") - .def_property_readonly("nr_destinations", &Edge::getNumberOfDestinations, "nr edge destinations") - .def_property_readonly("guard", &Edge::getGuard, "edge guard") - .def("substitute", &Edge::substitute, py::arg("mapping")) - .def("has_silent_action", &Edge::hasSilentAction, "Is the edge labelled with the silent action"); + .def_property_readonly("destinations", &Edge::getDestinations, "edge destinations") + .def_property_readonly("nr_destinations", &Edge::getNumberOfDestinations, "nr edge destinations") + .def_property_readonly("guard", &Edge::getGuard, "edge guard") + .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()); py::class_> edgeDestination(m, "JaniEdgeDestination", "Destination in Jani"); edgeDestination.def_property_readonly("target_location_index", &EdgeDestination::getLocationIndex) - .def_property_readonly("probability", &EdgeDestination::getProbability) - .def_property_readonly("assignments", &EdgeDestination::getOrderedAssignments) + .def_property_readonly("probability", &EdgeDestination::getProbability) + .def_property_readonly("assignments", &EdgeDestination::getOrderedAssignments) ; + py::class_> orderedAssignments(m, "JaniOrderedAssignments", "Set of assignments"); orderedAssignments.def("__iter__", [](OrderedAssignments &v) { return py::make_iterator(v.begin(), v.end()); }, py::keep_alive<0, 1>()) /* Keep vector alive while iterator is used */ - .def("__str__", &streamToString) - ; + .def("__str__", &streamToString) + ; + py::class_> assignment(m, "JaniAssignment", "Jani Assignment"); assignment.def("__str__", &streamToString) - .def_property("expression", &Assignment::getAssignedExpression, &Assignment::setAssignedExpression) + .def_property("expression", &Assignment::getAssignedExpression, &Assignment::setAssignedExpression) ; + py::class_> constant(m, "JaniConstant", "A Constant in JANI"); constant.def_property_readonly("defined", &Constant::isDefined, "is constant defined by some expression") - .def_property_readonly("name", &Constant::getName, "name of constant") - .def_property_readonly("type", &Constant::getType, "type of constant") - .def_property_readonly("expression_variable", &Constant::getExpressionVariable, "expression variable for this constant"); + .def_property_readonly("name", &Constant::getName, "name of constant") + .def_property_readonly("type", &Constant::getType, "type of constant") + .def_property_readonly("expression_variable", &Constant::getExpressionVariable, "expression variable for this constant") + ; + + + m.def("eliminate_reward_accumulations", [](const Model& model, std::vector& properties) { + storm::logic::RewardAccumulationEliminationVisitor v(model); + v.eliminateRewardAccumulations(properties); + return properties; + }, "Eliminate reward accumulations", py::arg("model"), py::arg("properties")); + } \ No newline at end of file diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index a750c74..1d4b15f 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -32,17 +32,18 @@ class TestModelChecking: def test_model_checking_jani_dtmc(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) - formula = properties["Probability to throw a six"] - formula2 = properties["Expected number of coin flips"] - model = stormpy.build_model(jani_model, [formula, formula2]) + formulas = [properties["Probability to throw a six"], properties["Expected number of coin flips"]] + formulas = stormpy.eliminate_reward_accumulations(jani_model, formulas) + assert len(formulas) == 2 + model = stormpy.build_model(jani_model, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 assert len(model.initial_states) == 1 initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formula) + result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 1 / 6) - result = stormpy.model_checking(model, formula2) + result = stormpy.model_checking(model, formulas[1]) assert math.isclose(result.at(initial_state), 11 / 3) def test_model_checking_dtmc_all_labels(self):