kleinj
commented
8 years ago Hi,
PRISM is building the part of the model that is reachable from the initial state (0). As your states 9, 10 and 11 are not reachable, they are not output.
If you want these states in your model, consider using the init ... endinit modelling construct to specify multiple initial states.
For such small models, exporting to a DOT file using the -exporttransdotstate output.dot switch is an easy way to get a graphical representation of the model that is useful for debugging your model.
yijunyu
Hi,
I created a DTMC model: ======= example.pm ====== dtmc module example s : [0..11] init 0; []s=0->0.01:(s'=0)+0.40:(s'=1)+0.40:(s'=2)+0.19:(s'=8); []s=1->0.20:(s'=0)+0.80:(s'=3); []s=2->0.40:(s'=0)+0.5:(s'=3)+0.1:(s'=5); []s=3->0.20:(s'=0)+0.3:(s'=1)+0.3:(s'=2)+0.2:(s'=4); []s=4->1:(s'=4); []s=5->0.75:(s'=2)+0.25:(s'=6); []s=6->0.30:(s'=5)+0.7:(s'=7); []s=7->1.00:(s'=3); []s=8->0.9:(s'=0)+0.1:(s'=8); []s=9->0.35:(s'=8)+0.6:(s'=10)+0.05:(s'=11); []s=10->0.8:(s'=9)+0.2:(s'=11); []s=11->1:(s'=4); endmodule
Then invoking prism using the following command:
prism example.pm -exportmodel example.all -const p=0.9
Instead of receiving a state machine of 12 states, only 9 states were reported in the transition matrix. I have checked the parser of the pm input file, and couldn't find problem there.
9 21 0 0 0.01 0 1 0.4 0 2 0.4 0 8 0.19 1 0 0.2 1 3 0.8 2 0 0.4 2 3 0.5 2 5 0.1 3 0 0.2 3 1 0.3 3 2 0.3 3 4 0.2 4 4 1 5 2 0.75 5 6 0.25 6 5 0.3 6 7 0.7 7 3 1 8 0 0.9 8 8 0.1
Best regards, Yijun