Hi,
Welcome! PRISM has several distinct model checking engines which are
rather different in nature. For prototypes, people often build on the
"explicit" engine, which is pure Java and mainly based on sparse matrix
data structures for porobabilistic models. There are also "symbolic"
engines. These can be more efficient for large models, but there is a
much steeper learning curve for development. Let us know which you plan
to use (my suggestion would be "explicit") and then I can send some
pointers.
Best wishes,
Dave
On 07/04/2019 21:05,
calvinc...@gmail.com wrote:
> Hello everyone!
>
> I am new to prism and for my thesis I am supposed to extend prism by the
> ability to compute a bisimulation matrix. I am considering an action
> deterministic MDP and need to access the transition matrix of every action.
>
> Currently I am considering this model:
>
> *mdp
>
> module M1
>
> x:[0..6];
>
> [a] x=0 -> 1.0:(x'=1);
> [a] x=1 -> 0.5:(x'=2) + 0.5:(x'=3);
> [b] x=2 -> 1.0:(x'=2);
> [c] x=3 -> 1.0:(x'=3);
> [a] x=4 -> 1.0:(x'=2);
> [a] x=5 -> 1.0:(x'=3);
> [a] x=6 -> 0.5:(x'=4) + 0.5:(x'=5);
>
> endmodule
>
> init x=0 | x=6 endinit*
>
> and for action c for example I would like to get the following matrix:
>
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 1 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
>
> Is there any simple way of doing this? I am sorry if I am missing
> something obvious.
>
> Thank you very much in advance!
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to
prismmodelchecke...@googlegroups.com
> <mailto:
prismmodelchecke...@googlegroups.com>.
> To post to this group, send email to
>
prismmodel...@googlegroups.com
> <mailto:
prismmodel...@googlegroups.com>.
> Visit this group at
https://groups.google.com/group/prismmodelchecker-dev.