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