Commit d73ce7d5 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Optimize using ordered sets in place of vectors

Thanks Thanassis
parent 168e24e1
......@@ -81,7 +81,8 @@ with Ada.Unchecked_Conversion;
with System;
with Ada.Strings.Hash;
with Ada.Containers.Ordered_maps;
with Ada.Containers.Ordered_Maps;
with Ada.Containers.Ordered_Sets;
with Ada.Containers.Vectors;
use Ada.Containers;
......@@ -158,8 +159,10 @@ procedure model_checker is
Index_type => Vect_Count);
use Lists;
package Sets is new Ordered_Sets(Element_Type => Hash_Type);
queue : Lists.Vector;
visited : Lists.Vector;
visited : Sets.Set;
-- Check all properties in one go, and if one fails, set errno
function check_properties(errno: out natural) return boolean is
......@@ -173,25 +176,17 @@ procedure model_checker is
procedure check_and_report (S_Hash: Hash_Type) is
errno: Natural := 0;
stop_condition: boolean := false;
done : boolean := false;
begin
if check_properties(errno) then
put_line("Property " & errno'img & " is verified, at step " & count'img);
stop_condition := true;
end if;
for each_hash of visited loop
if each_hash = S_Hash then
done := true;
exit;
end if;
end loop;
if not done then
visited.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;
......@@ -212,7 +207,7 @@ begin
S_Hash := Add_to_graph(event => event);
check_and_report(S_Hash);
queue.append(S_Hash);
visited.append(S_Hash);
visited.include(S_Hash);
while queue.Length > 0 loop
Process_Ctxt := Grafset.Element(Key => queue.Last_Element).Context;
exhaustive_simulation;
......
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