// Tele-Assistance System (TAS) from Baresi et al. (2007)
// Parametric Markov chain adapted from Calinescu et al. (2013)

probabilistic


const double pAlarm = 0.8800362098297202 ;
const double pPharmacy = 0.8709937565036421 ;
const double pAnalysis = 0.9700562922783393 ;

// known probabilities of different outcomes 
const double p_analyzeData_sendAlarm = 0.004; 
const double p_analyzeData_changeDrug = 0.3; 
const double p_analyzeData_doNothing = 0.696; 
const double p_request_sendAlarm = 0.1;
const double p_request_analyzeData = 0.9;

module TeleAssistance
  a : [0..10] init 0;

  [initial]        (a=0)  ->  1.0:(a'=2); //request?
  [final]          (a=1)  ->  true; //FINAL
  [request]     (a=2)  ->  p_request_sendAlarm:(a'=5) + 
                              p_request_analyzeData:(a'=3);
  [analysis]       (a=3)  ->  pAnalysis:(a'=4) + (1-pAnalysis):(a'=9);
  [result]         (a=4)  ->  p_analyzeData_sendAlarm:(a'=5) + 
                              p_analyzeData_changeDrug:(a'=6)+
                                             p_analyzeData_doNothing:(a'=10);
  [alarm]                (a=5)  ->  pAlarm:(a'=10) + (1-pAlarm):(a'=7);
  [pharmacy]          (a=6)  ->  pPharmacy:(a'=10) + (1-pPharmacy):(a'=8);
  [failedAlarm]        (a=7)  ->  1.0:(a'=10); //failed send alarm
  [failedPharmacy]  (a=8)  ->  1.0:(a'=10); //failed changed drug
  [failedAnalysis]    (a=9)  ->  1.0:(a'=10); //failed analysis
  [done]                 (a=10) ->  0.02:(a'=1) + 0.98:(a'=0); //stop prob 0.02
endmodule

rewards "cost"
  (a=5) :  2.7; //cost of invoking alarm 
  (a=3) :  0.03;//cost of invoking analysis 
  (a=6) :  0.24;//cost of invoking drug 
endrewards

// labels
label "done" = a=10;
label "failedAlarm" = a=7; 
label "failedService" = a=7|a=8|a=9; 
label "final" = a=1;
label "analysis" = a=3;