smg
player investor1 [invest1], [noinvest1], [cashin1] endplayer
player investor2 [invest2], [noinvest2], [cashin2] endplayer
player market [nobar], [bar1], [bar2], sched, [month], [done] endplayer
const double pterm = 0.01;
module sched
term: [0..1];
t: [0..3];
m1 : [0..2];
m2 : [0..2];
[] t=0 & m1=0 & i1!=2 & term=0 -> (1-pterm):(t'=1) + pterm:(term'=1);
[] t=0 & m2=0 & i2!=2 & term=0 -> (1-pterm):(t'=2) + pterm:(term'=1);
[] t=0 & (m1!=0 | i1=2) & (m2!=0 | i2=2) & term=0 -> (t'=3);
[noinvest1] m1=0 & t=1 -> (m1'=1) & (t'=0);
[invest1] m1=0 & t=1 -> (m1'=1) & (t'=0);
[noinvest2] m2=0 & t=2 -> (m2'=1) & (t'=0);
[invest2] m2=0 & t=2 -> (m2'=1) & (t'=0);
[nobar] (m1=1 | i1=2) & (m2=1 | i2=2) & t=3 & !(i1=2 & i2=2) -> (m1'=2) & (m2'=2);
[bar1] m1=1 & t=3 -> (m1'=2) & (m2'=2);
[bar2] m2=1 & t=3 -> (m1'=2) & (m2'=2);
[month] m1=2 & m2=2 -> (m1'=0) & (m2'=0) & (t'=0);
[cashin1] m1=0 & t=1 -> (m1'=0) & (t'=0);
[cashin2] m2=0 & t=2 -> (m2'=0) & (t'=0);
[done] m1=0 & m2=0 & t=3 | term=1 -> true;
endmodule
module investor1
i1 : [0..2];
[noinvest1] i1=0 | i1=1 & b1=1 -> (i1'=0);
[invest1] i1=0 | i1=1 & b1=1 -> (i1'=1);
[cashin1] i1=1 & b1=0 -> (i1'=2);
[done] i1=2 | term=1-> true;
endmodule
module investor2 = investor1 [
i1=i2,
b1=b2,
noinvest1=noinvest2,
invest1=invest2,
cashin1=cashin2
]
endmodule
const vmax=10;
const vinit=5;
module market
b1 : [0..1] init 1;
b2 : [0..1] init 1;
v : [0..vmax] init vinit;
[nobar] true -> (b1'=0) & (b2'=0);
[bar1] b1=0 -> (b1'=1) & (b2'=0);
[bar2] b2=0 -> (b2'=1) & (b1'=0);
[month] true -> p/10 : (v'=up)
+ (1-p/10) : (v'=down);
endmodule
const int pmax = 10;
module probability
p : [0..pmax] init floor(pmax/2);
[month] (v<5) -> 2/3 : (p'=min(p+1,pmax)) + 1/3 : (p'=max(p-1,0));
[month] (v=5) -> 1/2 : (p'=min(p+1,pmax)) + 1/2 : (p'=max(p-1,0));
[month] (v>5) -> 1/3 : (p'=min(p+1,pmax)) + 2/3 : (p'=max(p-1,0));
endmodule
const int cmax = vmax;
module cap
c : [0..cmax] init cmax;
[month] true -> 1/2 : (c'=max(c-1,0)) + 1/2 : (c'=c);
endmodule
label "done" = i1=2 & i2=2;
label "done1" = i1=2;
label "done2" = i2=2;
formula up = min(v+1,c,vmax);
formula down = min(max(v-1,0),c);
rewards "profit1"
[cashin1] i1=1 : v;
endrewards
rewards "profit2"
[cashin2] i2=1 : v;
endrewards
rewards "profit12"
[cashin1] i1=1 : v;
[cashin2] i2=1 : v;
endrewards