support for JANI

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 <Model,Formulas>
     py::class_<storm::storage::ModelFormulasPair>(m, "ModelFormulasPair", "Pair of model and formulas")
         .def_property_readonly("model", [](storm::storage::ModelFormulasPair const& pair) {

src/core/input.cpp

@@ -4,6 +4,7 @@
 void define_property(py::module& m) {
     py::class_<storm::jani::Property>(m, "Property", "Property")
         .def(py::init<std::string const&, std::shared_ptr<storm::logic::Formula const> const&, std::string const&>(), "Construct property from formula", py::arg("name"), py::arg("formula"), py::arg("comment") = "")
+        .def(py::init<storm::jani::Property>())
         .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<storm::jani::Property>)
@@ -36,14 +37,6 @@ void define_input(py::module& m) {
         .value("UNDEFINED", storm::jani::ModelType::UNDEFINED)
     ;
 
-    // Jani Model
-    py::class_<storm::jani::Model>(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_<storm::storage::SymbolicModelDescription>(m, "SymbolicModelDescription", "Symbolic description of model")
         .def(py::init<storm::prism::Program const&>(), "Construct from Prism program", py::arg("prism_program"))

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<double>(m, "Double");

src/storage/jani.cpp

@@ -0,0 +1,60 @@
+#include "jani.h"
+#include <storm/storage/jani/Model.h>
+#include <storm/storage/jani/JSONExporter.h>
+#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_<Model, std::shared_ptr<Model>> 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, std::shared_ptr<Automaton>> 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, std::shared_ptr<Edge>> 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, std::shared_ptr<TemplateEdge>> templateEdge(m, "JaniTemplateEdge", "Template edge, internal data structure for edges");
+    templateEdge.def(py::init<storm::expressions::Expression>());
+
+    py::class_<EdgeDestination, std::shared_ptr<EdgeDestination>> 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, std::shared_ptr<OrderedAssignments>> 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<OrderedAssignments>)
+            ;
+    py::class_<Assignment, std::shared_ptr<Assignment>> assignment(m, "JaniAssignment", "Jani Assignment");
+    assignment.def("__str__", &streamToString<Assignment>)
+            .def_property("expression", &Assignment::getAssignedExpression, &Assignment::setAssignedExpression)
+    ;
+    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")
+            .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");
+
+
+}

src/storage/jani.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_jani(py::module& m);

src/storage/prism.cpp

@@ -2,7 +2,7 @@
 #include <storm/storage/prism/Program.h>
 #include "src/helpers.h"
 #include <storm/storage/expressions/ExpressionManager.h>
-
+#include <storm/storage/jani/Model.h>
 
 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<storm::prism::Program>);
 
     py::class_<Module> module(m, "PrismModule", "A module in a Prism program");