smg

//Environment actions control failures in the model and retry procedure that happens afterwards
player env
	[web_stock_0_fail],	[web_stock_1_fail],	[web_stock_2_fail],
	[retry_stock], [loop]
endplayer
//Each controller actiond models stock query using a different data provider
player controller
	[web_stock_0],	[web_stock_1],	[web_stock_2]
 endplayer
 //------------------------------------------------------------------------
const int    max_retry;//Maximum number of retries
const int    stock_to_query;//Number of stocks to query
const int    web_stock_number=3;//Number of data providers
const double web_stock_0_fail=0.001;//Probability of failure for each data provider
const double web_stock_1_fail=0.002;
const double web_stock_2_fail=0.003;
//-----------------------------------------------------------------------
module QueryStock

    web_stock_0_retry : [0..max_retry+1] init 0;
    web_stock_1_retry : [0..max_retry+1] init 0;
    web_stock_2_retry : [0..max_retry+1] init 0;

    pc : [0..5] init 0;
    last_stock_webservice : [0..web_stock_number+1] init 0;
    stock_querued : [0..stock_to_query+1] init 0;
    
    //If the number of queried stock is lower than the stock_to_query the controller can pick any data provider
    //which can fail with specified probability. In case of failure the query can be rerun until specified number
    //of retries is reached.
    [web_stock_0] (pc=0)&(stock_querued<stock_to_query)&(web_stock_0_retry<max_retry) -> (pc'=1)&(last_stock_webservice'=0);
    [web_stock_0_fail] (pc=1)&(last_stock_webservice=0) ->(web_stock_0_fail) : (pc'=2) + (1-web_stock_0_fail) : (pc'=0)&(stock_querued'=min(stock_querued+1,stock_to_query));
    [retry_stock] (pc=2)&(last_stock_webservice=0) -> (pc'=0)&(web_stock_0_retry'=min(web_stock_0_retry+1,max_retry));
    [loop] (pc=2)&(last_stock_webservice=0)&(web_stock_0_retry=max_retry) -> (pc'=0);

    [web_stock_1] (pc=0)&(stock_querued<stock_to_query)&(web_stock_1_retry<max_retry) -> (pc'=1)&(last_stock_webservice'=1);
    [web_stock_1_fail] (pc=1)&(last_stock_webservice=1) ->(web_stock_1_fail) : (pc'=2) + (1-web_stock_1_fail) : (pc'=0)&(stock_querued'=min(stock_querued+1,stock_to_query));
    [retry_stock] (pc=2)&(last_stock_webservice=1) -> (pc'=0)&(web_stock_1_retry'=min(web_stock_1_retry+1,max_retry));
    [loop] (pc=2)&(last_stock_webservice=1)&(web_stock_1_retry=max_retry) -> (pc'=0);

    [web_stock_2] (pc=0)&(stock_querued<stock_to_query)&(web_stock_2_retry<max_retry) -> (pc'=1)&(last_stock_webservice'=2);
    [web_stock_2_fail] (pc=1)&(last_stock_webservice=2) ->(web_stock_2_fail) : (pc'=2) + (1-web_stock_2_fail) : (pc'=0)&(stock_querued'=min(stock_querued+1,stock_to_query));
    [retry_stock] (pc=2)&(last_stock_webservice=2) -> (pc'=0)&(web_stock_2_retry'=min(web_stock_2_retry+1,max_retry));
    [loop] (pc=2)&(last_stock_webservice=2)&(web_stock_2_retry=max_retry) -> (pc'=0);

    //If we queried for all stocks we loop indefinitely
    [loop] (pc=0)&(stock_querued=stock_to_query) -> true;
    [loop] (pc=0)&(web_stock_0_retry=max_retry)&(web_stock_1_retry=max_retry)&(web_stock_2_retry=max_retry) -> true;

endmodule

//We model different response times using rewards where reward value is specified in milliseconds
rewards "time" 

[web_stock_0] true : 100;
[web_stock_1] true : 200;
[web_stock_2] true : 300;

endrewards

//We assign penalties to actions in a way that if the static penalty is < 1 then it is 
//never the case that we block two actions in a state

rewards "penalties" 

[web_stock_0] true : 1;
[web_stock_1] true : 1;
[web_stock_2] web_stock_1_retry=max_retry | web_stock_0_retry=max_retry : 1;
[web_stock_2] web_stock_1_retry<max_retry & web_stock_0_retry<max_retry : 0.00001;

//Penalty for randomised experiments
//We assign penalties that are inverse proportional to the action reward, in such case multi-strategy would prefer to block
//actions with higher response times
//[web_stock_0] true : 1 + 1/100;
//[web_stock_1] true : 1 + 1/200;
//[web_stock_2] true : 1 + 1/300;

endrewards

label "done" = stock_querued=stock_to_query&web_stock_0_retry=0;