Commit 9005b24e authored by Maxime Perrotin's avatar Maxime Perrotin

Fix code style

parent 7e973df2
-- (c) 2017 European Space Agency / TASTE Project -- (c) 2017-2020 European Space Agency / TASTE Project
package body ASN1_Iterators.Exhaustive_Simulation is package body ASN1_Iterators.Exhaustive_Simulation is
function State_Hash(Context: Context_Ty) return Hash_Type is function State_Hash (Context : Context_Ty) return Hash_Type is
(Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(Context'Address).all))); (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 -- Add a state to the graph:
function Add_to_graph(event : Event_ty) return Hash_Type is -- 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_State: State_Access;
New_Hash : Hash_Type; 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 begin
New_Hash := State_Hash(Process_Ctxt.all); New_Hash := State_Hash (Process_Ctxt.all);
if not Grafset.Contains(Key => New_Hash) then if not Grafset.Contains (Key => New_Hash) then
New_State := new Global_State; New_State := new Global_State;
New_State.context := Process_Ctxt.all; New_State.Context := Process_Ctxt.all;
Grafset.Insert(Key => New_Hash, New_Item => New_State); Grafset.Insert (Key => New_Hash, New_Item => New_State);
else else
New_State := Grafset.Element(Key => New_Hash); New_State := Grafset.Element (Key => New_Hash);
end if; end if;
New_State.edges.append(New_Edge); New_State.edges.append (New_Edge);
return New_Hash; return New_Hash;
end; end Add_To_Graph;
-- Report the result of the property check to the user -- Report the result of the property check to the user
procedure Check_And_Report (S_Hash: Hash_Type) is procedure Check_And_Report (S_Hash : Hash_Type) is
errno: Natural := 0; errno : Natural := 0;
stop_condition: boolean := false; Stop_Condition : Boolean := False;
begin begin
count := count + 1; Count := Count + 1;
if check_properties(errno) then if Check_Properties (errno) then
put_line("Property " & errno'img & " is verified, at step " & count'img); Put_Line
stop_condition := true; ("Property "
if properties.Length <= 10 then & errno'Img & " is verified, at step " & Count'Img);
properties.include(s_hash); Stop_Condition := True;
if Properties.Length <= 10 then
Properties.Include (S_Hash);
end if; end if;
end if; end if;
if not visited.contains(s_hash) then if not Visited.Contains (S_Hash) then
visited.insert(s_hash); Visited.Insert (S_Hash);
if stop_condition = false then if Stop_Condition = False then
queue.append(S_Hash); Queue.Append (S_Hash);
end if; end if;
end if; end if;
end; end Check_And_Report;
procedure Generate_MSC is procedure Generate_MSC is
package Loc_Maps is new Ordered_Maps(Key_Type => Hash_Type, package Loc_Maps is new Ordered_Maps (Key_Type => Hash_Type,
Element_Type => Boolean); Element_Type => Boolean);
package Evt_Lists is new Vectors(Element_Type => Event_ty, package Evt_Lists is new Vectors (Element_Type => Event_ty,
Index_Type => Natural); Index_Type => Natural);
package Parent_Maps is new Ordered_Maps(Key_Type => Hash_Type, package Parent_Maps is new Ordered_Maps (Key_Type => Hash_Type,
Element_Type => Edge_ty); Element_Type => Edge_ty);
function Find_Path(From: Hash_Type) return Evt_Lists.Vector is function Find_Path (From : Hash_Type) return Evt_Lists.Vector is
Loc_Q : Lists.Vector; Loc_Q : Lists.Vector;
Loc_Visited : Loc_Maps.Map; Loc_Visited : Loc_Maps.Map;
Next_Hash : Hash_Type; Next_Hash : Hash_Type;
...@@ -60,42 +64,45 @@ package body ASN1_Iterators.Exhaustive_Simulation is ...@@ -60,42 +64,45 @@ package body ASN1_Iterators.Exhaustive_Simulation is
Edge : Edge_Ty; Edge : Edge_Ty;
Scenario : Evt_Lists.Vector; Scenario : Evt_Lists.Vector;
begin begin
Loc_Q.append(From); Loc_Q.append (From);
Loc_Visited.Include(Key => From, New_Item => True); Loc_Visited.Include (Key => From, New_Item => True);
while not Loc_Q.Is_Empty loop while not Loc_Q.Is_Empty loop
Next_Hash := Loc_Q.Last_Element; Next_Hash := Loc_Q.Last_Element;
exit when Next_Hash = Start_Hash; 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 for each_edge of State.Edges loop
if not Loc_Visited.Contains(each_edge.state) then if not Loc_Visited.Contains (each_edge.State) then
Loc_Q.append(Each_Edge.state); Loc_Q.Append (each_edge.State);
Loc_Visited.Include(Key => Each_Edge.State, Loc_Visited.Include (Key => each_edge.State,
New_Item => True); New_Item => True);
Parent_Map.Include(Key => Each_Edge.State, Parent_Map.Include (Key => each_edge.State,
New_Item => (State => Next_Hash, New_Item =>
Event => Each_Edge.Event)); (State => Next_Hash,
Event => each_edge.Event));
end if; end if;
end loop; end loop;
Loc_Q.Delete_Last; Loc_Q.Delete_Last;
end loop; end loop;
Curr := Start_Hash; Curr := Start_Hash;
Put_Line("Found path!"); Put_Line ("Found path!");
while Parent_Map.Contains(Curr) loop while Parent_Map.Contains (Curr) loop
Edge := Parent_Map.Element(Curr); Edge := Parent_Map.Element (Curr);
Curr := Edge.State; Curr := Edge.State;
Scenario.Append(Edge.Event); Scenario.Append (Edge.Event);
end loop; end loop;
return Scenario; return Scenario;
end; end Find_Path;
Scenario : Evt_Lists.Vector; Scenario : Evt_Lists.Vector;
begin begin
for each_hash of properties loop for each_hash of Properties loop
put_line("Path from hash " & each_hash'img & " to hash " & start_hash'img); Put_Line
Scenario := Find_Path(each_hash); ("Path from hash "
& each_hash'Img & " to hash " & Start_Hash'Img);
Scenario := Find_Path (each_hash);
for each_evt of Scenario loop for each_evt of Scenario loop
Print_Event(each_evt); Print_Event (each_evt);
end loop; end loop;
end loop; end loop;
end; end Generate_MSC;
end ASN1_Iterators.Exhaustive_Simulation; end ASN1_Iterators.Exhaustive_Simulation;
...@@ -25,9 +25,9 @@ generic ...@@ -25,9 +25,9 @@ generic
package ASN1_Iterators.Exhaustive_Simulation is package ASN1_Iterators.Exhaustive_Simulation is
-- To save/restore the context when calling a PI: -- To save/restore the context when calling a PI:
backup_ctxt : Context_ty; Backup_Ctxt : Context_ty;
backup_hash : Hash_Type; Backup_Hash : Hash_Type;
start_hash : Hash_Type; Start_Hash : Hash_Type;
-- An edge is made of a past state reference and an event to leave it -- An edge is made of a past state reference and an event to leave it
type Edge_ty is type Edge_ty is
......
...@@ -145,7 +145,7 @@ procedure Model_Checker is ...@@ -145,7 +145,7 @@ procedure Model_Checker is
end; end;
-- Check all properties in one go, and if one fails, set errno -- 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 is
Res : Boolean := False; Res : Boolean := False;
begin begin
{indent(6, check_properties)} {indent(6, check_properties)}
...@@ -187,10 +187,10 @@ begin ...@@ -187,10 +187,10 @@ begin
if Properties.Length > 0 then if Properties.Length > 0 then
Generate_MSC; Generate_MSC;
end if; end if;
Put_Line ("Executed" & ES.count'Img & " functions"); Put_Line ("Executed" & ES.Count'Img & " functions");
Put_Line ("Visited" & Grafset.Length'img & " states"); Put_Line ("Visited" & Grafset.Length'Img & " states");
Put_Line ("Execution time:" & Duration'Image(Clock - Start_Time) & "s."); Put_Line ("Execution time:" & Duration'Image (Clock - Start_Time) & "s.");
end; end Model_Checker;
''' '''
def generate(ast, stop_conditions): def generate(ast, stop_conditions):
......
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