ocarina-backends-alloy.adb 11.1 KB
Newer Older
yoogx's avatar
yoogx committed
1 2 3 4 5 6 7 8
------------------------------------------------------------------------------
--                                                                          --
--                           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                                  --
--                                                                          --
yoogx's avatar
yoogx committed
9
--                   Copyright (C) 2014-2016 ESA & ISAE.                    --
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
--                                                                          --
-- Ocarina  is free software; you can redistribute it and/or modify under   --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion. 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.                     --
--                                                                          --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception,   --
-- version 3.1, as published by the Free Software Foundation.               --
--                                                                          --
-- You should have received a copy of the GNU General Public License and    --
-- a copy of the GCC Runtime Library Exception along with this program;     --
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
-- <http://www.gnu.org/licenses/>.                                          --
yoogx's avatar
yoogx committed
26 27 28 29 30
--                                                                          --
--                 Ocarina is maintained by the TASTE project               --
--                      (taste-users@lists.tuxfamily.org)                   --
--                                                                          --
------------------------------------------------------------------------------
31

yoogx's avatar
yoogx committed
32
with Charset;           use Charset;
yoogx's avatar
yoogx committed
33 34 35
with Ocarina.Namet;
with Ocarina.ME_AADL;
with Ocarina.ME_AADL.AADL_Instances.Nodes;
yoogx's avatar
yoogx committed
36
with Ocarina.Instances; use Ocarina.Instances;
yoogx's avatar
yoogx committed
37
with Ocarina.ME_AADL.AADL_Instances.Entities;
38 39
use Ocarina.ME_AADL.AADL_Instances.Entities;

yoogx's avatar
yoogx committed
40
with Ocarina.Backends.Utils;
yoogx's avatar
yoogx committed
41 42 43 44 45 46 47 48 49
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;
yoogx's avatar
yoogx committed
50
   use Ocarina.Backends.Utils;
yoogx's avatar
yoogx committed
51 52 53 54 55 56 57 58
   use AIN;

   procedure Visit (E : Node_Id);

   procedure Visit_Architecture_Instance (E : Node_Id);

   procedure Visit_Component_Instance (E : Node_Id);

yoogx's avatar
yoogx committed
59
   FD               : File_Type;
yoogx's avatar
yoogx committed
60
   Root_System_Name : Name_Id;
yoogx's avatar
yoogx committed
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

   -----------
   -- 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
      Category_Name_String : constant array
yoogx's avatar
yoogx committed
95
      (Component_Category'Range) of Name_Id :=
yoogx's avatar
yoogx committed
96 97 98 99 100 101 102 103 104 105 106 107 108
        (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,
yoogx's avatar
yoogx committed
109 110
         CC_Virtual_Bus       => Get_String_Name ("virtual_bus"),
         CC_Virtual_Processor => Get_String_Name ("virtual_processor"));
yoogx's avatar
yoogx committed
111 112 113 114 115 116 117 118 119 120 121

      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
yoogx's avatar
yoogx committed
122 123 124 125 126 127 128
         Put_Line
           (FD,
            "one sig " &
            To_Lower
              (Get_Name_String
                 (Normalize_Name (Fully_Qualified_Instance_Name (E)))) &
            " extends Component{}{");
yoogx's avatar
yoogx committed
129

yoogx's avatar
yoogx committed
130
      else
yoogx's avatar
yoogx committed
131
         Root_System_Name := Normalize_Name (Display_Name (Identifier (E)));
yoogx's avatar
yoogx committed
132

yoogx's avatar
yoogx committed
133 134 135 136 137
         Put_Line
           (FD,
            "one sig " &
            To_Lower (Get_Name_String (Root_System_Name)) &
            " extends Component{}{");
yoogx's avatar
yoogx committed
138 139
      end if;

yoogx's avatar
yoogx committed
140 141 142 143 144
      Put_Line
        (FD,
         ASCII.HT &
         "type=" &
         Get_Name_String (Category_Name_String (Category)));
yoogx's avatar
yoogx committed
145 146 147 148 149 150 151 152 153

      --  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 :=
yoogx's avatar
yoogx committed
154
                 To_Lower
yoogx's avatar
yoogx committed
155 156 157 158
                   (Get_Name_String
                      (Normalize_Name
                         (Fully_Qualified_Instance_Name
                            (Corresponding_Instance (T)))));
yoogx's avatar
yoogx committed
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
            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;

yoogx's avatar
yoogx committed
174
      --  Rule #3: list properties
yoogx's avatar
yoogx committed
175 176 177 178 179

      Put (FD, ASCII.HT & "properties=");
      if Present (AIN.Properties (E)) then
         T := First_Node (AIN.Properties (E));
         while Present (T) loop
yoogx's avatar
yoogx committed
180 181 182 183 184
            Put
              (FD,
               To_Lower
                 (Get_Name_String
                    (Normalize_Name (Display_Name (Identifier (T))))));
yoogx's avatar
yoogx committed
185 186 187 188 189
            T := Next_Node (T);
            if Present (T) then
               Put (FD, "+");
            end if;
         end loop;
yoogx's avatar
yoogx committed
190
         New_Line (FD);
yoogx's avatar
yoogx committed
191 192 193 194 195 196 197 198

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

      --  Close create of component

      Put_Line (FD, "}");
yoogx's avatar
yoogx committed
199
      New_Line (FD);
yoogx's avatar
yoogx committed
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

      --  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
      Instance_Root : Node_Id;
230

yoogx's avatar
yoogx committed
231 232 233 234 235 236 237 238 239 240
   begin
      --  Instantiate the AADL tree

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

      --  Open a new .als file

241
      Create (File => FD, Name => "con_model.als");
yoogx's avatar
yoogx committed
242

yoogx's avatar
yoogx committed
243 244 245
      Put_Line (FD, "// This file has been generated by Ocarina");
      Put_Line (FD, "// DO NOT EDIT IT");
      New_Line (FD);
246
      Put_Line (FD, "module con_model");
yoogx's avatar
yoogx committed
247
      Put_Line (FD, "open lib/data_structure");
yoogx's avatar
yoogx committed
248
      New_Line (FD);
yoogx's avatar
yoogx committed
249

yoogx's avatar
yoogx committed
250
      --  Visit instance model
251

yoogx's avatar
yoogx committed
252 253 254
      New_Line (FD);
      Put_Line (FD, "// Mapping of the AADL instance tree");
      New_Line (FD);
yoogx's avatar
yoogx committed
255 256 257

      Visit_Architecture_Instance (Instance_Root);

yoogx's avatar
yoogx committed
258 259 260
      --  Add global contract

      New_Line (FD);
yoogx's avatar
yoogx committed
261 262 263
      Put_Line
        (FD,
         "// Declaration of the contract(s) " & "representing the model(s)");
yoogx's avatar
yoogx committed
264
      New_Line (FD);
yoogx's avatar
yoogx committed
265
      Put_Line (FD, "one sig aadl_model extends Contract{}{");
yoogx's avatar
yoogx committed
266 267 268
      Put_Line (FD, ASCII.HT & "assumption=none");
      Put_Line (FD, ASCII.HT & "input=none");
      Put_Line (FD, ASCII.HT & "guarantee=none");
269 270 271 272

      --  Generate output

      declare
yoogx's avatar
yoogx committed
273 274 275
         Print_Subcomponents : Boolean          := True;
         E                   : constant Node_Id := Root_System (Instance_Root);
         T                   : Node_Id;
276 277 278 279 280 281 282 283
      begin
         --  We consider two patterns
         --  a) system with subcomponents as system/bus/device only
         --  b) general case

         if Present (Subcomponents (E)) then
            T := First_Node (Subcomponents (E));
            while Present (T) loop
yoogx's avatar
yoogx committed
284 285 286 287 288 289
               Print_Subcomponents :=
                 Print_Subcomponents
                 and then
                 (Get_Category_Of_Component (T) = CC_System
                  or else Get_Category_Of_Component (T) = CC_Device
                  or else Get_Category_Of_Component (T) = CC_Bus);
290 291 292 293 294 295 296
               T := Next_Node (T);
            end loop;
         end if;

         --  We are in case a), generate all subcomponents of root system

         if Print_Subcomponents then
yoogx's avatar
yoogx committed
297
            Put (FD, ASCII.HT & "output=");
298 299 300 301 302 303
            if Present (Subcomponents (E)) then
               T := First_Node (Subcomponents (E));
               while Present (T) loop
                  declare
                     Subcomponent_Name : constant String :=
                       To_Lower
yoogx's avatar
yoogx committed
304 305 306 307
                         (Get_Name_String
                            (Normalize_Name
                               (Fully_Qualified_Instance_Name
                                  (Corresponding_Instance (T)))));
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324
                  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;
         else
            --  We are in case b), generate only root system

yoogx's avatar
yoogx committed
325 326 327 328 329
            Put_Line
              (FD,
               ASCII.HT &
               "output=" &
               To_Lower (Get_Name_String (Root_System_Name)));
330 331 332
         end if;
      end;

yoogx's avatar
yoogx committed
333 334 335
      Put_Line (FD, "}");

      --  Close file descriptor
yoogx's avatar
yoogx committed
336 337 338 339 340 341 342 343 344 345 346 347 348 349

      Close (FD);
   end Generate;

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

   procedure Reset is
   begin
      null;
   end Reset;

end Ocarina.Backends.Alloy;