Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DdPrismModelBuilderTest.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/exceptions/WrongFormatException.h"
8#include "storm/models/symbolic/Ctmc.h"
9#include "storm/models/symbolic/Dtmc.h"
10#include "storm/models/symbolic/Mdp.h"
11#include "storm/models/symbolic/StandardRewardModel.h"
12#include "storm/settings/SettingsManager.h"
13#include "storm/settings/modules/BuildSettings.h"
14#include "storm/storage/SymbolicModelDescription.h"
15
16class Cudd {
17 public:
18 static void checkLibraryAvailable() {
19#ifndef STORM_HAVE_CUDD
20 GTEST_SKIP() << "Library CUDD not available.";
21#endif
22 }
23
24 static const storm::dd::DdType DdType = storm::dd::DdType::CUDD;
25};
26
27class Sylvan {
28 public:
29 static void checkLibraryAvailable() {
30#ifndef STORM_HAVE_SYLVAN
31 GTEST_SKIP() << "Library Sylvan not available.";
32#endif
33 }
34
35 static const storm::dd::DdType DdType = storm::dd::DdType::Sylvan;
36};
37
38template<typename TestType>
39class DdPrismModelBuilderTest : public ::testing::Test {
40 public:
41 void SetUp() override {
42 TestType::checkLibraryAvailable();
43 }
44
45 static const storm::dd::DdType DdType = TestType::DdType;
46};
47
48typedef ::testing::Types<Cudd, Sylvan> TestingTypes;
49TYPED_TEST_SUITE(DdPrismModelBuilderTest, TestingTypes, );
50
51TYPED_TEST(DdPrismModelBuilderTest, Dtmc) {
52 const storm::dd::DdType DdType = TestFixture::DdType;
53 storm::Environment env;
54 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
55 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
56
57 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
58 EXPECT_EQ(13ul, model->getNumberOfStates());
59 EXPECT_EQ(20ul, model->getNumberOfTransitions());
60
61 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm");
62 program = modelDescription.preprocess().asPrismProgram();
63 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
64 EXPECT_EQ(677ul, model->getNumberOfStates());
65 EXPECT_EQ(867ul, model->getNumberOfTransitions());
66
67 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm");
68 program = modelDescription.preprocess().asPrismProgram();
69 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
70 EXPECT_EQ(8607ul, model->getNumberOfStates());
71 EXPECT_EQ(15113ul, model->getNumberOfTransitions());
72
73 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
74 program = modelDescription.preprocess().asPrismProgram();
75 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
76 EXPECT_EQ(273ul, model->getNumberOfStates());
77 EXPECT_EQ(397ul, model->getNumberOfTransitions());
78
79 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm");
80 program = modelDescription.preprocess().asPrismProgram();
81 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
82 EXPECT_EQ(1728ul, model->getNumberOfStates());
83 EXPECT_EQ(2505ul, model->getNumberOfTransitions());
84}
85
86TYPED_TEST(DdPrismModelBuilderTest, Ctmc) {
87 const storm::dd::DdType DdType = TestFixture::DdType;
88 storm::Environment env;
89 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", true);
90 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
91
92 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
93 EXPECT_EQ(276ul, model->getNumberOfStates());
94 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
95
96 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm", true);
97 program = modelDescription.preprocess().asPrismProgram();
98 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
99 EXPECT_EQ(3478ul, model->getNumberOfStates());
100 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
101
102 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm", true);
103 program = modelDescription.preprocess().asPrismProgram();
104 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
105 EXPECT_EQ(12ul, model->getNumberOfStates());
106 EXPECT_EQ(22ul, model->getNumberOfTransitions());
107
108 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm", true);
109 program = modelDescription.preprocess().asPrismProgram();
110 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
111 EXPECT_EQ(810ul, model->getNumberOfStates());
112 EXPECT_EQ(3699ul, model->getNumberOfTransitions());
113
114 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", true);
115 program = modelDescription.preprocess().asPrismProgram();
116 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
117 EXPECT_EQ(66ul, model->getNumberOfStates());
118 EXPECT_EQ(189ul, model->getNumberOfTransitions());
119}
120
121TYPED_TEST(DdPrismModelBuilderTest, Mdp) {
122 const storm::dd::DdType DdType = TestFixture::DdType;
123 storm::Environment env;
124 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
125 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
126 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
127
128 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
129 std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
130
131 EXPECT_EQ(169ul, mdp->getNumberOfStates());
132 EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
133 EXPECT_EQ(254ul, mdp->getNumberOfChoices());
134
135 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm");
136 program = modelDescription.preprocess().asPrismProgram();
137 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
138 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
139 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
140
141 EXPECT_EQ(364ul, mdp->getNumberOfStates());
142 EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
143 EXPECT_EQ(573ul, mdp->getNumberOfChoices());
144
145 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm");
146 program = modelDescription.preprocess().asPrismProgram();
147 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
148 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
149 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
150
151 EXPECT_EQ(272ul, mdp->getNumberOfStates());
152 EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
153 EXPECT_EQ(400ul, mdp->getNumberOfChoices());
154
155 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm");
156 program = modelDescription.preprocess().asPrismProgram();
157 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
158 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
159 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
160
161 EXPECT_EQ(1038ul, mdp->getNumberOfStates());
162 EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
163 EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
164
165 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm");
166 program = modelDescription.preprocess().asPrismProgram();
167 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
168 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
169 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
170
171 EXPECT_EQ(4093ul, mdp->getNumberOfStates());
172 EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
173 EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
174
175 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm");
176 program = modelDescription.preprocess().asPrismProgram();
177 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
178 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
179 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
180
181 EXPECT_EQ(37ul, mdp->getNumberOfStates());
182 EXPECT_EQ(59ul, mdp->getNumberOfTransitions());
183 EXPECT_EQ(59ul, mdp->getNumberOfChoices());
184
185 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/sync.nm");
186 program = modelDescription.preprocess().asPrismProgram();
187 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
188 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
189 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
190
191 EXPECT_EQ(5ul, mdp->getNumberOfStates());
192 EXPECT_EQ(24ul, mdp->getNumberOfTransitions());
193 EXPECT_EQ(12ul, mdp->getNumberOfChoices());
194}
195
196TYPED_TEST(DdPrismModelBuilderTest, Composition) {
197 const storm::dd::DdType DdType = TestFixture::DdType;
198 storm::Environment env;
199
200 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm");
201 storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
202
203 std::shared_ptr<storm::models::symbolic::Model<DdType>> model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
204
205 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
206 std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
207
208 EXPECT_EQ(21ul, mdp->getNumberOfStates());
209 EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
210 EXPECT_EQ(61ul, mdp->getNumberOfChoices());
211
212 modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition2.nm");
213 program = modelDescription.preprocess().asPrismProgram();
214 model = storm::builder::DdPrismModelBuilder<DdType>().build(env, program);
215 EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
216 mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
217
218 EXPECT_EQ(8ul, mdp->getNumberOfStates());
219 EXPECT_EQ(21ul, mdp->getNumberOfTransitions());
220 EXPECT_EQ(21ul, mdp->getNumberOfChoices());
221}
222
223TYPED_TEST(DdPrismModelBuilderTest, UnboundedMdp) {
224 const storm::dd::DdType DdType = TestFixture::DdType;
225 storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm");
226 storm::prism::Program program = modelDescription.preprocess("N=1").asPrismProgram();
227 EXPECT_FALSE(storm::builder::DdPrismModelBuilder<DdType>().canHandle(program));
228}
TYPED_TEST_SUITE
TYPED_TEST_SUITE(DdPrismModelBuilderTest, TestingTypes,)
TYPED_TEST
TYPED_TEST(DdPrismModelBuilderTest, Dtmc)
Definition DdPrismModelBuilderTest.cpp:51
Dtmc
storm::models::sparse::Dtmc< double > Dtmc
Definition JaniLocalEliminatorTests.cpp:22
Mdp
storm::models::sparse::Mdp< double > Mdp
Definition JaniLocalEliminatorTests.cpp:23
Cudd::checkLibraryAvailable
static void checkLibraryAvailable()
Definition DdPrismModelBuilderTest.cpp:18
Cudd::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:33
DdPrismModelBuilderTest::DdType
static const storm::dd::DdType DdType
Definition DdPrismModelBuilderTest.cpp:45
Sylvan::DdType
static const storm::dd::DdType DdType
Definition GraphTest.cpp:44
Sylvan::checkLibraryAvailable
static void checkLibraryAvailable()
Definition DdPrismModelBuilderTest.cpp:29
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::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::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
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:61
storm_gtest.h