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

csg

player investor1 investor1 endplayer
player investor2 investor2 endplayer
player market market endplayer
	
const int months; // number of months

// 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)) -> (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))) -> 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)
endmodule

// investor 2
module investor2=investor1[i1=i2,b1=b2,noinvest1=noinvest2,invest1=invest2,cashin1=cashin2] 
endmodule

// the market
module market
	b1 : [0..1] init 1; // initially cannot bar
	b2 : [0..1] init 1; // initially cannot bar
    	// b=0 - not barred and b=1 - barred
    	
    	// do not bar this month
    	[nobar] m=0 & r<months & !(((i1=1 & b1=0) | i1=2) & ((i2=1 & b2=0) | i2=2)) -> (b1'=0) & (b2'=0); 
    	// bar 1 this month (cannot have barred previous month) 
    	[bar1] m=0 & b1=0 & r<months & !((i1=1 & b1=0) | i1=2) -> (b1'=1) & (b2'=0); 
    	// bar 2 this month (cannot have barred previous month) 
    	[bar2] m=0 & b2=0 & r<months & !((i2=1 & b2=0) | i2=2) -> (b2'=1) & (b1'=0);
    	// bar 1 and 2 this month (cannot have barred previous month) 
    	[bar12] m=0 & b1=0 & b2=0 & r<months & !(((i1=1 & b1=0) | i1=2) & ((i2=1 & b2=0) | i2=2)) -> (b1'=1) & (b2'=1); 
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 "finished1" = m=0 & (i1=2 | ((i1=0 | i1=1 & b1=1) & r=months));
label "finished2" = m=0 & (i2=2 | ((i2=0 | i2=1 & b2=1) & r=months));
label "finished12" = 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) : v; // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*0.75; // both cash in
endrewards

// normal market - both investors
// (profit equals share value)
rewards "profit12"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) : v; // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*0.75; // both cash in
	[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) : v; // cash in alone
	[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 : v*0.75; // both cash in
endrewards

// later cash-ins - investor 1
// (profit increases for same share value if cashed-in later)
rewards "profit1_lc"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) : v*(1 + (r-1)/months); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*(1 + (r-1)/months)*0.75; // both cash in
endrewards

// later cash-ins - both investors
// (profit increases for same share value if cashed-in later)
rewards "profit12_lc"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) : v*(1 + (r-1)/months); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*(1 + (r-1)/months)*0.75; // both cash in
	[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) : v*(1 + (r-1)/months); // cash in alone
	[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 : v*(1 + (r-1)/months)*0.75; // both cash in
endrewards

// later cash-ins with fluctuations - investor 1
//  (profit increases for same share value if cashed-in later but there are fluctuations)
rewards "profit1_mc"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) : v*(1 + (r-1)/months)*(1 + mod(r,4)/3); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*(1 + (r-1)/months)*(1 + mod(r,4)/3)*0.75; // both cash in
endrewards

// later cash-ins with fluctuations - both investors
//  (profit increases for same share value if cashed-in later but there are fluctuations)
rewards "profit12_mc"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) : v*(1 + (r-1)/months)*(1 + mod(r,4)/3); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*(1 + (r-1)/months)*(1 + mod(r,4)/3)*0.75; // both cash in
	[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) : v*(1 + (r-1)/months)*(1 + mod(r,4)/3); // cash in alone
	[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 : v*(1 + (r-1)/months)*(1 + mod(r,4)/3)*0.75; // both cash in
endrewards


// earlier cash-ins - investor 1
//  (profit increases for same share value if cashed-in earlier)
rewards "profit1_ec"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) : v*(1 + months/(5*(r+1))); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*(1 + months/(5*(r+1)))*0.75; // both cash in
endrewards

// earlier cash-ins - both investors
//  (profit increases for same share value if cashed-in earlier)
rewards "profit12_ec"
	[cashin1] m=0 & i1=1 & b1=0 & !(i2=1 & b2=0) : v*(1 + months/(5*(r+1))); // cash in alone
	[cashin1] m=0 & i1=1 & b1=0 & i2=1 & b2=0 : v*(1 + months/(5*(r+1)))*0.75; // both cash in
	[cashin2] m=0 & i2=1 & b2=0 & !(i1=1 & b1=0) : v*(1 + months/(5*(r+1))); // cash in alone
	[cashin2] m=0 & i2=1 & b2=0 & i1=1 & b1=0 : v*(1 + months/(5*(r+1)))*0.75; // both cash in
endrewards