From 3b9740c95d3589c01b9d5f4f43bf22eb3ceb999d Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 14 Jun 2016 19:19:05 +0200 Subject: [PATCH] fixed model files for team benchmark Former-commit-id: e253457611e8523aaa070cca499e375c75890f88 --- .../multi-objective/mdp/team/team2obj_3.nm | 45 ++++++++--------- .../multi-objective/mdp/team/team2obj_4.nm | 49 +++++++++--------- .../multi-objective/mdp/team/team2obj_5.nm | 50 +++++++++---------- .../multi-objective/mdp/team/team3obj_3.nm | 49 +++++++++--------- .../multi-objective/mdp/team/team3obj_4.nm | 46 +++++++++-------- .../multi-objective/mdp/team/team3obj_5.nm | 47 ++++++++--------- 6 files changed, 146 insertions(+), 140 deletions(-) diff --git a/examples/multi-objective/mdp/team/team2obj_3.nm b/examples/multi-objective/mdp/team/team2obj_3.nm index 8a754d922..cd17863ca 100644 --- a/examples/multi-objective/mdp/team/team2obj_3.nm +++ b/examples/multi-objective/mdp/team/team2obj_3.nm @@ -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 diff --git a/examples/multi-objective/mdp/team/team2obj_4.nm b/examples/multi-objective/mdp/team/team2obj_4.nm index bc9e536c2..05cd399ec 100644 --- a/examples/multi-objective/mdp/team/team2obj_4.nm +++ b/examples/multi-objective/mdp/team/team2obj_4.nm @@ -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 diff --git a/examples/multi-objective/mdp/team/team2obj_5.nm b/examples/multi-objective/mdp/team/team2obj_5.nm index 4a02b8746..264b124c9 100644 --- a/examples/multi-objective/mdp/team/team2obj_5.nm +++ b/examples/multi-objective/mdp/team/team2obj_5.nm @@ -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); diff --git a/examples/multi-objective/mdp/team/team3obj_3.nm b/examples/multi-objective/mdp/team/team3obj_3.nm index 8a754d922..9e677312d 100644 --- a/examples/multi-objective/mdp/team/team3obj_3.nm +++ b/examples/multi-objective/mdp/team/team3obj_3.nm @@ -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); diff --git a/examples/multi-objective/mdp/team/team3obj_4.nm b/examples/multi-objective/mdp/team/team3obj_4.nm index bc9e536c2..67781f25a 100644 --- a/examples/multi-objective/mdp/team/team3obj_4.nm +++ b/examples/multi-objective/mdp/team/team3obj_4.nm @@ -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); - diff --git a/examples/multi-objective/mdp/team/team3obj_5.nm b/examples/multi-objective/mdp/team/team3obj_5.nm index 4a02b8746..818bbd0a3 100644 --- a/examples/multi-objective/mdp/team/team3obj_5.nm +++ b/examples/multi-objective/mdp/team/team3obj_5.nm @@ -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