// futures market investor (McIver and Morgan 2007)

csg

player investor investor 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 & !((i=1 & b=0) | i=2) -> (m'=1); // start of month: invest and bar decision
	[] m=1 & r<months -> (m'=0) & (r'=r+1); // end of month: shares change value
	[] m=0 & (i=2 | (r=months & (i=0 | (i=1 & b=1)))) -> true; // loop when finished
	// finished: either cashed in or run out of months
endmodule

module investor
	i : [0..2]; // i - 0 no reservation, i - 1 made reservation, i - 2 cashed in
	[noinvest] m=0 & (i=0 | (i=1 & b=1)) & r<months -> (i'=0); // do nothing
	[invest] m=0 & (i=0 | (i=1 & b=1)) & r<months -> (i'=1); // make reservation
	[cashin] m=0 & i=1 & b=0 -> (i'=2); // cash in shares (not barred)
endmodule

module market
	b : [0..1] init 1; // initially cannot bar
    	// b=0 not barred and b=1 barred
	[nobar] m=0 & r<months & !((i=1 & b=0) | i=2) -> (b'=0); // do not bar this month
	[bar] m=0 & b=0 & r<months & !((i=1 & b=0) | i=2) -> (b'=1); // bar this month (cannot have barred previous month) 
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;
	[] 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
	[] m=1 -> 1/2 : (c'=max(c-1,0)) + 1/2 : (c'=c); // probability 1/2 the cap decreases
endmodule

// labels
label "finished" = m=0 & (i=2 | ((i=0 | i=1 & b=1) & r=months));

// normal market
// (profit equals share value)
rewards "profit"
	[cashin] m=0 & i=1 & b=0 : v;
endrewards 

// later cash-ins 
// (profit increases for same share value if cashed-in later)
rewards "profit_lc"
	[cashin] m=0 & i=1 & b=0 : v * (1 + (r-1)/months); // cash in
endrewards 

// later cash-ins with fluctuations
//  (profit increases for same share value if cashed-in later but there are fluctuations)
rewards "profit_mc"
	[cashin] m=0 & i=1 & b=0 : v * (1 + (r-1)/months) * (1 + mod(r,4)/3);
endrewards

// early cash-ins
//  (profit increases for same share value if cashed-in earlier)
rewards "profit_ec"
	[cashin] m=0 & i=1 & b=0 : v * (1 + months/(5*(r+1))); // cash in
endrewards