-------------------------------------------------------- ------------------------ -- -- -- OCARINA COMPONENTS -- -- -- -- O C A R I N A . P N . C O M P O N E N T S -- -- -- -- B o d y -- -- -- -- Copyright (C) 2006, GET-Telecom Paris. -- -- -- -- 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 Ocarina team -- -- (ocarina-users@listes.enst.fr) -- -- -- ------------------------------------------------------------------------------ with Ocarina.Nodes; with Namet; with Ocarina.PN.Nodes; with Ocarina.PN.Nutils; with Ocarina.PN.Root; with Ocarina.Entities; with Ocarina.Entities.Components; with Ocarina.Expander.Queries; with Ocarina.Nutils; with Ocarina.AADL_Values; package body Ocarina.PN.Components is package ON renames Ocarina.Nodes; package OPU renames Ocarina.PN.Nutils; package OPN renames Ocarina.PN.Nodes; package ONU renames Ocarina.Nutils; function Process_Component_Instance (Instance : Types.Node_Id; PN_Root : Types.Node_Id) return Boolean; function Process_Thread_Instance (Instance : Types.Node_Id; PN_Root : Types.Node_Id) return Boolean; function Process_Virtual_Connections (Instance_Root : Types.Node_Id; PN_Root : Types.Node_Id) return Boolean; function Create_PN_Connection (Instance_Root, Port_Instance, PN_Root : Types.Node_Id) return Types.Node_Id; procedure Create_Connection_Arcs (PN_Connection, PN_Root : Types.Node_Id); procedure Create_Acknowledgement_Arc (Srce_Thread, Dest_Thread, PN_Root : Types.Node_Id); procedure Process_Thread_Port (Port_Instance, PN_Thread, PN_Root : Types.Node_Id; Value_Var, Control_Var : in out Types.Node_Id; Success : out Boolean); procedure Make_Ack_Place (PN_Root, PN_Thread : Types.Node_Id); -------------------- -- Make_Ack_Place -- -------------------- procedure Make_Ack_Place (PN_Root, PN_Thread : Types.Node_Id) is use Types; use Namet; use Ocarina.PN.Nodes; use Ocarina.PN.Nutils; use Ocarina.Expander.Queries; pragma Assert (PN_Root /= No_Node and then Kind (PN_Root) = K_Root_Node); pragma Assert (PN_Thread /= No_Node and then Kind (PN_Thread) = K_Thread_Box); begin if Ack_Place (PN_Thread) = No_Node then Set_Str_To_Name_Buffer (Get_Name_String (Name (Identifier (PN_Thread)))); Add_Str_To_Name_Buffer ("_ack"); Set_Ack_Place (PN_Thread, Make_Place_Declaration (Place_Name => Name_Find, Color_Class => Class_Control (PN_Root))); Set_Ack_Link (PN_Thread, Make_Connection (Body_Transition (PN_Thread), Ack_Place (PN_Thread), Make_Marking (No_Node, False))); end if; end Make_Ack_Place; ----------------------------------- -- Process_Architecture_Instance -- ----------------------------------- function Process_Architecture_Instance (Architecture_Instance : Types.Node_Id; Options : PN_Options) return Types.Node_Id is use Types; use Ocarina.Nodes; use Ocarina.PN.Root; use Ocarina.Nutils; pragma Unreferenced (Options); pragma Assert (Architecture_Instance /= No_Node and then Kind (Architecture_Instance) = K_Architecture_Instance); Instance : Node_Id; PN_Tree_Root : Node_Id; Success : Boolean; begin Instance := Root_System (Architecture_Instance); -- We get the root system of the AADL architecture PN_Tree_Root := Make_Root_Node; -- Preparing the neutral tree root if Instance /= No_Node then Success := Process_Component_Instance (Instance, PN_Tree_Root) and then Process_Virtual_Connections (Architecture_Instance, PN_Tree_Root); end if; if Success then return PN_Tree_Root; else return No_Node; end if; end Process_Architecture_Instance; -------------------------------- -- Process_Component_Instance -- -------------------------------- function Process_Component_Instance (Instance : Types.Node_Id; PN_Root : Types.Node_Id) return Boolean is use Ocarina.Entities.Components; use Ocarina.PN.Nodes; use Types; use Ocarina.Nodes; use Ocarina.Entities; pragma Assert (Instance /= No_Node and then Kind (Instance) = ON.K_Component_Instance and then (Get_Category_Of_Component (Instance) = CC_System or else Get_Category_Of_Component (Instance) = CC_Process)); pragma Assert (PN_Root /= No_Node and then Kind (PN_Root) = K_Root_Node); Success : Boolean := True; List_Node : Node_Id; Active_Subcomponents : Integer := 0; begin if not ONU.Is_Empty (Subcomponents (Instance)) then List_Node := ON.First_Node (Subcomponents (Instance)); while List_Node /= No_Node loop case Get_Category_Of_Component (Corresponding_Instance (List_Node)) is when CC_Process | CC_System => Success := Process_Component_Instance (Corresponding_Instance (List_Node), PN_Root) and then Success; Active_Subcomponents := Active_Subcomponents + 1; when CC_Thread => Success := Process_Thread_Instance (Corresponding_Instance (List_Node), PN_Root) and then Success; Active_Subcomponents := Active_Subcomponents + 1; when others => null; end case; List_Node := ON.Next_Node (List_Node); end loop; end if; -- If the component instance did not contain any active -- subcomponent (thread, process, system), then we -- assimilate it with a thread. if Active_Subcomponents = 0 then Success := Process_Thread_Instance (Instance, PN_Root); end if; return Success; end Process_Component_Instance; ----------------------------- -- Process_Thread_Instance -- ----------------------------- function Process_Thread_Instance (Instance : Types.Node_Id; PN_Root : Types.Node_Id) return Boolean is use Types; use Namet; use ON; use Ocarina.AADL_Values; use Ocarina.PN.Nodes; use Ocarina.PN.Nutils; use Ocarina.Entities; use Ocarina.Entities.Components; use Ocarina.Expander.Queries; use Ocarina.PN.Root; pragma Assert (Instance /= No_Node and then ON.Kind (Instance) = ON.K_Component_Instance and then (Get_Category_Of_Component (Instance) = CC_Thread or else Get_Category_Of_Component (Instance) = CC_Process or else Get_Category_Of_Component (Instance) = CC_System)); -- Empty processes or systems are assimilated with threads pragma Assert (PN_Root /= No_Node and then OPN.Kind (PN_Root) = OPN.K_Root_Node); Identifier, List_Node : Node_Id; Thread_Name : Name_Id; PN_Instance : constant Node_Id := New_Node (K_Thread_Box); Is_Cyclic : Boolean; Success : Boolean := True; Value_Var, Control_Var : Types.Node_Id; begin Is_Cyclic := not (Is_Defined_Enumeration_Property (Instance, Get_Name_String (Dispatch_Property)) and then Get_Enumeration_Property (Instance, Get_Name_String (Dispatch_Property)) = Background_Dispatch); -- By default, thread are considered cyclic Thread_Name := Compute_Absolute_Name_Of_Entity (Instance, Separator); Identifier := Make_Identifier (PN_Instance, Thread_Name); OPN.Set_Identifier (PN_Instance, Identifier); Set_Control_Color_Value (PN_Instance, New_Value (Declare_New_Thread (PN_Root))); Set_Arcs (PN_Instance, New_List (K_List_Id)); Set_Place_Fusions (PN_Instance, New_List (K_List_Id)); Set_Arc_Fusions (PN_Instance, New_List (K_List_Id)); Set_Subnets (PN_Instance, New_List (K_List_Id)); Set_Include_Call (PN_Instance, No_Node); Set_Ports (PN_Instance, New_List (K_List_Id)); Set_Ack_Place (PN_Instance, No_Node); Set_Ack_Link (PN_Instance, No_Node); -- create the standard thread pattern Control_Var := Get_New_Control_Variable (PN_Root, No_Node); Value_Var := No_Node; Get_Name_String (Thread_Name); Add_Str_To_Name_Buffer ("_restart"); Set_Begin_Node (PN_Instance, Make_Place_Declaration (Place_Name => Name_Find, Color_Class => Class_Control (PN_Root), Initial_Marking => Make_Marking (Make_Color_Variable (Control_Color_Value (PN_Instance))))); Get_Name_String (Thread_Name); Add_Str_To_Name_Buffer ("_finish"); Set_End_Node (PN_Instance, Make_Place_Declaration (Place_Name => Name_Find, Color_Class => Class_Control (PN_Root))); Get_Name_String (Thread_Name); Set_Body_Transition (PN_Instance, Make_Transition_Declaration (Transition_Name => Name_Find)); Append_Node_To_List (Make_Connection (Begin_Node (PN_Instance), Body_Transition (PN_Instance), Make_Marking (Make_Color_Variable (Control_Color_Value (PN_Instance)))), Arcs (PN_Instance)); Append_Node_To_List (Make_Connection (Body_Transition (PN_Instance), End_Node (PN_Instance), Make_Marking (Make_Color_Variable (Control_Color_Value (PN_Instance)))), Arcs (PN_Instance)); if Is_Cyclic then Get_Name_String (Thread_Name); Add_Str_To_Name_Buffer ("_reset"); Set_Reset_Transition (PN_Instance, Make_Transition_Declaration (Transition_Name => Name_Find)); Append_Node_To_List (Make_Equal_Guard (Var => OPN.Value (Control_Var), Cst => Control_Color_Value (PN_Instance)), Guards (Reset_Transition (PN_Instance))); Append_Node_To_List (Make_Connection (End_Node (PN_Instance), Reset_Transition (PN_Instance), Make_Marking (Make_Color_Variable (OPN.Value (Control_Var)))), Arcs (PN_Instance)); -- We use a variable here instead of the constant color of -- the thread number so that we can set a guard with this -- variable name. Thus we avoid having to check if an arc -- will point to the transition reset from another thread, -- since we ensure the variable name of the guard will be -- used in any case. Append_Node_To_List (Make_Connection (Reset_Transition (PN_Instance), Begin_Node (PN_Instance), Make_Marking (Make_Color_Variable (Control_Color_Value (PN_Instance)))), Arcs (PN_Instance)); end if; -- manage the ports if not Ocarina.Nutils.Is_Empty (Features (Instance)) then List_Node := ON.First_Node (Features (Instance)); while List_Node /= No_Node loop if Kind (List_Node) = K_Port_Spec_Instance then Process_Thread_Port (List_Node, PN_Instance, PN_Root, Value_Var, Control_Var, Success); end if; List_Node := ON.Next_Node (List_Node); end loop; end if; OPU.Append_Node_To_List (PN_Instance, Subnets (PN_Root)); return Success; end Process_Thread_Instance; ------------------------- -- Process_Thread_Port -- ------------------------- procedure Process_Thread_Port (Port_Instance, PN_Thread, PN_Root : Types.Node_Id; Value_Var, Control_Var : in out Types.Node_Id; Success : out Boolean) is use Types; use Namet; use ON; use OPN; use Ocarina.PN.Nutils; use Ocarina.Expander.Queries; use Ocarina.AADL_Values; use Ocarina.PN.Root; pragma Assert (PN_Thread /= No_Node and then OPN.Kind (PN_Thread) = OPN.K_Thread_Box); pragma Assert (Port_Instance /= No_Node and then ON.Kind (Port_Instance) = ON.K_Port_Spec_Instance); pragma Assert (PN_Root /= No_Node and then OPN.Kind (PN_Root) = OPN.K_Root_Node); New_Port : Node_Id; Marking : Node_Id; Value_Val, Control_Val : Value_Id; begin if Is_In (Port_Instance) then Value_Var := Get_New_Value_Variable (PN_Root, Value_Var); Control_Var := Get_New_Control_Variable (PN_Root, Control_Var); Value_Val := OPN.Value (Value_Var); Control_Val := OPN.Value (Control_Var); if ON.Is_Event (Port_Instance) then New_Port := Make_Place_Declaration (Place_Name => Compute_Absolute_Name_Of_Entity (Port_Instance, Separator), Color_Class => Domain_Comm (PN_Root)); Set_Kind (New_Port, K_Port); Set_Parent_Box (New_Port, PN_Thread); Set_Corresponding_Feature (New_Port, Port_Instance); Set_Is_Event_Port (New_Port, True); Marking := Make_Marking (Make_Color_Variable (Value_Val)); Add_Token_To_Marking (Marking, Make_Color_Variable (Control_Val)); Set_Tuple (Marking, True); Append_Node_To_List (Make_Connection (Srce => New_Port, Dest => Body_Transition (PN_Thread), Marking => Marking), Arcs (PN_Thread)); else Set_Str_To_Name_Buffer ("u"); Marking := Make_Marking (Make_Color_Variable (New_String_Value (Name_Find))); Add_Token_To_Marking (Marking, Make_Color_Variable (Control_Color_Value (PN_Thread))); Set_Tuple (Marking, True); New_Port := Make_Place_Declaration (Place_Name => Compute_Absolute_Name_Of_Entity (Port_Instance, Separator), Color_Class => Domain_Comm (PN_Root), Initial_Marking => Marking); Set_Kind (New_Port, K_Port); Set_Parent_Box (New_Port, PN_Thread); Set_Corresponding_Feature (New_Port, Port_Instance); Set_Is_Event_Port (New_Port, False); -- XXX we should reference the declaration of the undefined -- value Marking := Make_Marking (Make_Color_Variable (Value_Val)); Add_Token_To_Marking (Marking, Make_Color_Variable (Control_Val)); Set_Tuple (Marking, True); Append_Node_To_List (Make_Connection (Srce => New_Port, Dest => Body_Transition (PN_Thread), Marking => Marking), Arcs (PN_Thread)); Append_Node_To_List (Make_Connection (Srce => Body_Transition (PN_Thread), Dest => New_Port, Marking => Marking), Arcs (PN_Thread)); -- This second connection is the feedback for non event -- ports Append_Node_To_List (Make_Unequal_Guard (Var => Value_Val, Cst => New_String_Value (Undefined_Value_Variable)), Guards (Body_Transition (PN_Thread))); end if; Append_Node_To_List (New_Port, Ports (PN_Thread)); -- acknowledgement places Make_Ack_Place (PN_Root, PN_Thread); Add_Token_To_Marking (OPN.Marking (Ack_Link (PN_Thread)), Make_Color_Variable (OPN.Value (Control_Var))); -- the acknowledgement place will hold a token of same color as -- the corresponding input port end if; if Is_Out (Port_Instance) then New_Port := Make_Place_Declaration (Place_Name => Compute_Absolute_Name_Of_Entity (Port_Instance, Separator), Color_Class => Domain_Comm (PN_Root)); Set_Kind (New_Port, K_Port); Set_Parent_Box (New_Port, PN_Thread); Set_Corresponding_Feature (New_Port, Port_Instance); Set_Is_Event_Port (New_Port, True); Set_Str_To_Name_Buffer ("d"); Marking := Make_Marking (Make_Color_Variable (New_String_Value (Name_Find))); Add_Token_To_Marking (Marking, Make_Color_Variable (Control_Color_Value (PN_Thread))); Set_Tuple (Marking, True); -- the output ports are marked with the defined value and -- the control color of the thread Append_Node_To_List (Make_Connection (Srce => Body_Transition (PN_Thread), Dest => New_Port, Marking => Marking), Arcs (PN_Thread)); Append_Node_To_List (New_Port, Ports (PN_Thread)); end if; Success := True; end Process_Thread_Port; --------------------------------- -- Process_Virtual_Connections -- --------------------------------- function Process_Virtual_Connections (Instance_Root : Types.Node_Id; PN_Root : Types.Node_Id) return Boolean is use Types; use ONU; use OPU; use ON; use OPN; pragma Assert (Instance_Root /= No_Node and then ON.Kind (Instance_Root) = ON.K_Architecture_Instance); pragma Assert (PN_Root /= No_Node and then OPN.Kind (PN_Root) = OPN.K_Root_Node); List_Node, Port_Node : Node_Id; PN_Connection : Node_Id; begin if not OPU.Is_Empty (Subnets (PN_Root)) then List_Node := OPN.First_Node (Subnets (PN_Root)); while List_Node /= No_Node loop if Kind (List_Node) = K_Thread_Box and then not OPU.Is_Empty (Ports (List_Node)) then Port_Node := OPN.First_Node (Ports (List_Node)); while Port_Node /= No_Node loop PN_Connection := Create_PN_Connection (Instance_Root, Port_Node, PN_Root); if PN_Connection /= No_Node then Create_Connection_Arcs (PN_Connection, PN_Root); OPU.Append_Node_To_List (PN_Connection, OPN.Connections (PN_Root)); end if; Port_Node := OPN.Next_Node (Port_Node); end loop; end if; List_Node := OPN.Next_Node (List_Node); end loop; end if; return True; end Process_Virtual_Connections; ---------------------------- -- Create_Connection_Arcs -- ---------------------------- procedure Create_Connection_Arcs (PN_Connection, PN_Root : Types.Node_Id) is use Types; use Ocarina.PN.Nodes; use Ocarina.PN.Root; use Ocarina.PN.Nutils; pragma Assert (PN_Connection /= No_Node and then Kind (PN_Connection) = K_Connection); pragma Assert (PN_Root /= No_Node and then Kind (PN_Root) = K_Root_Node); Marking : Node_Id; List_Node : Node_Id; Control_Var : constant Node_Id := Get_New_Control_Variable (PN_Root, No_Node); Value_Var : constant Node_Id := Get_New_Value_Variable (PN_Root, No_Node); Value_Val : constant Value_Id := OPN.Value (Value_Var); Control_Val : constant Value_Id := OPN.Value (Control_Var); begin Marking := Make_Marking (Make_Color_Variable (Value_Val)); Add_Token_To_Marking (Marking, Make_Color_Variable (Control_Val)); Set_Tuple (Marking, True); Append_Node_To_List (Make_Connection (Source (PN_Connection), Connection_Transition (PN_Connection), Marking), Arcs (PN_Connection)); List_Node := First_Node (Destinations (PN_Connection)); while List_Node /= No_Node loop Append_Node_To_List (Make_Connection (Connection_Transition (PN_Connection), Item (List_Node), Marking), Arcs (PN_Connection)); if not Is_Event (PN_Connection) then Append_Node_To_List (Make_Connection (Item (List_Node), Connection_Transition (PN_Connection), Marking), Arcs (PN_Connection)); -- If the connection connects data ports, we set a back -- arc to replace the token of the destination place end if; List_Node := Next_Node (List_Node); end loop; end Create_Connection_Arcs; -------------------------- -- Create_PN_Connection -- -------------------------- function Create_PN_Connection (Instance_Root, Port_Instance, PN_Root : Types.Node_Id) return Types.Node_Id is use Types; use Ocarina.PN.Nutils; use ON; use OPN; use ONU; pragma Assert (Instance_Root /= No_Node and then ON.Kind (Instance_Root) = ON.K_Architecture_Instance); pragma Assert (PN_Root /= No_Node and then OPN.Kind (PN_Root) = OPN.K_Root_Node); Cnx_Node : Node_Id; PN_Connection : Node_Id := No_Node; Success : Boolean := True; begin if not ONU.Is_Empty (Virtual_Connections (Instance_Root)) then Cnx_Node := ON.First_Node (Virtual_Connections (Instance_Root)); while Cnx_Node /= No_Node loop if ON.Source (Cnx_Node) = Corresponding_Feature (Port_Instance) then if PN_Connection = No_Node then PN_Connection := Make_PN_Connection (PN_Root, Cnx_Node); Success := (PN_Connection /= No_Node); else Success := Aggregate_Virtual_Connection (PN_Root, Cnx_Node, PN_Connection) and then Success; end if; if Success then Create_Acknowledgement_Arc (Srce_Thread => Parent_Box (OPN.Item (OPN.Last_Node (OPN.Destinations (PN_Connection)))), Dest_Thread => Parent_Box (OPN.Source (PN_Connection)), PN_Root => PN_Root); -- we build the acknowledgement arc that -- corresponds to the newly created connection end if; end if; Cnx_Node := ON.Next_Node (Cnx_Node); end loop; end if; if Success then return PN_Connection; else return No_Node; end if; end Create_PN_Connection; -------------------------------- -- Create_Acknowledgement_Arc -- -------------------------------- procedure Create_Acknowledgement_Arc (Srce_Thread, Dest_Thread, PN_Root : Types.Node_Id) is use Types; use Ocarina.PN.Nodes; use Ocarina.PN.Nutils; use Ocarina.PN.Root; pragma Assert (PN_Root /= No_Node and then Kind (PN_Root) = K_Root_Node); pragma Assert (Srce_Thread /= No_Node and then Kind (Srce_Thread) = K_Thread_Box); pragma Assert (Dest_Thread /= No_Node and then Kind (Dest_Thread) = K_Thread_Box); List_Node : Node_Id; Ack_Place : constant Node_Id := OPN.Ack_Place (Srce_Thread); Reset_Transition : constant Node_Id := OPN.Reset_Transition (Dest_Thread); begin if Reset_Transition /= No_Node then -- we only build an acknowledgement arc if the sender thread -- is cyclic if not Is_Empty (Arcs (PN_Root)) then List_Node := First_Node (Arcs (PN_Root)); while List_Node /= No_Node loop if First_Reference (List_Node) = Ack_Place and then Second_Reference (List_Node) = Reset_Transition then Add_Token_To_Marking (Marking => Marking (List_Node), Token => Make_Color_Variable (Value (Get_New_Control_Variable (PN_Root, No_Node)))); -- if the arc already exists, we add a marking to it return; end if; List_Node := Next_Node (List_Node); end loop; end if; -- else we create a new arc List_Node := Make_Connection (Ack_Place, Reset_Transition, Make_Marking (Make_Color_Variable (Value (Get_New_Control_Variable (PN_Root, No_Node))), False)); Append_Node_To_List (List_Node, Arcs (PN_Root)); end if; end Create_Acknowledgement_Arc; end Ocarina.PN.Components;