Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GraphTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/parser/PrismParser.h"
5#include "storm/builder/DdPrismModelBuilder.h"
6#include "storm/builder/ExplicitModelBuilder.h"
7#include "storm/models/sparse/Dtmc.h"
8#include "storm/models/sparse/Mdp.h"
9#include "storm/models/sparse/StandardRewardModel.h"
10#include "storm/models/symbolic/Dtmc.h"
11#include "storm/models/symbolic/Mdp.h"
12#include "storm/models/symbolic/StandardRewardModel.h"
13#include "storm/storage/SymbolicModelDescription.h"
14#include "storm/storage/dd/Add.h"
15#include "storm/storage/dd/Bdd.h"
16#include "storm/storage/dd/DdManager.h"
17#include "storm/utility/graph.h"
18
19class Cudd {
20 public:
21 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
22};
23
24class Sylvan {
25 public:
26 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
27};
28
29template<typename TestType>
30class GraphTestSymbolic : public ::testing::Test {
31 public:
32 static const storm::dd::DdType DdType = TestType::DdType;
33
34 protected:
35 void SetUp() override {
36#ifndef STORM_HAVE_Z3
37 GTEST_SKIP() << "Z3 not available.";
38#endif
39 }
40};
41
42class GraphTestExplicit : public ::testing::Test {
43 protected:
44 void SetUp() override {
45#ifndef STORM_HAVE_Z3
46 GTEST_SKIP() << "Z3 not available.";
47#endif
48 }
49};
50
51typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
52TYPED_TEST_SUITE(GraphTestSymbolic, TestingTypes, );
53
54TYPED_TEST(GraphTestSymbolic, SymbolicProb01) {
55 const storm::dd::DdType DdType = TestFixture::DdType;
56 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
57 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
58 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
59
60 ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
61
62 {
63 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
64 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
65
66 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->template as<storm::models::symbolic::Dtmc<DdType>>(),
67 model->getReachableStates(), model->getStates("observe0Greater1")));
68 EXPECT_EQ(4409ull, statesWithProbability01.first.getNonZeroCount());
69 EXPECT_EQ(1316ull, statesWithProbability01.second.getNonZeroCount());
70
71 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->template as<storm::models::symbolic::Dtmc<DdType>>(),
72 model->getReachableStates(), model->getStates("observeIGreater1")));
73 EXPECT_EQ(1091ull, statesWithProbability01.first.getNonZeroCount());
74 EXPECT_EQ(4802ull, statesWithProbability01.second.getNonZeroCount());
75
76 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->template as<storm::models::symbolic::Dtmc<DdType>>(),
77 model->getReachableStates(), model->getStates("observeOnlyTrueSender")));
78 EXPECT_EQ(5829ull, statesWithProbability01.first.getNonZeroCount());
79 EXPECT_EQ(1032ull, statesWithProbability01.second.getNonZeroCount());
80 }
81}
82
83TYPED_TEST(GraphTestSymbolic, SymbolicProb01MinMax) {
84 const storm::dd::DdType DdType = TestFixture::DdType;
85 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
86 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
87 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
88
89 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
90
91 {
92 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
93 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
94
95 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
96 model->getReachableStates(), model->getStates("elected")));
97 EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount());
98 EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount());
99
100 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
101 model->getReachableStates(), model->getStates("elected")));
102 EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount());
103 EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount());
104 }
105
106 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
107 program = modelDescription.preprocess().asPrismProgram();
108 model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
109
110 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
111
112 {
113 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
114 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
115
116 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
117 model->getReachableStates(), model->getStates("all_coins_equal_0")));
118 EXPECT_EQ(77ull, statesWithProbability01.first.getNonZeroCount());
119 EXPECT_EQ(149ull, statesWithProbability01.second.getNonZeroCount());
120
121 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
122 model->getReachableStates(), model->getStates("all_coins_equal_0")));
123 EXPECT_EQ(74ull, statesWithProbability01.first.getNonZeroCount());
124 EXPECT_EQ(198ull, statesWithProbability01.second.getNonZeroCount());
125
126 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
127 model->getReachableStates(), model->getStates("all_coins_equal_1")));
128 EXPECT_EQ(94ull, statesWithProbability01.first.getNonZeroCount());
129 EXPECT_EQ(33ull, statesWithProbability01.second.getNonZeroCount());
130
131 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
132 model->getReachableStates(), model->getStates("all_coins_equal_1")));
133 EXPECT_EQ(83ull, statesWithProbability01.first.getNonZeroCount());
134 EXPECT_EQ(35ull, statesWithProbability01.second.getNonZeroCount());
135 }
136
137 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
138 program = modelDescription.preprocess().asPrismProgram();
139 model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
140
141 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
142
143 {
144 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
145 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
146
147 ASSERT_NO_THROW(statesWithProbability01 =
148 storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(), model->getReachableStates(),
149 model->getStates("collision_max_backoff")));
150 EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount());
151 EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount());
152
153 ASSERT_NO_THROW(statesWithProbability01 =
154 storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(), model->getReachableStates(),
155 model->getStates("collision_max_backoff")));
156 EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount());
157 EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount());
158 }
159}
160
161TEST_F(GraphTestExplicit, ExplicitProb01) {
162 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
163 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
164 std::shared_ptr<storm::models::sparse::Model<double>> model =
165 storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
166
167 ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
168
169 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
170
171 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(),
172 storm::storage::BitVector(model->getNumberOfStates(), true),
173 model->getStates("observe0Greater1")));
174 EXPECT_EQ(4409ull, statesWithProbability01.first.getNumberOfSetBits());
175 EXPECT_EQ(1316ull, statesWithProbability01.second.getNumberOfSetBits());
176
177 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(),
178 storm::storage::BitVector(model->getNumberOfStates(), true),
179 model->getStates("observeIGreater1")));
180 EXPECT_EQ(1091ull, statesWithProbability01.first.getNumberOfSetBits());
181 EXPECT_EQ(4802ull, statesWithProbability01.second.getNumberOfSetBits());
182
183 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(),
184 storm::storage::BitVector(model->getNumberOfStates(), true),
185 model->getStates("observeOnlyTrueSender")));
186 EXPECT_EQ(5829ull, statesWithProbability01.first.getNumberOfSetBits());
187 EXPECT_EQ(1032ull, statesWithProbability01.second.getNumberOfSetBits());
188}
189
190TEST_F(GraphTestExplicit, ExplicitProb01MinMax) {
191 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
192 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
193 std::shared_ptr<storm::models::sparse::Model<double>> model =
194 storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
195
196 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
197
198 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
199
200 ASSERT_NO_THROW(statesWithProbability01 =
201 storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
202 storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
203 EXPECT_EQ(0ull, statesWithProbability01.first.getNumberOfSetBits());
204 EXPECT_EQ(364ull, statesWithProbability01.second.getNumberOfSetBits());
205
206 ASSERT_NO_THROW(statesWithProbability01 =
207 storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
208 storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
209 EXPECT_EQ(0ull, statesWithProbability01.first.getNumberOfSetBits());
210 EXPECT_EQ(364ull, statesWithProbability01.second.getNumberOfSetBits());
211
212 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
213 program = modelDescription.preprocess().asPrismProgram();
214 model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
215
216 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
217
218 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
219 storm::storage::BitVector(model->getNumberOfStates(), true),
220 model->getStates("all_coins_equal_0")));
221 EXPECT_EQ(77ull, statesWithProbability01.first.getNumberOfSetBits());
222 EXPECT_EQ(149ull, statesWithProbability01.second.getNumberOfSetBits());
223
224 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
225 storm::storage::BitVector(model->getNumberOfStates(), true),
226 model->getStates("all_coins_equal_0")));
227 EXPECT_EQ(74ull, statesWithProbability01.first.getNumberOfSetBits());
228 EXPECT_EQ(198ull, statesWithProbability01.second.getNumberOfSetBits());
229
230 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
231 storm::storage::BitVector(model->getNumberOfStates(), true),
232 model->getStates("all_coins_equal_1")));
233 EXPECT_EQ(94ull, statesWithProbability01.first.getNumberOfSetBits());
234 EXPECT_EQ(33ull, statesWithProbability01.second.getNumberOfSetBits());
235
236 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
237 storm::storage::BitVector(model->getNumberOfStates(), true),
238 model->getStates("all_coins_equal_1")));
239 EXPECT_EQ(83ull, statesWithProbability01.first.getNumberOfSetBits());
240 EXPECT_EQ(35ull, statesWithProbability01.second.getNumberOfSetBits());
241
242 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
243 program = modelDescription.preprocess().asPrismProgram();
244 model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
245
246 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
247
248 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
249 storm::storage::BitVector(model->getNumberOfStates(), true),
250 model->getStates("collision_max_backoff")));
251 EXPECT_EQ(993ull, statesWithProbability01.first.getNumberOfSetBits());
252 EXPECT_EQ(16ull, statesWithProbability01.second.getNumberOfSetBits());
253
254 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
255 storm::storage::BitVector(model->getNumberOfStates(), true),
256 model->getStates("collision_max_backoff")));
257 EXPECT_EQ(993ull, statesWithProbability01.first.getNumberOfSetBits());
258 EXPECT_EQ(16ull, statesWithProbability01.second.getNumberOfSetBits());
259}
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:25
GraphTestExplicit::SetUp
void SetUp() override
Definition GraphTest.cpp:44
GraphTestSymbolic::SetUp
void SetUp() override
Definition GraphTest.cpp:35
GraphTestSymbolic::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:32
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:30
storm::builder::DdPrismModelBuilder::build
std::shared_ptr< storm::models::symbolic::Model< Type, ValueType > > build(storm::prism::Program const &program, Options const &options=Options())
Translates the given program into a symbolic model (i.e.
Definition DdPrismModelBuilder.cpp:1576
storm::builder::ExplicitModelBuilder::build
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
Definition ExplicitModelBuilder.cpp:91
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:14
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:14
storm::models::symbolic::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:15
storm::models::symbolic::Mdp
This class represents a discrete-time Markov decision process.
Definition Mdp.h:15
storm::models::symbolic::Model::getReachableStates
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:102
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
storm::storage::SymbolicModelDescription::asPrismProgram
storm::prism::Program const & asPrismProgram() const
Definition SymbolicModelDescription.cpp:112
storm::storage::SymbolicModelDescription::preprocess
SymbolicModelDescription preprocess(std::string const &constantDefinitionString="") const
Definition SymbolicModelDescription.cpp:162
storm::utility::graph::performProb01
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01(storm::models::sparse::DeterministicModel< T > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi i...
Definition graph.cpp:400
storm::utility::graph::performProb01Max
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Max(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition graph.cpp:835
storm::utility::graph::performProb01Min
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Min(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition graph.cpp:1079
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
TEST_F
TEST_F(GraphTestExplicit, ExplicitProb01)
Definition GraphTest.cpp:161
storm_gtest.h