// 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