asn1-iterators/src/asn1_iterators-exhaustive_simulation.adb

--- (c) 2017 European Space Agency / TASTE Project
+-- (c) 2017-2020 European Space Agency / TASTE Project
 package body ASN1_Iterators.Exhaustive_Simulation is
 
-    function State_Hash(Context: Context_Ty) return Hash_Type is
-        (Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(Context'Address).all)));
+    function State_Hash (Context : Context_Ty) return Hash_Type is
+        (Ada.Strings.Hash
+            (GNAT.MD5.Digest (as_sea_ptr (Context'Address).all)));
 
-    -- Add a state to the graph: compute the hash (key) and store if not already there
-    function Add_to_graph(event : Event_ty) return Hash_Type is
+    --  Add a state to the graph:
+    --  compute the hash (key) and store if not already there
+    function Add_To_Graph (Event : Event_ty) return Hash_Type is
         New_State: State_Access;
         New_Hash : Hash_Type;
-        New_Edge : constant Edge_ty := (event => event, state => backup_hash);
+        New_Edge : constant Edge_ty := (Event => Event, State => Backup_Hash);
     begin
-        New_Hash := State_Hash(Process_Ctxt.all);
-        if not Grafset.Contains(Key => New_Hash) then
+        New_Hash := State_Hash (Process_Ctxt.all);
+        if not Grafset.Contains (Key => New_Hash) then
             New_State := new Global_State;
-            New_State.context := Process_Ctxt.all;
-            Grafset.Insert(Key => New_Hash, New_Item => New_State);
+            New_State.Context := Process_Ctxt.all;
+            Grafset.Insert (Key => New_Hash, New_Item => New_State);
         else
-            New_State := Grafset.Element(Key => New_Hash);
+            New_State := Grafset.Element (Key => New_Hash);
         end if;
-        New_State.edges.append(New_Edge);
+        New_State.edges.append (New_Edge);
         return New_Hash;
-    end;
+    end Add_To_Graph;
 
-    -- Report the result of the property check to the user
-    procedure Check_And_Report (S_Hash: Hash_Type) is
-        errno: Natural := 0;
-        stop_condition: boolean := false;
+    --  Report the result of the property check to the user
+    procedure Check_And_Report (S_Hash : Hash_Type) is
+        errno          : Natural := 0;
+        Stop_Condition : Boolean := False;
     begin
-        count := count + 1;
-        if check_properties(errno) then
-            put_line("Property " & errno'img & " is verified, at step " & count'img);
-            stop_condition := true;
-            if properties.Length <= 10 then
-                properties.include(s_hash);
+        Count := Count + 1;
+        if Check_Properties (errno) then
+            Put_Line
+                ("Property "
+                & errno'Img & " is verified, at step " & Count'Img);
+            Stop_Condition := True;
+            if Properties.Length <= 10 then
+                Properties.Include (S_Hash);
             end if;
         end if;
-        if not visited.contains(s_hash) then
-            visited.insert(s_hash);
-            if stop_condition = false then
-                queue.append(S_Hash);
+        if not Visited.Contains (S_Hash) then
+            Visited.Insert (S_Hash);
+            if Stop_Condition = False then
+                Queue.Append (S_Hash);
             end if;
         end if;
-    end;
+    end Check_And_Report;
 
     procedure Generate_MSC is
-        package Loc_Maps is new Ordered_Maps(Key_Type     => Hash_Type,
-                                             Element_Type => Boolean);
-        package Evt_Lists is new Vectors(Element_Type => Event_ty,
-                                         Index_Type   => Natural);
-        package Parent_Maps is new Ordered_Maps(Key_Type     => Hash_Type,
-                                                Element_Type => Edge_ty);
-        function Find_Path(From: Hash_Type) return Evt_Lists.Vector is
+        package Loc_Maps is new Ordered_Maps (Key_Type     => Hash_Type,
+                                              Element_Type => Boolean);
+        package Evt_Lists is new Vectors (Element_Type => Event_ty,
+                                          Index_Type   => Natural);
+        package Parent_Maps is new Ordered_Maps (Key_Type     => Hash_Type,
+                                                 Element_Type => Edge_ty);
+        function Find_Path (From : Hash_Type) return Evt_Lists.Vector is
             Loc_Q       : Lists.Vector;
             Loc_Visited : Loc_Maps.Map;
             Next_Hash   : Hash_Type;
@@ -60,42 +64,45 @@ package body ASN1_Iterators.Exhaustive_Simulation is
             Edge        : Edge_Ty;
             Scenario    : Evt_Lists.Vector;
         begin
-            Loc_Q.append(From);
-            Loc_Visited.Include(Key => From, New_Item => True);
+            Loc_Q.append (From);
+            Loc_Visited.Include (Key => From, New_Item => True);
             while not Loc_Q.Is_Empty loop
                 Next_Hash := Loc_Q.Last_Element;
                 exit when Next_Hash = Start_Hash;
-                State := Grafset.Element(Key => Next_Hash);
+                State := Grafset.Element (Key => Next_Hash);
                 for each_edge of State.Edges loop
-                    if not Loc_Visited.Contains(each_edge.state) then
-                        Loc_Q.append(Each_Edge.state);
-                        Loc_Visited.Include(Key      => Each_Edge.State,
-                                            New_Item => True);
-                        Parent_Map.Include(Key      => Each_Edge.State,
-                                           New_Item => (State => Next_Hash,
-                                                        Event => Each_Edge.Event));
+                    if not Loc_Visited.Contains (each_edge.State) then
+                        Loc_Q.Append (each_edge.State);
+                        Loc_Visited.Include (Key      => each_edge.State,
+                                             New_Item => True);
+                        Parent_Map.Include (Key      => each_edge.State,
+                                            New_Item =>
+                                              (State => Next_Hash,
+                                               Event => each_edge.Event));
                     end if;
                 end loop;
                 Loc_Q.Delete_Last;
             end loop;
             Curr := Start_Hash;
-            Put_Line("Found path!");
-            while Parent_Map.Contains(Curr) loop
-                Edge := Parent_Map.Element(Curr);
+            Put_Line ("Found path!");
+            while Parent_Map.Contains (Curr) loop
+                Edge := Parent_Map.Element (Curr);
                 Curr := Edge.State;
-                Scenario.Append(Edge.Event);
+                Scenario.Append (Edge.Event);
             end loop;
             return Scenario;
-        end;
+        end Find_Path;
 
         Scenario : Evt_Lists.Vector;
     begin
-        for each_hash of properties loop
-            put_line("Path from hash " & each_hash'img & " to hash " & start_hash'img);
-            Scenario := Find_Path(each_hash);
+        for each_hash of Properties loop
+            Put_Line
+                ("Path from hash "
+                & each_hash'Img & " to hash " & Start_Hash'Img);
+            Scenario := Find_Path (each_hash);
             for each_evt of Scenario loop
-                Print_Event(each_evt);
+                Print_Event (each_evt);
             end loop;
         end loop;
-    end;
+    end Generate_MSC;
 end ASN1_Iterators.Exhaustive_Simulation;

asn1-iterators/src/asn1_iterators-exhaustive_simulation.ads

@@ -25,9 +25,9 @@ generic
 package ASN1_Iterators.Exhaustive_Simulation is
 
     -- To save/restore the context when calling a PI:
-    backup_ctxt : Context_ty;
-    backup_hash : Hash_Type;
-    start_hash  : Hash_Type;
+    Backup_Ctxt : Context_ty;
+    Backup_Hash : Hash_Type;
+    Start_Hash  : Hash_Type;
 
     -- An edge is made of a past state reference and an event to leave it
     type Edge_ty is

asn1-iterators/src/asn1_iterators-generic_basic.ads

@@ -15,7 +15,7 @@ package ASN1_Iterators.Generic_Basic is
       Is_Valid : Boolean := True;
    end record
        with Default_Iterator  => Iterate,
-            Iterator_Element  => P.Sort,
+            Iterator_Element  => Sort,
             Constant_Indexing => Element;
 
    procedure Initialize (Container : in out ASN1_Container);

taste-properties/properties/checker.py

@@ -64,7 +64,7 @@ def exhaust_procedure (interface: str, sort: str, model: str, param: bool) -> st
     if param:
         return f'''procedure Exhaust_{interface} is
    {interface}_It : {sort}_pkg.Instance;
-   Event  : Event_Ty ({interface}_PI);
+   Event  : Event_ty ({interface}_PI);
    S_Hash : Hash_Type;
 begin
    for Each of {interface}_it loop
@@ -79,7 +79,7 @@ begin
 end Exhaust_{interface};'''
     else:
         return f'''procedure Exhaust_{interface} is
-   Event  : Event_Ty ({interface}_PI);
+   Event  : Event_ty ({interface}_PI);
    S_Hash : Hash_Type;
 begin
    {model}.{interface};
@@ -125,7 +125,7 @@ procedure Model_Checker is
 
    --  Type representing an event (input or output)
    type Interfaces is (Start, {", ".join(interfaces)});
-   type Event_ty (Option: Interfaces := Start) is
+   type Event_ty (Option : Interfaces := Start) is
       record
          case Option is
             when Start =>
@@ -135,6 +135,7 @@ procedure Model_Checker is
       end record;
 
    --  Display scenario (in the future: generate MSC)
+   procedure Print_Event (Event: Event_ty);
    procedure Print_Event (Event: Event_ty) is
    begin
       case Event.Option is
@@ -142,10 +143,11 @@ procedure Model_Checker is
             Put_Line ("START");
          {indent(9, print_events)}
       end case;
-   end;
+   end Print_Event;
 
    --  Check all properties in one go, and if one fails, set errno
-   function Check_Properties (Errno: out Natural) return Boolean is
+   function Check_Properties (Errno : out Natural) return Boolean;
+   function Check_Properties (Errno : out Natural) return Boolean is
       Res : Boolean := False;
    begin
       {indent(6, check_properties)}
@@ -155,7 +157,7 @@ procedure Model_Checker is
    package ES is new Exhaustive_Simulation
      (Context_ty       => {model}_Ctxt_Ty,
       Process_Ctxt     => Process_Ctxt'access,
-      Event_Ty         => Event_ty,
+      Event_ty         => Event_ty,
       Print_Event      => Print_Event,
       Check_Properties => Check_Properties);
    use ES;
@@ -187,10 +189,10 @@ begin
    if Properties.Length > 0 then
       Generate_MSC;
    end if;
-   Put_Line ("Executed" & ES.count'Img & " functions");
-   Put_Line ("Visited" & Grafset.Length'img & " states");
-   Put_Line ("Execution time:" & Duration'Image(Clock - Start_Time) & "s.");
-end;
+   Put_Line ("Executed" & ES.Count'Img & " functions");
+   Put_Line ("Visited" & Grafset.Length'Img & " states");
+   Put_Line ("Execution time:" & Duration'Image (Clock - Start_Time) & "s.");
+end Model_Checker;
 '''
 
 def generate(ast, stop_conditions):