From 4f3c51fc4f37d5ef44231070165f54c9a8dc3819 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Wed, 14 Dec 2016 21:47:16 +0100 Subject: [PATCH 1/9] add empty module --- CMakeLists.txt | 6 ++++++ lib/stormpy/utility/__init__.py | 2 ++ setup.py | 4 ++-- src/CMakeLists.txt | 10 ++++++++++ 4 files changed, 20 insertions(+), 2 deletions(-) create mode 100644 lib/stormpy/utility/__init__.py 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}) From 77dff27866a769b91611d06dbacf9b2ad0a67906 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Thu, 15 Dec 2016 00:09:40 +0100 Subject: [PATCH 2/9] Path (from storm::utility::ksp) pybind proof of concept this stuff is not fun. --- src/mod_utility.cpp | 9 ++++++ src/utility/shortestPaths.cpp | 61 +++++++++++++++++++++++++++++++++++ src/utility/shortestPaths.h | 8 +++++ 3 files changed, 78 insertions(+) create mode 100644 src/mod_utility.cpp create mode 100644 src/utility/shortestPaths.cpp create mode 100644 src/utility/shortestPaths.h 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/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp new file mode 100644 index 0000000..13b8c34 --- /dev/null +++ b/src/utility/shortestPaths.cpp @@ -0,0 +1,61 @@ +#include "shortestPaths.h" +#include "storm/utility/shortestPaths.h" + +#include + +using namespace pybind11::literals; + +void define_ksp(py::module& m) { + + using Path = storm::utility::ksp::Path; + using state_t = storm::utility::ksp::state_t; + + // (k-shortest) Path + py::class_(m, "Path") + // Fuck all this. FIXME + + //.def(py::init, unsigned long, double>()) // does not work (because it's an aggregate initialized struct?) + + // this may or may not be working (i.e., initializing with the values as expected) + // https://pybind11.readthedocs.io/en/latest/advanced/classes.html#custom-constructors + .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) + + // this actually seemed to work, once!, but not anymore + .def(py::self == py::self) + + .def("__repr__", + [](Path const& a) { + // shit this is ugly. but it's a proof of concept -- at least it works + std::string str = ">(m, "ShortestPathsGenerator") + ; + */ +} \ 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_ */ From e1472a258d431985197bcceb53ebe85722320837 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 18 Dec 2016 00:01:54 +0100 Subject: [PATCH 3/9] use pybind11::literals namespace --- src/common.h | 1 + src/utility/shortestPaths.cpp | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) 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/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 13b8c34..89caa27 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -3,7 +3,6 @@ #include -using namespace pybind11::literals; void define_ksp(py::module& m) { From d955bcb1c2208507bc5aa6621d810478658105da Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 18 Dec 2016 00:02:43 +0100 Subject: [PATCH 4/9] add BitVector binding --- src/mod_storage.cpp | 2 ++ src/storage/bitvector.cpp | 39 +++++++++++++++++++++++++++++++++++++++ src/storage/bitvector.h | 8 ++++++++ 3 files changed, 49 insertions(+) create mode 100644 src/storage/bitvector.cpp create mode 100644 src/storage/bitvector.h 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/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_ */ From 6f347ee3549aa791ee9134f88bf4534c0165b809 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 18 Dec 2016 00:37:05 +0100 Subject: [PATCH 5/9] add ShortestPathsGenerator binding (ctors, TODO: rest) --- src/utility/shortestPaths.cpp | 60 ++++++++++++----------------- tests/utility/test_shortestpaths.py | 57 +++++++++++++++++++++++++++ 2 files changed, 81 insertions(+), 36 deletions(-) create mode 100644 tests/utility/test_shortestpaths.py diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 89caa27..4313969 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -1,22 +1,22 @@ #include "shortestPaths.h" #include "storm/utility/shortestPaths.h" +#include #include +#include void define_ksp(py::module& m) { - using Path = storm::utility::ksp::Path; - using state_t = storm::utility::ksp::state_t; + // long types shortened for readability + using Path = storm::utility::ksp::Path; + using state_t = storm::utility::ksp::state_t; + using ShortestPathsGenerator = storm::utility::ksp::ShortestPathsGenerator; + using Model = storm::models::sparse::Model; + using BitVector = storm::storage::BitVector; - // (k-shortest) Path py::class_(m, "Path") - // Fuck all this. FIXME - - //.def(py::init, unsigned long, double>()) // does not work (because it's an aggregate initialized struct?) - - // this may or may not be working (i.e., initializing with the values as expected) - // https://pybind11.readthedocs.io/en/latest/advanced/classes.html#custom-constructors + // 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) @@ -25,36 +25,24 @@ void define_ksp(py::module& m) { new (&instance) Path { boost::none, preK, distance }; }, "predecessorK"_a, "distance"_a) - // this actually seemed to work, once!, but not anymore - .def(py::self == py::self) - - .def("__repr__", - [](Path const& a) { - // shit this is ugly. but it's a proof of concept -- at least it works - std::string str = ""; + return oss.str(); }) - .def_readwrite("predecessorNode", &Path::predecessorNode) // does not work (again due to struct??) FIXME + .def_readwrite("predecessorNode", &Path::predecessorNode) // TODO (un-)wrap boost::optional so it's usable .def_readwrite("predecessorK", &Path::predecessorK) .def_readwrite("distance", &Path::distance) - ; - - // TODO continue - /* - // ShortestPathsGenerator - py::class_>(m, "ShortestPathsGenerator") - ; - */ + ; + + 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) + ; } \ No newline at end of file diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py new file mode 100644 index 0000000..102b5fc --- /dev/null +++ b/tests/utility/test_shortestpaths.py @@ -0,0 +1,57 @@ +import stormpy +import stormpy.logic +from stormpy.storage import BitVector +from stormpy.utility import ShortestPathsGenerator +from helpers.helper import get_example_path + +import pytest + + +@pytest.fixture +def test_model(scope="module", program_path=get_example_path("dtmc", "die.pm"), raw_formula="P=? [ F \"one\" ]"): + program = stormpy.parse_prism_program(program_path) + formulas = stormpy.parse_formulas_for_prism_program(raw_formula, program) + test_model = stormpy.build_model(program, formulas[0]) + return test_model + + +@pytest.fixture +def test_state(test_model): + some_state = 7 + assert test_model.nr_states > some_state, "test model too small" + return some_state + + +@pytest.fixture +def test_state_list(test_model): + some_state_list = [4, 5, 7] + assert test_model.nr_states > max(some_state_list), "test model too small" + return some_state_list + + +@pytest.fixture +def test_state_bitvector(test_model, test_state_list): + return BitVector(length=test_model.nr_states, set_entries=test_state_list) + + +@pytest.fixture +def test_label(test_model): + some_label = "one" + assert some_label in test_model.labels, "test model does not contain label '" + some_label + "'" + return some_label + + +class TestShortestPaths: + def test_spg_ctor_bitvector_target(self, test_model, test_state_bitvector): + _ = ShortestPathsGenerator(test_model, test_state_bitvector) + + def test_spg_ctor_single_state_target(self, test_model, test_state): + _ = ShortestPathsGenerator(test_model, test_state) + + def test_spg_ctor_state_list_target(self, test_model, test_state_list): + _ = ShortestPathsGenerator(test_model, test_state_list) + + def test_spg_ctor_label_target(self, test_model, test_label): + _ = ShortestPathsGenerator(test_model, test_label) + + # TODO: add tests that check actual functionality From b85f6ae1dad8173501e7b53b2f5bf4d282a11b21 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 18 Dec 2016 01:05:54 +0100 Subject: [PATCH 6/9] fix KSP test model fixture scope --- tests/utility/test_shortestpaths.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index 102b5fc..217f780 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -7,8 +7,8 @@ from helpers.helper import get_example_path import pytest -@pytest.fixture -def test_model(scope="module", program_path=get_example_path("dtmc", "die.pm"), raw_formula="P=? [ F \"one\" ]"): +@pytest.fixture(scope="module") +def test_model(program_path=get_example_path("dtmc", "die.pm"), raw_formula="P=? [ F \"one\" ]"): program = stormpy.parse_prism_program(program_path) formulas = stormpy.parse_formulas_for_prism_program(raw_formula, program) test_model = stormpy.build_model(program, formulas[0]) From 1dd14e6e80761dec1d984aa67a251c65a50f6dad Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 18 Dec 2016 01:08:40 +0100 Subject: [PATCH 7/9] simplify KSP test fixture names --- tests/utility/test_shortestpaths.py | 38 ++++++++++++++--------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index 217f780..ea01047 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -8,50 +8,50 @@ import pytest @pytest.fixture(scope="module") -def test_model(program_path=get_example_path("dtmc", "die.pm"), raw_formula="P=? [ F \"one\" ]"): +def model(program_path=get_example_path("dtmc", "die.pm"), raw_formula="P=? [ F \"one\" ]"): program = stormpy.parse_prism_program(program_path) formulas = stormpy.parse_formulas_for_prism_program(raw_formula, program) - test_model = stormpy.build_model(program, formulas[0]) - return test_model + return stormpy.build_model(program, formulas[0]) @pytest.fixture -def test_state(test_model): +def state(model): some_state = 7 - assert test_model.nr_states > some_state, "test model too small" + assert model.nr_states > some_state, "test model too small" return some_state @pytest.fixture -def test_state_list(test_model): +def state_list(model): some_state_list = [4, 5, 7] - assert test_model.nr_states > max(some_state_list), "test model too small" + assert model.nr_states > max(some_state_list), "test model too small" return some_state_list @pytest.fixture -def test_state_bitvector(test_model, test_state_list): - return BitVector(length=test_model.nr_states, set_entries=test_state_list) +def state_bitvector(model, state_list): + return BitVector(length=model.nr_states, set_entries=state_list) @pytest.fixture -def test_label(test_model): +def label(model): some_label = "one" - assert some_label in test_model.labels, "test model does not contain label '" + some_label + "'" + assert some_label in model.labels, "test model does not contain label '" + some_label + "'" return some_label class TestShortestPaths: - def test_spg_ctor_bitvector_target(self, test_model, test_state_bitvector): - _ = ShortestPathsGenerator(test_model, test_state_bitvector) + def test_spg_ctor_bitvector_target(self, model, state_bitvector): + _ = ShortestPathsGenerator(model, state_bitvector) - def test_spg_ctor_single_state_target(self, test_model, test_state): - _ = ShortestPathsGenerator(test_model, test_state) + def test_spg_ctor_single_state_target(self, model, state): + _ = ShortestPathsGenerator(model, state) - def test_spg_ctor_state_list_target(self, test_model, test_state_list): - _ = ShortestPathsGenerator(test_model, test_state_list) + def test_spg_ctor_state_list_target(self, model, state_list): + _ = ShortestPathsGenerator(model, state_list) + + def test_spg_ctor_label_target(self, model, label): + _ = ShortestPathsGenerator(model, label) - def test_spg_ctor_label_target(self, test_model, test_label): - _ = ShortestPathsGenerator(test_model, test_label) # TODO: add tests that check actual functionality From 5b782b5ca7c149dfc1e4a6f7fa1c6722921b2d6a Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 18 Dec 2016 01:23:30 +0100 Subject: [PATCH 8/9] add ShortestPathsGenerator matrix/vector ctor bindings --- src/utility/shortestPaths.cpp | 23 ++++++++++++++++++--- tests/utility/test_shortestpaths.py | 31 +++++++++++++++++++++++++++++ 2 files changed, 51 insertions(+), 3 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 4313969..9ff97b4 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -9,11 +9,18 @@ void define_ksp(py::module& m) { // long types shortened for readability - using Path = storm::utility::ksp::Path; - using state_t = storm::utility::ksp::state_t; - using ShortestPathsGenerator = storm::utility::ksp::ShortestPathsGenerator; + // + // 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 @@ -39,10 +46,20 @@ void define_ksp(py::module& m) { .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) + + // ShortestPathsGenerator(Matrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat); + // ShortestPathsGenerator(Matrix const& maybeTransitionMatrix, StateProbMap const& targetProbMap, BitVector const& initialStates, MatrixFormat matrixFormat); ; } \ No newline at end of file diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index ea01047..70451fd 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -2,6 +2,7 @@ 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 @@ -40,6 +41,31 @@ def label(model): return some_label +@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) @@ -53,5 +79,10 @@ class TestShortestPaths: def test_spg_ctor_label_target(self, model, label): _ = ShortestPathsGenerator(model, 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) # TODO: add tests that check actual functionality From 09b2bfcf67a9656b5ef777c2190954b91d94fcac Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Sun, 18 Dec 2016 02:29:13 +0100 Subject: [PATCH 9/9] add ShortestPathsGenerator method binding (and fancy test fixture) --- src/utility/shortestPaths.cpp | 5 +- tests/utility/test_shortestpaths.py | 85 ++++++++++++++++++++++++----- 2 files changed, 74 insertions(+), 16 deletions(-) diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 9ff97b4..f0817ca 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -59,7 +59,8 @@ void define_ksp(py::module& m) { .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) - // ShortestPathsGenerator(Matrix const& transitionMatrix, std::vector const& targetProbVector, BitVector const& initialStates, MatrixFormat matrixFormat); - // ShortestPathsGenerator(Matrix const& maybeTransitionMatrix, StateProbMap const& targetProbMap, BitVector const& initialStates, MatrixFormat matrixFormat); + .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/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index 70451fd..45f4d96 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -6,13 +6,67 @@ 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 model(program_path=get_example_path("dtmc", "die.pm"), raw_formula="P=? [ F \"one\" ]"): - program = stormpy.parse_prism_program(program_path) - formulas = stormpy.parse_formulas_for_prism_program(raw_formula, program) - return stormpy.build_model(program, formulas[0]) +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 @@ -34,13 +88,6 @@ def state_bitvector(model, state_list): return BitVector(length=model.nr_states, set_entries=state_list) -@pytest.fixture -def label(model): - some_label = "one" - assert some_label in model.labels, "test model does not contain label '" + some_label + "'" - return some_label - - @pytest.fixture def transition_matrix(model): return model.transition_matrix @@ -76,8 +123,8 @@ class TestShortestPaths: def test_spg_ctor_state_list_target(self, model, state_list): _ = ShortestPathsGenerator(model, state_list) - def test_spg_ctor_label_target(self, model, label): - _ = ShortestPathsGenerator(model, label) + 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) @@ -85,4 +132,14 @@ class TestShortestPaths: 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) - # TODO: add tests that check actual functionality + 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)