From e7e474bebcc732e27d85a92721f8c7abf8e69e4c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 2 Apr 2018 17:25:00 +0200 Subject: [PATCH] support for JANI --- src/core/core.cpp | 2 ++ src/core/input.cpp | 9 +------ src/mod_storage.cpp | 2 ++ src/storage/jani.cpp | 60 +++++++++++++++++++++++++++++++++++++++++++ src/storage/jani.h | 5 ++++ src/storage/prism.cpp | 3 ++- 6 files changed, 72 insertions(+), 9 deletions(-) create mode 100644 src/storage/jani.cpp create mode 100644 src/storage/jani.h diff --git a/src/core/core.cpp b/src/core/core.cpp index d32af44..dddb7d6 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -35,6 +35,8 @@ void define_parse(py::module& m) { :return: A list of properties )dox", py::arg("formula_string"), py::arg("prism_program"), py::arg("property_filter") = boost::none); + m.def("parse_properties_for_jani_model", &storm::api::parsePropertiesForJaniModel, py::arg("formula_string"), py::arg("jani_model"), py::arg("property_filter") = boost::none); + // Pair py::class_(m, "ModelFormulasPair", "Pair of model and formulas") .def_property_readonly("model", [](storm::storage::ModelFormulasPair const& pair) { diff --git a/src/core/input.cpp b/src/core/input.cpp index 1ce6a5a..29c7c3e 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -4,6 +4,7 @@ void define_property(py::module& m) { py::class_(m, "Property", "Property") .def(py::init const&, std::string const&>(), "Construct property from formula", py::arg("name"), py::arg("formula"), py::arg("comment") = "") + .def(py::init()) .def_property_readonly("name", &storm::jani::Property::getName, "Obtain the name of the property") .def_property_readonly("raw_formula", &storm::jani::Property::getRawFormula, "Obtain the formula directly") .def("__str__", &streamToString) @@ -36,14 +37,6 @@ void define_input(py::module& m) { .value("UNDEFINED", storm::jani::ModelType::UNDEFINED) ; - // Jani Model - py::class_(m, "JaniModel", "Jani Model") - .def_property_readonly("name", &storm::jani::Model::getName, "Name of the jani model") - .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type") - .def_property_readonly("has_undefined_constants", &storm::jani::Model::hasUndefinedConstants, "Flag if Jani model has undefined constants") - .def_property_readonly("undefined_constants_are_graph_preserving", &storm::jani::Model::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") - ; - // SymbolicModelDescription py::class_(m, "SymbolicModelDescription", "Symbolic description of model") .def(py::init(), "Construct from Prism program", py::arg("prism_program")) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 4fd3cbd..28a328e 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -6,6 +6,7 @@ #include "storage/distribution.h" #include "storage/scheduler.h" #include "storage/prism.h" +#include "storage/jani.h" #include "storage/state.h" #include "storage/labeling.h" #include "storage/expressions.h" @@ -23,6 +24,7 @@ PYBIND11_MODULE(storage, m) { define_sparse_matrix(m); define_state(m); define_prism(m); + define_jani(m); define_labeling(m); define_expressions(m); define_scheduler(m, "Double"); diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp new file mode 100644 index 0000000..3574a35 --- /dev/null +++ b/src/storage/jani.cpp @@ -0,0 +1,60 @@ +#include "jani.h" +#include +#include +#include "src/helpers.h" + +using namespace storm::jani; + +std::string janiToString(Model const& m) { + std::stringstream str; + JsonExporter::toStream(m, {}, str); + return str.str(); +} + +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("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("__str__", &janiToString) + .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); + 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"); + 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) + ; + 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) + ; + py::class_> assignment(m, "JaniAssignment", "Jani Assignment"); + assignment.def("__str__", &streamToString) + .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"); + + +} \ No newline at end of file diff --git a/src/storage/jani.h b/src/storage/jani.h new file mode 100644 index 0000000..27d5cef --- /dev/null +++ b/src/storage/jani.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_jani(py::module& m); diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index c011fcc..01338ea 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -2,7 +2,7 @@ #include #include "src/helpers.h" #include - +#include using namespace storm::prism; @@ -20,6 +20,7 @@ void define_prism(py::module& m) { .def("simplify", &Program::simplify, "Simplify") .def("used_constants",&Program::usedConstants, "Compute Used Constants") .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program") + .def("to_jani", &Program::toJani, "Transform to Jani program", py::arg("all_variables_global")=false) .def("__str__", &streamToString); py::class_ module(m, "PrismModule", "A module in a Prism program");