------------------------------------------------------------------------------ ------------------------------------------------------------------------------ -- Cheddar is a GNU GPL real-time scheduling analysis tool. -- This program provides services to automatically check schedulability and -- other performance criteria of real-time architecture models. -- -- Copyright (C) 2002-2016, Frank Singhoff, Alain Plantec, Jerome Legrand -- -- The Cheddar project was started in 2002 by -- Frank Singhoff, Lab-STICC UMR 6285 laboratory, Université de Bretagne Occidentale -- -- Cheddar has been published in the "Agence de Protection des Programmes/France" in 2008. -- Since 2008, Ellidiss technologies also contributes to the development of -- Cheddar and provides industrial support. -- -- The full list of contributors and sponsors can be found in AUTHORS.txt and SPONSORS.txt -- -- This program is free software; you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation; either version 2 of the License, or -- (at your option) any later version. -- -- This program 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 -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA -- -- -- Contact : cheddar@listes.univ-brest.fr -- ------------------------------------------------------------------------------ -- Last update : -- $Rev: 1249 $ -- $Date: 2014-08-28 07:02:15 +0200 (Fri, 28 Aug 2014) $ -- $Author: singhoff $ ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ with applicability_constraint.all_tasks_are_periodic; use applicability_constraint.all_tasks_are_periodic; with applicability_constraint.all_tasks_are_periodic_or_sporadic; use applicability_constraint.all_tasks_are_periodic_or_sporadic; with applicability_constraint.no_shared_cpu; use applicability_constraint.no_shared_cpu; with applicability_constraint.allowed_protocol; use applicability_constraint.allowed_protocol; with applicability_constraint.Pip_No_Deadlock; use applicability_constraint.Pip_No_Deadlock; with applicability_constraint.no_buffer; use applicability_constraint.no_buffer; with applicability_constraint.no_dependencies; use applicability_constraint.no_dependencies; with applicability_constraint.Ceiling_Priority_Assignment; use applicability_constraint.Ceiling_Priority_Assignment; with applicability_constraint.at_least_one_data; use applicability_constraint.at_least_one_data; with applicability_constraint.no_shared_resources; use applicability_constraint.no_shared_resources; with applicability_constraint.data_sharing_protocol; use applicability_constraint.data_sharing_protocol; with applicability_constraint.data_connectivity; use applicability_constraint.data_connectivity; with applicability_constraint.Unsimultaneous_Release_Time_Constraint; use applicability_constraint.Unsimultaneous_Release_Time_Constraint; with applicability_constraint.Simultaneous_Release_Time_Constraint; use applicability_constraint.Simultaneous_Release_Time_Constraint; with applicability_constraint.Period_Equal_Deadline_Constraint; use applicability_constraint.Period_Equal_Deadline_Constraint; with applicability_constraint.Period_Smaller_Than_Deadline_Constraint; use applicability_constraint.Period_Smaller_Than_Deadline_Constraint; with applicability_constraint.Period_Larger_Than_Deadline_Constraint; use applicability_constraint.Period_Larger_Than_Deadline_Constraint; with feasibility_tests_for_Time_Triggered_Communication; use feasibility_tests_for_Time_Triggered_Communication; with Applicability_Constraints_Main_Structure; use Applicability_Constraints_Main_Structure; with Applicability_Constraints_Main_Structure.extended; use Applicability_Constraints_Main_Structure.extended; with feasibility_tests_main_structure_factory; use feasibility_tests_main_structure_factory; with applicability_constraint.Uniprocessor_Scheduling_Protocol; use applicability_constraint.Uniprocessor_Scheduling_Protocol; with applicability_constraint.Uniprocessor_Quantum; use applicability_constraint.Uniprocessor_Quantum; with applicability_constraint.Uniprocessor_Preemptivity; use applicability_constraint.Uniprocessor_Preemptivity; with applicability_constraint.Uniprocessor; use applicability_constraint.Uniprocessor; with Generic_Graph; use Generic_Graph; with Dependencies; use Dependencies; with Ada.IO_Exceptions; use Ada.IO_Exceptions; with GNAT.Current_Exception; use GNAT.Current_Exception; with Unbounded_Strings; use Unbounded_Strings; with GNAT.Command_Line; use GNAT.Command_Line; with GNAT.OS_Lib; use GNAT.OS_Lib; with Text_IO; use Text_IO; with Version; use Version; with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with Systems; use Systems; with Task_Set; use Task_Set; with Task_Dependencies; use Task_Dependencies; use Task_Dependencies.Half_Dep_Set; with Processor_Set; use Processor_Set; with Address_Space_Set; use Address_Space_Set; with Resource_Set; use Resource_Set; with Buffer_Set; use Buffer_Set; with Call_Framework; use Call_Framework; with Tasks; use Tasks; use Task_Set.Generic_Task_Set; with Debug; use Debug; with Generic_Graph; use Generic_Graph; use Generic_Graph.Edge_Lists_Package; use Generic_Graph.Node_Lists_Package; with DP_Graph; use DP_Graph; with DP_Graph.Extended; use DP_Graph.Extended; with DP_Graph_view; use DP_Graph_view; use DP_Graph_view.Graph_List_Package; with architecture_factory; use architecture_factory; with Debug; use Debug; with Ada.Real_Time; use Ada.Real_Time; with translate; use translate; package body architecture_analyzer is function analyze (Sys : System) return Unbounded_String is result : Boolean := True; ACS : All_Cases_Structure; G : Graph; G2 : Graph; G3 : Graph; G_List : Graph_List; --temporary G_Iterator : Graph_List_Iterator; dp : design_pattern; compliant : Boolean; T_start : Time; T_stop : Time; execution_time : Time_Span; MS : Time_Span; execution_time_int : Integer; file_content : Unbounded_String; return_to_user : Unbounded_String; begin --Initialization -- MS := Milliseconds (1); T_start := Clock; return_to_user := empty_string; Initialize (G); G.cheddar_private_id := To_Unbounded_String ("Testing Graph"); return_to_user := return_to_user & To_Unbounded_String ("System Metrics: ") & unbounded_lf & To_Unbounded_String ("Number of resources:") & To_Unbounded_String (Get_Number_Of_Elements (Sys.Resources)'Img) & unbounded_lf & To_Unbounded_String ("Number of dependencies:") & To_Unbounded_String (Get_Number_Of_Elements (Sys.Dependencies.Depends)'Img) & unbounded_lf & To_Unbounded_String ("Number of tasks:") & To_Unbounded_String (Get_Number_Of_Elements (Sys.Tasks)'Img)& unbounded_lf & To_Unbounded_String ("Number of buffers:") & To_Unbounded_String (Get_Number_Of_Elements (Sys.buffers)'Img)& unbounded_lf & To_Unbounded_String ("Number of processors:") & To_Unbounded_String (Get_Number_Of_Elements (Sys.Processors)'Img)& unbounded_lf & unbounded_lf ; --Step 0: Environment verification -- if not Environment_Uni_Processor_Bool(Sys) then return_to_user := return_to_user & "The environment does not meet Uniprocessor Environment Constraint" & unbounded_lf & "The system will not be analyzed."& unbounded_lf & unbounded_lf & Environment_Uni_Processor_Txt(Sys); return return_to_user; end if; --Step 1: Building Dependency Graph -- put_debug(return_to_user); Put_Debug ("STEP1"); G := Build_Graph_From_System (Sys); Put_debug("************************Graph"); put_debug(To_Unbounded_String ("Nodes: ") & To_Unbounded_String (Get_Number_Of_Elements (G.nodes)'IMG)); put_debug(To_Unbounded_String ("Edges: ") & To_Unbounded_String (Get_Number_Of_Elements (G.edges)'IMG)); Put_debug("************************Graph"); -- Step 2 Graph analysis -- Put_Debug ("STEP2"); G_List := Connexity_View (G); put_debug(To_Unbounded_String ("GraphListLEnght: ") & To_Unbounded_String (Get_Number_Of_Elements (G_List)'IMG)); Put_Debug ("STEP2BIS"); dp := compose (G_List); compliant := False; Put_Debug ("STEP3"); -- Step 3 Design Pattern confirmation: Applying Applicability constraints -- case dp is when Time_Triggered_Communication => if Time_Triggered_Communication_Bool (Sys) then return_to_user := return_to_user & ("The system is a Time Triggered Communication Design Pattern instance.") & Unbounded_Lf; compliant := True; else return_to_user := return_to_user & Time_Triggered_Communication_Txt (Sys) & unbounded_lf; end if; when Ravenscar => if Ravenscar_Bool (Sys) then return_to_user := return_to_user & ("The system is a Ravenscar Design Pattern instance.") & Unbounded_Lf; compliant := True; else return_to_user := return_to_user & Ravenscar_Txt (Sys); end if; when Unplugged => if Unplugged_Bool (Sys) then return_to_user := return_to_user & ("The system is a Unplugged Design Pattern instance.") & Unbounded_Lf; compliant := True; else return_to_user := return_to_user & Unplugged_Txt (Sys); end if; end case; Put_Debug ("STEP4"); -- Step 4 Applicability case of feasibility tests determination -- if (compliant) then case dp is when Time_Triggered_Communication => Put_Debug("Before Building Main structure"); Time_Triggered_Communication_feasibility_tests_main_structure (ACS, Sys); Put_Debug("After Building Main structure"); evaluate (ACS, Sys); Put_Debug("Displaying AC evaluation"); Put(ACS); T_stop := Clock; execution_time := T_stop - T_start; execution_time_int := execution_time / MS; file_content := "Time_Triggered_Communication design pattern, selected feasibility tests: " & file_content & unbounded_lf & get_tests_list (ACS) & " Compute time:" & execution_time_int'Img; return_to_user := return_to_user & file_content; when Ravenscar => ravenscar_feasibility_tests_main_structure (ACS, Sys); evaluate (ACS, Sys); T_stop := Clock; execution_time := T_stop - T_start; execution_time_int := execution_time / MS; file_content := "Ravenscar design pattern, selected feasibility tests:" & file_content & get_tests_list (ACS) & " Compute time:" & execution_time_int'Img; return_to_user := return_to_user & file_content; when Unplugged => unplugged_feasibility_tests_main_structure (ACS, Sys); evaluate (ACS, Sys); T_stop := Clock; execution_time := T_stop - T_start; execution_time_int := execution_time / MS; file_content := "Unplugged design pattern, selected feasibility tests:" & file_content & get_tests_list (ACS) & " Compute time:" & execution_time_int'Img; return_to_user := return_to_user & file_content; end case; end if; return return_to_user; end analyze; function Time_Triggered_Communication_Txt (Sys : System) return Unbounded_String is result : Unbounded_String := "The system may be a Time_Triggered_Communication design pattern intance," & unbounded_lf & "but the following constraints are not met."& Unbounded_Lf; temp : Boolean := False; begin temp := R1 (Sys); if not (temp) then result := result & R1_txt & unbounded_lf; end if; temp := R5 (Sys); if not (temp) then result := result & R5_txt & unbounded_lf; end if; temp := R6 (Sys); if not (temp) then result := result & R6_txt & unbounded_lf; end if; temp := R7 (Sys); if not (temp) then result := result & R7_txt & unbounded_lf; end if; temp := R9_2 (Sys); if not (temp) then result := result & R9_2_txt & unbounded_lf; end if; return result; end Time_Triggered_Communication_Txt; function Time_Triggered_Communication_Bool (Sys : System) return boolean is result : Boolean := True; temp : Boolean := False; begin temp := R1 (Sys); result := (result and temp); temp := R5 (Sys); result := (result and temp); temp := R9_2 (Sys); result := (result and temp); temp := R6 (Sys); result := (result and temp); temp := R7 (Sys); result := (result and temp); temp := R9_2 (Sys); result := (result and temp); return result; end Time_Triggered_Communication_Bool; function Ravenscar_Txt (Sys : System) return Unbounded_String is result : Unbounded_String := "The system may be a Ravenscar design pattern intance," & unbounded_lf & "but the following constraints are not met."& Unbounded_Lf; temp : Boolean := False; begin temp := R8 (Sys); if not (temp) then result := result & R8_txt & unbounded_lf; end if; temp := R9_1 (Sys); if not (temp) then result := result & R9_1_txt & unbounded_lf; end if; temp := R9_2 (Sys); if not (temp) then result := result & R9_2_txt & unbounded_lf; end if; temp := R10 (Sys); if not (temp) then result := result & R10_txt & unbounded_lf; end if; temp := R11 (Sys); if not (temp) then result := result & R11_txt & unbounded_lf; end if; temp := R12 (Sys); if not (temp) then result := result & R12_txt & unbounded_lf; end if; temp := R13 (Sys); if not (temp) then result := result & R13_txt & unbounded_lf; end if; return result; end Ravenscar_Txt; function Ravenscar_Bool (Sys : System) return boolean is result : Boolean := True; temp : Boolean := False; begin temp := R8 (Sys); result := (result and temp); temp := R9_1 (Sys); result := (result and temp); temp := R9_2 (Sys); result := (result and temp); temp := R10 (Sys); result := (result and temp); temp := R11 (Sys); result := (result and temp); temp := R12 (Sys); result := (result and temp); temp := R13 (Sys); result := (result and temp); return result; end Ravenscar_Bool; function Unplugged_Txt (Sys : System) return Unbounded_String is result : Unbounded_String := "The system may be a Unplugged design pattern intance," & unbounded_lf & "but the following constraints are not met."& unbounded_lf ; temp : Boolean := False; begin temp := R7 (Sys); if not (temp) then result := result & R7_txt & unbounded_lf ; end if; temp := R8 (Sys); if not (temp) then result := result & R8_txt & unbounded_lf ; end if; temp := R15 (Sys); if not (temp) then result := result & R15_txt & unbounded_lf ; end if; return result; end Unplugged_Txt; function Unplugged_Bool (Sys : System) return boolean is result : Boolean := True; temp : Boolean := False; begin temp := R7 (Sys); result := (result and temp); temp := R8 (Sys); result := (result and temp); temp := R15 (Sys); result := (result and temp); return result; end Unplugged_Bool; function Environment_Uni_Processor_Txt (Sys : System) return Unbounded_String is result : Unbounded_String := empty_string; temp : Boolean := False; begin temp := R0 (Sys); if not (temp) then result := result & R0_txt & unbounded_lf; return result; end if; temp := R2 (Sys); if not (temp) then result := result & R2_txt & unbounded_lf; end if; temp := R3 (Sys); if not (temp) then result := result & R3_txt & unbounded_lf; end if; temp := R4 (Sys); if not (temp) then result := result & R4_txt & unbounded_lf; end if; return result; end Environment_Uni_Processor_Txt; function Environment_Uni_Processor_Bool (Sys : System) return boolean is result : Boolean := True; temp : Boolean := False; begin temp := R0 (Sys); result := (result and temp); if not result then return result; end if; temp := R2 (Sys); result := (result and temp); temp := R3 (Sys); result := (result and temp); temp := R4 (Sys); result := (result and temp); return result; end Environment_Uni_Processor_Bool; procedure write_result_to_file (Res : in Unbounded_String; File_Name : in Unbounded_String) is Into : File_Type; begin -- Create (Into, Mode => Out_File, Name => To_String (File_Name)); New_Line (Into); -- Put_Line (Into, To_String (Res)); New_Line (Into); Close (Into); end write_result_to_file; end architecture_analyzer;