//DTMC MODEL FOR TRAVEL ASSISTANT. 
//adapted from: 
//L. Zeng, B. Benatallah, A. H.H. Ngu, M. Dumas, J. Kalagnanam, and H. Chang, 
//“Qos-aware middleware for web services composition,” IEEE Trans. Softw. Eng., vol. 30, no. 5, pp. 311–327, May 2004.

// 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 pFlight   = %Flight_p;//1 - 0.01;
const double pHotel    = %Hotel_p;//1 - 0.01;
const double pBike     = %Bike_p;//1 - 0.01;
const double pCar      = %Car_p;//1 - 0.01;
const double pAttract  = %Attract_p;//1 - 0.01;

//non-parameterised for now.
//const double pDistance = 1 - 0.01;
const double N = 10.0; // Expected number of workflow executions before STOP
const double pStop = 1.0/(N + 1);  



//transitions parameters
//TODO: ADD TRANSITION PARAMETERS


rewards
(s=2) : %Attract_COST;
(s=3) : %Flight_COST;
(s=6) : %Hotel_COST;
(s=10): %Car_COST;
(s=11): %Bike_COST;
endrewards


module traveladvisor

s : [0..14] init 0;

//request
[] (s=0) -> (s'=1);

//look for attractions or book flights
[] (s=1) -> 0.1:(s'=2) + 0.9:(s'=3);

[] (s=2) -> pAttract:(s'=8) + (1-pAttract):(s'=5);
[] (s=3) -> pFlight:(s'=6) + (1-pFlight):(s'=4);

[] (s=4) -> 1.0:(s'=13);
[] (s=5) -> 1.0:(s'=13);

[] (s=6) -> pHotel:(s'=8) + (1-pHotel):(s'=7);

[] (s=7) -> 1.0:(s'=13);


//car or bike?
[] (s=8) -> 0.7:(s'=10) + 0.3:(s'=11);

[] (s=9) -> 1.0:(s'=13);


[] (s=10) -> pCar:(s'=13) + (1-pCar):(s'=9);
[] (s=11) -> pBike:(s'=13) + (1-pBike):(s'=12);

[] (s=12) -> 1.0:(s'=13);
[] (s=13) -> pStop:(s'=14)+ (1-pStop):(s'=0);
[] (s=14) -> true;

endmodule