ocarina-backends-alloy.adb 8.32 KB
Newer Older
yoogx's avatar
yoogx 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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
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
------------------------------------------------------------------------------
--                                                                          --
--                           OCARINA COMPONENTS                             --
--                                                                          --
--               O C A R I N A . B A C K E N D S . A L L O Y                --
--                                                                          --
--                                 B o d y                                  --
--                                                                          --
--                     Copyright (C) 2014 ESA & ISAE.                       --
--                                                                          --
-- Ocarina  is free software;  you  can  redistribute  it and/or  modify    --
-- it under terms of the GNU General Public License as published by the     --
-- Free Software Foundation; either version 2, or (at your option) any      --
-- later version. Ocarina is distributed  in  the  hope  that it will be    --
-- useful, but WITHOUT ANY WARRANTY;  without even the implied warranty of  --
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General --
-- Public License for more details. You should have received  a copy of the --
-- GNU General Public License distributed with Ocarina; see file COPYING.   --
-- If not, write to the Free Software Foundation, 51 Franklin Street, Fifth --
-- Floor, Boston, MA 02111-1301, USA.                                       --
--                                                                          --
-- As a special exception,  if other files  instantiate  generics from this --
-- unit, or you link  this unit with other files  to produce an executable, --
-- this  unit  does not  by itself cause  the resulting  executable to be   --
-- covered  by the  GNU  General  Public  License. This exception does not  --
-- however invalidate  any other reasons why the executable file might be   --
-- covered by the GNU Public License.                                       --
--                                                                          --
--                 Ocarina is maintained by the TASTE project               --
--                      (taste-users@lists.tuxfamily.org)                   --
--                                                                          --
------------------------------------------------------------------------------

with Ocarina.Namet;
with Ocarina.ME_AADL;
with Ocarina.ME_AADL.AADL_Instances.Nodes;
with Ocarina.Instances;           use Ocarina.Instances;
with Ocarina.ME_AADL.AADL_Instances.Entities;
with GNAT.Command_Line;

with Ada.Text_IO;

package body Ocarina.Backends.Alloy is

   package AIN renames Ocarina.ME_AADL.AADL_Instances.Nodes;

   use Ocarina.Namet;
   use Ada.Text_IO;
   use Ocarina.ME_AADL;
   use AIN;

   procedure Visit (E : Node_Id);

   procedure Visit_Architecture_Instance (E : Node_Id);

   procedure Visit_Component_Instance (E : Node_Id);

   FD            : File_Type;

   -----------
   -- Visit --
   -----------

   procedure Visit (E : Node_Id) is
   begin
      case Kind (E) is
         when K_Architecture_Instance =>
            Visit_Architecture_Instance (E);

         when K_Component_Instance =>
            Visit_Component_Instance (E);

         when others =>
            null;
      end case;
   end Visit;

   ---------------------------------
   -- Visit_Architecture_Instance --
   ---------------------------------

   procedure Visit_Architecture_Instance (E : Node_Id) is
   begin
      Visit (Root_System (E));
   end Visit_Architecture_Instance;

   ------------------------------
   -- Visit_Component_Instance --
   ------------------------------

   procedure Visit_Component_Instance (E : Node_Id) is
      use Ocarina.ME_AADL.AADL_Instances.Entities;

      Category_Name_String : constant array
        (Component_Category'Range) of Name_Id :=
        (CC_Abstract          => Get_String_Name ("abstract"),
         CC_Bus               => Get_String_Name ("bus"),
         CC_Data              => Get_String_Name ("data"),
         CC_Device            => Get_String_Name ("device"),
         CC_Memory            => Get_String_Name ("memory"),
         CC_Process           => Get_String_Name ("process"),
         CC_Processor         => Get_String_Name ("processor"),
         CC_Subprogram        => Get_String_Name ("subprogram"),
         CC_Subprogram_Group  => Get_String_Name ("subprogram group"),
         CC_System            => Get_String_Name ("system"),
         CC_Thread            => Get_String_Name ("thread"),
         CC_Thread_Group      => Get_String_Name ("thread group"),
         CC_Unknown           => No_Name,
         CC_Virtual_Bus       => Get_String_Name ("virtual bus"),
         CC_Virtual_Processor => Get_String_Name ("virtual processor"));

      Category : constant Component_Category := Get_Category_Of_Component (E);

      T : Node_Id;
   begin
      --  Create Alloy component

      --  Rule #1: the name of this component is deduced from the name
      --  of the corresponding instance name

      if Present (Parent_Subcomponent (E)) then
         Put_Line (FD, "one sig " &
                     Get_Name_String
                     (Display_Name (Identifier (Parent_Subcomponent (E))))
                     & " extends Component{}{");
      else
         Put_Line (FD, "one sig " &
                  Get_Name_String (Display_Name (Identifier (E)))
                  & " extends Component{}{");

      end if;

      Put_Line (FD, ASCII.HT & "type="
                  & Get_Name_String (Category_Name_String (Category)));

      --  Rule #2: list subcomponents

      Put (FD, ASCII.HT & "subcomponents=");
      if Present (Subcomponents (E)) then
         T := First_Node (Subcomponents (E));
         while Present (T) loop
            declare
               Subcomponent_Name : constant String :=
                 String'(Get_Name_String
                           (Display_Name
                              (Identifier (T))));
            begin
               Put (FD, Subcomponent_Name);

               T := Next_Node (T);
               if Present (T) then
                  Put (FD, "+");
               end if;
            end;
         end loop;
         New_Line (FD);

      else
         Put_Line (FD, "none");
      end if;

      --  Rule#3: list properties

      Put (FD, ASCII.HT & "properties=");
      if Present (AIN.Properties (E)) then
         T := First_Node (AIN.Properties (E));
         while Present (T) loop
            Put (FD, Get_Name_String (Display_Name (Identifier (T))));
            T := Next_Node (T);
            if Present (T) then
               Put (FD, "+");
            end if;
         end loop;
         New_Line (Fd);

      else
         Put_Line (FD, "none");
      end if;

      --  Close create of component

      Put_Line (FD, "}");

      --  Iterate over subcomponents

      if Present (Subcomponents (E)) then
         T := First_Node (Subcomponents (E));
         while Present (T) loop
            Visit (Corresponding_Instance (T));

            T := Next_Node (T);
         end loop;
      end if;
   end Visit_Component_Instance;

   ----------
   -- Init --
   ----------

   procedure Init is
   begin
      --  Registration of the generator

      Register_Backend ("alloy", Generate'Access, Alloy_Backend);
   end Init;

   --------------
   -- Generate --
   --------------

   procedure Generate (AADL_Root : Node_Id) is
      use GNAT.Command_Line;

      Instance_Root : Node_Id;
   begin
      --  Instantiate the AADL tree

      Instance_Root := Instantiate_Model (AADL_Root);
      if No (Instance_Root) then
         raise Program_Error;
      end if;

      Initialize_Option_Scan;
      loop
         case Getopt ("* ") is

            when ASCII.NUL =>
               exit;

            when others =>
               null;
         end case;
      end loop;

      --  Open a new .als file

yoogx's avatar
yoogx committed
237
238
239
240
      Create (File => FD, Name => "tran_model.als");

      Put_Line (FD, "module tran_model");
      Put_Line (FD, "open lib_sig");
yoogx's avatar
yoogx committed
241

yoogx's avatar
yoogx committed
242
      --  Visit instance model
yoogx's avatar
yoogx committed
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260

      Visit_Architecture_Instance (Instance_Root);

      --  Close file descriptors

      Close (FD);
   end Generate;

   -----------
   -- Reset --
   -----------

   procedure Reset is
   begin
      null;
   end Reset;

end Ocarina.Backends.Alloy;