// DTMC model for an e-commerce application: 
//From: A formal approach to adaptive software: continous assurance of non-functional requirements 

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


//Reliability requirements formulated as PCTL PROPERTIES

//The probability of eventually reaching state 16, corresponding to the successful completetion of the workflow
//P>0.8[F (s=16)]

//the probability of eventually reaching state 13, corresponding to a failed express shipment, given that
//the customer is a returning customer
//filter(forall,P<=0.035[F(s=13)],s=1)


//filter(max,P=?[F(s=13)],s=1)
//This gives the maximum value, starting from any state satisfying s=1, 
//of the probability of reaching the express service "fail" state 13



//the probability of eventually reaching the failed login state is less than 0.06
//P<0.06[F s=5]


dtmc
label "wfSUCC" = (s=16);
label "wfFAIL" = (s=15)|(s=5)|(s=13)|(s=8);

//paramaters for reliability learning
const double pAuthSUCC = %authorize_p; //1- 0.03;
const double pNormShippingSUCC = %normalShipping_p;// 1-0.05;
const double pExpShippingSUCC =  %expressShipping_p;//1- 0.02;
const double pPaymentSUCC=   %payment_p;// 1- 0.01;

//costs of services
rewards
 (s=0) : %authorize_COST;   //authentication service
(s=10) : %expressShipping_COST;  //express shipping
(s=11) : %payment_COST; //payment
(s=12) : %normalShipping_COST;  //normal shipping
(s=14) : %authorize_COST;  //authentication (logout)
endrewards


//constant for learning transitions 
const double p_RETURNBUY_SEARCH = 0.2;
const double p_RETURNBUY_EXPRESS = 0.5;
const double p_RETURNBUY_NORMAL = 0.3;


const double p_NEWBUY_SEARCH = 0.15;
const double p_NEWBUY_EXPRESS = 0.25;
const double p_NEWBUY_NORMAL = 0.6;

const double p_PROFILER_NEW = 0.65;
const double p_PROFILER_RETURN = 0.35;

module ecommercewf
s : [0..16] init 0;

//authentication service invocation (login)
[](s=0) -> (pAuthSUCC):(s'=2) + (1-pAuthSUCC):(s'=5);
[] (s=5) -> true;//absorbing state modelling login failure
 
//paritioning of new/returning customers.
[] (s=2) -> p_PROFILER_NEW:(s'=1) + p_PROFILER_RETURN:(s'=3);

[] (s=1) -> 1:(s'=4);
[] (s=4) -> 1:(s'=7);
[] (s=3) -> 1:(s'=6);
[] (s=6) -> 1:(s'=9);

//choice between shipping method or continuing search (returning user)
[] (s=7) -> p_RETURNBUY_SEARCH:(s'=4)+p_RETURNBUY_EXPRESS:(s'=10)+p_RETURNBUY_NORMAL:(s'=12);

//choice between shipping method or continung search (new user)
[] (s=9) -> p_NEWBUY_EXPRESS:(s'=10) + p_NEWBUY_NORMAL:(s'=12) + p_NEWBUY_SEARCH:(s'=9);


//Shipping service invocation (express)
[] (s=10) -> (pExpShippingSUCC):(s'=11) + (1-pExpShippingSUCC):(s'=13);
[] (s=13) -> true;//express shipping failure
 

//Shipping service invocation (normal)
[] (s=12) -> (pNormShippingSUCC):(s'=11) + (1-pNormShippingSUCC):(s'=15);
[] (s=15) -> true;//normal shipping failure

 
//authentication service invocation (logout)
[] (s=14) -> (pAuthSUCC):(s'=16)+(1-pAuthSUCC):(s'=5);
[] (s=16) -> true;//absorbing state modelling logout success
 

//payment service invocation (payment)
[] (s=11) -> (pPaymentSUCC):(s'=14) + (1-pPaymentSUCC):(s'=8);
[](s=8) -> true;//payment failure

endmodule