From 8bb25234a325078dce6a01fce364b5d2388f56b5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 20 Jun 2016 13:43:14 +0200 Subject: [PATCH] fixed prism model code (formula used before definition) Former-commit-id: d610960b0e0b85fe132af22ad98be2c2f2cf139d --- .../multi-objective/mdp/team/team2obj_4.nm | 21 ++++++++++--------- .../multi-objective/mdp/team/team2obj_5.nm | 21 ++++++++++--------- .../multi-objective/mdp/team/team3obj_4.nm | 18 ++++++++-------- .../multi-objective/mdp/team/team3obj_5.nm | 20 +++++++++--------- 4 files changed, 41 insertions(+), 39 deletions(-) diff --git a/examples/multi-objective/mdp/team/team2obj_4.nm b/examples/multi-objective/mdp/team/team2obj_4.nm index 05cd399ec..2ad4536e3 100644 --- a/examples/multi-objective/mdp/team/team2obj_4.nm +++ b/examples/multi-objective/mdp/team/team2obj_4.nm @@ -318,6 +318,17 @@ formula finished = (status=6); label "end" = (status=7); +formula task1_completed = finished + & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1))) + & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2))) + & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3))); + +formula task2_completed = finished + & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1))) + & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2))) + & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3))); + + formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1); formula agent1_joins_successful_team_of_1 = (task1_completed & m1_t1=1 & team_size_t1=1) | (task2_completed & m1_t2=1 & team_size_t2=1); formula agent1_joins_successful_team_of_2 = (task1_completed & m1_t1=1 & team_size_t1=2) | (task2_completed & m1_t2=1 & team_size_t2=2); @@ -338,16 +349,6 @@ formula agent4_joins_successful_team_of_1 = (task1_completed & m4_t1=1 & team_si formula agent4_joins_successful_team_of_2 = (task1_completed & m4_t1=1 & team_size_t1=2) | (task2_completed & m4_t2=1 & team_size_t2=2); formula agent4_joins_successful_team_of_3 = (task1_completed & m4_t1=1 & team_size_t1=3) | (task2_completed & m4_t2=1 & team_size_t2=3); -formula task1_completed = finished - & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1))) - & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2))) - & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3))); - -formula task2_completed = finished - & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1))) - & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2))) - & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3))); - // rewards rewards "w_1_total" [] agent1_joins_successful_team : 1; diff --git a/examples/multi-objective/mdp/team/team2obj_5.nm b/examples/multi-objective/mdp/team/team2obj_5.nm index 264b124c9..2bab4d7f4 100644 --- a/examples/multi-objective/mdp/team/team2obj_5.nm +++ b/examples/multi-objective/mdp/team/team2obj_5.nm @@ -476,6 +476,17 @@ formula finished = (status=7); label "end" = (status=8); +formula task1_completed = finished + & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1)|(m5_t1=1&resource5=1))) + & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2)|(m5_t1=1&resource5=2))) + & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3)|(m5_t1=1&resource5=3))); + +formula task2_completed = finished + & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1)|(m5_t2=1&resource5=1))) + & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2)|(m5_t2=1&resource5=2))) + & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3)|(m5_t2=1&resource5=3))); + + formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1); formula agent1_joins_successful_team_of_1 = (task1_completed & m1_t1=1 & team_size_t1=1) | (task2_completed & m1_t2=1 & team_size_t2=1); formula agent1_joins_successful_team_of_2 = (task1_completed & m1_t1=1 & team_size_t1=2) | (task2_completed & m1_t2=1 & team_size_t2=2); @@ -501,16 +512,6 @@ formula agent5_joins_successful_team_of_1 = (task1_completed & m5_t1=1 & team_si formula agent5_joins_successful_team_of_2 = (task1_completed & m5_t1=1 & team_size_t1=2) | (task2_completed & m5_t2=1 & team_size_t2=2); formula agent5_joins_successful_team_of_3 = (task1_completed & m5_t1=1 & team_size_t1=3) | (task2_completed & m5_t2=1 & team_size_t2=3); -formula task1_completed = finished - & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1)|(m5_t1=1&resource5=1))) - & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2)|(m5_t1=1&resource5=2))) - & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3)|(m5_t1=1&resource5=3))); - -formula task2_completed = finished - & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1)|(m5_t2=1&resource5=1))) - & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2)|(m5_t2=1&resource5=2))) - & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3)|(m5_t2=1&resource5=3))); - // rewards rewards "w_1_total" [] agent1_joins_successful_team : 1; diff --git a/examples/multi-objective/mdp/team/team3obj_4.nm b/examples/multi-objective/mdp/team/team3obj_4.nm index 67781f25a..77a74d3f1 100644 --- a/examples/multi-objective/mdp/team/team3obj_4.nm +++ b/examples/multi-objective/mdp/team/team3obj_4.nm @@ -316,6 +316,15 @@ endmodule formula finished = (status=6); label "end" = (status=7); +formula task1_completed = finished + & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1))) + & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2))) + & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3))); + +formula task2_completed = finished + & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1))) + & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2))) + & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3))); formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1); formula agent1_joins_successful_team_of_1 = (task1_completed & m1_t1=1 & team_size_t1=1) | (task2_completed & m1_t2=1 & team_size_t2=1); @@ -337,15 +346,6 @@ formula agent4_joins_successful_team_of_1 = (task1_completed & m4_t1=1 & team_si formula agent4_joins_successful_team_of_2 = (task1_completed & m4_t1=1 & team_size_t1=2) | (task2_completed & m4_t2=1 & team_size_t2=2); formula agent4_joins_successful_team_of_3 = (task1_completed & m4_t1=1 & team_size_t1=3) | (task2_completed & m4_t2=1 & team_size_t2=3); -formula task1_completed = finished - & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1))) - & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2))) - & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3))); - -formula task2_completed = finished - & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1))) - & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2))) - & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3))); // rewards rewards "w_1_total" diff --git a/examples/multi-objective/mdp/team/team3obj_5.nm b/examples/multi-objective/mdp/team/team3obj_5.nm index 818bbd0a3..85214bc8c 100644 --- a/examples/multi-objective/mdp/team/team3obj_5.nm +++ b/examples/multi-objective/mdp/team/team3obj_5.nm @@ -477,6 +477,16 @@ formula finished = (status=7); label "end" = (status=8); +formula task1_completed = finished + & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1)|(m5_t1=1&resource5=1))) + & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2)|(m5_t1=1&resource5=2))) + & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3)|(m5_t1=1&resource5=3))); + +formula task2_completed = finished + & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1)|(m5_t2=1&resource5=1))) + & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2)|(m5_t2=1&resource5=2))) + & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3)|(m5_t2=1&resource5=3))); + formula agent1_joins_successful_team = (task1_completed & m1_t1=1) | (task2_completed & m1_t2=1); formula agent1_joins_successful_team_of_1 = (task1_completed & m1_t1=1 & team_size_t1=1) | (task2_completed & m1_t2=1 & team_size_t2=1); formula agent1_joins_successful_team_of_2 = (task1_completed & m1_t1=1 & team_size_t1=2) | (task2_completed & m1_t2=1 & team_size_t2=2); @@ -502,16 +512,6 @@ formula agent5_joins_successful_team_of_1 = (task1_completed & m5_t1=1 & team_si formula agent5_joins_successful_team_of_2 = (task1_completed & m5_t1=1 & team_size_t1=2) | (task2_completed & m5_t2=1 & team_size_t2=2); formula agent5_joins_successful_team_of_3 = (task1_completed & m5_t1=1 & team_size_t1=3) | (task2_completed & m5_t2=1 & team_size_t2=3); -formula task1_completed = finished - & ((t1_r1=1)=>((m1_t1=1&resource1=1)|(m2_t1=1&resource2=1)|(m3_t1=1&resource3=1)|(m4_t1=1&resource4=1)|(m5_t1=1&resource5=1))) - & ((t1_r2=1)=>((m1_t1=1&resource1=2)|(m2_t1=1&resource2=2)|(m3_t1=1&resource3=2)|(m4_t1=1&resource4=2)|(m5_t1=1&resource5=2))) - & ((t1_r3=1)=>((m1_t1=1&resource1=3)|(m2_t1=1&resource2=3)|(m3_t1=1&resource3=3)|(m4_t1=1&resource4=3)|(m5_t1=1&resource5=3))); - -formula task2_completed = finished - & ((t2_r1=1)=>((m1_t2=1&resource1=1)|(m2_t2=1&resource2=1)|(m3_t2=1&resource3=1)|(m4_t2=1&resource4=1)|(m5_t2=1&resource5=1))) - & ((t2_r2=1)=>((m1_t2=1&resource1=2)|(m2_t2=1&resource2=2)|(m3_t2=1&resource3=2)|(m4_t2=1&resource4=2)|(m5_t2=1&resource5=2))) - & ((t2_r3=1)=>((m1_t2=1&resource1=3)|(m2_t2=1&resource2=3)|(m3_t2=1&resource3=3)|(m4_t2=1&resource4=3)|(m5_t2=1&resource5=3))); - // rewards rewards "w_1_total" [] agent1_joins_successful_team : 1;