Storm 1.11.1.1
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 void checkLibraryAvailable() {
22#ifndef STORM_HAVE_CUDD
23 GTEST_SKIP() << "Library CUDD not available.";
24#endif
25 }
26
27 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
28};
29
30class Sylvan {
31 public:
32 static void checkLibraryAvailable() {
33#ifndef STORM_HAVE_SYLVAN
34 GTEST_SKIP() << "Library Sylvan not available.";
35#endif
36 }
37
38 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
39};
40
41template<typename TestType>
42class GraphTestSymbolic : public ::testing::Test {
43 public:
44 static const storm::dd::DdType DdType = TestType::DdType;
45
46 protected:
47 void SetUp() override {
48#ifndef STORM_HAVE_Z3
49 GTEST_SKIP() << "Library Z3 not available.";
50#endif
51 TestType::checkLibraryAvailable();
52 }
53};
54
55class GraphTestExplicit : public ::testing::Test {
56 protected:
57 void SetUp() override {
58#ifndef STORM_HAVE_Z3
59 GTEST_SKIP() << "Library Z3 not available.";
60#endif
61 }
62};
63
64typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
65TYPED_TEST_SUITE(GraphTestSymbolic, TestingTypes, );
66
67TYPED_TEST(GraphTestSymbolic, SymbolicProb01) {
68 const storm::dd::DdType DdType = TestFixture::DdType;
69 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
70 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
71 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
72
73 ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
74
75 {
76 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
77 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
78
79 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->template as<storm::models::symbolic::Dtmc<DdType>>(),
80 model->getReachableStates(), model->getStates("observe0Greater1")));
81 EXPECT_EQ(4409ull, statesWithProbability01.first.getNonZeroCount());
82 EXPECT_EQ(1316ull, statesWithProbability01.second.getNonZeroCount());
83
84 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->template as<storm::models::symbolic::Dtmc<DdType>>(),
85 model->getReachableStates(), model->getStates("observeIGreater1")));
86 EXPECT_EQ(1091ull, statesWithProbability01.first.getNonZeroCount());
87 EXPECT_EQ(4802ull, statesWithProbability01.second.getNonZeroCount());
88
89 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->template as<storm::models::symbolic::Dtmc<DdType>>(),
90 model->getReachableStates(), model->getStates("observeOnlyTrueSender")));
91 EXPECT_EQ(5829ull, statesWithProbability01.first.getNonZeroCount());
92 EXPECT_EQ(1032ull, statesWithProbability01.second.getNonZeroCount());
93 }
94}
95
96TYPED_TEST(GraphTestSymbolic, SymbolicProb01MinMax) {
97 const storm::dd::DdType DdType = TestFixture::DdType;
98 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
99 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
100 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
101
102 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
103
104 {
105 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
106 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
107
108 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
109 model->getReachableStates(), model->getStates("elected")));
110 EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount());
111 EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount());
112
113 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
114 model->getReachableStates(), model->getStates("elected")));
115 EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount());
116 EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount());
117 }
118
119 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
120 program = modelDescription.preprocess().asPrismProgram();
121 model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
122
123 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
124
125 {
126 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
127 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
128
129 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
130 model->getReachableStates(), model->getStates("all_coins_equal_0")));
131 EXPECT_EQ(77ull, statesWithProbability01.first.getNonZeroCount());
132 EXPECT_EQ(149ull, statesWithProbability01.second.getNonZeroCount());
133
134 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
135 model->getReachableStates(), model->getStates("all_coins_equal_0")));
136 EXPECT_EQ(74ull, statesWithProbability01.first.getNonZeroCount());
137 EXPECT_EQ(198ull, statesWithProbability01.second.getNonZeroCount());
138
139 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
140 model->getReachableStates(), model->getStates("all_coins_equal_1")));
141 EXPECT_EQ(94ull, statesWithProbability01.first.getNonZeroCount());
142 EXPECT_EQ(33ull, statesWithProbability01.second.getNonZeroCount());
143
144 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(),
145 model->getReachableStates(), model->getStates("all_coins_equal_1")));
146 EXPECT_EQ(83ull, statesWithProbability01.first.getNonZeroCount());
147 EXPECT_EQ(35ull, statesWithProbability01.second.getNonZeroCount());
148 }
149
150 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
151 program = modelDescription.preprocess().asPrismProgram();
152 model = storm::builder::DdPrismModelBuilder<DdType>().build(program);
153
154 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
155
156 {
157 // This block is necessary, so the BDDs get disposed before the manager (contained in the model).
158 std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01;
159
160 ASSERT_NO_THROW(statesWithProbability01 =
161 storm::utility::graph::performProb01Min(*model->template as<storm::models::symbolic::Mdp<DdType>>(), model->getReachableStates(),
162 model->getStates("collision_max_backoff")));
163 EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount());
164 EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount());
165
166 ASSERT_NO_THROW(statesWithProbability01 =
167 storm::utility::graph::performProb01Max(*model->template as<storm::models::symbolic::Mdp<DdType>>(), model->getReachableStates(),
168 model->getStates("collision_max_backoff")));
169 EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount());
170 EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount());
171 }
172}
173
174TEST_F(GraphTestExplicit, ExplicitProb01) {
175 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
176 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
177 std::shared_ptr<storm::models::sparse::Model<double>> model =
178 storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
179
180 ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
181
182 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
183
184 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(),
185 storm::storage::BitVector(model->getNumberOfStates(), true),
186 model->getStates("observe0Greater1")));
187 EXPECT_EQ(4409ull, statesWithProbability01.first.getNumberOfSetBits());
188 EXPECT_EQ(1316ull, statesWithProbability01.second.getNumberOfSetBits());
189
190 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(),
191 storm::storage::BitVector(model->getNumberOfStates(), true),
192 model->getStates("observeIGreater1")));
193 EXPECT_EQ(1091ull, statesWithProbability01.first.getNumberOfSetBits());
194 EXPECT_EQ(4802ull, statesWithProbability01.second.getNumberOfSetBits());
195
196 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::sparse::Dtmc<double>>(),
197 storm::storage::BitVector(model->getNumberOfStates(), true),
198 model->getStates("observeOnlyTrueSender")));
199 EXPECT_EQ(5829ull, statesWithProbability01.first.getNumberOfSetBits());
200 EXPECT_EQ(1032ull, statesWithProbability01.second.getNumberOfSetBits());
201}
202
203TEST_F(GraphTestExplicit, ExplicitProb01MinMax) {
204 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
205 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
206 std::shared_ptr<storm::models::sparse::Model<double>> model =
207 storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
208
209 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
210
211 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
212
213 ASSERT_NO_THROW(statesWithProbability01 =
214 storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
215 storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
216 EXPECT_EQ(0ull, statesWithProbability01.first.getNumberOfSetBits());
217 EXPECT_EQ(364ull, statesWithProbability01.second.getNumberOfSetBits());
218
219 ASSERT_NO_THROW(statesWithProbability01 =
220 storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
221 storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected")));
222 EXPECT_EQ(0ull, statesWithProbability01.first.getNumberOfSetBits());
223 EXPECT_EQ(364ull, statesWithProbability01.second.getNumberOfSetBits());
224
225 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
226 program = modelDescription.preprocess().asPrismProgram();
227 model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
228
229 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
230
231 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
232 storm::storage::BitVector(model->getNumberOfStates(), true),
233 model->getStates("all_coins_equal_0")));
234 EXPECT_EQ(77ull, statesWithProbability01.first.getNumberOfSetBits());
235 EXPECT_EQ(149ull, statesWithProbability01.second.getNumberOfSetBits());
236
237 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
238 storm::storage::BitVector(model->getNumberOfStates(), true),
239 model->getStates("all_coins_equal_0")));
240 EXPECT_EQ(74ull, statesWithProbability01.first.getNumberOfSetBits());
241 EXPECT_EQ(198ull, statesWithProbability01.second.getNumberOfSetBits());
242
243 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
244 storm::storage::BitVector(model->getNumberOfStates(), true),
245 model->getStates("all_coins_equal_1")));
246 EXPECT_EQ(94ull, statesWithProbability01.first.getNumberOfSetBits());
247 EXPECT_EQ(33ull, statesWithProbability01.second.getNumberOfSetBits());
248
249 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
250 storm::storage::BitVector(model->getNumberOfStates(), true),
251 model->getStates("all_coins_equal_1")));
252 EXPECT_EQ(83ull, statesWithProbability01.first.getNumberOfSetBits());
253 EXPECT_EQ(35ull, statesWithProbability01.second.getNumberOfSetBits());
254
255 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
256 program = modelDescription.preprocess().asPrismProgram();
257 model = storm::builder::ExplicitModelBuilder<double>(program, storm::generator::NextStateGeneratorOptions(false, true)).build();
258
259 ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
260
261 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::sparse::Mdp<double>>(),
262 storm::storage::BitVector(model->getNumberOfStates(), true),
263 model->getStates("collision_max_backoff")));
264 EXPECT_EQ(993ull, statesWithProbability01.first.getNumberOfSetBits());
265 EXPECT_EQ(16ull, statesWithProbability01.second.getNumberOfSetBits());
266
267 ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::sparse::Mdp<double>>(),
268 storm::storage::BitVector(model->getNumberOfStates(), true),
269 model->getStates("collision_max_backoff")));
270 EXPECT_EQ(993ull, statesWithProbability01.first.getNumberOfSetBits());
271 EXPECT_EQ(16ull, statesWithProbability01.second.getNumberOfSetBits());
272}
Cudd::checkLibraryAvailable
static void checkLibraryAvailable()
Definition GraphTest.cpp:21
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:31
GraphTestExplicit::SetUp
void SetUp() override
Definition GraphTest.cpp:57
GraphTestSymbolic::SetUp
void SetUp() override
Definition GraphTest.cpp:47
GraphTestSymbolic::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:44
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:42
Sylvan::checkLibraryAvailable
static void checkLibraryAvailable()
Definition GraphTest.cpp:32
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:92
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:13
storm::models::symbolic::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:13
storm::models::symbolic::Mdp
This class represents a discrete-time Markov decision process.
Definition Mdp.h:13
storm::models::symbolic::Model::getReachableStates
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:97
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:16
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:399
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:825
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:1069
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:62
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:59
TEST_F
TEST_F(GraphTestExplicit, ExplicitProb01)
Definition GraphTest.cpp:174
storm_gtest.h