From 7bc01687755d1a9ff5d52b229ffa56d29398e676 Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 26 Jun 2020 11:28:38 +0200 Subject: [PATCH] completed dtmc tests --- .../examples/files/pomdp/3x3grid.prism | 59 +++++++++++++++++++ src/storage/labeling.cpp | 14 +++-- src/storage/model.cpp | 6 +- tests/storage/test_model_components.py | 49 +++++++++------ 4 files changed, 104 insertions(+), 24 deletions(-) create mode 100644 lib/stormpy/examples/files/pomdp/3x3grid.prism diff --git a/lib/stormpy/examples/files/pomdp/3x3grid.prism b/lib/stormpy/examples/files/pomdp/3x3grid.prism new file mode 100644 index 0000000..a332fa3 --- /dev/null +++ b/lib/stormpy/examples/files/pomdp/3x3grid.prism @@ -0,0 +1,59 @@ + + +// 3x3 grid +// based on Littman, Cassandra and Kaelbling +// Learning policies for partially observable environments: Scaling up +// Technical Report CS, Brown University + +pomdp + + + +// only the target is observable which is in the south east corner +observables + o +endobservables + +module grid + + x : [0..2]; // x coordinate + y : [0..2]; // y coordinate + o : [0..2]; // observables + // 0 - initial observation + // 1 - in the grid (not target) + // 2 - observe target + + // initially randomly placed within the grid (not at the target) + [] o=0 -> 1/8 : (o'=1) & (x'=0) & (y'=0) + + 1/8 : (o'=1) & (x'=0) & (y'=1) + + 1/8 : (o'=1) & (x'=0) & (y'=2) + + 1/8 : (o'=1) & (x'=1) & (y'=0) + + 1/8 : (o'=1) & (x'=1) & (y'=1) + + 1/8 : (o'=1) & (x'=1) & (y'=2) + // + 1/8 : (o'=1) & (x'=2) & (y'=0) the target + + 1/8 : (o'=1) & (x'=2) & (y'=1) + + 1/8 : (o'=1) & (x'=2) & (y'=2); + + // move around the grid + [east] o=1 & !(x=1 & y=0) -> (x'=min(x+1,2)); // not reached target + [east] o=1 & x=1 & y=0 -> (x'=min(x+1,2)) & (o'=2); + [west] o=1 -> (x'=max(x-1,0)); // not reached target + [north] o=1 -> (y'=min(y+1,2)); // reached target + [south] o=1 & !(x=2 & y=1) -> (y'=max(y-1,0)); // not reached target + [south] o=1 & x=2 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target + + // reached target + [done] o=2 -> true; + +endmodule + +// reward structure for number of steps to reach the target +rewards + [east] true : 1; + [west] true : 1; + [north] true : 1; + [south] true : 1; +endrewards + +// target observation +label "goal" = o=2; diff --git a/src/storage/labeling.cpp b/src/storage/labeling.cpp index 2ee7fc1..fd60c84 100644 --- a/src/storage/labeling.cpp +++ b/src/storage/labeling.cpp @@ -21,20 +21,26 @@ void define_labeling(py::module& m) { // StateLabeling py::class_>(m, "StateLabeling", "Labeling for states", labeling) - .def(py::init(), "state_count"_a) // todo tests + .def(py::init(), "state_count"_a) .def("get_labels_of_state", &storm::models::sparse::StateLabeling::getLabelsOfState, "Get labels of given state", py::arg("state")) .def("add_label_to_state", &storm::models::sparse::StateLabeling::addLabelToState, "Add label to state", py::arg("label"), py::arg("state")) .def("has_state_label", &storm::models::sparse::StateLabeling::getStateHasLabel, "Check if the given state has the given label", py::arg("label"), py::arg("state")) .def("get_states", &storm::models::sparse::StateLabeling::getStates, "Get all states which have the given label", py::arg("label")) .def("set_states", [](storm::models::sparse::StateLabeling& labeling, std::string const& label, storm::storage::BitVector const& states) { labeling.setStates(label, states); - }, "Set all states which have the given label", py::arg("label"), py::arg("states")) + }, "Add a label to the given states", py::arg("label"), py::arg("states")) .def("__str__", &streamToString) ; py::class_(m, "ChoiceLabeling", "Labeling for choices", labeling) - .def(py::init(), "choice_count"_a) // todo tests - .def("get_labels_of_choice", &storm::models::sparse::ChoiceLabeling::getLabelsOfChoice, py::arg("choice"), "get labels of a choice") + .def(py::init(), "choice_count"_a) + .def("get_labels_of_choice", &storm::models::sparse::ChoiceLabeling::getLabelsOfChoice, py::arg("choice"), "Get labels of the given choice") + .def("add_label_to_choice", &storm::models::sparse::ChoiceLabeling::addLabelToChoice, "Adds a label to a given choice", py::arg("label"), py::arg("state")) + .def("get_choices", &storm::models::sparse::ChoiceLabeling::getChoices, py::arg("label"), "Get all choices which have the given label") + .def("set_choices", [](storm::models::sparse::ChoiceLabeling& labeling, std::string const& label, storm::storage::BitVector const& choices) { + labeling.setChoices(label, choices); + }, "Add a label to a the given choices", py::arg("label"), py::arg("choices")) + .def("__str__", &streamToString) ; } diff --git a/src/storage/model.cpp b/src/storage/model.cpp index faae858..ee97b69 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -221,14 +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")) - .def_property_readonly("exit_rates", [](SparseCtmc const& ctmc) { return ctmc.getExitRateVector(); }) //todo new: tests + .def_property_readonly("exit_rates", [](SparseCtmc const& ctmc) { return ctmc.getExitRateVector(); }) .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")) .def_property_readonly("exit_rates", [](SparseMarkovAutomaton const& ma) { return ma.getExitRates(); }) - .def_property_readonly("markovian_states", [](SparseMarkovAutomaton const& ma) { return ma.getMarkovianStates(); }) //todo new: tests + .def_property_readonly("markovian_states", [](SparseMarkovAutomaton const& ma) { return ma.getMarkovianStates(); }) .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) @@ -239,7 +239,7 @@ void define_sparse_model(py::module& m) { py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") .def(py::init> const&, boost::optional> const&, boost::optional> const&>(), py::arg("optional_state_reward_vector") = boost::none, - py::arg("optional_state_action_reward_vector") = boost::none, py::arg("optional_transition_reward_matrix") = boost::none) // todo tests + py::arg("optional_state_action_reward_vector") = boost::none, py::arg("optional_transition_reward_matrix") = boost::none) .def_property_readonly("has_state_rewards", &SparseRewardModel::hasStateRewards) .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index 35621e1..f890afd 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -16,8 +16,14 @@ class TestSparseModelComponents: assert components.player1_matrix is None assert not components.rate_transitions + # todo: ctmc + # todo: ma + # todo mdp + # todo pomdp? + def test_build_dtmc_from_model_components(self): nr_states = 13 + nr_choices = 13 # TransitionMatrix builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, @@ -45,8 +51,8 @@ class TestSparseModelComponents: # StateLabeling state_labeling = stormpy.storage.StateLabeling(nr_states) - labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} - for label in labels: + state_labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + for label in state_labels: state_labeling.add_label(label) # Add label to one state state_labeling.add_label_to_state('init', 0) @@ -65,8 +71,8 @@ class TestSparseModelComponents: action_reward = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0] reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) - # todo state valuations - manager = stormpy.ExpressionManager() # todo correct? + # StateValuations + manager = stormpy.ExpressionManager() var_s = manager.create_integer_variable(name='s') var_d = manager.create_integer_variable(name='d') v_builder = stormpy.StateValuationsBuilder() @@ -74,11 +80,10 @@ class TestSparseModelComponents: v_builder.add_variable(var_s) v_builder.add_variable(var_d) - for s in range(7): - v_builder.add_state(state=s,integer_values=[s,0]) - for s in range(7,13): - v_builder.add_state(state=s,integer_values=[7,s-6]) + v_builder.add_state(state=s, integer_values=[s, 0]) + for s in range(7, 13): + v_builder.add_state(state=s, integer_values=[7, s - 6]) state_valuations = v_builder.build(13) @@ -88,8 +93,7 @@ class TestSparseModelComponents: id_to_command_set_mapping = [stormpy.FlatSet() for _ in range(9)] for i in range(1, 8): # 0: no origin id_to_command_set_mapping[i].insert(i - 1) - for i in range(8, 14): - id_to_command_set_mapping[8].insert(7) + id_to_command_set_mapping[8].insert(7) # choice_origins = stormpy.PrismChoiceOrigins(prism_program, index_to_identifier_mapping, id_to_command_set_mapping) @@ -106,8 +110,8 @@ class TestSparseModelComponents: assert not dtmc.supports_parameters # test transition matrix - assert dtmc.nr_choices == 13 - assert dtmc.nr_states == 13 + assert dtmc.nr_choices == nr_choices + assert dtmc.nr_states == nr_states assert dtmc.nr_transitions == 20 assert dtmc.transition_matrix.nr_entries == dtmc.nr_transitions for e in dtmc.transition_matrix: @@ -126,10 +130,21 @@ class TestSparseModelComponents: assert reward == 1.0 or reward == 0.0 assert not dtmc.reward_models["coin_flips"].has_transition_rewards - # choice_labeling + # test choice_labeling assert not dtmc.has_choice_labeling() - # todo state_valuations - assert dtmc.has_state_valuations() # todo more tests - # todo choice_origins - assert dtmc.has_choice_origins() #todo more tests + + # test state_valuations + assert dtmc.has_state_valuations() + assert dtmc.state_valuations + value_s = [None] * nr_states + value_d = [None] * nr_states + for s in range(0, dtmc.nr_states): + value_s[s] = dtmc.state_valuations.get_integer_value(s, var_s) + value_d[s] = dtmc.state_valuations.get_integer_value(s, var_d) + assert value_s == [0, 1, 2, 3, 4, 5, 6, 7, 7, 7, 7, 7, 7] + assert value_d == [0, 0, 0, 0, 0, 0, 0, 1, 2, 3, 4, 5, 6] + + # todo choice_origins more tests + assert dtmc.has_choice_origins() assert dtmc.choice_origins is components.choice_origins + assert dtmc.choice_origins.get_number_of_identifiers() == 9