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