Prism generated adversary for MDP

[Rayhanul Islam]

Hello,
I am confused about the prism-generated adversary of the following MDP-

mdp

module M

s:[0..3] init 0;

[] s=0 -> 0.3:(s'=1)+ 0.7:(s'=2);
[] s=1 -> 1:(s'=2) ;

[] s=2 -> 1:(s'=0);
[] s=2 -> 1:(s'=1);
[] s=2 -> 1:(s'=3);
[] s=3 -> 1:(s'=3);

endmodule

label "b" = s=1;
label "a" = s=3;

Here, reachable states are
0:(0)
1:(1)
2:(2)
3:(3)

And transition matrix is
4 6 7
0 0 1 0.3
0 0 2 0.7
1 0 2 1
2 0 0 1
2 1 1 1
2 2 3 1
3 0 3 1
where 4 means the number of states, 6 means the number of choices, and 7 is the number of transitions.

However, when I verify the property like Pmax=? [ (G !"b")&(G F "a") ], prism generates the following adversary-
8 4
5 0 1
6 2 0.3
6 7 0.7
7 5 1
I believe entries like (5 0 1) denote the transition from state 5 to state 0 with probability 1.

However, there are no states named 5 in the MDP. Would anyone please explain how to interpret the generated adversaries in prism?  

Thank you in advance.

Regards

Rayhanul