Updated example drn file

7 years ago · 717fa454d2
2 changed files with 47 additions and 45 deletions
--- 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
--- 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)