csg
player investor1 investor1 endplayer
player investor2 investor2 endplayer
player investor3 investor3 endplayer
const int months;
const double pbar;
module month
m : [0..1];
r : [0.. months];
[] m=0 & r<months & (!((i1=1 & b1=0) | i1=2) | !((i2=1 & b2=0) | i2=2) | !((i3=1 & b3=0) | i3=2)) -> (m'=1);
[] m=1 -> (m'=0) & (r'=r+1);
[] m=0 & !(r<months & (!((i1=1 & b1=0) | i1=2) | !((i2=1 & b2=0) | i2=2) | !((i3=1 & b3=0) | i3=2))) -> true;
endmodule
module investor1
i1 : [0..2];
[noinvest1] m=0 & (i1=0 | (i1=1 & b1=1)) & r<months -> (i1'=0);
[invest1] m=0 & (i1=0 | (i1=1 & b1=1)) & r<months -> (i1'=1);
[cashin1] m=0 & i1=1 & b1=0 -> (i1'=2);
[end1] m=0 & (i1=0 | (i1=1 & b1=1)) & r=months -> (i1'=2);
endmodule
module investor2=investor1[i1=i2,b1=b2,noinvest1=noinvest2,invest1=invest2,cashin1=cashin2,end1=end2] endmodule
module investor3=investor1[i1=i3,b1=b3,noinvest1=noinvest3,invest1=invest3,cashin1=cashin3,end1=end3] endmodule
module market1
b1 : [0..1] init 0;
[] m=0 & r<months & b1=1 -> (b1'=0);
[] m=0 & r<months & b1=0 & !((i1=1 & b1=0) | i1=2) -> pbar : (b1'=1) + 1-pbar : (b1'=0);
endmodule
module market2 = market1[b1=b2,i1=i2] endmodule
module market3 = market1[b1=b3,i1=i3] endmodule
module value
v : [0..10] init 5;
[] m=1 -> p/10 : (v'=min(v+1,c)) + (1-p/10) : (v'=min(max(v-1,0),c));
endmodule
module probability
p : [0..10] init 5;
[] m=1 & v<5 -> 2/3 : (p'=min(p+1,10)) + 1/3 : (p'=max(p-1,0));
[] m=1 & v=5 -> 1/2 : (p'=min(p+1,10)) + 1/2 : (p'=max(p-1,0));
[] m=1 & v>5 -> 1/3 : (p'=min(p+1,10)) + 2/3 : (p'=max(p-1,0));
endmodule
module cap
c : [0..10] init 10;
[] m=1 -> 1/2 : (c'=max(c-1,0)) + 1/2 : (c'=c);
endmodule
label "cashed_in1" = m=0 & (i1=2 | ((i1=0 | i1=1 & b1=1) & r=months));
label "cashed_in2" = m=0 & (i2=2 | ((i2=0 | i2=1 & b2=1) & r=months));
label "cashed_in3" = m=0 & (i3=2 | ((i3=0 | i3=1 & b3=1) & r=months));
label "cashed_in12" = m=0 & (i1=2 | ((i1=0 | i1=1 & b1=1) & r=months)) & (i2=2 | ((i2=0 | i2=1 & b2=1) & r=months));
rewards "profit1"
[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) & !(i3=1 & b3=0) : v;
[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) & i3=1 & b3=0 : v*(3/4);
[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 & !(i3=1 & b3=0) : v*(3/4);
[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 & i3=1 & b3=0 : v*(1/2);
endrewards
rewards "profit2"
[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & !(i3=1 & b3=0) : v;
[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & i3=1 & b3=0 : v*(3/4);
[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & !(i3=1 & b3=0) : v*(3/4);
[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & i3=1 & b3=0 : v*(1/2);
endrewards
rewards "profit3"
[cashin3] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & !(i3=1 & b3=0) : v;
[cashin3] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & i3=1 & b3=0 : v*(3/4);
[cashin3] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & !(i3=1 & b3=0) : v*(3/4);
[cashin3] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & i3=1 & b3=0 : v*(1/2);
endrewards