...
 
Commits (2)
-- (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;
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,
package Loc_Maps is new Ordered_Maps (Key_Type => Hash_Type,
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);
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);
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_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,
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));
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;
......@@ -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
......
......@@ -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);
......
......@@ -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):
......