// Public good game // Players receive a capital of einit, which they can invest into a common stock, entirely or in parts. An examiner then multiplies the invested amount by a factor f and distribute it among all the participants equally. csg player p1 m1 endplayer player p2 m2 endplayer player p3 m3 endplayer player p4 m3 endplayer player p5 m5 endplayer const int kmax; // number of rounds const int emax = 500; // cap on the captial held by ecah player const int einit1=5; // initial capital const int einit2=5; // initial capital const int einit3=5; // initial capital const int einit4=5; // initial capital const int einit5=5; // initial capital const int n = 5; // number of players const double f; // multiplier module cc k : [0..kmax+1] init 0; // round [] k<kmax -> (k'=min(kmax,k+1)); [] k=kmax -> (k'=k+1); endmodule module m1 e1 : [0..emax] init einit1; l1 : [0..emax] init 0; [i1_0] k<kmax -> (l1'=0) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3'+l4'+l5')))); // [i1_1] k<kmax -> (l1'=floor(0.1*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); // [i1_2] k<kmax -> (l1'=floor(0.2*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); // [i1_3] k<kmax -> (l1'=floor(0.3*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); // [i1_4] k<kmax -> (l1'=floor(0.4*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); [i1_5] k<kmax -> (l1'=floor(e1/2)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3'+l4'+l5')))); // [i1_6] k<kmax -> (l1'=floor(0.6*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); // [i1_7] k<kmax -> (l1'=floor(0.7*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); // [i1_8] k<kmax -> (l1'=floor(0.8*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); // [i1_9] k<kmax -> (l1'=floor(0.9*e1)) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3')))); [i1_10] k<kmax -> (l1'=e1) & (e1'=min(emax,e1-l1'+floor((f/n)*(l1'+l2'+l3'+l4'+l5')))); [done1] k>=kmax -> (e1'=0) & (l1'=0); endmodule module m2 = m1[e1=e2,l1=l2,l2=l3,l3=l4,l4=l5,l5=l1 einit1=einit2, i1_0=i2_0, // i1_1=i2_1, // i1_2=i2_2, // i1_3=i2_3, // i1_4=i2_4, i1_5=i2_5, // i1_6=i2_6, // i1_7=i2_7, // i1_8=i2_8, // i1_9=i2_9, i1_10=i2_10, done1=done2] endmodule module m3 = m1[e1=e3,l1=l3,l2=l4,l3=l5,l4=l1,l5=l2 einit1=einit3, i1_0=i3_0, // i1_1=i3_1, // i1_2=i3_2, // i1_3=i3_3, // i1_4=i3_4, i1_5=i3_5, // i1_6=i3_6, // i1_7=i3_7, // i1_8=i3_8, // i1_9=i3_9, i1_10=i3_10, done1=done3] endmodule module m4 = m1[e1=e4,l1=l4,l2=l5,l3=l1,l4=l2,l5=l3 einit1=einit4, i1_0=i4_0, // i1_1=i4_1, // i1_2=i4_2, // i1_3=i4_3, // i1_4=i4_4, i1_5=i4_5, // i1_6=i4_6, // i1_7=i4_7, // i1_8=i4_8, // i1_9=i4_9, i1_10=i4_10, done1=done4] endmodule module m5 = m1[e1=e5,l1=l5,l2=l1,l3=l2,l4=l3,l5=l4 einit1=einit5, i1_0=i5_0, // i1_1=i5_1, // i1_2=i5_2, // i1_3=i5_3, // i1_4=i5_4, i1_5=i5_5, // i1_6=i5_6, // i1_7=i5_7, // i1_8=i5_8, // i1_9=i5_9, i1_10=i5_10, done1=done5] endmodule // inst reward for player 1 rewards "r1i" true : e1; endrewards // inst reward for player 2 rewards "r2i" true : e2; endrewards // inst reward for player 3 rewards "r3i" true : e3; endrewards // inst reward for player 4 rewards "r4i" true : e4; endrewards // inst reward for player 4 rewards "r4i" true : e5; endrewards rewards "done1" k=kmax : e1; endrewards rewards "done2" k=kmax : e2; endrewards rewards "done3" k=kmax : e3; endrewards rewards "done4" k=kmax : e4; endrewards rewards "done5" k=kmax : e5; endrewards