23 views

Skip to first unread message

Aug 7, 2018, 8:04:38 PM8/7/18

to PRISM model checker developers

Hi,

This seems a trivial question, but I could not find an answer to it. Given a dtmc model, which is an instance of ProbModel class and the model's transition matrix "trans", how can I extract transition probability between any two states, for instance between states 1 and 2 ?

Aug 8, 2018, 6:48:00 AM8/8/18

to Ali A. Noroozi, PRISM model checker developers

Hi Ali,

In the MTBDD world, questions are seldom trivial :)

Depending on what you want to do, there are several approaches. If you

consider the matrix to range over the full state space that is spanned

by the row and column MTBDD variables (i.e., for n row/col variables you

have states 0 ... 2^n-1), you can encode the row index as an assignment

to the row variables, the column index as an assignment to the column

variables and then use Cudd_Eval to obtain the constant corresponding to

that matrix entry. See, e.g., the code in DD_PrintMatrix

https://github.com/prismmodelchecker/prism/blob/a8999396873a4fc4636b67f93fba6fc3fd0c82ac/prism/src/dd/dd_matrix.cc#L463

If you want to consider trans to be a matrix over a subset of the state

space (i.e., only the reachable states), things get a bit more tricky.

Here, you have to be able to convert between the state index (0th

reachable state, 1st reachable state, ...) and the corresponding

assignment. For that purpose, PRISM maintains an ODD data structure that

allows to compute the state index of a row variable assignment and vice

versa. Consider the code in

https://github.com/prismmodelchecker/prism/blob/f767eb70d04103233d1b68ee2c7b673d0b0a31bd/prism/src/sparse/PS_ExportMatrix.cc#L40

which is used for this purpose (e.g., for exporting the .tra file of the

transition matrix). For convenience, an explicit (sparse) matrix is

generated here (over the reachable states, taking the ODD information

into account) and then there is iteration over the entries of that matrix.

Does this help?

Cheers,

Joachim Klein

Depending on what you want to do, there are several approaches. If you

consider the matrix to range over the full state space that is spanned

by the row and column MTBDD variables (i.e., for n row/col variables you

have states 0 ... 2^n-1), you can encode the row index as an assignment

to the row variables, the column index as an assignment to the column

variables and then use Cudd_Eval to obtain the constant corresponding to

that matrix entry. See, e.g., the code in DD_PrintMatrix

https://github.com/prismmodelchecker/prism/blob/a8999396873a4fc4636b67f93fba6fc3fd0c82ac/prism/src/dd/dd_matrix.cc#L463

If you want to consider trans to be a matrix over a subset of the state

space (i.e., only the reachable states), things get a bit more tricky.

Here, you have to be able to convert between the state index (0th

reachable state, 1st reachable state, ...) and the corresponding

assignment. For that purpose, PRISM maintains an ODD data structure that

allows to compute the state index of a row variable assignment and vice

versa. Consider the code in

https://github.com/prismmodelchecker/prism/blob/f767eb70d04103233d1b68ee2c7b673d0b0a31bd/prism/src/sparse/PS_ExportMatrix.cc#L40

which is used for this purpose (e.g., for exporting the .tra file of the

transition matrix). For convenience, an explicit (sparse) matrix is

generated here (over the reachable states, taking the ODD information

into account) and then there is iteration over the entries of that matrix.

Does this help?

Cheers,

Joachim Klein

Aug 9, 2018, 3:38:44 AM8/9/18

to PRISM model checker developers

Dear Joachim,

Yes, it helped. I wanted transitions of reachable states. I was already working on PS_ExportMatrix.cc, but I was in doubt that maybe there was an easier way.

Anyway, I implemented a function similar to first part of PS_ExportMatrix to build the explicit sparse matrix and another function for querying the transition probability of two arbitrary state indexes. It seems it is working fine.

Anyway, thanks for your answer.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu