From 89f3924b8c39a01fb9f24711698ab9e9990b5d20 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Mon, 17 Aug 2020 21:10:30 -0700
Subject: [PATCH] finding explicit states in models

---
 src/core/core.cpp           | 17 +++++++++++++++++
 tests/core/test_building.py | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+)
 create mode 100644 tests/core/test_building.py

diff --git a/src/core/core.cpp b/src/core/core.cpp
index 725f849..2f218a9 100644
--- a/src/core/core.cpp
+++ b/src/core/core.cpp
@@ -110,6 +110,23 @@ void define_build(py::module& m) {
     m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
 
+    m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
+    m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
+
+    py::class_<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder_Double", "Model builder for sparse models")
+        .def("build", &storm::builder::ExplicitModelBuilder<double>::build, "Build the model")
+        .def("export_lookup", &storm::builder::ExplicitModelBuilder<double>::exportExplicitStateLookup, "Export a lookup model")
+    ;
+
+    py::class_<storm::builder::ExplicitModelBuilder<storm::RationalFunction>>(m, "ExplicitModelBuilder_RF", "Model builder for sparse models")
+        .def("build", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::build, "Build the model")
+        .def("export_lookup", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::exportExplicitStateLookup, "Export a lookup model")
+    ;
+
+    py::class_<storm::builder::ExplicitStateLookup<uint32_t>>(m, "ExplicitStateLookup", "Lookup model for states")
+        .def("lookup", &storm::builder::ExplicitStateLookup<uint32_t>::lookup, py::arg("state_description"))
+    ;
+
 
     py::class_<storm::builder::BuilderOptions>(m, "BuilderOptions", "Options for building process")
             .def(py::init<std::vector<std::shared_ptr<storm::logic::Formula const>> const&>(), "Initialise with formulae to preserve", py::arg("formulae"))
diff --git a/tests/core/test_building.py b/tests/core/test_building.py
new file mode 100644
index 0000000..1352545
--- /dev/null
+++ b/tests/core/test_building.py
@@ -0,0 +1,36 @@
+import stormpy
+import stormpy.examples
+import stormpy.examples.files
+
+class TestBuilding:
+    def test_explicit_builder(self):
+        path = stormpy.examples.files.prism_dtmc_die
+        prism_program = stormpy.parse_prism_program(path)
+        formula_str = "P=? [F s=7 & d=2]"
+        properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
+
+        # Fix variables in the program.
+        module = prism_program.modules[0]
+        s_var = module.get_integer_variable("s").expression_variable
+        d_var = module.get_integer_variable("d").expression_variable
+
+        # Construct the model
+        options = stormpy.BuilderOptions([p.raw_formula for p in properties])
+        options.set_build_state_valuations()
+        model_builder = stormpy.make_sparse_model_builder(prism_program, options)
+        model = model_builder.build()
+        # and export the model from building
+        state_mapping = model_builder.export_lookup()
+
+        #lookup 1
+        state = { s_var : prism_program.expression_manager.create_integer(3), d_var : prism_program.expression_manager.create_integer(0)}
+        id = state_mapping.lookup(state)
+        assert model.state_valuations.get_integer_value(id, s_var) == 3
+        assert model.state_valuations.get_integer_value(id, d_var) == 0
+
+        #lookup 2
+        state = { s_var : prism_program.expression_manager.create_integer(7), d_var : prism_program.expression_manager.create_integer(3)}
+        id = state_mapping.lookup(state)
+        assert model.state_valuations.get_integer_value(id, s_var) == 7
+        assert model.state_valuations.get_integer_value(id, d_var) == 3
+