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