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