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