Commit dbc15b29 authored by yoogx's avatar yoogx
Browse files

* Update Alloy backend to consider two kind of root systems

parent f37afb13
......@@ -36,6 +36,8 @@ with Ocarina.ME_AADL;
with Ocarina.ME_AADL.AADL_Instances.Nodes;
with Ocarina.Instances; use Ocarina.Instances;
with Ocarina.ME_AADL.AADL_Instances.Entities;
use Ocarina.ME_AADL.AADL_Instances.Entities;
with GNAT.Command_Line;
with Ocarina.Backends.Utils;
with Ada.Text_IO;
......@@ -91,8 +93,6 @@ package body Ocarina.Backends.Alloy is
------------------------------
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"),
......@@ -250,16 +250,17 @@ package body Ocarina.Backends.Alloy is
-- Open a new .als file
Create (File => FD, Name => "tran_model.als");
Create (File => FD, Name => "con_model.als");
Put_Line (FD, "// This file has been generated by Ocarina");
Put_Line (FD, "// DO NOT EDIT IT");
New_Line (FD);
Put_Line (FD, "module tran_model");
Put_Line (FD, "open lib_sig");
Put_Line (FD, "module con_model");
Put_Line (FD, "open alloy/common/lib_sig");
New_Line (FD);
-- Visit instance model
New_Line (FD);
Put_Line (FD, "// Mapping of the AADL instance tree");
New_Line (FD);
......@@ -276,8 +277,65 @@ package body Ocarina.Backends.Alloy is
Put_Line (FD, ASCII.HT & "assumption=none");
Put_Line (FD, ASCII.HT & "input=none");
Put_Line (FD, ASCII.HT & "guarantee=none");
Put_Line (FD, ASCII.HT & "output="
& To_Lower (Get_Name_String (Root_System_Name)));
-- Generate output
declare
Print_Subcomponents : Boolean := True;
E : constant Node_Id := Root_System (Instance_Root);
T : Node_Id;
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
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);
T := Next_Node (T);
end loop;
end if;
-- We are in case a), generate all subcomponents of root system
if Print_Subcomponents then
Put (Fd, ASCII.HT & "output=");
if Present (Subcomponents (E)) then
T := First_Node (Subcomponents (E));
while Present (T) loop
declare
Subcomponent_Name : constant String :=
To_Lower
(Get_Name_String
(Normalize_Name
(Fully_Qualified_Instance_Name
(Corresponding_Instance (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;
else
-- We are in case b), generate only root system
Put_Line (FD, ASCII.HT & "output="
& To_Lower (Get_Name_String (Root_System_Name)));
end if;
end;
Put_Line (FD, "}");
-- Close file descriptor
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment