diff --git a/CMakeLists.txt b/CMakeLists.txt index 24e30ce..fd9bf4f 100644 --- a/CMakeLists.txt +++ b/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) + diff --git a/lib/stormpy/utility/__init__.py b/lib/stormpy/utility/__init__.py new file mode 100644 index 0000000..bdc2591 --- /dev/null +++ b/lib/stormpy/utility/__init__.py @@ -0,0 +1,2 @@ +from . import utility +from .utility import * \ No newline at end of file diff --git a/setup.py b/setup.py index 9664512..08b97fa 100755 --- a/setup.py +++ b/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'], diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9882d8a..e898052 100644 --- a/src/CMakeLists.txt +++ b/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}) diff --git a/src/common.h b/src/common.h index e81b417..6be9148 100644 --- a/src/common.h +++ b/src/common.h @@ -13,6 +13,7 @@ #include namespace py = pybind11; +using namespace pybind11::literals; #if PY_MAJOR_VERSION >= 3 #define PY_DIV "__truediv__" diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 835f1e7..221cbbe 100644 --- a/src/mod_storage.cpp +++ b/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(); diff --git a/src/mod_utility.cpp b/src/mod_utility.cpp new file mode 100644 index 0000000..f222c8f --- /dev/null +++ b/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(); +} diff --git a/src/storage/bitvector.cpp b/src/storage/bitvector.cpp new file mode 100644 index 0000000..dc24960 --- /dev/null +++ b/src/storage/bitvector.cpp @@ -0,0 +1,39 @@ +#include "bitvector.h" +#include "storm/storage/BitVector.h" + +#include + +void define_bitvector(py::module& m) { + using BitVector = storm::storage::BitVector; + + py::class_(m, "BitVector") + .def(py::init<>()) + .def(py::init(), "other"_a) + .def(py::init(), "length"_a) + .def(py::init(), "length"_a, "init"_a) + .def(py::init>(), "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 + ; + +} diff --git a/src/storage/bitvector.h b/src/storage/bitvector.h new file mode 100644 index 0000000..9c548da --- /dev/null +++ b/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_ */ diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp new file mode 100644 index 0000000..f0817ca --- /dev/null +++ b/src/utility/shortestPaths.cpp @@ -0,0 +1,66 @@ +#include "shortestPaths.h" +#include "storm/utility/shortestPaths.h" + +#include +#include + +#include + +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; + using BitVector = storm::storage::BitVector; + using Matrix = storm::storage::SparseMatrix; + using MatrixFormat = storm::utility::ksp::MatrixFormat; + using Path = storm::utility::ksp::Path; + using ShortestPathsGenerator = storm::utility::ksp::ShortestPathsGenerator; + using state_t = storm::utility::ksp::state_t; + using StateProbMap = std::unordered_map; + + py::class_(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(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 << ""; + 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_(m, "MatrixFormat") + .value("Straight", MatrixFormat::straight) + .value("I_Minus_P", MatrixFormat::iMinusP) + ; + + py::class_(m, "ShortestPathsGenerator") + .def(py::init(), "model"_a, "target_bitvector"_a) + .def(py::init(), "model"_a, "target_state"_a) + .def(py::init const&>(), "model"_a, "target_state_list"_a) + .def(py::init(), "model"_a, "target_label"_a) + .def(py::init const&, BitVector const&, MatrixFormat>(), "transition_matrix"_a, "target_prob_vector"_a, "initial_states"_a, "matrix_format"_a) + .def(py::init(), "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) + ; +} \ No newline at end of file diff --git a/src/utility/shortestPaths.h b/src/utility/shortestPaths.h new file mode 100644 index 0000000..5cc0a97 --- /dev/null +++ b/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_ */ diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py new file mode 100644 index 0000000..45f4d96 --- /dev/null +++ b/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)