Skip to content
GitLab
Commit 74a59dd6 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Optimize test-iterators 

Use Containers.Ordered_Maps instead of Hashed_Sets.
parent ba8d4a08
Hide whitespace changes
Inline Side-by-side
tests/regression/test-iterators/Makefile
View file @ 74a59dd6
......@@ -16,7 +16,7 @@ test-ada:
../../../../opengeode/opengeode.py orchestrator.pr --shared && \
$(ASN1SCC) -Ada dataview-uniq.asn -typePrefix asn1Scc -equal && \
taste-properties -d -s properties orchestrator.pr && \
gnat make test && ./test
gnat make test -O2 && ./test
simu: test-ada
cd build && make -f Makefile.properties && \
......
tests/regression/test-iterators/test.adb
View file @ 74a59dd6
......@@ -16,6 +16,7 @@ with system;
with ada.strings.hash;
with Ada.containers.hashed_sets;
with Ada.containers.ordered_maps;
with Ada.containers.vectors;
use Ada.containers;
......@@ -35,8 +36,6 @@ procedure test is
-- To save/restore the context when calling a PI:
backup_ctxt : orchestrator_ctxt_ty;
-- stop condition set to true when a property is verified
stop_condition : boolean := false;
-- Type representing an event (input or output)
type Interfaces is (start, pulse_pi, arr_pi, paramless_pi);
......@@ -55,10 +54,10 @@ procedure test is
end record;
-- Type representing an entry in the state graph (could be generic)
type Global_State is
type Global_State (I: Interfaces) is
record
event : access Event_ty;
context : Orchestrator_ctxt_ty;
event : Event_ty(I);
context : Orchestrator_ctxt_ty;
end record;
-- We'll store only pointers to graph states in the set
......@@ -76,8 +75,8 @@ procedure test is
orchestrator_ctxt := backup_ctxt;
end;
-- We will store the state graph in a hashed set. Use md5 to hash the
-- SDL context.
-- We will store the state graph in an ordered map. Use md5 to hash the
-- SDL context and use as map key.
Ctxt_Size: constant stream_element_offset :=
orchestrator_ctxt_ty'object_size / stream_element'size;
type SEA_Pointer is
......@@ -89,42 +88,36 @@ procedure test is
function State_Hash(state: State_Access) return Hash_Type is
(Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(state.context'address).all)));
package State_graph is new Hashed_Sets
(Element_Type => State_Access,
Hash => State_Hash,
Equivalent_Elements => "=");
package State_graph is new Ordered_Maps
(Key_Type => Hash_Type,
Element_Type => State_Access);
Grafset : State_graph.Set;
Grafset : State_graph.Map;
function Add_to_graph(event : Event_ty;
ctxt : orchestrator_ctxt_ty) return Hash_Type is
New_State: constant State_Access := new Global_State;
New_State: constant State_Access := new Global_State(event.Option);
New_Hash : Hash_Type;
begin
New_State.event := new Event_ty (event.Option);
New_State.event.all := event;
New_State.context := ctxt;
Grafset.Insert(New_State);
return State_Hash(New_State);
New_State.event := event;
New_State.context := ctxt;
New_Hash := State_Hash(New_State);
if not Grafset.Contains(Key => New_Hash) then
Grafset.Insert(Key => New_Hash, New_Item => New_State);
end if;
return New_Hash;
end;
-- Build up a function to retrieve a state in the graph based on the hash
function Get_Hash(S : State_Access) return Hash_Type is (State_Hash(S));
function Hash_Hash(N : Hash_Type) return Hash_Type is (Hash_Type(N));
package State_Keys is new State_graph.Generic_Keys (Key_Type => Hash_Type,
Key => Get_Hash,
Hash => Hash_Hash,
Equivalent_Keys => "=");
function Retrieve_State (Hash: Hash_Type) return access Global_State is
C: constant State_graph.Cursor :=
State_Keys.Find (Grafset, Hash);
begin
if State_graph.Has_Element(C) then
return State_graph.Element(C);
else
return Null;
end if;
end Retrieve_State;
-- Vector of hashes (integers) used for the model checking
subtype Vect_Count is Positive range 1 .. 1000;
package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count);
use Lists;
queue : Lists.Vector;
qcursor : Lists.Cursor := queue.First;
visited : Lists.Vector;
-- Check all properties in one go, and if one fails, set errno
function check_properties(errno: out natural) return boolean is
......@@ -132,30 +125,33 @@ procedure test is
begin
errno := 0;
res := orchestrator_stop_conditions.pproperty_0;
count := count + 1;
return res;
end;
-- Report the result of the property check to the user
procedure check_and_report 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;
end;
-- Vector of hashes (integers) used for the model checking
subtype Vect_Count is Positive range 1 .. 1000;
package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count);
use Lists;
queue : Lists.Vector;
qcursor : Lists.Cursor := queue.First;
visited : Lists.Vector;
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 stop_condition = false then
queue.append(S_Hash);
end if;
end if;
end;
-- One function per PI to exhaust the interface parameters
procedure exhaust_pulse is
......@@ -163,34 +159,17 @@ procedure test is
asn1_p : aliased asn1SccT_Int;
event : Event_ty (pulse_pi);
S_Hash : Hash_Type;
done : boolean := false;
begin
save_context;
for each of pulse_it loop
stop_condition := false;
done := false;
save_context;
event.pulse_param := asn1SccT_Int(each);
asn1_p := asn1SccT_Int'(event.pulse_param);
orchestrator.pulse(asn1_p'access);
count := count + 1;
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
check_and_report;
check_and_report(S_Hash);
restore_context;
for each_hash of visited loop
-- We should check the hash, not the full value..
if each_hash = S_Hash then
done := true;
exit;
end if;
end loop;
if not done then
visited.append(S_Hash);
if stop_condition = false then
queue.append(S_Hash);
end if;
end if;
end loop;
end;
......@@ -199,36 +178,20 @@ procedure test is
asn1_p : aliased asn1SccT_SeqOf;
event : Event_ty (arr_pi);
S_Hash : Hash_Type;
done : boolean := false;
begin
save_context;
for each of arr_it loop
stop_condition := false;
done := false;
save_context;
asn1_p.Length := each.Length;
for idx in 1..asn1_p.Length loop
asn1_p.Data(idx) := asn1SccT_Int'(asn1SccT_Int(each.Data(idx)));
end loop;
event.Arr_Param := asn1_p;
orchestrator.arr(asn1_p'access);
count := count + 1;
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
check_and_report;
check_and_report(S_Hash);
restore_context;
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 stop_condition = false then
queue.append(S_Hash);
end if;
end if;
end loop;
end;
......@@ -238,9 +201,10 @@ procedure test is
begin
save_context;
orchestrator.paramless;
count := count + 1;
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
check_and_report;
check_and_report(S_Hash);
restore_context;
end;
......@@ -256,16 +220,15 @@ procedure test is
begin
put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
orchestrator.startup;
check_and_report;
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
check_and_report(S_Hash);
queue.append(S_Hash);
visited.append(S_Hash);
while queue.Length > 0 loop
--put_line (queue.length'img);
orchestrator_ctxt := Retrieve_State(queue.Last_Element).Context;
orchestrator_ctxt := Grafset.Element(Key => queue.Last_Element).Context;
exhaustive_simulation;
-- discard the event for now (needed to generate MSC)
queue.delete_last;
end loop;
put_line("Executed" & count'img & " functions");
......
Supports Markdown
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