Different number of rows in states.tra and adv.tra

[Ashutosh Pandey]

Hi,

Using prism, I dumped all the possible states in a text file using "-exportstates states.tra" switch. Similarly, I dumped adversary in a text file using "-exportadv adv.tra" switch.

I believe adv.tra file should have rows equal to the number of states i.e. number of rows in the state.tra file. However, in my case, number of rows in adv.tra (3419641) and states.tra (3765259) are quite different. Is this because non-reachable states are not written to adv.tra file? Please explain.

Thanks,

Ashutosh

[Dave Parker]

Hi Ashutosh,

There are two different sources of discrepancy that I can think of.
Firstly, By default, the .tra file for the adversary contains the
transitions of the induced Markov chain, so there is one for each
transition, not for each state. Secondly, the .tra file does not show
optimal choices for target states, so these are missing.

Best wishes,

Dave.

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To post to this group, send email to prismmod...@googlegroups.com
> <mailto:prismmod...@googlegroups.com>.
> Visit this group at http://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.