LNT_Generic_Process_For_Port_Connections_BA.lnt 4.1 KB
Newer Older
hana's avatar
update:    
hana committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
module LNT_Generic_Process_For_Port_Connections_BA (BA_Types) is -- With Behavior Annex
--  data port --
   process Data_Port [
   Input: LNT_Channel_Data_Port, 
   Output: LNT_Channel_Data_Port] 
   is 
      var Data : LNT_Type_Data in
         Data := DATA_INIT;
         loop 
            select 
               Input (?Data)
               [] 
               Output (Data)
            end select 
         end loop
      end var
   end process

--  event port --
--  for no periodic threads --
   process Event_Port [
   Input: LNT_Channel_Event_Port, 
   Output: LNT_Channel_Event_Port,
   Notify: LNT_Channel_Event](
   Queue_Size: Nat) 
   is 
      var 
         Nb_Events : Nat,
         Is_New : bool         
      in 
         Nb_Events := 0; 
         Is_New := false; 
         loop 
            select 
               Input (true); 
               Is_New := true;               
               if (Nb_Events < Queue_Size) then
                  Nb_Events := Nb_Events + 1
               end if
               []
               if (Nb_Events > 0) then 
                  Output (true);
                  Nb_Events := Nb_Events - 1
               else
                  Output (false)
               end if   
               []
               if (Is_New) then 
                  Notify (Incoming_Event); 
                  Is_New := false
               else 
                  Notify (No_Event)
               end if
            end select 
         end loop
      end var
   end process
   
-- for periodic threads --
   process Event_Port_For_Periodic [
   Input: LNT_Channel_Event_Port, 
   Output: LNT_Channel_Event_Port](
   Queue_Size: Nat) 
   is 
      var 
         Nb_Events : Nat
      in 
         Nb_Events := 0; 
         loop 
            select 
               Input (true); 
               if (Nb_Events < Queue_Size) then
                  Nb_Events := Nb_Events + 1
               end if
               []
               if (Nb_Events > 0) then 
                  Output (true);
                  Nb_Events := Nb_Events - 1
               else
                  Output (false)
               end if   
            end select 
         end loop
      end var
   end process

-- event data port
-- for no periodic threads --
   process Event_Data_Port_Sporadic [
   Input: LNT_Channel_Event_Data_Port, 
   Output: LNT_Channel_Event_Data_Port,
   Notify: LNT_Channel_Event](
   Queue_Size: Nat) 
   is 
      var 
         FIFO : LNT_Type_Data_FIFO,
         Is_New : bool,
         D : LNT_Type_Data
      in 
      
         FIFO := {};
         D := DATA_INIT; 
         Is_New := false;
         loop 
            select 
               Input (?D, true); 
               Is_New := true;
               if length (FIFO) >= Queue_Size then
                  FIFO := tail (FIFO)
               end if;
               FIFO := append (D, FIFO)
               []
               if (Is_New) then 
                  Notify (Incoming_Event); 
                  Is_New := false
               else 
                  Notify (No_Event)
               end if
               []
               if (FIFO != {}) then 
                  Output (Head (FIFO), true);
                  FIFO := tail (FIFO)
               else
                  Output (D,false)
               end if
            end select 
         end loop
      end var
   end process

-- for periodic threads --
   process Event_Data_Port_For_Periodic [
   Input: LNT_Channel_Event_Data_Port, 
   Output: LNT_Channel_Event_Data_Port](
   Queue_Size: Nat) 
   is 
      var 
         FIFO : LNT_Type_Data_FIFO,
         D : LNT_Type_Data
      in 
         FIFO := {};
         D := DATA_INIT; 
         loop 
            select 
               Input (?D, true); 
               if length (FIFO) >= Queue_Size then
                  FIFO := tail (FIFO)
               end if;
               FIFO := append (D, FIFO)
               []
               if (FIFO != {}) then 
                  Output (Head (FIFO), true);
                  FIFO := tail (FIFO)
               else
                  Output (D,false)
               end if
            end select 
         end loop
      end var
   end process
end module