// Futures market investor (McIver and Morgan 2007)
// Extended to two investors, probabilistic market

csg

player investor1 investor1 endplayer
player investor2 investor2 endplayer
player investor3 investor3 endplayer
	
const int months; // number of months
const double pbar;

// module use to decide who can move
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); // start of month: invest and bar decision
	[] m=1 -> (m'=0) & (r'=r+1); // shares change value
	[] m=0 & !(r<months & (!((i1=1 & b1=0) | i1=2) | !((i2=1 & b2=0) | i2=2) | !((i3=1 & b3=0) | i3=2))) -> true; // loop when finished
	// finished: either investors cashed in or reached final round and cannot cash in
endmodule

// investor 1
module investor1
	i1 : [0..2]; // i1=0 no reservation, i1=1 made reservation, i1=2 cashed in (done)
	[noinvest1] m=0 & (i1=0 | (i1=1 & b1=1)) & r<months -> (i1'=0); // do nothing
	[invest1] m=0 & (i1=0 | (i1=1 & b1=1)) & r<months -> (i1'=1); // make reservation
	[cashin1] m=0 & i1=1 & b1=0 -> (i1'=2); // cash in shares (not barred)
	[end1] m=0 & (i1=0 | (i1=1 & b1=1)) & r=months -> (i1'=2);
endmodule

// investor 2
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

// the market
// baring first investor
module market1
	b1 : [0..1] init 0;
	//barred previous month
	[] m=0 & r<months & b1=1 -> (b1'=0);
	// barr investor1
	[] m=0 & r<months & b1=0 & !((i1=1 & b1=0) | i1=2) -> pbar : (b1'=1) + 1-pbar : (b1'=0);
endmodule

// barring second
module market2 = market1[b1=b2,i1=i2] endmodule
module market3 = market1[b1=b3,i1=i3] endmodule

// value of the shares
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

// probability of shares going up/down
module probability
	p : [0..10] init 5; // probabilitity is p/10 and initially the probability is 1/2
	[] 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

// cap on the value of the shares
module cap
	c : [0..10] init 10; // cap on the shares
	// probability 1/2 the cap decreases
	[] m=1 -> 1/2 : (c'=max(c-1,0)) + 1/2 : (c'=c); 
endmodule

// labels
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));

// normal market - investor 1
// (profit equals share value)
rewards "profit1"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) & !(i3=1 & b3=0) : v; // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) & i3=1 & b3=0 : v*(3/4); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0    & !(i3=1 & b3=0) : v*(3/4); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 & i3=1 & b3=0 : v*(1/2); // both cash in
endrewards

// normal market - investor 2
// (profit equals share value)
rewards "profit2"
	[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & !(i3=1 & b3=0) : v; // cash in alone
	[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & i3=1 & b3=0 : v*(3/4); // cash in alone
	[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & !(i3=1 & b3=0) : v*(3/4); // cash in alone
	[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & i3=1 & b3=0 : v*(1/2); // both cash in
endrewards

rewards "profit3"
	[cashin3] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & !(i3=1 & b3=0) : v; // cash in alone
	[cashin3] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) & i3=1 & b3=0 : v*(3/4); // both cash in
	[cashin3] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & !(i3=1 & b3=0) : v*(3/4); // both cash in
	[cashin3] m=0 & i2=1 & b2=0 & i1=1 & b1=0 & i3=1 & b3=0 : v*(1/2); // both cash in
endrewards