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)