From ee59f772b063a30bafae778b7d55d263c2c83a6a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 30 Aug 2016 10:55:28 +0200 Subject: [PATCH] fixed prism code for polling example Former-commit-id: fe8443626c02fba5a02350a131019e27ff7b8d5f --- examples/multiobjective/ma/polling/polling.ma | 72 +++++++++---------- 1 file changed, 34 insertions(+), 38 deletions(-) diff --git a/examples/multiobjective/ma/polling/polling.ma b/examples/multiobjective/ma/polling/polling.ma index ef9c4958e..a7523d2c6 100644 --- a/examples/multiobjective/ma/polling/polling.ma +++ b/examples/multiobjective/ma/polling/polling.ma @@ -3,31 +3,27 @@ ma -const int J; // number of job types (should be in [1..6]) +const int N; // number of job types (should be at most 6) const int Q; // Maximum queue size in each station -const bool samerate=false; // true if all stations should have the same rate // Formulae to control the LIFO queue of the stations. -// The queue is represented by some integer whose base J representation has at most Q digits, each representing one of the job types 0, 1, ..., J-1. +// The queue is represented by some integer whose base N representation has at most Q digits, each representing one of the job types 0, 1, ..., N-1. // In addition, we store the current size of the queue which is needed to distinguish an empty queue from a queue holding job of type 0 formula queue1_empty = q1Size=0; formula queue1_full = q1Size=Q; -formula queue1_pop = floor(q1/J); -formula queue1_head = q1 - (queue1_pop * J); // i.e. q1 modulo J -formula queue1_push = q1*J; +formula queue1_pop = floor(q1/N); +formula queue1_head = q1 - (queue1_pop * N); // i.e. q1 modulo N +formula queue1_push = q1*N; formula queue2_empty = q2Size=0; formula queue2_full = q2Size=Q; -formula queue2_pop = floor(q2/J); -formula queue2_head = q2 - (queue2_pop * J); // i.e. q2 modulo J -formula queue2_push = q2*J; +formula queue2_pop = floor(q2/N); +formula queue2_head = q2 - (queue2_pop * N); // i.e. q2 modulo N +formula queue2_push = q2*N; -const int queue_maxValue = (J^Q)-1; +const int queue_maxValue = (N^Q)-1; - - -const double inRate1 = 3; // = (2*1) + 1; -const double inRate2 = 5; // = (2*2) + 1; -const double inRate3 = 7; // = (2*3) + 1; +const double inRate1 = 3; // = (2 * #station) + 1; +const double inRate2 = 5; // = (2 * #station) + 1; module pollingsys // The queues for the stations @@ -36,37 +32,37 @@ module pollingsys q2 : [0..queue_maxValue]; q2Size : [0..Q]; - // Store the job that is currently processed by the server. j=J means that no job is processed. - j : [0..J] init J; + // Store the job that is currently processed by the server. j=N means that no job is processed. + j : [0..N] init N; // Flag indicating whether a new job arrived newJob1 : bool init false; newJob2 : bool init false; - //<> !newJob1 & !newJob2 & !queue1_full & queue2_full & j=J -> inRate1 : (newJob1'=true); - //<> !newJob1 & !newJob2 & queue1_full & !queue2_full & j=J -> inRate2 : (newJob2'=true); - <> !newJob1 & !newJob2 & !queue1_full & !queue2_full & j=J -> inRate1 : (newJob1'=true) + inRate2 : (newJob2'=true); - <> !newJob1 & !newJob2 & queue1_full & queue2_full & j 2*(j+1) : (j'=J); - <> !newJob1 & !newJob2 & !queue1_full & queue2_full & j inRate1 : (newJob1'=true) + 2*(j+1) : (j'=J); - <> !newJob1 & !newJob2 & queue1_full & !queue2_full & j inRate2 : (newJob2'=true) + 2*(j+1) : (j'=J); - <> !newJob1 & !newJob2 & !queue1_full & !queue2_full & j inRate1 : (newJob1'=true) + inRate2 : (newJob2'=true) + 2*(j+1) : (j'=J); + //<> !newJob1 & !newJob2 & !queue1_full & queue2_full & j=N -> inRate1 : (newJob1'=true); + //<> !newJob1 & !newJob2 & queue1_full & !queue2_full & j=N -> inRate2 : (newJob2'=true); + <> !newJob1 & !newJob2 & !queue1_full & !queue2_full & j=N -> inRate1 : (newJob1'=true) + inRate2 : (newJob2'=true); + <> !newJob1 & !newJob2 & queue1_full & queue2_full & j 2*(j+1) : (j'=N); + <> !newJob1 & !newJob2 & !queue1_full & queue2_full & j inRate1 : (newJob1'=true) + 2*(j+1) : (j'=N); + <> !newJob1 & !newJob2 & queue1_full & !queue2_full & j inRate2 : (newJob2'=true) + 2*(j+1) : (j'=N); + <> !newJob1 & !newJob2 & !queue1_full & !queue2_full & j inRate1 : (newJob1'=true) + inRate2 : (newJob2'=true) + 2*(j+1) : (j'=N); - [] newJob1 & J>=1 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+0) & (newJob1'=false); - [] newJob1 & J>=2 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+1) & (newJob1'=false); - [] newJob1 & J>=3 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+2) & (newJob1'=false); - [] newJob1 & J>=4 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+3) & (newJob1'=false); - [] newJob1 & J>=5 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+4) & (newJob1'=false); - [] newJob1 & J>=6 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+5) & (newJob1'=false); + [] newJob1 & N>=1 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+0) & (newJob1'=false); + [] newJob1 & N>=2 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+1) & (newJob1'=false); + [] newJob1 & N>=3 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+2) & (newJob1'=false); + [] newJob1 & N>=4 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+3) & (newJob1'=false); + [] newJob1 & N>=5 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+4) & (newJob1'=false); + [] newJob1 & N>=6 -> 1 : (q1Size'=q1Size+1) & (q1'=queue1_push+5) & (newJob1'=false); - [] newJob2 & J>=1 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+0) & (newJob2'=false); - [] newJob2 & J>=2 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+1) & (newJob2'=false); - [] newJob2 & J>=3 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+2) & (newJob2'=false); - [] newJob2 & J>=4 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+3) & (newJob2'=false); - [] newJob2 & J>=5 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+4) & (newJob2'=false); - [] newJob2 & J>=6 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+5) & (newJob2'=false); + [] newJob2 & N>=1 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+0) & (newJob2'=false); + [] newJob2 & N>=2 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+1) & (newJob2'=false); + [] newJob2 & N>=3 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+2) & (newJob2'=false); + [] newJob2 & N>=4 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+3) & (newJob2'=false); + [] newJob2 & N>=5 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+4) & (newJob2'=false); + [] newJob2 & N>=6 -> 1 : (q2Size'=q2Size+1) & (q2'=queue2_push+5) & (newJob2'=false); - [copy1] !newJob1 & !newJob2 & !queue1_empty & j=J -> 0.9 : (j'=queue1_head) & (q1Size'=q1Size-1) & (q1'=queue1_pop) + 0.1 : (j'=queue1_head); - [copy2] !newJob1 & !newJob2 & !queue2_empty & j=J -> 0.9 : (j'=queue2_head) & (q2Size'=q2Size-1) & (q2'=queue2_pop) + 0.1 : (j'=queue2_head); + [copy1] !newJob1 & !newJob2 & !queue1_empty & j=N -> 0.9 : (j'=queue1_head) & (q1Size'=q1Size-1) & (q1'=queue1_pop) + 0.1 : (j'=queue1_head); + [copy2] !newJob1 & !newJob2 & !queue2_empty & j=N -> 0.9 : (j'=queue2_head) & (q2Size'=q2Size-1) & (q2'=queue2_pop) + 0.1 : (j'=queue2_head); endmodule