add k-shortest paths binding (ShortestPathsGenerator)

Merge branch 'ksp_generator'

CMakeLists.txt

@@ -38,3 +38,9 @@ pybind11_add_module(storage ${CMAKE_CURRENT_SOURCE_DIR}/src/mod_storage.cpp ${ST
 target_include_directories(storage PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR})
 target_link_libraries(storage PRIVATE storm)
 
+file(GLOB_RECURSE STORM_UTILITY_SOURCES ${CMAKE_CURRENT_SOURCE_DIR}/src/utility/*.cpp)
+
+pybind11_add_module(utility ${CMAKE_CURRENT_SOURCE_DIR}/src/mod_utility.cpp ${STORM_UTILITY_SOURCES})
+target_include_directories(utility PUBLIC ${CMAKE_CURRENT_SOURCE_DIR} ${storm_INCLUDE_DIR})
+target_link_libraries(utility PRIVATE storm)
+

lib/stormpy/utility/__init__.py

@@ -0,0 +1,2 @@
+from . import utility
+from .utility import *

setup.py

@@ -76,10 +76,10 @@ setup(
       maintainer_email="sebastian.junges@cs.rwth-aachen.de",
       url="http://moves.rwth-aachen.de",
       description="stormpy - Python Bindings for Storm",
-      packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage'],
+      packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility'],
       package_dir={'':'lib'},
       ext_package='stormpy',
-      ext_modules=[CMakeExtension('core', subdir=''), CMakeExtension('info', subdir='info'),CMakeExtension('expressions', subdir='expressions'), CMakeExtension('logic', subdir='logic'), CMakeExtension('storage', subdir='storage')],
+      ext_modules=[CMakeExtension('core', subdir=''), CMakeExtension('info', subdir='info'), CMakeExtension('expressions', subdir='expressions'), CMakeExtension('logic', subdir='logic'), CMakeExtension('storage', subdir='storage'), CMakeExtension('utility', subdir='utility')],
       cmdclass=dict(build_ext=CMakeBuild),
       zip_safe=False,
       install_requires=['pytest'],

src/CMakeLists.txt

@@ -7,11 +7,13 @@ FILE(GLOB core_files "core/*.cpp")
 #FILE(GLOB info_files "info/*.cpp")
 #FILE(GLOB expressions_files "expressions/*.cpp")
 FILE(GLOB storage_files "storage/*.cpp")
+FILE(GLOB utility_files "utility/*.cpp")
 FILE(GLOB logic_files "logic/*.cpp")
 ADD_LIBRARY(stormpy_core SHARED mod_core.cpp ${core_files})
 ADD_LIBRARY(stormpy_info SHARED mod_info.cpp)
 ADD_LIBRARY(stormpy_expressions SHARED mod_expressions.cpp)
 ADD_LIBRARY(stormpy_storage SHARED mod_storage.cpp ${storage_files})
+ADD_LIBRARY(stormpy_utility SHARED mod_utility.cpp ${utility_files})
 ADD_LIBRARY(stormpy_logic SHARED mod_logic.cpp ${logic_files})
 
 SET_TARGET_PROPERTIES(stormpy_core PROPERTIES
@@ -42,6 +44,13 @@ SET_TARGET_PROPERTIES(stormpy_storage PROPERTIES
         LIBRARY_OUTPUT_DIRECTORY ${STORMPY_OUTPUT_DIR}/storage
 )
 
+SET_TARGET_PROPERTIES(stormpy_utility PROPERTIES
+        OUTPUT_NAME utility
+        PREFIX ""
+        SUFFIX ".so"
+        LIBRARY_OUTPUT_DIRECTORY ${STORMPY_OUTPUT_DIR}/utility
+        )
+
 SET_TARGET_PROPERTIES(stormpy_logic PROPERTIES
         OUTPUT_NAME logic
         PREFIX ""
@@ -53,4 +62,5 @@ TARGET_LINK_LIBRARIES(stormpy_core storm ${PYTHON_LIBRARIES})
 TARGET_LINK_LIBRARIES(stormpy_info storm ${PYTHON_LIBRARIES})
 TARGET_LINK_LIBRARIES(stormpy_expressions storm ${PYTHON_LIBRARIES})
 TARGET_LINK_LIBRARIES(stormpy_storage storm ${PYTHON_LIBRARIES})
+TARGET_LINK_LIBRARIES(stormpy_utility storm ${PYTHON_LIBRARIES})
 TARGET_LINK_LIBRARIES(stormpy_logic storm ${PYTHON_LIBRARIES})

src/common.h

@@ -13,6 +13,7 @@
 #include <tuple>
 
 namespace py = pybind11;
+using namespace pybind11::literals;
 
 #if PY_MAJOR_VERSION >= 3
 #define PY_DIV "__truediv__"

src/mod_storage.cpp

@@ -1,10 +1,12 @@
 #include "common.h"
 
+#include "storage/bitvector.h"
 #include "storage/model.h"
 #include "storage/matrix.h"
 
 PYBIND11_PLUGIN(storage) {
     py::module m("storage");
+    define_bitvector(m);
     define_model(m);
     define_sparse_matrix(m);
     return m.ptr();

src/mod_utility.cpp

@@ -0,0 +1,9 @@
+#include "common.h"
+
+#include "utility/shortestPaths.h"
+
+PYBIND11_PLUGIN(utility) {
+    py::module m("utility", "Dumping ground of stuff that really should be somewhere more reasonable");
+    define_ksp(m);
+    return m.ptr();
+}

src/storage/bitvector.cpp

@@ -0,0 +1,39 @@
+#include "bitvector.h"
+#include "storm/storage/BitVector.h"
+
+#include <sstream>
+
+void define_bitvector(py::module& m) {
+    using BitVector = storm::storage::BitVector;
+
+    py::class_<BitVector>(m, "BitVector")
+        .def(py::init<>())
+        .def(py::init<BitVector>(), "other"_a)
+        .def(py::init<uint_fast64_t>(), "length"_a)
+        .def(py::init<uint_fast64_t, bool>(), "length"_a, "init"_a)
+        .def(py::init<uint_fast64_t, std::vector<uint_fast64_t>>(), "length"_a, "set_entries"_a)
+
+        .def("size", &BitVector::size)
+        .def("number_of_set_bits", &BitVector::getNumberOfSetBits)
+      //.def("get", &BitVector::get, "index"_a) // no idea why this does not work
+        .def("get", [](BitVector const& b, uint_fast64_t i) { return b.get(i); }, "index"_a)
+
+        .def(py::self == py::self)
+        .def(py::self != py::self)
+
+        .def(py::self < py::self)
+        .def(py::self & py::self)
+        .def(py::self | py::self)
+        .def(py::self ^ py::self)
+        .def(py::self % py::self)
+        .def(~py::self)
+
+        .def(py::self &= py::self)
+        .def(py::self |= py::self)
+
+        .def("__repr__", [](BitVector const& b) { std::ostringstream oss; oss << b; return oss.str(); })
+
+        // TODO (when needed): iterator
+    ;
+
+}

src/storage/bitvector.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_STORAGE_BITVECTOR_H_
+#define PYTHON_STORAGE_BITVECTOR_H_
+
+#include "common.h"
+
+void define_bitvector(py::module& m);
+
+#endif /* PYTHON_STORAGE_BITVECTOR_H_ */

src/utility/shortestPaths.cpp

@@ -0,0 +1,66 @@
+#include "shortestPaths.h"
+#include "storm/utility/shortestPaths.h"
+
+#include <sstream>
+#include <string>
+
+#include <boost/optional/optional_io.hpp>
+
+void define_ksp(py::module& m) {
+
+    // long types shortened for readability
+    //
+    // this could be templated rather than hardcoding double, but the actual
+    // bindings must refer to instantiated versions anyway (i.e., overloaded
+    // for each template instantiation) -- and double is enough for me
+    using Model                  = storm::models::sparse::Model<double>;
+    using BitVector              = storm::storage::BitVector;
+    using Matrix                 = storm::storage::SparseMatrix<double>;
+    using MatrixFormat           = storm::utility::ksp::MatrixFormat;
+    using Path                   = storm::utility::ksp::Path<double>;
+    using ShortestPathsGenerator = storm::utility::ksp::ShortestPathsGenerator<double>;
+    using state_t                = storm::utility::ksp::state_t;
+    using StateProbMap           = std::unordered_map<state_t, double>;
+
+    py::class_<Path>(m, "Path")
+        // overload constructor rather than dealing with boost::optional
+        .def("__init__", [](Path &instance, state_t preNode, unsigned long preK, double distance) {
+                new (&instance) Path { boost::optional<state_t>(preNode), preK, distance };
+            }, "predecessorNode"_a, "predecessorK"_a, "distance"_a)
+
+        .def("__init__", [](Path &instance, unsigned long preK, double distance) {
+                new (&instance) Path { boost::none, preK, distance };
+            }, "predecessorK"_a, "distance"_a)
+
+        .def(py::self == py::self, "Compares predecessor node and index, ignoring distance")
+
+        .def("__repr__", [](Path const& p) {
+                std::ostringstream oss;
+                oss << "<Path with predecessorNode: '" << ((p.predecessorNode) ? std::to_string(p.predecessorNode.get()) : "None");
+                oss << "' predecessorK: '" << p.predecessorK << "' distance: '" << p.distance << "'>";
+                return oss.str();
+            })
+
+        .def_readwrite("predecessorNode", &Path::predecessorNode) // TODO (un-)wrap boost::optional so it's usable
+        .def_readwrite("predecessorK", &Path::predecessorK)
+        .def_readwrite("distance", &Path::distance)
+    ;
+
+    py::enum_<MatrixFormat>(m, "MatrixFormat")
+        .value("Straight", MatrixFormat::straight)
+        .value("I_Minus_P", MatrixFormat::iMinusP)
+    ;
+
+    py::class_<ShortestPathsGenerator>(m, "ShortestPathsGenerator")
+        .def(py::init<Model const&, BitVector>(), "model"_a, "target_bitvector"_a)
+        .def(py::init<Model const&, state_t>(), "model"_a, "target_state"_a)
+        .def(py::init<Model const&, std::vector<state_t> const&>(), "model"_a, "target_state_list"_a)
+        .def(py::init<Model const&, std::string>(), "model"_a, "target_label"_a)
+        .def(py::init<Matrix const&, std::vector<double> const&, BitVector const&, MatrixFormat>(), "transition_matrix"_a, "target_prob_vector"_a, "initial_states"_a, "matrix_format"_a)
+        .def(py::init<Matrix const&, StateProbMap const&, BitVector const&, MatrixFormat>(), "transition_matrix"_a, "target_prob_map"_a, "initial_states"_a, "matrix_format"_a)
+
+        .def("get_distance", &ShortestPathsGenerator::getDistance, "k"_a)
+        .def("get_states", &ShortestPathsGenerator::getStates, "k"_a)
+        .def("get_path_as_list", &ShortestPathsGenerator::getPathAsList, "k"_a)
+    ;
+}

src/utility/shortestPaths.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_UTILITY_SHORTESTPATHS_H_
+#define PYTHON_UTILITY_SHORTESTPATHS_H_
+
+#include "src/common.h"
+
+void define_ksp(py::module& m);
+
+#endif /* PYTHON_UTILITY_SHORTESTPATHS_H_ */

tests/utility/test_shortestpaths.py

@@ -0,0 +1,145 @@
+import stormpy
+import stormpy.logic
+from stormpy.storage import BitVector
+from stormpy.utility import ShortestPathsGenerator
+from stormpy.utility import MatrixFormat
+from helpers.helper import get_example_path
+
+import pytest
+import math
+
+
+# this is admittedly slightly overengineered
+
+class ModelWithKnownShortestPaths:
+    """Knuth's die model with reference kSP methods"""
+    def __init__(self):
+        self.target_label = "one"
+
+        program_path = get_example_path("dtmc", "die.pm")
+        raw_formula = "P=? [ F \"" + self.target_label + "\" ]"
+        program = stormpy.parse_prism_program(program_path)
+        formulas = stormpy.parse_formulas_for_prism_program(raw_formula, program)
+
+        self.model = stormpy.build_model(program, formulas[0])
+
+    def probability(self, k):
+        return (1/2)**((2 * k) + 1)
+
+    def state_set(self, k):
+        return BitVector(self.model.nr_states, [0, 1, 3, 7])
+
+    def path(self, k):
+        path = [0] + k * [1, 3] + [7]
+        return list(reversed(path))  # SPG returns traversal from back
+
+
+@pytest.fixture(scope="module", params=[1, 2, 3, 3000, 42])
+def index(request):
+    return request.param
+
+
+@pytest.fixture(scope="module")
+def model_with_known_shortest_paths():
+    return ModelWithKnownShortestPaths()
+
+
+@pytest.fixture(scope="module")
+def model(model_with_known_shortest_paths):
+    return model_with_known_shortest_paths.model
+
+
+@pytest.fixture(scope="module")
+def expected_distance(model_with_known_shortest_paths):
+    return model_with_known_shortest_paths.probability
+
+
+@pytest.fixture(scope="module")
+def expected_state_set(model_with_known_shortest_paths):
+    return model_with_known_shortest_paths.state_set
+
+
+@pytest.fixture(scope="module")
+def expected_path(model_with_known_shortest_paths):
+    return model_with_known_shortest_paths.path
+
+
+@pytest.fixture(scope="module")
+def target_label(model_with_known_shortest_paths):
+    return model_with_known_shortest_paths.target_label
+
+
+@pytest.fixture
+def state(model):
+    some_state = 7
+    assert model.nr_states > some_state, "test model too small"
+    return some_state
+
+
+@pytest.fixture
+def state_list(model):
+    some_state_list = [4, 5, 7]
+    assert model.nr_states > max(some_state_list), "test model too small"
+    return some_state_list
+
+
+@pytest.fixture
+def state_bitvector(model, state_list):
+    return BitVector(length=model.nr_states, set_entries=state_list)
+
+
+@pytest.fixture
+def transition_matrix(model):
+    return model.transition_matrix
+
+
+@pytest.fixture
+def target_prob_map(model, state_list):
+    return {i: (1.0 if i in state_list else 0.0) for i in range(model.nr_states)}
+
+
+@pytest.fixture
+def target_prob_list(target_prob_map):
+    return [target_prob_map[i] for i in range(max(target_prob_map.keys()))]
+
+
+@pytest.fixture
+def initial_states(model):
+    return BitVector(model.nr_states, model.initial_states)
+
+
+@pytest.fixture
+def matrix_format():
+    return MatrixFormat.Straight
+
+
+class TestShortestPaths:
+    def test_spg_ctor_bitvector_target(self, model, state_bitvector):
+        _ = ShortestPathsGenerator(model, state_bitvector)
+
+    def test_spg_ctor_single_state_target(self, model, state):
+        _ = ShortestPathsGenerator(model, state)
+
+    def test_spg_ctor_state_list_target(self, model, state_list):
+        _ = ShortestPathsGenerator(model, state_list)
+
+    def test_spg_ctor_label_target(self, model, target_label):
+        _ = ShortestPathsGenerator(model, target_label)
+
+    def test_spg_ctor_matrix_vector(self, transition_matrix, target_prob_list, initial_states, matrix_format):
+        _ = ShortestPathsGenerator(transition_matrix, target_prob_list, initial_states, matrix_format)
+
+    def test_spg_ctor_matrix_map(self, transition_matrix, target_prob_map, initial_states, matrix_format):
+        _ = ShortestPathsGenerator(transition_matrix, target_prob_map, initial_states, matrix_format)
+
+    def test_spg_distance(self, model, target_label, index, expected_distance):
+        spg = ShortestPathsGenerator(model, target_label)
+        assert math.isclose(spg.get_distance(index), expected_distance(index))
+
+    def test_spg_state_set(self, model, target_label, index, expected_state_set):
+        spg = ShortestPathsGenerator(model, target_label)
+        assert spg.get_states(index) == expected_state_set(index)
+
+    def test_spg_state_list(self, model, target_label, index, expected_path):
+        spg = ShortestPathsGenerator(model, target_label)
+        assert spg.get_path_as_list(index) == expected_path(index)