Changing Transitions and Rewards over Time

[Ian Riley]

Hello,

I'm trying to model a Shapley game where each state has a probability distribution over possible alternatives and each alternative has its own reward. There are many states. I'm currently representing the matrix game with a 3x3 with discrete values but would like to move up to larger matrices with real values.

I've only spent a small amount of time reading over the language specs for PRISM and PRISM-games. It won't be feasible for me to hardcode the entire reward structure or distribution of transition probabilities. I was hoping that through the Java API I might be able to programmatically update the probabilities and rewards as I step through the sim.

Is that possible in PRISM?

Regards,

Ian Riley

[Kaustabha Ray]

Hi,

There is an explicit model importer from the command line version with more details in the following pages

http://www.prismmodelchecker.org/manual/RunningPRISM/ExplicitModelImport

http://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles

You may want to write a Java program to create files in the specific input format to use in the command line.

--
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.
To view this discussion on the web, visit https://groups.google.com/d/msgid/prismmodelchecker/9d0e3b53-6faa-498d-8ae2-72bb77908e1en%40googlegroups.com.

[Dave Parker]

Hi Ian,

You can also construct and solve/verify models programmatically with
PRISM via Java. There are some instructions and examples here:

https://github.com/prismmodelchecker/prism-api

The "model generator" examples are most relevant to what you want to do.
Please feel free to ask here on the forum for further help.

Best wishes,

Dave

On 09/12/2022 16:58, Kaustabha Ray wrote:
> Hi,
>
> There is an explicit model importer from the command line version with
> more details in the following pages
>
> http://www.prismmodelchecker.org/manual/RunningPRISM/ExplicitModelImport

> <http://www.prismmodelchecker.org/manual/RunningPRISM/ExplicitModelImport>
>
> http://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles

> <mailto:prismmodelchec...@googlegroups.com>.

> To view this discussion on the web, visit

> https://groups.google.com/d/msgid/prismmodelchecker/9d0e3b53-6faa-498d-8ae2-72bb77908e1en%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/9d0e3b53-6faa-498d-8ae2-72bb77908e1en%40googlegroups.com?utm_medium=email&utm_source=footer>.

>
> --
> 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 view this discussion on the web, visit

> https://groups.google.com/d/msgid/prismmodelchecker/CADQEYKFOA_KYD0Z3M-d2w4H6uK_WVqgtYBX0bO8FX1_rf1q%2B9A%40mail.gmail.com <https://groups.google.com/d/msgid/prismmodelchecker/CADQEYKFOA_KYD0Z3M-d2w4H6uK_WVqgtYBX0bO8FX1_rf1q%2B9A%40mail.gmail.com?utm_medium=email&utm_source=footer>.