// futures market investor (McIver and Morgan 2007)

smg

player investor [invest], [noinvest], [cashin], [done] endplayer
player market [bar], [nobar], [month] endplayer

const int months; // number of months

// scheduler use to synchronise system transitions
module sched
	m : [0..2];
	r : [0..months];
	// at the start of the month, investor makes decision or cashes in
	[noinvest] m=0 & r<months -> (m'=1); 
	[invest] m=0 & r<months -> (m'=1);
	[cashin] m=0 -> true;
	// then, decision is made whether to bar or not
	[bar] m=1 -> (m'=2);
	[nobar] m=1 -> (m'=2);
	// then, market changes
	[month] m=2 & r<months -> (m'=0) & (r'=r+1);
	[done] m=0 & (i=2 | ((i=0 | i=1 & b=1) & r=months)) -> true; // loop when finished
	// finished: investor 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
	// decide whether to do nothing or make reservation
	// (if currently not reserving or was barred last time)
	[noinvest] (i=0 | i=1 & b=1) -> (i'=0);
	[invest] (i=0 | i=1 & b=1) -> (i'=1);
	// cash in shares (if not barred)
	[cashin] i=1 & b=0 -> (i'=2);

endmodule

// bar on the investor
module barred
	b : [0..1] init 1; // initially cannot bar
	// b=0 not barred and b=1 barred
	// bar or not bar (cannot if do so last month)
	[nobar] true -> (b'=0);
	[bar] b=0 -> (b'=1);
endmodule

// value of the shares
module value	
	v : [0..10] init 5;
	[month] true -> p/10 : (v'=min(v+1,c,10)) + (1-p/10) : (v'=min(max(v-1,0),c));
endmodule

// probability of shares going up/down
module probability
	p : [0..10] init 5;
	[month] (v<5) -> 2/3 : (p'=min(p+1,10)) + 1/3 : (p'=max(p-1,0));
	[month] (v=5) -> 1/2 : (p'=min(p+1,10)) + 1/2 : (p'=max(p-1,0));
	[month] (v>5) -> 1/3 : (p'=min(p+1,10)) + 2/3 : (p'=max(p-1,0));
endmodule

module cap	
	c : [0..10] init 10;
	[month] true -> 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