Tests for DRN parser

resources/examples/testfiles/ma/jobscheduler.drn

@@ -0,0 +1,71 @@
+// Exported by storm
+// Original model type: Markov Automaton
+@type: Markov Automaton
+@parameters
+
+@reward_models
+avg_waiting_time 
+@nr_states
+17
+@model
+state 0 !0 [1] init
+	action 0 [0]
+		1 : 1
+	action 1 [0]
+		2 : 1
+	action 2 [0]
+		3 : 1
+state 1 !3 [1]
+	action 0 [0]
+		4 : 0.333333
+		5 : 0.666667
+state 2 !4 [1]
+	action 0 [0]
+		4 : 0.25
+		6 : 0.75
+state 3 !5 [1]
+	action 0 [0]
+		5 : 0.4
+		6 : 0.6
+state 4 !0 [0.666667] one_job_finished slowest_before_fastest
+	action 0 [0]
+		7 : 1
+state 5 !0 [0.666667] one_job_finished
+	action 0 [0]
+		8 : 1
+state 6 !0 [0.666667] one_job_finished
+	action 0 [0]
+		9 : 1
+state 7 !5 [0.666667] one_job_finished slowest_before_fastest
+	action 0 [0]
+		10 : 0.4
+		11 : 0.6
+state 8 !4 [0.666667] one_job_finished
+	action 0 [0]
+		10 : 0.25
+		12 : 0.75
+state 9 !3 [0.666667] one_job_finished
+	action 0 [0]
+		11 : 0.333333
+		12 : 0.666667
+state 10 !0 [0.333333] half_of_jobs_finished slowest_before_fastest
+	action 0 [0]
+		13 : 1
+state 11 !0 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		14 : 1
+state 12 !0 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		15 : 1
+state 13 !3 [0.333333] half_of_jobs_finished slowest_before_fastest
+	action 0 [0]
+		16 : 1
+state 14 !2 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		16 : 1
+state 15 !1 [0.333333] half_of_jobs_finished
+	action 0 [0]
+		16 : 1
+state 16 !1 [0] all_jobs_finished deadlock
+	action 0 [0]
+		16 : 1

resources/examples/testfiles/mdp/two_dice.drn

@@ -3,6 +3,8 @@
 @type: MDP
 @parameters
 
+@reward_models
+coinflips 
 @nr_states
 169
 @model

src/test/storm/parser/DirectEncodingParserTest.cpp

@@ -1,23 +1,24 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 
+#include "storm/parser/DirectEncodingParser.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/models/sparse/Mdp.h"
-#include "storm/parser/DirectEncodingParser.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
 
-TEST(DirectEncodingParserTest, CtmcParsing) {
-    std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.drn");
+TEST(DirectEncodingParserTest, DtmcParsing) {
+    std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.drn");
 
     // Test if parsed correctly.
-    ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType());
-    ASSERT_EQ(276ul, modelPtr->getNumberOfStates());
-    ASSERT_EQ(1120ul, modelPtr->getNumberOfTransitions());
+    ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
+    ASSERT_EQ(8607ul, modelPtr->getNumberOfStates());
+    ASSERT_EQ(15113ul, modelPtr->getNumberOfTransitions());
     ASSERT_TRUE(modelPtr->hasLabel("init"));
     ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
-    ASSERT_TRUE(modelPtr->hasLabel("premium"));
-    ASSERT_EQ(64ul, modelPtr->getStates("premium").getNumberOfSetBits());
-    ASSERT_TRUE(modelPtr->hasLabel("minimum"));
-    ASSERT_EQ(132ul, modelPtr->getStates("minimum").getNumberOfSetBits());
+    ASSERT_TRUE(modelPtr->hasLabel("observeIGreater1"));
+    ASSERT_EQ(4650ul, modelPtr->getStates("observeIGreater1").getNumberOfSetBits());
+    ASSERT_TRUE(modelPtr->hasLabel("observe0Greater1"));
+    ASSERT_EQ(1260ul, modelPtr->getStates("observe0Greater1").getNumberOfSetBits());
 }
 
 TEST(DirectEncodingParserTest, MdpParsing) {
@@ -36,3 +37,36 @@ TEST(DirectEncodingParserTest, MdpParsing) {
     ASSERT_EQ(2ul, modelPtr->getStates("eleven").getNumberOfSetBits());
 }
 
+TEST(DirectEncodingParserTest, CtmcParsing) {
+    std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.drn");
+
+    // Test if parsed correctly.
+    ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType());
+    ASSERT_EQ(276ul, modelPtr->getNumberOfStates());
+    ASSERT_EQ(1120ul, modelPtr->getNumberOfTransitions());
+    ASSERT_TRUE(modelPtr->hasLabel("init"));
+    ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
+    ASSERT_TRUE(modelPtr->hasLabel("premium"));
+    ASSERT_EQ(64ul, modelPtr->getStates("premium").getNumberOfSetBits());
+    ASSERT_TRUE(modelPtr->hasLabel("minimum"));
+    ASSERT_EQ(132ul, modelPtr->getStates("minimum").getNumberOfSetBits());
+}
+
+TEST(DirectEncodingParserTest, MarkovAutomatonParsing) {
+    std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.drn");
+    std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = modelPtr->as<storm::models::sparse::MarkovAutomaton<double>>();
+
+    // Test if parsed correctly.
+    ASSERT_EQ(storm::models::ModelType::MarkovAutomaton, modelPtr->getType());
+    ASSERT_EQ(17ul, ma->getNumberOfStates());
+    ASSERT_EQ(25ul, ma->getNumberOfTransitions());
+    ASSERT_EQ(19ul, ma->getNumberOfChoices());
+    ASSERT_EQ(10ul, ma->getMarkovianStates().getNumberOfSetBits());
+    ASSERT_EQ(5, ma->getMaximalExitRate());
+    ASSERT_TRUE(ma->hasRewardModel("avg_waiting_time"));
+    ASSERT_TRUE(modelPtr->hasLabel("init"));
+    ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
+    ASSERT_TRUE(modelPtr->hasLabel("one_job_finished"));
+    ASSERT_EQ(6ul, modelPtr->getStates("one_job_finished").getNumberOfSetBits());
+}
+