From 717fa454d2e479318ae0e7b2bd37b497c24949b7 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 18 Apr 2018 15:15:39 +0200
Subject: [PATCH] Updated example drn file

---
 lib/stormpy/examples/files/ctmc/dft.drn | 90 +++++++++++++------------
 tests/core/test_modelchecking.py        |  2 +-
 2 files changed, 47 insertions(+), 45 deletions(-)

diff --git a/lib/stormpy/examples/files/ctmc/dft.drn b/lib/stormpy/examples/files/ctmc/dft.drn
index 1f1f317..91245df 100644
--- a/lib/stormpy/examples/files/ctmc/dft.drn
+++ b/lib/stormpy/examples/files/ctmc/dft.drn
@@ -3,71 +3,73 @@
 @type: CTMC
 @parameters
 
+@reward_models
+
 @nr_states
 16
 @model
-state 0 init
+state 0 !1 failed
 	action 0
-		1 : 0.5
-		2 : 0.5
-		3 : 0.5
-		4 : 0.5
-state 1
-	action 0
-		5 : 0.5
-		9 : 0.5
-		11 : 0.5
-state 2
-	action 0
-		5 : 0.5
-		14 : 0.5
-		15 : 0.5
-state 3
+		0 : 1
+state 1 !2 init
 	action 0
+		2 : 0.5
 		9 : 0.5
-		12 : 0.5
+		13 : 0.5
 		15 : 0.5
-state 4
-	action 0
-		11 : 0.5
-		12 : 0.5
-		14 : 0.5
-state 5
+state 2 !1.5
 	action 0
+		3 : 0.5
 		6 : 0.5
 		8 : 0.5
-state 6
+state 3 !1
 	action 0
-		7 : 0.5
-state 7 failed
+		4 : 0.5
+		5 : 0.5
+state 4 !0.5
+	action 0
+		0 : 0.5
+state 5 !0.5
 	action 0
-		7 : 1
-state 8
+		0 : 0.5
+state 6 !1
 	action 0
+		4 : 0.5
 		7 : 0.5
-state 9
+state 7 !0.5
 	action 0
-		8 : 0.5
-		10 : 0.5
-state 10
+		0 : 0.5
+state 8 !1
 	action 0
+		5 : 0.5
 		7 : 0.5
-state 11
+state 9 !1.5
 	action 0
-		6 : 0.5
+		3 : 0.5
 		10 : 0.5
-state 12
+		12 : 0.5
+state 10 !1
 	action 0
-		10 : 0.5
-		13 : 0.5
-state 13
+		4 : 0.5
+		11 : 0.5
+state 11 !0.5
 	action 0
-		7 : 0.5
-state 14
+		0 : 0.5
+state 12 !1
 	action 0
-		6 : 0.5
-		13 : 0.5
-state 15
+		5 : 0.5
+		11 : 0.5
+state 13 !1.5
 	action 0
 		8 : 0.5
-		13 : 0.5
+		12 : 0.5
+		14 : 0.5
+state 14 !1
+	action 0
+		7 : 0.5
+		11 : 0.5
+state 15 !1.5
+	action 0
+		6 : 0.5
+		10 : 0.5
+		14 : 0.5
diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py
index e4df9eb..89cce9e 100644
--- a/tests/core/test_modelchecking.py
+++ b/tests/core/test_modelchecking.py
@@ -124,6 +124,6 @@ class TestModelChecking:
         assert model.nr_transitions == 33
         assert len(model.initial_states) == 1
         initial_state = model.initial_states[0]
-        assert initial_state == 0
+        assert initial_state == 1
         result = stormpy.model_checking(model, formulas[0])
         assert math.isclose(result.at(initial_state), 4.166666667)