Bindings for JANI

src/core/input.cpp

@@ -14,8 +14,10 @@ void define_property(py::module& m) {
 // Define python bindings
 void define_input(py::module& m) {
 
-    // Parse prism program
-    m.def("parse_prism_program", &storm::api::parseProgram, "Parse prism program", py::arg("path"));
+    // Parse Prism program
+    m.def("parse_prism_program", &storm::api::parseProgram, "Parse Prism program", py::arg("path"));
+    // Parse Jani model
+    m.def("parse_jani_model", &storm::api::parseJaniModel, "Parse Jani model", py::arg("path"));
 
     // PrismType
     py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")
@@ -27,13 +29,6 @@ void define_input(py::module& m) {
         .value("UNDEFINED", storm::prism::Program::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");
-
-
-
     // PrismProgram
     py::class_<storm::prism::Program>(m, "PrismProgram", "Prism program")
         .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules")
@@ -41,13 +36,43 @@ void define_input(py::module& m) {
         .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants")
         .def("__str__", &streamToString<storm::prism::Program>)
     ;
+
+    // JaniType
+    py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model")
+        .value("DTMC", storm::jani::ModelType::DTMC)
+        .value("CTMC", storm::jani::ModelType::CTMC)
+        .value("MDP", storm::jani::ModelType::MDP)
+        .value("CTMDP", storm::jani::ModelType::CTMDP)
+        .value("MA", storm::jani::ModelType::MA)
+        .value("LTS", storm::jani::ModelType::LTS)
+        .value("TA", storm::jani::ModelType::TA)
+        .value("PTA", storm::jani::ModelType::PTA)
+        .value("STA", storm::jani::ModelType::STA)
+        .value("HA", storm::jani::ModelType::HA)
+        .value("PHA", storm::jani::ModelType::PHA)
+        .value("SHA", storm::jani::ModelType::SHA)
+        .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")
+    ;
     
     // 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"))
+        .def(py::init<storm::jani::Model const&>(), "Construct from Jani model", py::arg("jani_model"))
         .def_property_readonly("is_prism_program", &storm::storage::SymbolicModelDescription::isPrismProgram, "Flag if program is in Prism format")
+        .def_property_readonly("is_jani_model", &storm::storage::SymbolicModelDescription::isJaniModel, "Flag if program is in Jani format")
+        .def("instantiate_constants", [](storm::storage::SymbolicModelDescription const& description, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) {
+                return description.preprocess(constantDefinitions);
+            }, "Instantiate constants in symbolic model description", py::arg("constant_definitions"))
     ;
 
-    // PrismProgram can be converted into SymbolicModelDescription
+    // PrismProgram and JaniModel can be converted into SymbolicModelDescription
     py::implicitly_convertible<storm::prism::Program, storm::storage::SymbolicModelDescription>();
+    py::implicitly_convertible<storm::jani::Model, storm::storage::SymbolicModelDescription>();
 }

tests/core/test_parse.py

@@ -9,6 +9,9 @@ class TestParse:
         assert program.nr_modules == 1
         assert program.model_type == stormpy.PrismModelType.DTMC
         assert not program.has_undefined_constants
+        description = stormpy.SymbolicModelDescription(program)
+        assert description.is_prism_program
+        assert not description.is_jani_model
 
     def test_parse_parametric_prism_program(self):
         program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
@@ -16,6 +19,15 @@ class TestParse:
         assert program.model_type == stormpy.PrismModelType.DTMC
         assert program.has_undefined_constants
 
+    def test_parse_jani_model(self):
+        jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani"))
+        assert jani_model.name == "brp"
+        assert jani_model.model_type == stormpy.JaniModelType.DTMC
+        assert jani_model.has_undefined_constants
+        description = stormpy.SymbolicModelDescription(jani_model)
+        assert not description.is_prism_program
+        assert description.is_jani_model
+
     def test_parse_formula(self):
         formula = "P=? [F \"one\"]"
         properties = stormpy.parse_properties(formula)