Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ToStateBasedObservationTransformerTest.cpp
Go to the documentation of this file.
1#include <cstdint>
2#include <memory>
3#include <tuple>
4#include <utility>
5#include <vector>
6
7#include "test/storm_gtest.h"
8
9#include "storm-pomdp/transformer/ToStateBasedObservationTransformer.h"
10#include "storm/models/sparse/ChoiceLabeling.h"
11#include "storm/models/sparse/Mdp.h"
12#include "storm/models/sparse/Pomdp.h"
13#include "storm/models/sparse/StandardRewardModel.h"
14#include "storm/models/sparse/StateLabeling.h"
15#include "storm/storage/SparseMatrix.h"
16#include "storm/storage/sparse/ModelComponents.h"
17
18namespace {
19
20std::shared_ptr<storm::models::sparse::Mdp<double>> buildMdp() {
21 storm::storage::SparseMatrixBuilder<double> matrixBuilder(0, 0, 0, false, true);
22 matrixBuilder.newRowGroup(0);
23 matrixBuilder.addNextValue(0, 1, 1.0);
24 matrixBuilder.addNextValue(1, 1, 1.0);
25 matrixBuilder.newRowGroup(2);
26 matrixBuilder.addNextValue(2, 2, 1.0);
27 matrixBuilder.addNextValue(3, 2, 1.0);
28 matrixBuilder.newRowGroup(4);
29 matrixBuilder.addNextValue(4, 2, 1.0);
30
31 storm::models::sparse::StateLabeling labeling(3);
32 labeling.addLabel("init");
33 labeling.addLabelToState("init", 0);
34 storm::storage::sparse::ModelComponents<double> components(matrixBuilder.build(), std::move(labeling));
35 return std::make_shared<storm::models::sparse::Mdp<double>>(std::move(components));
36}
37
38storm::storage::sparse::ModelComponents<double> buildComponentsWithUnreachableState() {
39 storm::storage::SparseMatrixBuilder<double> matrixBuilder(0, 0, 0, false, true);
40 matrixBuilder.newRowGroup(0);
41 matrixBuilder.addNextValue(0, 1, 1.0);
42 matrixBuilder.newRowGroup(1);
43 matrixBuilder.addNextValue(1, 1, 1.0);
44 matrixBuilder.newRowGroup(2);
45 matrixBuilder.addNextValue(2, 1, 1.0);
46
47 storm::models::sparse::StateLabeling labeling(3);
48 labeling.addLabel("init");
49 labeling.addLabelToState("init", 0);
50 labeling.addLabel("isolated");
51 labeling.addLabelToState("isolated", 2);
52 storm::storage::sparse::ModelComponents<double> components(matrixBuilder.build(3, 3, 3), std::move(labeling));
53 components.rewardModels.emplace("r",
54 storm::models::sparse::StandardRewardModel<double>(std::vector<double>{0.0, 0.0, 7.0}, std::vector<double>{1.0, 1.0, 3.0}));
55 return components;
56}
57
58} // namespace
59
60TEST(ToStateBasedObservationTransformer, PassesLocalActionIndicesToCallback) {
61 auto const mdp = buildMdp();
62 std::vector<std::pair<uint64_t, uint64_t>> observedStateActions;
63
64 auto const result = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(
65 *mdp,
66 [&observedStateActions](uint64_t state, uint64_t action, uint64_t) {
67 observedStateActions.emplace_back(state, action);
68 return 0;
69 },
70 0);
71
72 EXPECT_NE(nullptr, result);
73 EXPECT_EQ((std::vector<std::pair<uint64_t, uint64_t>>{{0, 0}, {0, 1}, {1, 0}, {1, 1}, {2, 0}}), observedStateActions);
74}
75
76TEST(ToStateBasedObservationTransformer, KeepsNonInitialStateWithoutIncomingTransitions) {
77 auto const mdp = std::make_shared<storm::models::sparse::Mdp<double>>(buildComponentsWithUnreachableState());
78
79 auto const result =
80 storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(*mdp, [](uint64_t, uint64_t, uint64_t) { return 1; }, 0, false);
81
82 ASSERT_NE(nullptr, result);
83 EXPECT_EQ(3u, result->getNumberOfStates());
84 EXPECT_EQ(3u, result->getNumberOfChoices());
85 EXPECT_EQ((std::vector<uint32_t>{0, 1, 0}), result->getObservations());
86 EXPECT_TRUE(result->getStateLabeling().getStates("isolated").get(2));
87 EXPECT_FALSE(result->getInitialStates().get(2));
88 EXPECT_EQ(1u, result->getTransitionMatrix().getRowGroupSize(2));
89 EXPECT_EQ(1u, result->getTransitionMatrix().getRow(2).begin()->getColumn());
90 EXPECT_EQ(7.0, result->getRewardModel("r").getStateReward(2));
91 EXPECT_EQ(3.0, result->getRewardModel("r").getStateActionReward(2));
92}
93
94TEST(ToStateBasedObservationTransformer, RewardAwareTransformationKeepsUnreachableState) {
95 auto components = buildComponentsWithUnreachableState();
96 components.observabilityClasses = std::vector<uint32_t>{0, 1, 2};
97 auto const pomdp = std::make_shared<storm::models::sparse::Pomdp<double>>(std::move(components));
98
99 auto const result = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transformRewardAware(*pomdp, {"r"}, false);
100
101 ASSERT_NE(nullptr, result);
102 EXPECT_EQ(4u, result->getNumberOfStates());
103 EXPECT_EQ((std::vector<uint32_t>{0, 3, 4, 0}), result->getObservations());
104 EXPECT_TRUE(result->getStateLabeling().getStates("isolated").get(3));
105 EXPECT_EQ(7.0, result->getRewardModel("r").getStateReward(3));
106 EXPECT_EQ(3.0, result->getRewardModel("r").getStateActionReward(3));
107}
108
109TEST(ToStateBasedObservationTransformer, DropsUnreachableStateWithDifferentActionCount) {
110 storm::storage::SparseMatrixBuilder<double> matrixBuilder(0, 0, 0, false, true);
111 matrixBuilder.newRowGroup(0);
112 matrixBuilder.addNextValue(0, 1, 1.0);
113 matrixBuilder.newRowGroup(1);
114 matrixBuilder.addNextValue(1, 1, 1.0);
115 matrixBuilder.newRowGroup(2);
116 matrixBuilder.addNextValue(2, 1, 1.0);
117 matrixBuilder.addNextValue(3, 1, 1.0);
118 storm::models::sparse::StateLabeling labeling(3);
119 labeling.addLabel("init");
120 labeling.addLabelToState("init", 0);
121 storm::models::sparse::Mdp<double> mdp(matrixBuilder.build(4, 3, 3), std::move(labeling));
122
123 auto const result =
124 storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(mdp, [](uint64_t, uint64_t, uint64_t) { return 0; }, 0);
125
126 ASSERT_NE(nullptr, result);
127 EXPECT_EQ(2u, result->getNumberOfStates());
128 EXPECT_EQ(2u, result->getNumberOfChoices());
129 EXPECT_EQ((std::vector<uint32_t>{0, 0}), result->getObservations());
130 for (uint64_t state = 0; state < result->getNumberOfStates(); ++state) {
131 for (auto peer : result->getStatesWithObservation(result->getObservation(state))) {
132 EXPECT_EQ(result->getTransitionMatrix().getRowGroupSize(state), result->getTransitionMatrix().getRowGroupSize(peer));
133 }
134 }
135}
136
137TEST(ToStateBasedObservationTransformer, DropsDisconnectedCycle) {
138 storm::storage::SparseMatrixBuilder<double> matrixBuilder(0, 0, 0, false, true);
139 for (uint64_t state = 0; state < 4; ++state) {
140 matrixBuilder.newRowGroup(state);
141 matrixBuilder.addNextValue(state, state < 2 ? 1 : (state == 2 ? 3 : 2), 1.0);
142 }
143 storm::models::sparse::StateLabeling labeling(4);
144 labeling.addLabel("init");
145 labeling.addLabelToState("init", 0);
146 storm::models::sparse::Mdp<double> mdp(matrixBuilder.build(), std::move(labeling));
147
148 auto const result = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(
149 mdp,
150 [](uint64_t state, uint64_t, uint64_t) {
151 EXPECT_LT(state, 2u);
152 return 1;
153 },
154 0);
155
156 ASSERT_NE(nullptr, result);
157 EXPECT_EQ(2u, result->getNumberOfStates());
158 EXPECT_EQ(2u, result->getNumberOfChoices());
159 EXPECT_EQ((std::vector<uint32_t>{0, 1}), result->getObservations());
160}
161
162TEST(ToStateBasedObservationTransformer, RemapsMetadataAndIgnoresUnreachablePredecessorObservations) {
163 storm::storage::SparseMatrixBuilder<double> matrixBuilder(0, 0, 0, false, true);
164 matrixBuilder.newRowGroup(0);
165 matrixBuilder.addNextValue(0, 2, 1.0);
166 matrixBuilder.newRowGroup(1);
167 matrixBuilder.addNextValue(1, 2, 1.0);
168 matrixBuilder.addNextValue(2, 2, 1.0);
169 matrixBuilder.newRowGroup(3);
170 matrixBuilder.addNextValue(3, 3, 1.0);
171 matrixBuilder.addNextValue(4, 2, 1.0);
172 matrixBuilder.newRowGroup(5);
173 matrixBuilder.addNextValue(5, 3, 1.0);
174 storm::models::sparse::StateLabeling labeling(4);
175 labeling.addLabel("init");
176 labeling.addLabelToState("init", 0);
177 labeling.addLabel("removed");
178 labeling.addLabelToState("removed", 1);
179 labeling.addLabel("target");
180 labeling.addLabelToState("target", 2);
181 storm::storage::sparse::ModelComponents<double> components(matrixBuilder.build(), std::move(labeling));
182 components.choiceLabeling.emplace(6);
183 for (auto const& [label, choice] : std::vector<std::pair<std::string, uint64_t>>{{"removed", 1}, {"go", 3}, {"wait", 4}, {"finish", 5}}) {
184 components.choiceLabeling->addLabel(label);
185 components.choiceLabeling->addLabelToChoice(label, choice);
186 }
187 components.rewardModels.emplace(
188 "r", storm::models::sparse::StandardRewardModel<double>(std::vector<double>{10, 20, 30, 40}, std::vector<double>{100, 200, 201, 300, 301, 400}));
189 storm::models::sparse::Mdp<double> mdp(std::move(components));
190 std::vector<std::tuple<uint64_t, uint64_t, uint64_t>> callbackArguments;
191
192 auto const result = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(
193 mdp,
194 [&callbackArguments](uint64_t state, uint64_t action, uint64_t target) {
195 callbackArguments.emplace_back(state, action, target);
196 return state == 0 ? 1 : (state == 1 ? 99 : target);
197 },
198 0);
199
200 ASSERT_NE(nullptr, result);
201 EXPECT_EQ((std::vector<std::tuple<uint64_t, uint64_t, uint64_t>>{{0, 0, 2}, {2, 0, 3}, {2, 1, 2}, {3, 0, 3}}), callbackArguments);
202 EXPECT_EQ(4u, result->getNumberOfStates());
203 EXPECT_EQ(6u, result->getNumberOfChoices());
204 EXPECT_EQ((std::vector<uint32_t>{0, 1, 2, 3}), result->getObservations());
205 EXPECT_TRUE(result->getStateLabeling().getStates("removed").empty());
206 EXPECT_EQ(2u, result->getStateLabeling().getStates("target").getNumberOfSetBits());
207 EXPECT_TRUE(result->getStateLabeling().getStates("target").get(1));
208 EXPECT_TRUE(result->getStateLabeling().getStates("target").get(2));
209 EXPECT_EQ(1u, result->getInitialStates().getNumberOfSetBits());
210 EXPECT_TRUE(result->getInitialStates().get(0));
211 EXPECT_EQ((std::vector<double>{10, 30, 30, 40}), result->getRewardModel("r").getStateRewardVector());
212 EXPECT_EQ((std::vector<double>{100, 300, 301, 300, 301, 400}), result->getRewardModel("r").getStateActionRewardVector());
213 EXPECT_TRUE(result->getChoiceLabeling().getChoices("removed").empty());
214 EXPECT_EQ(2u, result->getChoiceLabeling().getChoices("go").getNumberOfSetBits());
215 EXPECT_EQ(2u, result->getChoiceLabeling().getChoices("wait").getNumberOfSetBits());
216 std::vector<uint64_t> const expectedTargets{1, 3, 2, 3, 2, 3};
217 auto const& resultMatrix = result->getTransitionMatrix();
218 for (uint64_t choice = 0; choice < expectedTargets.size(); ++choice) {
219 auto const row = resultMatrix.getRow(choice);
220 ASSERT_EQ(1u, row.getNumberOfEntries());
221 EXPECT_EQ(expectedTargets[choice], row.begin()->getColumn());
222 EXPECT_EQ(1.0, row.begin()->getValue());
223 if (choice == 1 || choice == 3) {
224 EXPECT_TRUE(result->getChoiceLabeling().getChoiceHasLabel("go", choice));
225 } else if (choice == 2 || choice == 4) {
226 EXPECT_TRUE(result->getChoiceLabeling().getChoiceHasLabel("wait", choice));
227 }
228 }
229 EXPECT_TRUE(result->getChoiceLabeling().getChoiceHasLabel("finish", 5));
230}
231
232TEST(ToStateBasedObservationTransformer, RetainsAllInitialStates) {
233 storm::storage::SparseMatrixBuilder<double> matrixBuilder(0, 0, 0, false, true);
234 for (uint64_t state = 0; state < 3; ++state) {
235 matrixBuilder.newRowGroup(state);
236 matrixBuilder.addNextValue(state, 2, 1.0);
237 }
238 storm::models::sparse::StateLabeling labeling(3);
239 labeling.addLabel("init");
240 labeling.addLabelToState("init", 0);
241 labeling.addLabelToState("init", 2);
242 storm::models::sparse::Mdp<double> mdp(matrixBuilder.build(), std::move(labeling));
243
244 auto const result = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(
245 mdp,
246 [](uint64_t state, uint64_t, uint64_t) {
247 EXPECT_NE(1u, state);
248 return 1;
249 },
250 0);
251
252 ASSERT_NE(nullptr, result);
253 EXPECT_EQ(3u, result->getNumberOfStates());
254 EXPECT_EQ((std::vector<uint32_t>{0, 0, 1}), result->getObservations());
255 EXPECT_EQ(2u, result->getInitialStates().getNumberOfSetBits());
256 EXPECT_TRUE(result->getInitialStates().get(0));
257 EXPECT_TRUE(result->getInitialStates().get(1));
258 EXPECT_FALSE(result->getInitialStates().get(2));
259}
260
261TEST(ToStateBasedObservationTransformer, IgnoresZeroProbabilityTransitionsWhenDroppingUnreachableStates) {
262 storm::storage::SparseMatrixBuilder<double> matrixBuilder(0, 0, 0, false, true);
263 matrixBuilder.newRowGroup(0);
264 matrixBuilder.addNextValue(0, 0, 1.0);
265 matrixBuilder.addNextValue(0, 1, 0.0);
266 matrixBuilder.newRowGroup(1);
267 matrixBuilder.addNextValue(1, 1, 1.0);
268 storm::models::sparse::StateLabeling labeling(2);
269 labeling.addLabel("init");
270 labeling.addLabelToState("init", 0);
271 storm::models::sparse::Mdp<double> mdp(matrixBuilder.build(), std::move(labeling));
272 ASSERT_EQ(3u, mdp.getTransitionMatrix().getEntryCount());
273 std::vector<std::tuple<uint64_t, uint64_t, uint64_t>> callbackArguments;
274 auto observationFunction = [&callbackArguments](uint64_t state, uint64_t action, uint64_t target) {
275 callbackArguments.emplace_back(state, action, target);
276 return target;
277 };
278
279 auto const result = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(mdp, observationFunction, 0);
280
281 ASSERT_NE(nullptr, result);
282 EXPECT_EQ(1u, result->getNumberOfStates());
283 EXPECT_EQ(1u, result->getNumberOfChoices());
284 EXPECT_EQ(1u, result->getTransitionMatrix().getEntryCount());
285 EXPECT_EQ((std::vector<std::tuple<uint64_t, uint64_t, uint64_t>>{{0, 0, 0}}), callbackArguments);
286
287 callbackArguments.clear();
288 auto const unpruned = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transform(mdp, observationFunction, 0, false);
289 EXPECT_EQ(2u, unpruned->getNumberOfStates());
290 EXPECT_EQ(3u, unpruned->getTransitionMatrix().getEntryCount());
291 EXPECT_EQ((std::vector<std::tuple<uint64_t, uint64_t, uint64_t>>{{0, 0, 0}, {0, 0, 1}, {1, 0, 1}}), callbackArguments);
292}
293
294TEST(ToStateBasedObservationTransformer, RewardAwareTransformationDropsUnreachableState) {
295 auto components = buildComponentsWithUnreachableState();
296 components.observabilityClasses = std::vector<uint32_t>{0, 1, 2};
297 auto const pomdp = std::make_shared<storm::models::sparse::Pomdp<double>>(std::move(components), true);
298
299 auto const result = storm::pomdp::transformer::ToStateBasedObservationTransformer<double>::transformRewardAware(*pomdp, {"r"});
300
301 ASSERT_NE(nullptr, result);
302 EXPECT_EQ(2u, result->getNumberOfStates());
303 EXPECT_EQ(2u, result->getNumberOfChoices());
304 EXPECT_EQ((std::vector<uint32_t>{0, 3}), result->getObservations());
305 EXPECT_TRUE(result->getStateLabeling().getStates("isolated").empty());
306 EXPECT_EQ((std::vector<double>{0.0, 0.0}), result->getRewardModel("r").getStateRewardVector());
307 EXPECT_EQ((std::vector<double>{1.0, 1.0}), result->getRewardModel("r").getStateActionRewardVector());
308 EXPECT_TRUE(result->isCanonic());
309}
TEST
TEST(ToStateBasedObservationTransformer, PassesLocalActionIndicesToCallback)
Definition ToStateBasedObservationTransformerTest.cpp:60
storm::models::sparse::ItemLabeling::addLabel
void addLabel(std::string const &label)
Adds a new label to the labelings.
Definition ItemLabeling.cpp:62
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:16
storm::models::sparse::Model::getTransitionMatrix
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:226
storm::models::sparse::StateLabeling
This class manages the labeling of the state space with a number of (atomic) labels.
Definition StateLabeling.h:16
storm::models::sparse::StateLabeling::addLabelToState
void addLabelToState(std::string const &label, storm::storage::sparse::state_type state)
Adds a label to a given state.
Definition StateLabeling.cpp:48
storm::pomdp::transformer::ToStateBasedObservationTransformer::transformRewardAware
static std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > transformRewardAware(storm::models::sparse::Pomdp< ValueType > const &pomdp, std::set< std::string > const &observableRewardModels, bool dropUnreachableStates=true)
Makes rewards observable by extending observations with the state and state-action reward values of t...
Definition ToStateBasedObservationTransformer.cpp:198
storm::pomdp::transformer::ToStateBasedObservationTransformer::transform
static std::shared_ptr< storm::models::sparse::Pomdp< ValueType > > transform(storm::models::sparse::Mdp< ValueType > const &mdp, TransitionObservationFunction const &transitionObservationFunction, ObservationType initialObservation, bool dropUnreachableStates=true)
Creates a POMDP (with state-based observations) out of an MDP and a transition-based observation func...
Definition ToStateBasedObservationTransformer.cpp:18
storm::storage::SparseMatrixBuilder
A class that can be used to build a sparse matrix by adding value by value.
Definition SparseMatrix.h:134
storm::storage::SparseMatrixBuilder::addNextValue
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
Definition SparseMatrix.cpp:198
storm::storage::SparseMatrixBuilder::newRowGroup
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
Definition SparseMatrix.cpp:265
storm::storage::SparseMatrixBuilder::build
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
Definition SparseMatrix.cpp:293
storm_gtest.h
storm::storage::sparse::ModelComponents::rewardModels
std::unordered_map< std::string, RewardModelType > rewardModels
Definition ModelComponents.h:63
storm::storage::sparse::ModelComponents::choiceLabeling
std::optional< storm::models::sparse::ChoiceLabeling > choiceLabeling
Definition ModelComponents.h:65