// THIS PARAMETERISED MODEL IS USED AS INPUT TO THE AUTONOMIC MANAGER AND CONTAINED PARAMETERISED VALUES
// A DEFAULT VALUE FOR EACH PARAMETER IS PROVIDED

dtmc

const double p_analyzeData_sendAlarm = 0.004; 
const double p_analyzeData_changeDrug = 0.3; 
const double p_request_sendAlarm = 0.1;
const double p_request_analyzeData = 0.9;


label "stop" = a=10;
label "FailedSendAlarm" = a=7; 
label "WF_fail" = a=7|a=8|a=9; 
label "analyseVitalParams" = a=3;  


//rewards structure that associates costs to the various service invocations
rewards
(a=5) :  %sendAlarm_COST; //cost of invoking alarm 
(a=3) :  %analyzeData_COST; //cost of invoking analysis 
(a=6) :  %changeDrug_COST;//cost of invoking drug 
endrewards

const double sendAlarm_p  = %sendAlarm_p;
const double analyzeData_p  = %analyzeData_p;
const double changeDrug_p  = %changeDrug_p;

const double N = 10.0; // Expected number of workflow executions before STOP
const double pStop = 1.0/(N + 1);  


module TAsimple
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);

[analyseVitalParams] (a=3) -> analyzeData_p:(a'=4) + (1-analyzeData_p):(a'=9);

[result] (a=4) -> p_analyzeData_sendAlarm:(a'=5) + 
                  p_analyzeData_changeDrug:(a'=6)+
                  (1-(p_analyzeData_sendAlarm + p_analyzeData_changeDrug)):(a'=10);

[sendAlarm] (a=5) -> sendAlarm_p:(a'=10) + (1-sendAlarm_p):(a'=7);
[changeDrug] (a=6) -> changeDrug_p:(a'=10) + (1-changeDrug_p):(a'=8);

[failedSendAlarm] (a=7) -> 1.0:(a'=10);//failed send alarm

[failedChangeDrug] (a=8) -> 1.0:(a'=10);//failed changed drug
[failedAnalysis] (a=9) -> 1.0:(a'=10);//failed analysis

[stop] (a=10) -> pStop:(a'=1) + (1-pStop):(a'=0);//stop?
endmodule