smg
const int N = 3;
const int K = 3;
const int L = 2;
const double Pexp=0.9;
const double eta=1;
const double gamma=0.9;
const double lambda=1;
const double Q1=1;
const double Q2=0.5;
const double Q3=0.25;
global confidence1 : [1..L];
global confidence2 : [1..L];
global confidence3 : [1..L];
global preference1 : [0..K] init 0;
global preference2 : [0..K] init 0;
global preference3 : [0..K] init 0;
global sched : [0..N];
module player0
[] sched = 0 -> 1/N : (sched'=1)
+ 1/N : (sched'=2)
+ 1/N : (sched'=3)
;
endmodule
player p1
player1, [exp1], [com1]
endplayer
module player1
[exp1] sched=1 -> 0 : true
+ 1/K * Pswitch1_1 : (preference1'=1) & (confidence1'=1) & (sched'=0)
+ 1/K * (1-Pswitch1_1) : (sched'=0)
+ 1/K * Pswitch1_2 : (preference1'=2) & (confidence1'=1) & (sched'=0)
+ 1/K * (1-Pswitch1_2) : (sched'=0)
+ 1/K * Pswitch1_3 : (preference1'=3) & (confidence1'=1) & (sched'=0)
+ 1/K * (1-Pswitch1_3) : (sched'=0)
;
[com1] sched=1 & preference1!=0 -> 0 : true
+ Pmeet_p1 * (preference1=preference2?1:0) : (confidence1'=inc_conf1) & (confidence2'=inc_conf2) & (sched'=0)
+ Pmeet_p1 * (preference1=preference2?0:1) * Pwin1_2 : (confidence1'=inc_conf1) & (preference2'=preference1) & (confidence2'=1) & (sched'=0)
+ Pmeet_p1 * (preference1=preference2?0:1) * (1-Pwin1_2) : (confidence1'=1) & (preference1'=preference2) & (confidence2'=inc_conf2) & (sched'=0)
+ Pmeet_p1 * (preference1=preference3?1:0) : (confidence1'=inc_conf1) & (confidence3'=inc_conf3) & (sched'=0)
+ Pmeet_p1 * (preference1=preference3?0:1) * Pwin1_3 : (confidence1'=inc_conf1) & (preference3'=preference1) & (confidence3'=1) & (sched'=0)
+ Pmeet_p1 * (preference1=preference3?0:1) * (1-Pwin1_3) : (confidence1'=1) & (preference1'=preference3) & (confidence3'=inc_conf3) & (sched'=0)
;
endmodule
player p2
player2, [exp2], [com2]
endplayer
module player2
[exp2] sched=2 -> 0 : true
+ 1/K * Pswitch2_1 : (preference2'=1) & (confidence2'=1) & (sched'=0)
+ 1/K * (1-Pswitch2_1) : (sched'=0)
+ 1/K * Pswitch2_2 : (preference2'=2) & (confidence2'=1) & (sched'=0)
+ 1/K * (1-Pswitch2_2) : (sched'=0)
+ 1/K * Pswitch2_3 : (preference2'=3) & (confidence2'=1) & (sched'=0)
+ 1/K * (1-Pswitch2_3) : (sched'=0)
;
[com2] sched=2 & preference2!=0 -> 0 : true
+ Pmeet_p2 * (preference2=preference1?1:0) : (confidence2'=inc_conf2) & (confidence1'=inc_conf1) & (sched'=0)
+ Pmeet_p2 * (preference2=preference1?0:1) * Pwin2_1 : (confidence2'=inc_conf2) & (preference1'=preference2) & (confidence1'=1) & (sched'=0)
+ Pmeet_p2 * (preference2=preference1?0:1) * (1-Pwin2_1) : (confidence2'=1) & (preference2'=preference1) & (confidence1'=inc_conf1) & (sched'=0)
+ Pmeet_p2 * (preference2=preference3?1:0) : (confidence2'=inc_conf2) & (confidence3'=inc_conf3) & (sched'=0)
+ Pmeet_p2 * (preference2=preference3?0:1) * Pwin2_3 : (confidence2'=inc_conf2) & (preference3'=preference2) & (confidence3'=1) & (sched'=0)
+ Pmeet_p2 * (preference2=preference3?0:1) * (1-Pwin2_3) : (confidence2'=1) & (preference2'=preference3) & (confidence3'=inc_conf3) & (sched'=0)
;
endmodule
player p3
player3, [exp3], [com3]
endplayer
module player3
[exp3] sched=3 -> 0 : true
+ 1/K * Pswitch3_1 : (preference3'=1) & (confidence3'=1) & (sched'=0)
+ 1/K * (1-Pswitch3_1) : (sched'=0)
+ 1/K * Pswitch3_2 : (preference3'=2) & (confidence3'=1) & (sched'=0)
+ 1/K * (1-Pswitch3_2) : (sched'=0)
+ 1/K * Pswitch3_3 : (preference3'=3) & (confidence3'=1) & (sched'=0)
+ 1/K * (1-Pswitch3_3) : (sched'=0)
;
[com3] sched=3 & preference3!=0 -> 0 : true
+ Pmeet_p3 * (preference3=preference1?1:0) : (confidence3'=inc_conf3) & (confidence1'=inc_conf1) & (sched'=0)
+ Pmeet_p3 * (preference3=preference1?0:1) * Pwin3_1 : (confidence3'=inc_conf3) & (preference1'=preference3) & (confidence1'=1) & (sched'=0)
+ Pmeet_p3 * (preference3=preference1?0:1) * (1-Pwin3_1) : (confidence3'=1) & (preference3'=preference1) & (confidence1'=inc_conf1) & (sched'=0)
+ Pmeet_p3 * (preference3=preference2?1:0) : (confidence3'=inc_conf3) & (confidence2'=inc_conf2) & (sched'=0)
+ Pmeet_p3 * (preference3=preference2?0:1) * Pwin3_2 : (confidence3'=inc_conf3) & (preference2'=preference3) & (confidence2'=1) & (sched'=0)
+ Pmeet_p3 * (preference3=preference2?0:1) * (1-Pwin3_2) : (confidence3'=1) & (preference3'=preference2) & (confidence2'=inc_conf2) & (sched'=0)
;
endmodule
formula inc_conf1 = confidence1=L ? L : (confidence1+1);
formula inc_conf2 = confidence2=L ? L : (confidence2+1);
formula inc_conf3 = confidence3=L ? L : (confidence3+1);
formula Pmeet_p1 = 1/(N-1);
formula Pmeet_p2 = 1/(N-1);
formula Pmeet_p3 = 1/(N-1);
formula Q_p1 = preference1=1 ? Q1 : ( preference1=1 ? Q2 : (Q3) ) ;
formula Q_p2 = preference2=1 ? Q1 : ( preference2=1 ? Q2 : (Q3) ) ;
formula Q_p3 = preference3=1 ? Q1 : ( preference3=1 ? Q2 : (Q3) ) ;
formula Pswitch1_1 = preference1=0 ? 1 : (preference1=1 ? 0 : pow(Q1, eta) / (pow(Q1, eta) + pow(Q_p1, eta)));
formula Pswitch1_2 = preference1=0 ? 1 : (preference1=2 ? 0 : pow(Q2, eta) / (pow(Q2, eta) + pow(Q_p1, eta)));
formula Pswitch1_3 = preference1=0 ? 1 : (preference1=3 ? 0 : pow(Q3, eta) / (pow(Q3, eta) + pow(Q_p1, eta)));
formula Pswitch2_1 = preference2=0 ? 1 : (preference2=1 ? 0 : pow(Q1, eta) / (pow(Q1, eta) + pow(Q_p2, eta)));
formula Pswitch2_2 = preference2=0 ? 1 : (preference2=2 ? 0 : pow(Q2, eta) / (pow(Q2, eta) + pow(Q_p2, eta)));
formula Pswitch2_3 = preference2=0 ? 1 : (preference2=3 ? 0 : pow(Q3, eta) / (pow(Q3, eta) + pow(Q_p2, eta)));
formula Pswitch3_1 = preference3=0 ? 1 : (preference3=1 ? 0 : pow(Q1, eta) / (pow(Q1, eta) + pow(Q_p3, eta)));
formula Pswitch3_2 = preference3=0 ? 1 : (preference3=2 ? 0 : pow(Q2, eta) / (pow(Q2, eta) + pow(Q_p3, eta)));
formula Pswitch3_3 = preference3=0 ? 1 : (preference3=3 ? 0 : pow(Q3, eta) / (pow(Q3, eta) + pow(Q_p3, eta)));
formula Pwin1_2 = (preference2=0?1:(preference1=0?0:((pow(Q_p1, lambda) * pow(confidence1, gamma)) /
((pow(Q_p1, lambda) * pow(confidence1, gamma))+(pow(Q_p2, lambda) * pow(confidence2, gamma))))));
formula Pwin1_3 = (preference3=0?1:(preference1=0?0:((pow(Q_p1, lambda) * pow(confidence1, gamma)) /
((pow(Q_p1, lambda) * pow(confidence1, gamma))+(pow(Q_p3, lambda) * pow(confidence3, gamma))))));
formula Pwin2_1 = 1-Pwin1_2;
formula Pwin2_3 = (preference3=0?1:(preference2=0?0:((pow(Q_p2, lambda) * pow(confidence2, gamma)) /
((pow(Q_p2, lambda) * pow(confidence2, gamma))+(pow(Q_p3, lambda) * pow(confidence3, gamma))))));
formula Pwin3_1 = 1-Pwin1_3;
formula Pwin3_2 = 1-Pwin2_3;
formula all_prefer_1 = preference1=1 & preference2=1 & preference3=1 ;
formula all_prefer_2 = preference1=2 & preference2=2 & preference3=2 ;
formula all_prefer_3 = preference1=3 & preference2=3 & preference3=3 ;
formula total_confidence = confidence1 + confidence2 + confidence3 ;
formula all_max_conf = total_confidence/N = L;
formula half_max_conf = (( confidence1=L?1:0 + confidence2=L?1:0 + confidence3=L?1:0 )/N) >= 0.5;
label "all_prefer_1" = all_prefer_1;
label "all_prefer_2" = all_prefer_2;
label "all_prefer_3" = all_prefer_3;
label "all_max_conf" = all_max_conf;
label "half_max_conf" = half_max_conf;
label "decision_made" = all_prefer_1 | all_prefer_2 | all_prefer_3 ;
const int k = 0;
const int communication_cost = 10;
const int exploration_cost = 1;
rewards "ncomm1"
[com1] true : communication_cost;
endrewards
rewards "ncomm12"
[com1] true : communication_cost;
[com2] true : communication_cost;
endrewards
rewards "ncomm123"
[com1] true : communication_cost;
[com2] true : communication_cost;
[com3] true : communication_cost;
endrewards
rewards "nexpl1"
[exp1] true : exploration_cost;
endrewards
rewards "nexpl12"
[exp1] true : exploration_cost;
[exp2] true : exploration_cost;
endrewards
rewards "nexpl123"
[exp1] true : exploration_cost;
[exp2] true : exploration_cost;
[exp3] true : exploration_cost;
endrewards
rewards "ntot1"
[exp1] true : exploration_cost;
[com1] true : communication_cost;
endrewards
rewards "ntot12"
[exp1] true : exploration_cost;
[com1] true : communication_cost;
[exp2] true : exploration_cost;
[com2] true : communication_cost;
endrewards
rewards "ntot123"
[exp1] true : exploration_cost;
[com1] true : communication_cost;
[exp2] true : exploration_cost;
[com2] true : communication_cost;
[exp3] true : exploration_cost;
[com3] true : communication_cost;
endrewards
rewards "runtime"
sched!=0 : 1;
endrewards
rewards "penalties"
[exp1] true : 0;
[com1] true : 1;
endrewards