smg

player env
	[web_stock_0_fail],	[web_stock_1_fail],	[web_stock_2_fail],
	[retry_stock], [no_retry_stock], [loop]
endplayer
player controller
	[web_stock_0],	[web_stock_1],	[web_stock_2]
 endplayer
 //------------------------------------------------------------------------
const int    max_retry;
const int    stock_to_query;
const int    web_stock_number=3;
const double web_stock_0_fail=0.001;
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;
    new_state: [-10000..10000] init -1234;
  	purpose: [-10000..10000] init -4321;

    [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));
    [no_retry_stock] (pc=2)&(last_stock_webservice=0) -> (pc'=0)&(web_stock_0_retry'=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));
    [no_retry_stock] (pc=2)&(last_stock_webservice=1) -> (pc'=0)&(web_stock_1_retry'=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));
    [no_retry_stock] (pc=2)&(last_stock_webservice=2) -> (pc'=0)&(web_stock_2_retry'=max_retry);
    [loop] (pc=2)&(last_stock_webservice=2)&(web_stock_2_retry=max_retry) -> (pc'=0);

    [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

rewards "response_time" 

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

endrewards

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;

//Reward for randomised experiments
//[web_stock_0] true : 1 + 1/100;
//[web_stock_1] true : 1 + 1/200;
//[web_stock_2] true : 1 + 1/300;

endrewards