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/models/sparse/Dtmc.h"
7#include "storm/models/sparse/MarkovAutomaton.h"
8#include "storm/models/sparse/Mdp.h"
9#include "storm/models/sparse/StandardRewardModel.h"
10
11TEST(DirectEncodingParserTest, DtmcParsing) {
12 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
13 storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.drn");
14
15 // Test if parsed correctly.
16 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
17 ASSERT_EQ(8607ul, modelPtr->getNumberOfStates());
18 ASSERT_EQ(15113ul, modelPtr->getNumberOfTransitions());
19 ASSERT_TRUE(modelPtr->hasLabel("init"));
20 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
21 ASSERT_TRUE(modelPtr->hasLabel("observeIGreater1"));
22 ASSERT_EQ(4650ul, modelPtr->getStates("observeIGreater1").getNumberOfSetBits());
23 ASSERT_TRUE(modelPtr->hasLabel("observe0Greater1"));
24 ASSERT_EQ(1260ul, modelPtr->getStates("observe0Greater1").getNumberOfSetBits());
25}
26
27TEST(DirectEncodingParserTest, MdpParsing) {
28 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
29 storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.drn");
30
31 // Test if parsed correctly.
32 ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType());
33 ASSERT_EQ(169ul, modelPtr->getNumberOfStates());
34 ASSERT_EQ(436ul, modelPtr->getNumberOfTransitions());
35 ASSERT_EQ(254ul, modelPtr->as<storm::models::sparse::Mdp<double>>()->getNumberOfChoices());
36 ASSERT_TRUE(modelPtr->hasLabel("init"));
37 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
38 ASSERT_TRUE(modelPtr->hasLabel("six"));
39 ASSERT_EQ(5ul, modelPtr->getStates("six").getNumberOfSetBits());
40 ASSERT_TRUE(modelPtr->hasLabel("eleven"));
41 ASSERT_EQ(2ul, modelPtr->getStates("eleven").getNumberOfSetBits());
42 ASSERT_EQ(1ul, modelPtr->getNumberOfRewardModels());
43 ASSERT_TRUE(modelPtr->hasRewardModel("coinflips"));
44 ASSERT_TRUE(!modelPtr->getRewardModel("coinflips").hasStateRewards());
45 ASSERT_TRUE(modelPtr->getRewardModel("coinflips").hasStateActionRewards());
46 ASSERT_TRUE(!modelPtr->getRewardModel("coinflips").isAllZero());
47}
48
49TEST(DirectEncodingParserTest, CtmcParsing) {
50 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
51 storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.drn");
52
53 // Test if parsed correctly.
54 ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType());
55 ASSERT_EQ(276ul, modelPtr->getNumberOfStates());
56 ASSERT_EQ(1120ul, modelPtr->getNumberOfTransitions());
57 ASSERT_TRUE(modelPtr->hasLabel("init"));
58 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
59 ASSERT_TRUE(modelPtr->hasLabel("premium"));
60 ASSERT_EQ(64ul, modelPtr->getStates("premium").getNumberOfSetBits());
61 ASSERT_TRUE(modelPtr->hasLabel("minimum"));
62 ASSERT_EQ(132ul, modelPtr->getStates("minimum").getNumberOfSetBits());
63 ASSERT_EQ(1ul, modelPtr->getNumberOfRewardModels());
64 ASSERT_TRUE(modelPtr->hasRewardModel("num_repairs"));
65 ASSERT_TRUE(!modelPtr->getRewardModel("num_repairs").hasStateRewards());
66 ASSERT_TRUE(modelPtr->getRewardModel("num_repairs").hasStateActionRewards());
67 ASSERT_TRUE(!modelPtr->getRewardModel("num_repairs").isAllZero());
68}
69
70TEST(DirectEncodingParserTest, MarkovAutomatonParsing) {
71 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
72 storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.drn");
73 std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = modelPtr->as<storm::models::sparse::MarkovAutomaton<double>>();
74
75 // Test if parsed correctly.
76 ASSERT_EQ(storm::models::ModelType::MarkovAutomaton, modelPtr->getType());
77 ASSERT_EQ(17ul, ma->getNumberOfStates());
78 ASSERT_EQ(25ul, ma->getNumberOfTransitions());
79 ASSERT_EQ(19ul, ma->getNumberOfChoices());
80 ASSERT_EQ(10ul, ma->getMarkovianStates().getNumberOfSetBits());
81 ASSERT_EQ(5, ma->getMaximalExitRate());
82 ASSERT_EQ(1ul, ma->getNumberOfRewardModels());
83 ASSERT_TRUE(ma->hasRewardModel("avg_waiting_time"));
84 ASSERT_TRUE(ma->getRewardModel("avg_waiting_time").hasStateRewards());
85 ASSERT_TRUE(!ma->getRewardModel("avg_waiting_time").hasStateActionRewards());
86 ASSERT_TRUE(!ma->getRewardModel("avg_waiting_time").isAllZero());
87 ASSERT_TRUE(modelPtr->hasLabel("init"));
88 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
89 ASSERT_TRUE(modelPtr->hasLabel("one_job_finished"));
90 ASSERT_EQ(6ul, modelPtr->getStates("one_job_finished").getNumberOfSetBits());
91}
92
93TEST(DirectEncodingParserTest, IntervalDtmcTest) {
94 std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr =
95 storm::parser::DirectEncodingParser<storm::Interval>::parseModel(STORM_TEST_RESOURCES_DIR "/idtmc/brp-16-2.drn");
96 std::shared_ptr<storm::models::sparse::Dtmc<storm::Interval>> dtmc = modelPtr->as<storm::models::sparse::Dtmc<storm::Interval>>();
97 ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
98 ASSERT_EQ(613ul, dtmc->getNumberOfStates());
99 EXPECT_TRUE(modelPtr->hasUncertainty());
100}
101
102TEST(DirectEncodingParserTest, PomdpParsing) {
103 std::shared_ptr<storm::models::sparse::Model<double>> modelPtr =
104 storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/pomdp/maze2_sl0.drn");
105
106 // Test if parsed correctly.
107 ASSERT_EQ(storm::models::ModelType::Pomdp, modelPtr->getType());
108 ASSERT_EQ(15ul, modelPtr->getNumberOfStates());
109 ASSERT_EQ(66ul, modelPtr->getNumberOfTransitions());
110 ASSERT_EQ(54ul, modelPtr->as<storm::models::sparse::Mdp<double>>()->getNumberOfChoices());
111 ASSERT_TRUE(modelPtr->hasLabel("init"));
112 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
113 ASSERT_TRUE(modelPtr->hasLabel("bad"));
114 ASSERT_EQ(2ul, modelPtr->getStates("bad").getNumberOfSetBits());
115 ASSERT_TRUE(modelPtr->hasLabel("goal"));
116 ASSERT_EQ(1ul, modelPtr->getStates("goal").getNumberOfSetBits());
117 ASSERT_EQ(1ul, modelPtr->getNumberOfRewardModels());
118 ASSERT_TRUE(modelPtr->hasRewardModel("rew"));
119 ASSERT_TRUE(!modelPtr->getRewardModel("rew").hasStateRewards());
120 ASSERT_TRUE(modelPtr->getRewardModel("rew").hasStateActionRewards());
121 ASSERT_TRUE(!modelPtr->getRewardModel("rew").isAllZero());
122
123 modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/pomdp/maze2_sl0_no_rew.drn");
124
125 // Test if parsed correctly.
126 ASSERT_EQ(storm::models::ModelType::Pomdp, modelPtr->getType());
127 ASSERT_EQ(15ul, modelPtr->getNumberOfStates());
128 ASSERT_EQ(66ul, modelPtr->getNumberOfTransitions());
129 ASSERT_EQ(54ul, modelPtr->as<storm::models::sparse::Mdp<double>>()->getNumberOfChoices());
130 ASSERT_TRUE(modelPtr->hasLabel("init"));
131 ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
132 ASSERT_TRUE(modelPtr->hasLabel("bad"));
133 ASSERT_EQ(2ul, modelPtr->getStates("bad").getNumberOfSetBits());
134 ASSERT_TRUE(modelPtr->hasLabel("goal"));
135 ASSERT_EQ(1ul, modelPtr->getStates("goal").getNumberOfSetBits());
136 ASSERT_EQ(0ul, modelPtr->getNumberOfRewardModels());
137 ASSERT_FALSE(modelPtr->hasRewardModel());
138}
TEST
TEST(DirectEncodingParserTest, DtmcParsing)
Definition DirectEncodingParserTest.cpp:11
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::DirectEncodingParser::parseModel
static std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > parseModel(std::string const &fil, DirectEncodingParserOptions const &options=DirectEncodingParserOptions())
Load a model in DRN format from a file and create the model.
Definition DirectEncodingParser.cpp:26
storm_gtest.h