// EXAMPLE: INVESTING IN THE FUTURES MARKET
// (McIver and Morgan 03)

mdp

// module use to synchronize transitions
module month
    
    m : [0..1];

    [invest] (m=0) -> (m'=1); // transitions made at the start of the month synchronize on 'invest'
    [month] (m=1) -> (m'=0); // transitions made during the month synchronize on 'month'
    [done] (m=0) -> (m'=0); // once investor has cashed in shares nothing changes

endmodule

// the investor
module investor
    
    i : [0..1]; // i=0 no reservation and i=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 previous month: try again and do nothing
    [invest] (i=1) & (b=1) -> (i'=1); // barred previous month: make reservation
    [done] (i=1) & (b=0) -> (i'=1); // cash in shares (not barred)

endmodule

// bar on the investor
module barred
    
    b : [0..1] init 1; // initially cannot bar
    // b=0 - not barred and b=1 - barred

    [invest] true  -> (b'=0); // do not bar this month
    [invest] (b=0) -> (b'=1); // bar this month (cannot have barred the previous month) 

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 and initially the probability is 1/2

    [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