State at which rewards for both players become equal

[Ramesh Kumar]

Dave,  thanks for your support. My csg for IPD seems to be running now. 

How to label an AP at which rewards for both players are equal? I am attempting with the following, it does not work

label "converge"=payoff_1=payoff_2;

Regards,     ...Ramesh

[Dave Parker]

Hi Ramesh,

Rewards just annotate the transitions here, they don't change the state.
In this case, your model has just a single state in fact. Labels
identify sets of states in the model. One option is to add another
module with a 0-1 variable, that is updated each step to reflect whether
the players chose the same action.

module m
same : [0..1];
[c1,c2] true -> (same'=1);
[c1,d2] true -> (same'=0);
[d1,c2] true -> (same'=0);
[d1,d2] true -> (same'=1);
endmodule

label "converge" = same=1;

Hope that helps.

Dave

[Ramesh Kumar]

Thanks, Dave, for the reply.

In that case, how to count the number of "same=1" state?. 

My formula as follows: x=number of rounds in which players used same action/total number of rounds

Regards,    ...Ramesh

[Dave Parker]

Hi Ramesh,

You could create a reward structure to count the number of rounds.
Assuming that there is one transition per round, try:

rewards "same" same=1: 1; endrewards

Then you could ask to maximise the expected number of rounds where the
players used the same (over k rounds) with e.g.:

<<p1>> R{"same"}max=? [C<=k]

Hope that helps,

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 view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/1f6d1864-7af4-4152-89eb-ccbc5ffd5371n%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker/1f6d1864-7af4-4152-89eb-ccbc5ffd5371n%40googlegroups.com?utm_medium=email&utm_source=footer>.