sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

fixed model files for team benchmark 

Former-commit-id: e253457611
tempestpy_adaptions
TimQu 9 years ago
parent
de35d40905
commit
3b9740c95d
6 changed files with 146 additions and 140 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 45
      examples/multi-objective/mdp/team/team2obj_3.nm
  2. 49
      examples/multi-objective/mdp/team/team2obj_4.nm
  3. 50
      examples/multi-objective/mdp/team/team2obj_5.nm
  4. 49
      examples/multi-objective/mdp/team/team3obj_3.nm
  5. 46
      examples/multi-objective/mdp/team/team3obj_4.nm
  6. 47
      examples/multi-objective/mdp/team/team3obj_5.nm

45
examples/multi-objective/mdp/team/team2obj_3.nm
View File

@ -22,6 +22,28 @@ const int e31=e13;
const int e32=e23;
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))) / (e12+e13);
module controller // schedules the algorithm
// algorithm status
@ -213,29 +235,6 @@ endmodule
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))) / (e12+e13);
// labels and formulae for property specification

49
examples/multi-objective/mdp/team/team2obj_4.nm
View File

@ -30,6 +30,32 @@ const int e42=e24;
const int e43=e34;
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))) / (e12+e13+e14);
module controller // schedules the algorithm
// algorithm status
@ -285,29 +311,6 @@ endmodule
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))) / (e12+e13+e14);
// labels and formulae for property specification

50
examples/multi-objective/mdp/team/team2obj_5.nm
View File

@ -39,6 +39,31 @@ const int e52=e25;
const int e53=e35;
const int e54=e45;
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1+m5_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2+m5_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 + e15*m5_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 + e15*m5_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4) | (m5_t1=1 & resource1=resource5);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4) | (m5_t2=1 & resource1=resource5);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))+e15*(1-((m5_t1+m5_t2)=0?0:1))) / (e12+e13+e14+e15);
module controller // schedules the algorithm
// algorithm status
@ -446,31 +471,6 @@ formula all_not_sched = !(s1_sched | s2_sched | s3_sched | s4_sched | s5_sched);
formula all_sched = (s1_sched & s2_sched & s3_sched & s4_sched & s5_sched);
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1+m5_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2+m5_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 + e15*m5_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 + e15*m5_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4) | (m5_t1=1 & resource1=resource5);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4) | (m5_t2=1 & resource1=resource5);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))+e15*(1-((m5_t1+m5_t2)=0?0:1))) / (e12+e13+e14+e15);
// labels and formulae for property specification
formula finished = (status=7);
label "end" = (status=8);

49
examples/multi-objective/mdp/team/team3obj_3.nm
View File

@ -22,6 +22,31 @@ const int e31=e13;
const int e32=e23;
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))) / (e12+e13);
module controller // schedules the algorithm
// algorithm status
@ -213,30 +238,6 @@ endmodule
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))) / (e12+e13);
// labels and formulae for property specification
formula finished = (status=5);

46
examples/multi-objective/mdp/team/team3obj_4.nm
View File

@ -30,6 +30,30 @@ const int e42=e24;
const int e43=e34;
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))) / (e12+e13+e14);
module controller // schedules the algorithm
// algorithm status
@ -285,28 +309,6 @@ endmodule
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))) / (e12+e13+e14);

47
examples/multi-objective/mdp/team/team3obj_5.nm
View File

@ -39,6 +39,30 @@ const int e52=e25;
const int e53=e35;
const int e54=e45;
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1+m5_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2+m5_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 + e15*m5_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 + e15*m5_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4) | (m5_t1=1 & resource1=resource5);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4) | (m5_t2=1 & resource1=resource5);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))+e15*(1-((m5_t1+m5_t2)=0?0:1))) / (e12+e13+e14+e15);
module controller // schedules the algorithm
// algorithm status
@ -446,29 +470,6 @@ formula all_not_sched = !(s1_sched | s2_sched | s3_sched | s4_sched | s5_sched);
formula all_sched = (s1_sched & s2_sched & s3_sched & s4_sched & s5_sched);
// agent is committed to some team
formula committed = (m1_t1+m1_t2) > 0;
// formulae to compute team sizes
formula team_size_t1 = m1_t1+m2_t1+m3_t1+m4_t1+m5_t1;
formula team_size_t2 = m1_t2+m2_t2+m3_t2+m4_t2+m5_t2;
// formulae to check whether the agent can join the team
formula can_join_t1 = e12*m2_t1 + e13*m3_t1 + e14*m4_t1 + e15*m5_t1 > 0;
formula can_join_t2 = e12*m2_t2 + e13*m3_t2 + e14*m4_t2 + e15*m5_t2 > 0;
// formulae to check whether agent has the resource required by the task
formula has_resource_t1 = ( (t1_r1=1&resource1=1) | (t1_r2=1&resource1=2) | (t1_r3=1&resource1=3) );
formula has_resource_t2 = ( (t2_r1=1&resource1=1) | (t2_r2=1&resource1=2) | (t2_r3=1&resource1=3) );
// formulae to check whether the resource of an agent has been already filled in the team
formula resource_filled_t1 = (m2_t1=1 & resource1=resource2) | (m3_t1=1 & resource1=resource3) | (m4_t1=1 & resource1=resource4) | (m5_t1=1 & resource1=resource5);
formula resource_filled_t2 = (m2_t2=1 & resource1=resource2) | (m3_t2=1 & resource1=resource3) | (m4_t2=1 & resource1=resource4) | (m5_t2=1 & resource1=resource5);
// formula to compute team initiation probability (assuming each agent has at least one connection)
formula IP = (e12*(1-((m2_t1+m2_t2)=0?0:1))+e13*(1-((m3_t1+m3_t2)=0?0:1))+e14*(1-((m4_t1+m4_t2)=0?0:1))+e15*(1-((m5_t1+m5_t2)=0?0:1))) / (e12+e13+e14+e15);
// labels and formulae for property specification

Write Preview
Loading…
Cancel
Save