dtmc

// unknown parameters for new component implementations
param pAuthSUCC : observations = 1 1 ; component = 1 ; cost = 3.7 ;         // p_{a}
param pStdShippingSUCC : observations = 1 1 ; component = 2 ; cost = 4.4 ;  // p_{ss}
param pFastShippingSUCC : observations = 1 1 ; component = 3 ; cost = 2.6 ; // p_{fs}
param pPaymentSUCC : observations = 1 1 ; component = 4 ; cost = 1.5 ;      // p_{p}


// known parameters for existing component implementations
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 OnlineShoppingWebApplication
  s : [0..16] init 0;

  // authentication component use (login)
  [] (s=0) -> (pAuthSUCC):(s'=2) + (1-pAuthSUCC):(s'=5);
  [] (s=5) -> true; // absorbing state for authentication component failure
 
  // partitioning 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 component use (fast)
  [] (s=10) -> (pFastShippingSUCC):(s'=11) + (1-pFastShippingSUCC):(s'=13);
  [] (s=13) -> true; // absorbing state for fast shipping failure
 
  // shipping service use (standard)
  [] (s=12) -> (pStdShippingSUCC):(s'=11) + (1-pStdShippingSUCC):(s'=15);
  [] (s=15) -> true; // absorbing state for standard shipping failure

  // authentication component use (logout)
  [] (s=14) -> (pAuthSUCC):(s'=16)+(1-pAuthSUCC):(s'=5);
  [] (s=16) -> true; // absorbing state modelling logout success
 
  // payment component use (payment)
  [] (s=11) -> (pPaymentSUCC):(s'=14) + (1-pPaymentSUCC):(s'=8);
  [] (s=8) -> true; // absorbing state modelling payment failure
endmodule


// counter of new component uses
rewards
  (s=0)  : 1;   // authentication (login)
  (s=10) : 1;   // fast shipping
  (s=11) : 1;   // payment
  (s=12) : 1;   // standard shipping
  (s=14) : 1;   // authentication (logout)
endrewards


label "success" = (s=16);
label "authFail" = (s=5);
label "done" = (s=15)|(s=5)|(s=13)|(s=8)|(s=16);