//Expand Components v 1.0 Nov 2018

//Annotated model for FXWorkflow.
//MODEL_PARAMETERS
//prob, cost, time
//MODEL_PATTERNS
/// 1:SEQ-R1(p11,c11,t11,p12,c12,t12,r1)
/// 2:SEQ-R1(p21,c21,t21,p22,c22,t22,r2)
/// 3:SEQ-R1(p31,c31,t31,p32,c32,t32,r3)
/// 4:SEQ-R1(p41,c41,t41,p42,c42,t42,r4)
/// 5:SEQ-R1(p51,c51,t51,p52,c52,t52,r5)
/// 6:SEQ-R1(p61,c61,t61,p62,c62,t62,r6)
//MONOLITHIC
//1,2,9;2,7,9;3,6,9;4,8,9;5,6,9;6,10,9
dtmc
const int INITSTATE = 0;
const int OP1 = 1;
const int OP2 = 2;
const int OP3   = 3;
const int OP4   = 4;
const int OP5   = 5;
const int OP6   = 6;
const int TA_RESULT = 7;
const int FA_RESULT = 8;
const int WF_FAIL=9;
const int WF_SUCC=10;

const double prob1;
const double prob2;
const double prob3;
const double prob4;
const double prob5;
const double prob6;
const double cost1;
const double cost2;
const double cost3;
const double cost4;
const double cost5;
const double cost6;
const double time1;
const double time2;
const double time3;
const double time4;
const double time5;
const double time6;


const double x; ///ePMC-Var
const double y1; ///ePMC-Var
const double y2; ///ePMC-Var
const double z1; ///ePMC-Var
const double z2; ///ePMC-Var

module fx
state : [0..11] init 0;
//Init
[choice] state = INITSTATE -> x : (state'=OP1) + (1-x) : (state'=OP4);
//Technical analysis result
[taResult] state=TA_RESULT-> y2:(state'=OP1)+y1:(state'=OP5)+(1-y1-y2):(state'=OP3);
//Fundamental analysis result
[faresult] state=FA_RESULT->z2:(state'=INITSTATE)+z1:(state'=OP5)+(1-z1-z2):(state'=OP4);//succ op4
//success or failure of workflow.
[success] state = WF_SUCC -> 1.0:(state'=INITSTATE);
[failure] state=WF_FAIL->1.0:(state'=WF_FAIL);//failed fx


//Op1: Market watch
[marketwatch] state = OP1->prob1:(state'=OP2)+(1-prob1):(state'=WF_FAIL);  //invoke op1
//Op2: Technical Analysis
[techanalysis]state = OP2->prob2:(state'=TA_RESULT)+(1-prob2):(state'=WF_FAIL);//invoke op2
//Op3: Alarm
[alarm] state=OP3->prob3:(state'=OP6)+(1-prob3):(state'=WF_FAIL);
//Op4: Fundamental Analysis
[fundanalysis] state=OP4->prob4:(state'=FA_RESULT)+(1-prob4):(state'=WF_FAIL);
//Op5: Place Order
[placeorder]state=OP5->prob5:(state'=OP6)+(1-prob5):(state'=WF_FAIL);
//Op6: Notify trader
[notification]state=OP6->prob6:(state'=WF_SUCC)+(1-prob6):(state'=WF_FAIL);
endmodule


rewards "time"
state=OP1 : time1;
state=OP2 : time2;
state=OP3 : time3;
state=OP4 : time4;
state=OP5 : time5;
state=OP6 : time6;
endrewards

rewards "cost"
state=OP1 : cost1;
state=OP2 : cost2;
state=OP3 : cost3;
state=OP4 : cost4;
state=OP5 : cost5;
state=OP6 : cost6;
endrewards