diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 8a465e3..ba53955 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -4,7 +4,7 @@ #include "storage/dd.h" #include "storage/model.h" #include "storage/matrix.h" -#include "storage/modelcomponents.h" +#include "storage/model_components.h" #include "storage/distribution.h" #include "storage/scheduler.h" #include "storage/prism.h" @@ -42,5 +42,5 @@ PYBIND11_MODULE(storage, m) { define_expressions(m); define_scheduler(m, "Double"); define_distribution(m, "Double"); - define_sparse_modelcomponents(m); + define_sparse_model_components(m); } diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 9be8f96..a6a2db3 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -221,11 +221,14 @@ void define_sparse_model(py::module& m) { py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) .def(py::init>(), py::arg("other_model")) .def(py::init const&>(), py::arg("components")) //todo tests + .def_property_readonly("exit_rates", [](SparseCtmc const& ctmc) { return ctmc.getExitRateVector(); }) //todo new: tests .def("__str__", &getModelInfoPrinter) ; py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) .def(py::init>(), py::arg("other_model")) - .def(py::init const&>(), py::arg("components")) //todo tests + .def(py::init const&>(), py::arg("components")) // todo tests + .def_property_readonly("exit_rates", [](SparseMarkovAutomaton const& ma) { return ma.getExitRates(); }) //todo new: tests + .def_property_readonly("markovian_states", [](SparseMarkovAutomaton const& ma) { return ma.getMarkovianStates(); }) //todo new: tests .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton const& ma) { return ma.getNondeterministicChoiceIndices(); }) .def("apply_scheduler", [](SparseMarkovAutomaton const& ma, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("__str__", &getModelInfoPrinter) diff --git a/src/storage/modelcomponents.cpp b/src/storage/model_components.cpp similarity index 96% rename from src/storage/modelcomponents.cpp rename to src/storage/model_components.cpp index 2adbcb6..9769e17 100644 --- a/src/storage/modelcomponents.cpp +++ b/src/storage/model_components.cpp @@ -1,4 +1,4 @@ -#include "modelcomponents.h" +#include "model_components.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/symbolic/StandardRewardModel.h" @@ -23,7 +23,7 @@ template using SparseModelComponents = storm::storage::spars // Parametric models, Valuetype: todo -void define_sparse_modelcomponents(py::module& m) { +void define_sparse_model_components(py::module& m) { // shared_ptr? todo py::class_, std::shared_ptr>>(m, "SparseModelComponents", "ModelComponents description..") //todo @@ -49,7 +49,7 @@ void define_sparse_modelcomponents(py::module& m) { // Continuous time specific components (CTMCs, Markov Automata): .def_readwrite("rate_transitions", &SparseModelComponents::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates") - .def_readwrite("exit_Rates", &SparseModelComponents::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.") + .def_readwrite("exit_rates", &SparseModelComponents::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.") .def_readwrite("markovian_states", &SparseModelComponents::markovianStates, "A vector that stores which states are markovian (only for Markov Automata)") // Stochastic two player game specific components: diff --git a/src/storage/modelcomponents.h b/src/storage/model_components.h similarity index 53% rename from src/storage/modelcomponents.h rename to src/storage/model_components.h index 50b053f..14117a7 100644 --- a/src/storage/modelcomponents.h +++ b/src/storage/model_components.h @@ -3,6 +3,6 @@ #include "common.h" -void define_sparse_modelcomponents(py::module& m); +void define_sparse_model_components(py::module& m); #endif /* PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H */ \ No newline at end of file diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py new file mode 100644 index 0000000..cebeaaf --- /dev/null +++ b/tests/storage/test_model_components.py @@ -0,0 +1,66 @@ +import stormpy +import stormpy.logic +from helpers.helper import get_example_path +import pytest + + +class TestSparseModelComponents: + def test_init_default(self): + components = stormpy.SparseModelComponents() + + assert components.state_labeling.get_labels() == set() + assert components.reward_models == {} + assert components.transition_matrix.nr_rows == 0 + assert components.transition_matrix.nr_columns == 0 + assert components.markovian_states is None + assert components.player1_matrix is None + assert not components.rate_transitions + + def test_build_dtmc_from_model_components(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + options = stormpy.BuilderOptions(True, True) + options.set_build_with_choice_origins() + options.set_build_state_valuations() + options.set_build_all_labels() + model = stormpy.build_sparse_model_with_options(program, options) + + components = stormpy.SparseModelComponents(transition_matrix=model.transition_matrix, + state_labeling=model.labeling, + reward_models=model.reward_models) + components.choice_origins = model.choice_origins + components.state_valuations = model.state_valuations + + dtmc = stormpy.storage.SparseDtmc(components) + + assert type(dtmc) is stormpy.SparseDtmc + assert not dtmc.supports_parameters + + # test transition matrix + assert dtmc.nr_choices == 13 + assert dtmc.nr_states == 13 + assert dtmc.nr_transitions == 20 + assert dtmc.transition_matrix.nr_entries == 20 + assert dtmc.transition_matrix.nr_entries == model.nr_transitions + for e in dtmc.transition_matrix: + assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) + for state in dtmc.states: + assert len(state.actions) <= 1 + + # test state_labeling + assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'} + + # test reward_models + assert len(model.reward_models) == 1 + assert not model.reward_models["coin_flips"].has_state_rewards + assert model.reward_models["coin_flips"].has_state_action_rewards + for reward in model.reward_models["coin_flips"].state_action_rewards: + assert reward == 1.0 or reward == 0.0 + assert not model.reward_models["coin_flips"].has_transition_rewards + + # choice_labeling + assert not dtmc.has_choice_labeling() + # state_valuations + assert dtmc.has_state_valuations() + # choice_origins + assert dtmc.has_choice_origins() + assert dtmc.choice_origins is components.choice_origins # todo correct? diff --git a/tests/storage/test_modelcomponents.py b/tests/storage/test_modelcomponents.py deleted file mode 100644 index 2334016..0000000 --- a/tests/storage/test_modelcomponents.py +++ /dev/null @@ -1,65 +0,0 @@ -import stormpy -import stormpy.logic -from helpers.helper import get_example_path -import pytest - - -class TestSparseModel: - def test_init_default(self): - components = stormpy.SparseModelComponents() - - assert components.state_labeling.get_labels() == set() - assert components.reward_models == {} - assert components.transition_matrix.nr_rows == 0 - assert components.transition_matrix.nr_columns == 0 - assert components.markovian_states is None - assert components.player1_matrix is None - assert not components.rate_transitions - - # def test_init(self): - # todo Build simple transition matrix etc - # transition_matrix = - - - def test_dtmc_modelcomponents(self): - program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - model = stormpy.build_model(program) - - components = stormpy.SparseModelComponents(transition_matrix=model.transition_matrix, - state_labeling=model.labeling, - reward_models=model.reward_models) - - dtmc = stormpy.storage.SparseDtmc(components) - - assert dtmc.model_type == stormpy.ModelType.DTMC - assert dtmc.initial_states == [0] - assert dtmc.nr_states == 13 - for state in dtmc.states: - assert len(state.actions) <= 1 - assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'} - assert dtmc.nr_transitions == 20 - assert len(dtmc.reward_models) == 1 - assert not dtmc.reward_models["coin_flips"].has_state_rewards - assert dtmc.reward_models["coin_flips"].has_state_action_rewards - for reward in dtmc.reward_models["coin_flips"].state_action_rewards: - assert reward == 1.0 or reward == 0.0 - assert not dtmc.reward_models["coin_flips"].has_transition_rewards - assert not dtmc.supports_parameters - - - def test_pmdp_modelcomponents(self): - program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) - model = stormpy.build_parametric_model(program) - - - def test_ma_modelcomponents(self): - program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) - formulas = stormpy.parse_properties_for_prism_program("Pmax=? [ F<=2 s=2 ]", program) - model = stormpy.build_model(program, formulas) - #todo create mc - - assert model.nr_states == 4 - assert model.nr_transitions == 7 - assert model.model_type == stormpy.ModelType.MA - assert not model.supports_parameters - assert type(model) is stormpy.SparseMA