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

several extensions and fixes for jani data structures

refactoring
Sebastian Junges 6 years ago
parent
65147aec12
commit
cec2861a5d
3 changed files with 33 additions and 15 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. 6
      src/storage/choiceorigins.cpp
  2. 42
      src/storage/jani.cpp
  3. 0
      tests/storage/test_jani.py

6
src/storage/choiceorigins.cpp
View File

@ -5,9 +5,11 @@
void define_origins(py::module& m) {
using ChoiceOrigins = storm::storage::sparse::ChoiceOrigins;
py::class_<ChoiceOrigins, std::shared_ptr<ChoiceOrigins>> 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_<JaniChoiceOrigins, std::shared_ptr<JaniChoiceOrigins>>(m, "JaniChoiceOrigins", "This class represents for each choice the origin in the jani spec.")
py::class_<JaniChoiceOrigins, std::shared_ptr<JaniChoiceOrigins>>(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"))
;
}

42
src/storage/jani.cpp
View File

@ -16,31 +16,40 @@ std::string janiToString(Model const& m) {
void define_jani(py::module& m) {
py::class_<Model, std::shared_ptr<Model>> md(m, "JaniModel", "A Jani Model");
md.def_property_readonly("name", &Model::getName, "model name")
md.def(py::init<Model>(), "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, std::shared_ptr<Automaton>> automaton(m, "JaniAutomaton", "A Jani Automation");
automaton.def(py::init<std::string, storm::expressions::Variable>())
.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<uint64_t, uint64_t, boost::optional<storm::expressions::Expression>, std::shared_ptr<TemplateEdge>, std::vector<std::pair<uint64_t, storm::expressions::Expression>>>(),
"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, std::shared_ptr<TemplateEdge>> templateEdge(m, "JaniTemplateEdge", "Template edge, internal data structure for edges");
templateEdge.def(py::init<storm::expressions::Expression>())
.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, std::shared_ptr<TemplateEdgeDestination>> templateEdgeDestination(m, "JaniTemplateEdgeDestination", "Template edge destination, internal data structure for edge destinations");
templateEdgeDestination.def(py::init<OrderedAssignments>(), "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, std::shared_ptr<OrderedAssignments>> 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<OrderedAssignments>)
.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, std::shared_ptr<Assignment>> assignment(m, "JaniAssignment", "Jani Assignment");
assignment.def("__str__", &streamToString<Assignment>)
assignment.def(py::init<Variable const&,storm::expressions::Expression const&,int64_t>(), "lhs"_a, "rhs"_a, "lvl"_a = 0)
.def("__str__", &streamToString<Assignment>)
.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, std::shared_ptr<Variable>> 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_<BoundedIntegerVariable> bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable);
py::class_<BoundedIntegerVariable, std::shared_ptr<BoundedIntegerVariable>> bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable);
bivariable.def(py::init<std::string, storm::expressions::Variable, storm::expressions::Expression, storm::expressions::Expression, storm::expressions::Expression>(),
"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<std::string, storm::expressions::Variable, storm::expressions::Expression, storm::expressions::Expression>(),
"name"_a, "expression_variable"_a, "lower_bound"_a, "upper_bound"_a);;
py::class_<Constant, std::shared_ptr<Constant>> constant(m, "JaniConstant", "A Constant in JANI");
constant.def_property_readonly("defined", &Constant::isDefined, "is constant defined by some expression")

0
tests/storage/test_jani.py
View File

Write Preview
Loading…
Cancel
Save