//MonoGenerator Tool Version 1.0
//efact

//MODEL_PARAMETERS
//prob, cost, time
//MODEL_PATTERNS
//1:SEQR1-3;2:SEQR1-3;3:SEQR1-3;4:SEQR1-3;5:SEQR1-3;6:SEQR1-3
/// 1:SEQ-R1(p111,c11,t11,r11,p121,c12,t12,r12,p131,c13,t13,r13)
/// 2:SEQ-R1(p211,c21,t21,r21,p221,c22,t22,r22,p231,c23,t23,r23)
/// 3:SEQ-R1(p311,c31,t31,r31,p321,c32,t32,r32,p331,c33,t33,r33)
/// 4:SEQ-R1(p411,c41,t41,r41,p421,c42,t42,r42,p431,c43,t43,r43)
/// 5:SEQ-R1(p511,c51,t51,r51,p521,c52,t52,r52,p531,c53,t53,r53)
/// 6:SEQ-R1(p611,c61,t61,r61,p621,c62,t62,r62,p631,c63,t63,r63)

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=0.9;
const double y1=0.5;
const double y2=0.2;
const double z1=0.2;
const double z2=0.5;

param p11 : observations = 100 1 ; component = 1 ; cost = 1.0 ;
param p21 : observations = 100 1 ; component = 2 ; cost = 1.0 ;
param p31 : observations = 100 1 ; component = 3 ; cost = 1.0 ;
param p41 : observations = 100 1 ; component = 4 ; cost = 1.0 ;
param p51 : observations = 100 1 ; component = 5 ; cost = 1.0 ;
param p61 : observations = 100 1 ; component = 6 ; cost = 1.0 ;
param p12 : observations = 100 1 ; component = 7 ; cost = 1.0 ;
param p22 : observations = 100 1 ; component = 8 ; cost = 1.0 ;
param p32 : observations = 100 1 ; component = 9 ; cost = 1.0 ;
param p42 : observations = 100 1 ; component = 10 ; cost = 1.0 ;
param p52 : observations = 100 1 ; component = 11 ; cost = 1.0 ;
param p62 : observations = 100 1 ; component = 12 ; cost = 1.0 ;
param p13 : observations = 100 1 ; component = 13 ; cost = 1.0 ;
param p23 : observations = 100 1 ; component = 14 ; cost = 1.0 ;
param p33 : observations = 100 1 ; component = 15 ; cost = 1.0 ;
param p43 : observations = 100 1 ; component = 16 ; cost = 1.0 ;
param p53 : observations = 100 1 ; component = 17 ; cost = 1.0 ;
param p63 : observations = 100 1 ; component = 18 ; cost = 1.0 ;

const double c11=1.0;
const double t11=2.0;
const double c21=1.2;
const double t21=1.0;
const double c31=1.5;
const double t31=2.1;
const double c41=1.3;
const double t41=2.2;
const double c51=1.9;
const double t51=2.4;
const double c61=1.1;
const double t61=2.2;

const double c12=1.3;
const double t12=2.7;
const double c22=1.7;
const double t22=2.4;
const double c32=1.2;
const double t32=1.1;
const double c42=1.4;
const double t42=2.3;
const double c52=1.0;
const double t52=2.5;
const double c62=1.5;
const double t62=2.8;

const double c13=1.2;
const double t13=1.9;
const double c23=2.0;
const double t23=2.1;
const double c33=1.1;
const double t33=1.5;
const double c43=1.2;
const double t43=2.3;
const double c53=1.7;
const double t53=2.2;
const double c63=1.6;
const double t63=1.9;

const double r11 = 0.01;
const double r12 = 0.01;
const double r13 = 0.01;

const double r21 = 0.01;
const double r22 = 0.01;
const double r23 = 0.01;

const double r31 = 0.01;
const double r32 = 0.01;
const double r33 = 0.01;

const double r41 = 0.01;
const double r42 = 0.01;
const double r43 = 0.01;

const double r51 = 0.01;
const double r52 = 0.01;
const double r53 = 0.01;

const double r61 = 0.01;
const double r62 = 0.01;
const double r63 = 0.01;
module vex
inter : [1..2] init 1;
retry : [1..2] init 1;
op1 : [1..3] init 1;
op2 : [1..3] init 1;
op3 : [1..3] init 1;
op4 : [1..3] init 1;
op5 : [1..3] init 1;
op6 : [1..3] init 1;
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