PRISM code for qMu futures example

// EXAMPLE: INVESTING IN THE FUTURES MARKET
// (McIver and Morgan 03)
// Script prepared by Gethin Norman (sep03)

nondeterministic

//-------------------------------------------------------------
// THE INVESTOR
module investor
	
	i : [0..1];
	// 0 initial (no reservation)
	// 1 made reservation

	[invest] (i=0) -> (i'=0); // do nothing
	[invest] (i=0) -> (i'=1); // make reservation

	[invest] (i=1) & (b=1) -> (i'=0); // barred so try again and do nothing
	[invest] (i=1) & (b=1) -> (i'=1); // barred so try again and make reservation
	[done]   (i=1) & (b=0) -> (i'=1); // cash in shares

endmodule

//------------------------------------------------------------
// VALUE OF THE SHARES
module value
	
	v : [0..10] init 10;

	[month] true -> 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

	[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

//-------------------------------------------------------------
// CAP ON THE VALUE OF THE SHARES
module cap
	
	c : [0..10] init 10; // cap on the shares

	[month] true -> 1/2 : (c'=max(c-1,0)) + 1/2 : (c'=c); // probability 1/2 the cap decreases

endmodule

//-------------------------------------------------------------
// BAR ON THE INVESTOR
module barred
	
	b : [0..1] init 1; // (initially cannot bar)
	// 0 - not barred
	// 1 - barred

	[invest] true  -> (b'=0); // no bar next month
	[invest] (b=0) -> (b'=1); // bar next month 

endmodule

//-------------------------------------------------------------
// MONTH IN THE MARKET
module month
	
	m : [0..1];
	// 0 - investor makes his choice at start of the month, then...
	// 1 - value of shares, cap and probability change through one month stock market activity

	[invest] (m=0) -> (m'=1); // investor makes his/her choice
	[month] (m=1) -> (m'=0); // one month passes

	[done] (m=0) -> (m'=0); // once investor cashes in nothing changes

endmodule