robot.aadl.out 21.1 KB
Newer Older
Bechir Zalila's avatar
Bechir Zalila committed
1
2
3
4
------------------------------------------
---------- Ocarina LNT Generator ---------
------------------------------------------

5
Begin Thread
Bechir Zalila's avatar
Bechir Zalila committed
6
7
8
Begin Processor
Begin Types
Begin Main
9
10
11
I am sporadic 
I am sporadic 
% DEFAULT_MCL_LIBRARIES="standard.mcl"
Bechir Zalila's avatar
Bechir Zalila committed
12
13
14
15
16
"Main.bcg"=  divbranching reduction of "ROBOT_Main.lnt";
property PROPERTY_Deadlock is
   deadlock of "Main.bcg";
   expected FALSE;
end property;
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
property Scheduling_Test (ID)
   "Scheduling Test "is
"Main.bcg"|= with evaluator3
   NEVER ("ACTIVATION_$ID !T_Error");
   expected TRUE;
end property;
check Scheduling_Test ( 1);
check Scheduling_Test ( 2);
check Scheduling_Test ( 3);
check Scheduling_Test ( 4);
check Scheduling_Test ( 5);
check Scheduling_Test ( 6);
property Connection (ID)
   "Connection Test "is
"Main.bcg"|= with evaluator3
   AFTER_1_INEVITABLE_2 ('SEND_$ID !*' , 'RECEIVE_$ID !*');
Bechir Zalila's avatar
Bechir Zalila committed
33
34
   expected TRUE;
end property;
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
property Is_Preempted (ID)
   "Is_Preempted Test "is
"Main.bcg"|= with evaluator3
   SOME (true* ."ACTIVATION_$ID !T_DISPATCH_PREEMPTION". true* . ("ACTIVATION_$ID !T_PREEMPTION")* . true* . "ACTIVATION_$ID !T_PREEMPTION_COMPLETION");
   expected TRUE;
end property;
check Is_Preempted ( 1);
check Is_Preempted ( 2);
check Is_Preempted ( 3);
check Is_Preempted ( 4);
check Is_Preempted ( 5);
check Is_Preempted ( 6);
property Data_Loss (ID)
   "Between two consecutive SEND_$ID actions, there is a RECEIVE_$ID" is
"Main.bcg"|= with evaluator3
   NEVER (true* ."SEND_$ID !AADLDATA". (not"RECEIVE_$ID !AADLDATA")* ."SEND_$ID !AADLDATA");
   expected TRUE;
end property;
property Transition (TH_NAME, Si, Sj)
   "Thread $TH_NAME, being in state $Si, the corresponding $Sj state is eventually reachable" is
"Main.bcg"|= with evaluator3
   AFTER_1_INEVITABLE_2 ("DISPLAY_STATE !$TH_NAME !$Si","DISPLAY_STATE !$TH_NAME !$Sj");
   expected TRUE;
end property;
Begin Port
module ROBOT_Threads (Types) is 
Bechir Zalila's avatar
Bechir Zalila committed
61
62
   process Thread_capteur_i [
   ACTIVATION: LNT_Channel_Dispatch, 
63
   PORT_EVENEMENT: LNT_Channel_Port]
Bechir Zalila's avatar
Bechir Zalila committed
64
   is 
65
66
67
68
69
      var 
         EVENEMENT : LNT_Type_Data
      in 
         EVENEMENT := AADLDATA; 
         loop 
Bechir Zalila's avatar
Bechir Zalila committed
70
            select 
71
72
73
74
75
76
77
78
79
80
81
82
               select 
                  ACTIVATION (T_Dispatch_Preemption)
                  []
                  ACTIVATION (T_Preemption_Completion); 
                  PORT_EVENEMENT (EVENEMENT)
                  []
                  ACTIVATION (T_Dispatch_Completion); 
                  PORT_EVENEMENT (EVENEMENT)
                  []
                  ACTIVATION (T_Preemption)
               end select ; 
               ACTIVATION (T_Complete)
Bechir Zalila's avatar
Bechir Zalila committed
83
               []
84
               ACTIVATION (T_Error)
Bechir Zalila's avatar
Bechir Zalila committed
85
               []
86
87
88
89
               ACTIVATION (T_Stop)
            end select 
         end loop
      end var
Bechir Zalila's avatar
Bechir Zalila committed
90
91
92
93
   end process 
   
   process Thread_controle_i [
   ACTIVATION: LNT_Channel_Dispatch, 
94
95
   PORT_COMM_SERVO_OUT: LNT_Channel_Port, 
   PORT_INFO_CAPTEUR_IN: LNT_Channel_Port]
Bechir Zalila's avatar
Bechir Zalila committed
96
97
   is 
      var 
98
99
         COMM_SERVO_OUT : LNT_Type_Data, 
         INFO_CAPTEUR_IN : LNT_Type_Data
Bechir Zalila's avatar
Bechir Zalila committed
100
      in 
101
102
         COMM_SERVO_OUT := AADLDATA; 
         INFO_CAPTEUR_IN := EMPTY; 
Bechir Zalila's avatar
Bechir Zalila committed
103
104
         loop 
            select 
105
106
107
108
109
110
111
112
113
114
115
116
117
118
               select 
                  ACTIVATION (T_Dispatch_Preemption); 
                  PORT_INFO_CAPTEUR_IN (?INFO_CAPTEUR_IN)
                  []
                  ACTIVATION (T_Preemption_Completion); 
                  PORT_COMM_SERVO_OUT (COMM_SERVO_OUT)
                  []
                  ACTIVATION (T_Dispatch_Completion); 
                  PORT_INFO_CAPTEUR_IN (?INFO_CAPTEUR_IN); 
                  PORT_COMM_SERVO_OUT (COMM_SERVO_OUT)
                  []
                  ACTIVATION (T_Preemption)
               end select ; 
               ACTIVATION (T_Complete)
Bechir Zalila's avatar
Bechir Zalila committed
119
               []
120
121
122
               ACTIVATION (T_Error)
               []
               ACTIVATION (T_Stop)
Bechir Zalila's avatar
Bechir Zalila committed
123
124
125
126
127
            end select 
         end loop
      end var
   end process 
   
128
129
130
   process Thread_servomoteur_i [
   ACTIVATION: LNT_Channel_Dispatch, 
   PORT_ORDRE: LNT_Channel_Port]
Bechir Zalila's avatar
Bechir Zalila committed
131
132
   is 
      var 
133
         ORDRE : LNT_Type_Data
Bechir Zalila's avatar
Bechir Zalila committed
134
      in 
135
         ORDRE := EMPTY; 
Bechir Zalila's avatar
Bechir Zalila committed
136
137
         loop 
            select 
138
139
140
141
142
143
144
145
146
147
148
149
               select 
                  ACTIVATION (T_Dispatch_Preemption); 
                  PORT_ORDRE (?ORDRE)
                  []
                  ACTIVATION (T_Preemption_Completion)
                  []
                  ACTIVATION (T_Dispatch_Completion); 
                  PORT_ORDRE (?ORDRE)
                  []
                  ACTIVATION (T_Preemption)
               end select ; 
               ACTIVATION (T_Complete)
Bechir Zalila's avatar
Bechir Zalila committed
150
               []
151
               ACTIVATION (T_Error)
Bechir Zalila's avatar
Bechir Zalila committed
152
               []
153
               ACTIVATION (T_Stop)
Bechir Zalila's avatar
Bechir Zalila committed
154
155
156
157
158
159
            end select 
         end loop
      end var
   end process 
   
end module 
160
module Types 
Bechir Zalila's avatar
Bechir Zalila committed
161
162
with "==",  "eq" , "<",  "lt" , "<=",  "le" , ">",  "gt" , ">=",  "ge" is 
   type LNT_Type_Data is 
163
      AADLDATA, EMPTY
Bechir Zalila's avatar
Bechir Zalila committed
164
165
   end type 
   
166
167
168
169
170
171
   type LNT_Type_Data_FIFO is 
      list of LNT_Type_Data
      with "==",  "eq" , "length" , "append" , "tail" , "head" , "<>",  "ne",  "!=" 
   end type 
   
   channel LNT_Channel_Port is 
Bechir Zalila's avatar
Bechir Zalila committed
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
      (LNT_Type_Data) 
   end channel
   type LNT_Type_Time_Constraint is 
      range 0 .. 240 of Nat
   end type 
   
   type LNT_Type_Thread is 
      array [0 .. 11 ]of LNT_Type_Time_Constraint
   end type 
   
   type LNT_Type_Thread_Array is 
      array [1 .. 6 ]of LNT_Type_Thread
   end type 
   
   type LNT_Type_Dispatch is 
187
      T_Dispatch_Preemption, T_Preemption_Completion, T_Dispatch_Completion, T_Preemption, T_Stop, T_Error, T_Complete
Bechir Zalila's avatar
Bechir Zalila committed
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
   end type 
   
   type LNT_Type_Event is 
      Incoming_Event, No_Event
   end type 
   
   channel LNT_Channel_Dispatch is 
      (LNT_Type_Dispatch) 
   end channel
   channel LNT_Channel_Event is 
      (LNT_Type_Event) 
   end channel
   function Thread_Number : Nat 
   is 
      return 6
   end function 
   
   function PPCM_THREAD : LNT_Type_Time_Constraint 
   is 
      return LNT_Type_Time_Constraint ( 120)
   end function 
   
   function _+_ (
      n1: LNT_Type_Time_Constraint, 
      n2: LNT_Type_Time_Constraint) : LNT_Type_Time_Constraint 
   is 
      return LNT_Type_Time_Constraint (Nat (n1) + Nat (n2) mod 240)
   end function 
   
   function _-_ (
      n1: LNT_Type_Time_Constraint, 
      n2: LNT_Type_Time_Constraint) : LNT_Type_Time_Constraint 
   is 
      if (n1 <  n2)
      then 
         return LNT_Type_Time_Constraint (((240 - Nat (n2))  + Nat (n1))  mod 240)
      else 
         return LNT_Type_Time_Constraint (Nat (n1) - Nat (n2) mod 240)
      end if
   end function 
   
   function _*_ (
      n1: LNT_Type_Time_Constraint, 
      n2: LNT_Type_Time_Constraint) : LNT_Type_Time_Constraint 
   is 
      return LNT_Type_Time_Constraint (Nat (n1) * Nat (n2) mod 240)
   end function 
   
end module 
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
module ROBOT_Main (Types, ROBOT_Processor, ROBOT_Threads, LNT_Generic_Process_For_Port_Connections) is 
   process Main [
   ACTIVATION_1: LNT_Channel_Dispatch, 
   SEND_con_1: LNT_Channel_Port, 
   ACTIVATION_2: LNT_Channel_Dispatch, 
   SEND_con_2: LNT_Channel_Port, 
   ACTIVATION_3: LNT_Channel_Dispatch, 
   SEND_con_3: LNT_Channel_Port, 
   RECEIVE_con_1: LNT_Channel_Port, 
   ACTIVATION_4: LNT_Channel_Dispatch, 
   SEND_con_4: LNT_Channel_Port, 
   RECEIVE_con_2: LNT_Channel_Port, 
   ACTIVATION_5: LNT_Channel_Dispatch, 
   RECEIVE_con_3: LNT_Channel_Port, 
   INCOMING_EVENT_5: LNT_Channel_Event, 
   ACTIVATION_6: LNT_Channel_Dispatch, 
   RECEIVE_con_4: LNT_Channel_Port, 
   INCOMING_EVENT_6: LNT_Channel_Event]
   is 
      par 
         ACTIVATION_1 , SEND_con_1 -> 
         Thread_capteur_i [ACTIVATION_1, SEND_con_1]
         ||
         ACTIVATION_2 , SEND_con_2 -> 
         Thread_capteur_i [ACTIVATION_2, SEND_con_2]
         ||
         ACTIVATION_3 , SEND_con_3 , SEND_con_1 -> 
         par 
            SEND_con_1 , RECEIVE_con_1 -> 
            Event_Port_For_Periodic [SEND_con_1, RECEIVE_con_1] ( 5)
            ||
            ACTIVATION_3 , SEND_con_3 , RECEIVE_con_1 -> 
            Thread_controle_i [ACTIVATION_3, SEND_con_3, RECEIVE_con_1]
         end par 
         ||
         ACTIVATION_4 , SEND_con_4 , SEND_con_2 -> 
         par 
            SEND_con_2 , RECEIVE_con_2 -> 
            Event_Port_For_Periodic [SEND_con_2, RECEIVE_con_2] ( 5)
            ||
            ACTIVATION_4 , SEND_con_4 , RECEIVE_con_2 -> 
            Thread_controle_i [ACTIVATION_4, SEND_con_4, RECEIVE_con_2]
         end par 
         ||
         ACTIVATION_5 , INCOMING_EVENT_5 , SEND_con_3 -> 
         par 
            SEND_con_3 , RECEIVE_con_3 , INCOMING_EVENT_5 -> 
            Event_Port [SEND_con_3, RECEIVE_con_3, INCOMING_EVENT_5] ( 2)
            ||
            ACTIVATION_5 , RECEIVE_con_3 -> 
            Thread_servomoteur_i [ACTIVATION_5, RECEIVE_con_3]
         end par 
         ||
         ACTIVATION_6 , INCOMING_EVENT_6 , SEND_con_4 -> 
         par 
            SEND_con_4 , RECEIVE_con_4 , INCOMING_EVENT_6 -> 
            Event_Port [SEND_con_4, RECEIVE_con_4, INCOMING_EVENT_6] ( 2)
            ||
            ACTIVATION_6 , RECEIVE_con_4 -> 
            Thread_servomoteur_i [ACTIVATION_6, RECEIVE_con_4]
         end par 
         ||
         ACTIVATION_1 , ACTIVATION_2 , ACTIVATION_3 , ACTIVATION_4 , ACTIVATION_5 , ACTIVATION_6 , INCOMING_EVENT_5 , INCOMING_EVENT_6 -> 
         Processor [ACTIVATION_1, ACTIVATION_2, ACTIVATION_3, ACTIVATION_4, ACTIVATION_5, ACTIVATION_6, INCOMING_EVENT_5, INCOMING_EVENT_6]
      end par 
   end process 
   
end module 
module ROBOT_Processor (Types) is 
Bechir Zalila's avatar
Bechir Zalila committed
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
   function Assign (
      in var Threads: LNT_Type_Thread_Array, 
      I: Nat, 
      K: Nat, 
      Val: LNT_Type_Time_Constraint) : LNT_Type_Thread_Array 
   is 
      var 
         P : LNT_Type_Thread
      in 
         P := Threads[I]; 
         P[K] := Val; 
         Threads[I] := P
      end var; 
      return Threads
   end function 
   
   function Update_Thread (
      in var Aux_Threads: LNT_Type_Thread_Array, 
      I: Nat, 
      TODO: LNT_Type_Time_Constraint) : LNT_Type_Thread_Array 
   is 
      var 
         P : LNT_Type_Thread
      in 
         P := Aux_Threads[I]; 
         if (P[2] ==  LNT_Type_Time_Constraint (0))
         then 
            P[6] := LNT_Type_Time_Constraint (1)
         end if; 
         P[2] := P[2] + TODO; 
         P[8] := LNT_Type_Time_Constraint (1); 
337
         if (P[2] ==  P[0])
Bechir Zalila's avatar
Bechir Zalila committed
338
339
340
         then 
            P[7] := LNT_Type_Time_Constraint (1); 
            P[2] := LNT_Type_Time_Constraint (0); 
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
            case P[11] of LNT_Type_Time_Constraint in 
            
               LNT_Type_Time_Constraint (1) -> 
                  P[4] := P[5] ; 
                  P[5] := PPCM_THREAD ; 
                  P[10] := LNT_Type_Time_Constraint (0)
               | 
               LNT_Type_Time_Constraint (0) | LNT_Type_Time_Constraint (3) -> 
                  if ((P[3] + LNT_Type_Time_Constraint (1) * P[1] <=  PPCM_THREAD)  and  (P[4] + P[1] <=  PPCM_THREAD) )
                  then 
                     P[4] := P[3] * P[1]; 
                     P[3] := P[3] + LNT_Type_Time_Constraint (1); 
                     P[5] := P[3] * P[1]
                  else 
                     P[10] := LNT_Type_Time_Constraint (0)
                  end if
               | 
               LNT_Type_Time_Constraint (2) -> 
                  if ((P[4] + P[1] <=  PPCM_THREAD)  and  (P[5] + P[1] <=  PPCM_THREAD) )
                  then 
                     P[4] := P[4] + P[1]; 
                     P[5] := P[5] + P[1]
                  else 
                     P[10] := LNT_Type_Time_Constraint (0)
                  end if
               | 
               any  -> 
                  null 
            end case 
Bechir Zalila's avatar
Bechir Zalila committed
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
         end if; 
         Aux_Threads[I] := P
      end var; 
      return Aux_Threads
   end function 
   
   process Sporadic_Notif [
   INCOMING_EVENT_GATE: LNT_Channel_Event](
   in out Threads: LNT_Type_Thread_Array,
   k: Nat,
   Counter: LNT_Type_Time_Constraint,
   in out Is_Activated: bool) 
   is 
      select 
         INCOMING_EVENT_GATE (Incoming_Event); 
         Threads := Assign (Threads, K, 3, (Threads[k][3] + LNT_Type_Time_Constraint (1)) )
         []
         INCOMING_EVENT_GATE (No_Event)
      end select ; 
      if ((Counter >=  Threads[k][4])  and  (Threads[k][3] >  LNT_Type_Time_Constraint (0)) )
      then 
         Threads := Assign (Threads, k, 4, Counter); 
         Threads := Assign (Threads, k, 5, (Counter + Threads[k][1]) ); 
         Threads := Assign (Threads, k, 10, LNT_Type_Time_Constraint (1)); 
         Threads := Assign (Threads, K, 3, (Threads[k][3] - LNT_Type_Time_Constraint (1)) ); 
         Is_Activated := true
      end if
   end process 
   
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
   process Timed_Hybrid_Notif [
   INCOMING_EVENT_GATE: LNT_Channel_Event](
   in out Threads: LNT_Type_Thread_Array,
   k: Nat,
   Counter: LNT_Type_Time_Constraint,
   in out Is_Activated: bool) 
   is 
      select 
         INCOMING_EVENT_GATE (Incoming_Event); 
         Threads := Assign (Threads, k, 4, Counter); 
         Threads := Assign (Threads, k, 5, (Counter + Threads[k][1]) ); 
         Is_Activated := true
         []
         INCOMING_EVENT_GATE (No_Event)
      end select 
   end process 
   
   process Activate_K [
   ACTIVATION_1: LNT_Channel_Dispatch, 
   ACTIVATION_2: LNT_Channel_Dispatch, 
   ACTIVATION_3: LNT_Channel_Dispatch, 
   ACTIVATION_4: LNT_Channel_Dispatch, 
   ACTIVATION_5: LNT_Channel_Dispatch, 
   ACTIVATION_6: LNT_Channel_Dispatch](
   in out Threads: LNT_Type_Thread_Array,
   K: Nat) 
   is 
      case k in 
      
          1 -> 
            Thread_Activation [ACTIVATION_1] (!?Threads,  1)
         | 
          2 -> 
            Thread_Activation [ACTIVATION_2] (!?Threads,  2)
         | 
          3 -> 
            Thread_Activation [ACTIVATION_3] (!?Threads,  3)
         | 
          4 -> 
            Thread_Activation [ACTIVATION_4] (!?Threads,  4)
         | 
          5 -> 
            Thread_Activation [ACTIVATION_5] (!?Threads,  5)
         | 
          6 -> 
            Thread_Activation [ACTIVATION_6] (!?Threads,  6)
         | 
         any  -> 
            null 
      end case 
   end process 
   
Bechir Zalila's avatar
Bechir Zalila committed
451
452
453
454
455
456
457
458
459
   process Thread_Activation [
   ACTIVATION: LNT_Channel_Dispatch](
   in out Threads: LNT_Type_Thread_Array,
   K: Nat) 
   is 
      if (Threads[K][8] ==  LNT_Type_Time_Constraint (1))
      then 
         if ((Threads[K][6] ==  LNT_Type_Time_Constraint (1))  and  (Threads[K][7] ==  LNT_Type_Time_Constraint (1)) )
         then 
460
            ACTIVATION (T_Dispatch_Completion); 
Bechir Zalila's avatar
Bechir Zalila committed
461
462
463
464
465
            Threads := Assign (Threads, K, 6, LNT_Type_Time_Constraint (0)); 
            Threads := Assign (Threads, K, 7, LNT_Type_Time_Constraint (0))
         elsif (Threads[K][7] ==  LNT_Type_Time_Constraint (1))
         then 
         
466
            ACTIVATION (T_Preemption_Completion); 
Bechir Zalila's avatar
Bechir Zalila committed
467
468
469
470
            Threads := Assign (Threads, K, 7, LNT_Type_Time_Constraint (0))
         elsif (Threads[K][6] ==  LNT_Type_Time_Constraint (1))
         then 
         
471
            ACTIVATION (T_Dispatch_Preemption); 
Bechir Zalila's avatar
Bechir Zalila committed
472
473
            Threads := Assign (Threads, K, 6, LNT_Type_Time_Constraint (0))
         else 
474
            ACTIVATION (T_Preemption)
Bechir Zalila's avatar
Bechir Zalila committed
475
476
         end if; 
         Threads := Assign (Threads, K, 8, LNT_Type_Time_Constraint (0)); 
477
         ACTIVATION (T_Complete)
Bechir Zalila's avatar
Bechir Zalila committed
478
479
480
481
482
483
484
485
486
487
488
489
490
491
      elsif (Threads[K][9] ==  LNT_Type_Time_Constraint (0))
      then 
      
         ACTIVATION (T_ERROR)
      end if
   end process 
   
   process Processor [
   ACTIVATION_1: LNT_Channel_Dispatch, 
   ACTIVATION_2: LNT_Channel_Dispatch, 
   ACTIVATION_3: LNT_Channel_Dispatch, 
   ACTIVATION_4: LNT_Channel_Dispatch, 
   ACTIVATION_5: LNT_Channel_Dispatch, 
   ACTIVATION_6: LNT_Channel_Dispatch, 
492
   INCOMING_EVENT_5: LNT_Channel_Event, 
Bechir Zalila's avatar
Bechir Zalila committed
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
   INCOMING_EVENT_6: LNT_Channel_Event]
   is 
      var 
         Threads : LNT_Type_Thread_Array, 
         Counter : LNT_Type_Time_Constraint, 
         I : Nat, 
         k : Nat, 
         Is_Activated : bool, 
         Preempt : bool, 
         TODO : LNT_Type_Time_Constraint, 
         Nb_Active_Thread : Nat
      in 
         Counter := LNT_Type_Time_Constraint (0); 
         Threads := LNT_Type_Thread_Array (LNT_Type_Thread (LNT_Type_Time_Constraint (0))); 
         Threads[ 1] := LNT_Type_Thread (LNT_Type_Time_Constraint (2), LNT_Type_Time_Constraint (8), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (8), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0)); 
         Threads[ 2] := LNT_Type_Thread (LNT_Type_Time_Constraint (2), LNT_Type_Time_Constraint (8), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (8), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0)); 
         Threads[ 3] := LNT_Type_Thread (LNT_Type_Time_Constraint (5), LNT_Type_Time_Constraint (10), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (10), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0)); 
         Threads[ 4] := LNT_Type_Thread (LNT_Type_Time_Constraint (5), LNT_Type_Time_Constraint (10), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (10), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0)); 
         Threads[ 5] := LNT_Type_Thread (LNT_Type_Time_Constraint (2), LNT_Type_Time_Constraint (12), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (12), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1)); 
         Threads[ 6] := LNT_Type_Thread (LNT_Type_Time_Constraint (2), LNT_Type_Time_Constraint (12), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (12), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1), LNT_Type_Time_Constraint (0), LNT_Type_Time_Constraint (1)); 
         loop 
514
515
516
517
518
519
520
521
            if (Counter <  PPCM_THREAD)
            then 
               Nb_Active_Thread := 0; 
               K := 1; 
               while (K <=  Thread_Number) loop
                  if ((Threads[K][10] ==  LNT_Type_Time_Constraint (1))  and  (Threads[K][9] ==  LNT_Type_Time_Constraint (1))  and  (Counter >=  Threads[K][4]) )
                  then 
                     if (Counter >=  Threads[K][5])
Bechir Zalila's avatar
Bechir Zalila committed
522
                     then 
523
524
525
526
                        Threads := Assign (Threads, K, 9, LNT_Type_Time_Constraint (0)); 
                        Activate_k [ACTIVATION_1, ACTIVATION_2, ACTIVATION_3, ACTIVATION_4, ACTIVATION_5, ACTIVATION_6] (!?Threads, k); 
                        k := k + 1
                     else 
Bechir Zalila's avatar
Bechir Zalila committed
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
                        Preempt := true; 
                        TODO := Threads[K][0] - Threads[K][2]; 
                        I := 1; 
                        while ((I <=  (K - 1) )  and  Preempt) loop
                           if ((Threads[I][10] ==  LNT_Type_Time_Constraint (1))  and  (Threads[I][9] ==  LNT_Type_Time_Constraint (1))  and  (Counter + TODO >  Threads[I][4]) )
                           then 
                              TODO := Threads[I][4] - Counter; 
                              Preempt := false
                           else 
                              I := I + 1
                           end if
                        end loop; 
                        Counter := Counter + TODO; 
                        Nb_Active_Thread := Nb_Active_Thread + 1; 
                        Threads := Update_Thread (Threads, K, TODO); 
542
543
                        Activate_k [ACTIVATION_1, ACTIVATION_2, ACTIVATION_3, ACTIVATION_4, ACTIVATION_5, ACTIVATION_6] (!?Threads, k); 
                        if (Preempt)
Bechir Zalila's avatar
Bechir Zalila committed
544
                        then 
545
                           k := I
Bechir Zalila's avatar
Bechir Zalila committed
546
547
548
549
                        else 
                           k := k + 1
                        end if
                     end if
550
551
552
553
554
555
556
                  else 
                     k := k + 1
                  end if; 
                  Is_Activated := false; 
                  Sporadic_Notif [INCOMING_EVENT_5] (!?Threads,  5, Counter, !?Is_Activated); 
                  Sporadic_Notif [INCOMING_EVENT_6] (!?Threads,  6, Counter, !?Is_Activated); 
                  if (Is_Activated)
Bechir Zalila's avatar
Bechir Zalila committed
557
                  then 
558
                     k := 1
Bechir Zalila's avatar
Bechir Zalila committed
559
                  end if
560
561
               end loop; 
               if (Nb_Active_Thread ==  0)
Bechir Zalila's avatar
Bechir Zalila committed
562
               then 
563
                  Counter := Counter + LNT_Type_Time_Constraint (1)
Bechir Zalila's avatar
Bechir Zalila committed
564
               end if
565
566
567
568
569
570
571
572
            else 
               ACTIVATION_1 (T_Stop); 
               ACTIVATION_2 (T_Stop); 
               ACTIVATION_3 (T_Stop); 
               ACTIVATION_4 (T_Stop); 
               ACTIVATION_5 (T_Stop); 
               ACTIVATION_6 (T_Stop)
            end if
Bechir Zalila's avatar
Bechir Zalila committed
573
574
575
576
577
         end loop
      end var
   end process 
   
end module