Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DirectEncodingParserTest.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/DirectEncodingParser.h"
5#include "storm/adapters/IntervalAdapter.h"
6#include "storm/exceptions/MissingLibraryException.h"
7#include "storm/exceptions/WrongFormatException.h"
8#include "storm/models/sparse/Dtmc.h"
9#include "storm/models/sparse/MarkovAutomaton.h"
10#include "storm/models/sparse/Mdp.h"
11#include "storm/models/sparse/StandardRewardModel.h"
12
13TEST(DirectEncodingParserTest, DtmcParsing) {
14 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
15 storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.drn");
16
17 // Test if parsed correctly.
18 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
19 ASSERT_EQ(8607ul, modelPtr->getNumberOfStates());
20 ASSERT_EQ(15113ul, modelPtr->getNumberOfTransitions());
21 ASSERT_TRUE(modelPtr->hasLabel("init"));
22 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
23 ASSERT_TRUE(modelPtr->hasLabel("observeIGreater1"));
24 ASSERT_EQ(4650ul, modelPtr->getStates("observeIGreater1").getNumberOfSetBits());
25 ASSERT_TRUE(modelPtr->hasLabel("observe0Greater1"));
26 ASSERT_EQ(1260ul, modelPtr->getStates("observe0Greater1").getNumberOfSetBits());
27
28 std::shared_ptr<storm::models::ModelBase> modelBasePtr =
29 storm::parser::parseDirectEncodingModel(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.drn", storm::parser::DirectEncodingValueType::Default);
30 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
31 auto dtmc = modelBasePtr->as<storm::models::sparse::Dtmc<double>>();
32 ASSERT_EQ(8607ul, dtmc->getNumberOfStates());
33}
34
35TEST(DirectEncodingParserTest, DtmcRationalParsing) {
36 std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> modelPtr =
37 storm::parser::parseDirectEncodingModel<storm::RationalNumber>(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.drn");
38
39 // Test if parsed correctly.
40 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
41 ASSERT_EQ(8607ul, modelPtr->getNumberOfStates());
42 ASSERT_EQ(15113ul, modelPtr->getNumberOfTransitions());
43 ASSERT_TRUE(modelPtr->hasLabel("init"));
44 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
45 ASSERT_TRUE(modelPtr->hasLabel("observeIGreater1"));
46 ASSERT_EQ(4650ul, modelPtr->getStates("observeIGreater1").getNumberOfSetBits());
47 ASSERT_TRUE(modelPtr->hasLabel("observe0Greater1"));
48 ASSERT_EQ(1260ul, modelPtr->getStates("observe0Greater1").getNumberOfSetBits());
49
50 std::shared_ptr<storm::models::ModelBase> modelBasePtr =
51 storm::parser::parseDirectEncodingModel(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.drn", storm::parser::DirectEncodingValueType::Rational);
52 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
53 auto dtmc = modelBasePtr->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
54 ASSERT_EQ(8607ul, dtmc->getNumberOfStates());
55}
56
57TEST(DirectEncodingParserTest, MdpParsing) {
58 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
59 storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.drn");
60
61 // Test if parsed correctly.
62 ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType());
63 ASSERT_EQ(169ul, modelPtr->getNumberOfStates());
64 ASSERT_EQ(436ul, modelPtr->getNumberOfTransitions());
65 ASSERT_EQ(254ul, modelPtr->as<storm::models::sparse::Mdp<double>>()->getNumberOfChoices());
66 ASSERT_TRUE(modelPtr->hasLabel("init"));
67 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
68 ASSERT_TRUE(modelPtr->hasLabel("six"));
69 ASSERT_EQ(5ul, modelPtr->getStates("six").getNumberOfSetBits());
70 ASSERT_TRUE(modelPtr->hasLabel("eleven"));
71 ASSERT_EQ(2ul, modelPtr->getStates("eleven").getNumberOfSetBits());
72 ASSERT_EQ(1ul, modelPtr->getNumberOfRewardModels());
73 ASSERT_TRUE(modelPtr->hasRewardModel("coinflips"));
74 ASSERT_TRUE(!modelPtr->getRewardModel("coinflips").hasStateRewards());
75 ASSERT_TRUE(modelPtr->getRewardModel("coinflips").hasStateActionRewards());
76 ASSERT_TRUE(!modelPtr->getRewardModel("coinflips").isAllZero());
77}
78
79TEST(DirectEncodingParserTest, CtmcParsing) {
80 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
81 storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.drn");
82
83 // Test if parsed correctly.
84 ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType());
85 ASSERT_EQ(276ul, modelPtr->getNumberOfStates());
86 ASSERT_EQ(1120ul, modelPtr->getNumberOfTransitions());
87 ASSERT_TRUE(modelPtr->hasLabel("init"));
88 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
89 ASSERT_TRUE(modelPtr->hasLabel("premium"));
90 ASSERT_EQ(64ul, modelPtr->getStates("premium").getNumberOfSetBits());
91 ASSERT_TRUE(modelPtr->hasLabel("minimum"));
92 ASSERT_EQ(132ul, modelPtr->getStates("minimum").getNumberOfSetBits());
93 ASSERT_EQ(1ul, modelPtr->getNumberOfRewardModels());
94 ASSERT_TRUE(modelPtr->hasRewardModel("num_repairs"));
95 ASSERT_TRUE(!modelPtr->getRewardModel("num_repairs").hasStateRewards());
96 ASSERT_TRUE(modelPtr->getRewardModel("num_repairs").hasStateActionRewards());
97 ASSERT_TRUE(!modelPtr->getRewardModel("num_repairs").isAllZero());
98}
99
100TEST(DirectEncodingParserTest, MarkovAutomatonParsing) {
101 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
102 storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.drn");
103 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = modelPtr->as<storm::models::sparse::MarkovAutomaton<double>>();
104
105 // Test if parsed correctly.
106 ASSERT_EQ(storm::models::ModelType::MarkovAutomaton, modelPtr->getType());
107 ASSERT_EQ(17ul, ma->getNumberOfStates());
108 ASSERT_EQ(25ul, ma->getNumberOfTransitions());
109 ASSERT_EQ(19ul, ma->getNumberOfChoices());
110 ASSERT_EQ(10ul, ma->getMarkovianStates().getNumberOfSetBits());
111 ASSERT_EQ(5, ma->getMaximalExitRate());
112 ASSERT_EQ(1ul, ma->getNumberOfRewardModels());
113 ASSERT_TRUE(ma->hasRewardModel("avg_waiting_time"));
114 ASSERT_TRUE(ma->getRewardModel("avg_waiting_time").hasStateRewards());
115 ASSERT_TRUE(!ma->getRewardModel("avg_waiting_time").hasStateActionRewards());
116 ASSERT_TRUE(!ma->getRewardModel("avg_waiting_time").isAllZero());
117 ASSERT_TRUE(modelPtr->hasLabel("init"));
118 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
119 ASSERT_TRUE(modelPtr->hasLabel("one_job_finished"));
120 ASSERT_EQ(6ul, modelPtr->getStates("one_job_finished").getNumberOfSetBits());
121}
122
123TEST(DirectEncodingParserTest, IntervalDtmcTest) {
124 std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr =
125 storm::parser::parseDirectEncodingModel<storm::Interval>(STORM_TEST_RESOURCES_DIR "/idtmc/brp-16-2.drn");
126 std::shared_ptr<storm::models::sparse::Dtmc<storm::Interval>> dtmc = modelPtr->as<storm::models::sparse::Dtmc<storm::Interval>>();
127 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
128 ASSERT_EQ(613ul, dtmc->getNumberOfStates());
129 EXPECT_TRUE(modelPtr->hasUncertainty());
130
131 std::shared_ptr<storm::models::ModelBase> modelBasePtr =
132 storm::parser::parseDirectEncodingModel(STORM_TEST_RESOURCES_DIR "/idtmc/brp-16-2.drn", storm::parser::DirectEncodingValueType::Default);
133 ASSERT_EQ(storm::models::ModelType::Dtmc, modelBasePtr->getType());
134 dtmc = modelBasePtr->as<storm::models::sparse::Dtmc<storm::Interval>>();
135 ASSERT_EQ(613ul, dtmc->getNumberOfStates());
136 EXPECT_TRUE(modelPtr->hasUncertainty());
137}
138
139TEST(DirectEncodingParserTest, RationalIntervalDtmcTest) {
140 std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> modelPtr =
141 storm::parser::parseDirectEncodingModel<storm::RationalInterval>(STORM_TEST_RESOURCES_DIR "/idtmc/rational-brp-16-2.drn");
142 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalInterval>> dtmc = modelPtr->as<storm::models::sparse::Dtmc<storm::RationalInterval>>();
143 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
144 ASSERT_EQ(613ul, dtmc->getNumberOfStates());
145 EXPECT_TRUE(modelPtr->hasUncertainty());
146
147 std::shared_ptr<storm::models::ModelBase> modelBasePtr =
148 storm::parser::parseDirectEncodingModel(STORM_TEST_RESOURCES_DIR "/idtmc/rational-brp-16-2.drn", storm::parser::DirectEncodingValueType::Default);
149 ASSERT_EQ(storm::models::ModelType::Dtmc, modelBasePtr->getType());
150 dtmc = modelBasePtr->as<storm::models::sparse::Dtmc<storm::RationalInterval>>();
151 ASSERT_EQ(613ul, dtmc->getNumberOfStates());
152 EXPECT_TRUE(modelPtr->hasUncertainty());
153}
154
155TEST(DirectEncodingParserTest, PomdpParsing) {
156 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
157 storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/pomdp/maze2_sl0.drn");
158
159 // Test if parsed correctly.
160 ASSERT_EQ(storm::models::ModelType::Pomdp, modelPtr->getType());
161 ASSERT_EQ(15ul, modelPtr->getNumberOfStates());
162 ASSERT_EQ(66ul, modelPtr->getNumberOfTransitions());
163 ASSERT_EQ(54ul, modelPtr->as<storm::models::sparse::Mdp<double>>()->getNumberOfChoices());
164 ASSERT_TRUE(modelPtr->hasLabel("init"));
165 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
166 ASSERT_TRUE(modelPtr->hasLabel("bad"));
167 ASSERT_EQ(2ul, modelPtr->getStates("bad").getNumberOfSetBits());
168 ASSERT_TRUE(modelPtr->hasLabel("goal"));
169 ASSERT_EQ(1ul, modelPtr->getStates("goal").getNumberOfSetBits());
170 ASSERT_EQ(1ul, modelPtr->getNumberOfRewardModels());
171 ASSERT_TRUE(modelPtr->hasRewardModel("rew"));
172 ASSERT_TRUE(!modelPtr->getRewardModel("rew").hasStateRewards());
173 ASSERT_TRUE(modelPtr->getRewardModel("rew").hasStateActionRewards());
174 ASSERT_TRUE(!modelPtr->getRewardModel("rew").isAllZero());
175
176 modelPtr = storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/pomdp/maze2_sl0_no_rew.drn");
177
178 // Test if parsed correctly.
179 ASSERT_EQ(storm::models::ModelType::Pomdp, modelPtr->getType());
180 ASSERT_EQ(15ul, modelPtr->getNumberOfStates());
181 ASSERT_EQ(66ul, modelPtr->getNumberOfTransitions());
182 ASSERT_EQ(54ul, modelPtr->as<storm::models::sparse::Mdp<double>>()->getNumberOfChoices());
183 ASSERT_TRUE(modelPtr->hasLabel("init"));
184 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
185 ASSERT_TRUE(modelPtr->hasLabel("bad"));
186 ASSERT_EQ(2ul, modelPtr->getStates("bad").getNumberOfSetBits());
187 ASSERT_TRUE(modelPtr->hasLabel("goal"));
188 ASSERT_EQ(1ul, modelPtr->getStates("goal").getNumberOfSetBits());
189 ASSERT_EQ(0ul, modelPtr->getNumberOfRewardModels());
190 ASSERT_FALSE(modelPtr->hasRewardModel());
191}
192
193TEST(DirectEncodingParserTest, CompressedParsing) {
194#ifndef STORM_HAVE_LIBARCHIVE
195 STORM_SILENT_EXPECT_THROW(storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.drn.gz"),
196 storm::exceptions::MissingLibraryException);
197 STORM_SILENT_EXPECT_THROW(storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.drn.xz"),
198 storm::exceptions::MissingLibraryException);
199 GTEST_SKIP() << "libarchive not available.";
200#endif
201 {
202 auto modelPtr = storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.drn.gz");
203 auto dtmc = modelPtr->as<storm::models::sparse::Dtmc<double>>();
204 ASSERT_EQ(677ul, dtmc->getNumberOfStates());
205 }
206 {
207 auto modelPtr = storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.drn.xz");
208 auto dtmc = modelPtr->as<storm::models::sparse::Dtmc<double>>();
209 ASSERT_EQ(677ul, dtmc->getNumberOfStates());
210 }
211}
212
213TEST(DirectEncodingParserTest, RewardAfterLabel) {
214 // The reward bracket must come before 'init'/other labels, not after.
215 STORM_SILENT_ASSERT_THROW(storm::parser::parseDirectEncodingModel<double>(STORM_TEST_RESOURCES_DIR "/dtmc/drn_rewardAfterLabel.drn"),
216 storm::exceptions::WrongFormatException);
217}
TEST
TEST(DirectEncodingParserTest, DtmcParsing)
Definition DirectEncodingParserTest.cpp:13
storm::models::sparse::Dtmc
This class represents a discrete-time Markov chain.
Definition Dtmc.h:16
storm::models::sparse::MarkovAutomaton
This class represents a Markov automaton.
Definition MarkovAutomaton.h:17
storm::models::sparse::Mdp
This class represents a (discrete-time) Markov decision process.
Definition Mdp.h:16
storm::models::sparse::NondeterministicModel::getNumberOfChoices
uint_fast64_t getNumberOfChoices(uint_fast64_t state) const
Definition NondeterministicModel.cpp:38
storm::parser::parseDirectEncodingModel< double >
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< double > > parseDirectEncodingModel< double >(std::filesystem::path const &file, DirectEncodingParserOptions const &options)
storm::parser::parseDirectEncodingModel< storm::RationalNumber >
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::RationalNumber > > parseDirectEncodingModel< storm::RationalNumber >(std::filesystem::path const &file, DirectEncodingParserOptions const &options)
storm::parser::parseDirectEncodingModel
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > parseDirectEncodingModel(std::filesystem::path const &file, DirectEncodingParserOptions const &options)
Parses the given file in DRN format.
Definition DirectEncodingParser.cpp:569
storm::parser::parseDirectEncodingModel< storm::RationalInterval >
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::RationalInterval > > parseDirectEncodingModel< storm::RationalInterval >(std::filesystem::path const &file, DirectEncodingParserOptions const &options)
storm::parser::parseDirectEncodingModel< storm::Interval >
template STORM_PARSERS_API std::shared_ptr< storm::models::sparse::Model< storm::Interval > > parseDirectEncodingModel< storm::Interval >(std::filesystem::path const &file, DirectEncodingParserOptions const &options)
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:21
STORM_SILENT_ASSERT_THROW
#define STORM_SILENT_ASSERT_THROW(statement, expected_exception)
Definition storm_gtest.h:16