Commit 02654e92 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Update test-iterators

parent b7c5a419
...@@ -242,22 +242,23 @@ LD_LIBRARY_PATH=. opengeode-simulator ...@@ -242,22 +242,23 @@ LD_LIBRARY_PATH=. opengeode-simulator
# Parallel states in a state aggregation may terminate # Parallel states in a state aggregation may terminate
full_statelist.add(u'{}finished'.format(UNICODE_SEP)) full_statelist.add(u'{}finished'.format(UNICODE_SEP))
context_decl = []
if full_statelist: if full_statelist:
process_level_decl.append(u'type States is ({});' context_decl.append(u'type States is ({});'
.format(u', '.join(full_statelist) or u'No_State')) .format(u', '.join(full_statelist) or u'No_State'))
# Generate the code to declare process-level context # Generate the code to declare process-level context
process_level_decl.extend(['type {}_Ty is'.format(LPREFIX), 'record']) context_decl.extend(['type {}_Ty is'.format(LPREFIX), 'record'])
if full_statelist: if full_statelist:
process_level_decl.append('state : States;') context_decl.append('state : States;')
process_level_decl.append('initDone : Boolean := False;') context_decl.append('initDone : Boolean := False;')
# State aggregation: add list of substates (XXX to be added in C generator) # State aggregation: add list of substates (XXX to be added in C generator)
for substates in aggregates.viewvalues(): for substates in aggregates.viewvalues():
for each in substates: for each in substates:
process_level_decl.append(u'{}{}state: States;' context_decl.append(u'{}{}state: States;'
.format(each.statename, UNICODE_SEP)) .format(each.statename, UNICODE_SEP))
for var_name, (var_type, def_value) in process.variables.viewitems(): for var_name, (var_type, def_value) in process.variables.viewitems():
...@@ -269,29 +270,33 @@ LD_LIBRARY_PATH=. opengeode-simulator ...@@ -269,29 +270,33 @@ LD_LIBRARY_PATH=. opengeode-simulator
if varbty.kind in ('SequenceOfType', 'OctetStringType'): if varbty.kind in ('SequenceOfType', 'OctetStringType'):
dstr = array_content(def_value, dstr, varbty) dstr = array_content(def_value, dstr, varbty)
assert not dst and not dlocal, 'DCL: Expecting a ground expression' assert not dst and not dlocal, 'DCL: Expecting a ground expression'
process_level_decl.append( context_decl.append(
u'{n} : aliased {sort}{default};' u'{n} : aliased {sort}{default};'
.format(n=var_name, .format(n=var_name,
sort=type_name(var_type), sort=type_name(var_type),
default=u' := ' + dstr if def_value else u'')) default=u' := ' + dstr if def_value else u''))
process_level_decl.append('end record;') context_decl.append('end record;')
process_level_decl.append('{ctxt}: {ctxt}_Ty;'.format(ctxt=LPREFIX)) context_decl.append('{ctxt}: {ctxt}_Ty;'.format(ctxt=LPREFIX))
if simu: if simu:
# Export the context, so that it can be manipulated from outside # Export the context, so that it can be manipulated from outside
# (in practice used by the "properties" module. # (in practice used by the "properties" module.
process_level_decl.append(u'pragma export (C, {ctxt}, "{ctxt}");' context_decl.append(u'pragma export (C, {ctxt}, "{ctxt}");'
.format(ctxt=LPREFIX)) .format(ctxt=LPREFIX))
# Exhaustive simulation needs a backup of the context to quickly undo # Exhaustive simulation needs a backup of the context to quickly undo
process_level_decl.append(u'{ctxt}_bk: {ctxt}_Ty;' context_decl.append(u'{ctxt}_bk: {ctxt}_Ty;'
.format(ctxt=LPREFIX)) .format(ctxt=LPREFIX))
elif import_context: elif import_context:
# Possibility to have the context defined outside the module # Possibility to have the context defined outside the module
# in order for a model checker to view/modify internals without any # in order for a model checker to view/modify internals without any
# copy at runtime # copy at runtime
process_level_decl.append(u'pragma import (C, ctxt, "{}_ctxt");' context_decl.append(u'pragma import (C, ctxt, "{}_ctxt");'
.format(import_context)) .format(import_context))
if not simu:
process_level_decl.extend(context_decl)
# Continuous State transition id
process_level_decl.append('CS_Only : constant Integer := {};' process_level_decl.append('CS_Only : constant Integer := {};'
.format(len(process.transitions))) .format(len(process.transitions)))
...@@ -382,6 +387,7 @@ package {process_name} is'''.format(process_name=process_name, ...@@ -382,6 +387,7 @@ package {process_name} is'''.format(process_name=process_name,
dll_api = [] dll_api = []
if simu: if simu:
ads_template.extend(context_decl)
ads_template.append('-- API for simulation via DLL') ads_template.append('-- API for simulation via DLL')
dll_api.append('-- API to remotely change internal data') dll_api.append('-- API to remotely change internal data')
# Add function allowing to trace current state as a string # Add function allowing to trace current state as a string
......
with SimpleTypes; with SimpleTypes;
with Generic_Basic; with Generic_Basic;
with Interfaces;
use Interfaces;
generic generic
Min: Integer; Min: Interfaces.Integer_64;
Max: Integer; Max: Interfaces.Integer_64;
package Generic_Integer is package Generic_Integer is
function Elem_Init return Integer is (Min); function Elem_Init return Interfaces.Integer_64 is (Min);
function Has_Elem (Value: Integer) return Boolean is (Value <= Max); function Has_Elem(Value: Interfaces.Integer_64) return Boolean is
function Elem_First return Integer is (Min); (Value <= Max);
function Elem_Next (Value: Integer) return Integer is (Value + 1); function Elem_First return Interfaces.Integer_64 is (Min);
function Elem_Next(Value: Interfaces.Integer_64) return Interfaces.Integer_64 is
(Value + 1);
package Integer_type is new SimpleTypes(Element => Integer, package Integer_type is new SimpleTypes(Element => Interfaces.Integer_64,
Elem_Init => Elem_Init, Elem_Init => Elem_Init,
Has_Elem => Has_Elem, Has_Elem => Has_Elem,
Elem_First => Elem_First, Elem_First => Elem_First,
......
...@@ -46,7 +46,7 @@ package body Generic_SeqOf is ...@@ -46,7 +46,7 @@ package body Generic_SeqOf is
-- Exhausted "rest": iterate on the first item -- Exhausted "rest": iterate on the first item
Ptr_elem := Ptr.LenIt.Next(Ptr_elem); Ptr_elem := Ptr.LenIt.Next(Ptr_elem);
if Length_Pkg.Has_Element (Ptr_elem) then if Length_Pkg.Has_Element (Ptr_elem) then
Ptr.Value.Length := Ptr_elem.Value.Value; Ptr.Value.Length := Integer(Ptr_elem.Value.Value);
Ptr.Length := Ptr.Value.Length; Ptr.Length := Ptr.Value.Length;
Ptr.RestVal := new P.ASN1_SeqOf(Ptr.Value.Length); Ptr.RestVal := new P.ASN1_SeqOf(Ptr.Value.Length);
Ptr.RestIt := new P.ASN1_SeqOf_It'(P.ASN1_SeqOf_It(Ptr.RestVal.Iterate)); Ptr.RestIt := new P.ASN1_SeqOf_It'(P.ASN1_SeqOf_It(Ptr.RestVal.Iterate));
......
...@@ -7,16 +7,20 @@ with generic_fixed_seqof; ...@@ -7,16 +7,20 @@ with generic_fixed_seqof;
with generic_integer; with generic_integer;
with generic_basic; with generic_basic;
with Interfaces;
use Interfaces;
-- Iterator for a variable-size array of basic type -- Iterator for a variable-size array of basic type
generic generic
Min : Integer; Min : Natural;
Max : Integer; Max : Natural;
with package Basic is new Generic_Basic (<>); with package Basic is new Generic_Basic (<>);
package Generic_SeqOf is package Generic_SeqOf is
Package P is new Generic_Fixed_SeqOF (P => Basic); Package P is new Generic_Fixed_SeqOF (P => Basic);
-- Create an integer type with a range constraint to iterate on -- Create an integer type with a range constraint to iterate on
package Length_ty is new Generic_Integer (Min, Max); package Length_ty is new Generic_Integer (Integer_64(Min),
Integer_64(Max));
-- Instantiate the package to iterate on the integer for the length -- Instantiate the package to iterate on the integer for the length
package Length_Pkg renames Length_ty.It; package Length_Pkg renames Length_ty.It;
......
with orchestrator; with orchestrator;
use orchestrator;
with orchestrator_stop_conditions; with orchestrator_stop_conditions;
with asn1_iterators; with asn1_iterators;
use asn1_iterators; use asn1_iterators;
...@@ -24,21 +25,21 @@ with ada.calendar; ...@@ -24,21 +25,21 @@ with ada.calendar;
use ada.calendar; use ada.calendar;
procedure test is procedure test is
-- Reproduce the Context, and import it subtype Context_ty is Orchestrator_Ctxt_ty;
type States is (running, wait); Process_Ctxt : Context_ty renames Orchestrator_Ctxt;
type orchestrator_ctxt_Ty is
record
state : States;
initDone : Boolean := False;
counter : aliased asn1SccT_Int := 0;
seqof : aliased asn1SccT_SeqOf;
t : aliased asn1SccT_Int := 0;
end record;
orchestrator_ctxt: orchestrator_ctxt_Ty;
pragma Import (C, orchestrator_ctxt, "orchestrator_ctxt");
-- To save/restore the context when calling a PI: -- To save/restore the context when calling a PI:
backup_ctxt : orchestrator_ctxt_ty; backup_ctxt : Context_ty;
procedure save_context is
begin
backup_ctxt := Process_Ctxt;
end;
procedure restore_context is
begin
Process_Ctxt := backup_ctxt;
end;
-- Type representing an event (input or output) -- Type representing an event (input or output)
type Interfaces is (start, pulse_pi, arr_pi, paramless_pi); type Interfaces is (start, pulse_pi, arr_pi, paramless_pi);
...@@ -48,40 +49,34 @@ procedure test is ...@@ -48,40 +49,34 @@ procedure test is
when start => when start =>
null; null;
when pulse_pi => when pulse_pi =>
Pulse_Param: asn1SccT_Int; Pulse_Param: aliased asn1SccT_Int;
when arr_pi => when arr_pi =>
Arr_Param: asn1SccT_SeqOf; Arr_Param: aliased asn1SccT_SeqOf;
when paramless_pi => when paramless_pi =>
null; null;
end case; end case;
end record; end record;
-- Type representing an entry in the state graph (could be generic) -- Type representing an entry in the state graph
type Global_State (I: Interfaces) is type Global_State (I: Interfaces) is
record record
event : Event_ty(I); event : Event_ty(I);
context : Orchestrator_ctxt_ty; context : Context_ty;
end record; end record;
-- We'll store only pointers to graph states in the set -- We'll store only pointers to graph states in the set
type State_Access is access Global_State; type State_Access is access Global_State;
count : natural := 0; -- The state graph itself is stored in a dictionary type (map)
package State_graph is new Ordered_Maps (Key_Type => Hash_Type,
procedure save_context is Element_Type => State_Access);
begin Grafset : State_graph.Map;
backup_ctxt := orchestrator_ctxt;
end;
procedure restore_context is
begin
orchestrator_ctxt := backup_ctxt;
end;
-- We will store the state graph in an ordered map. Use md5 to hash the -- State graph index: Use md5 first to get a string representing
-- SDL context and use as map key. -- the context object, then strings.hash to get a number that can be used
-- as a map key. This can surely be improved!
Ctxt_Size: constant stream_element_offset := Ctxt_Size: constant stream_element_offset :=
orchestrator_ctxt_ty'object_size / stream_element'size; Context_ty'object_size / stream_element'size;
type SEA_Pointer is type SEA_Pointer is
access all Stream_Element_Array (1 .. Ctxt_Size); access all Stream_Element_Array (1 .. Ctxt_Size);
...@@ -91,19 +86,13 @@ procedure test is ...@@ -91,19 +86,13 @@ procedure test is
function State_Hash(state: State_Access) return Hash_Type is function State_Hash(state: State_Access) return Hash_Type is
(Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(state.context'address).all))); (Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(state.context'address).all)));
package State_graph is new Ordered_Maps -- Add a state to the graph: compute the hash (key) and store if not already there
(Key_Type => Hash_Type, function Add_to_graph(event : Event_ty) return Hash_Type is
Element_Type => State_Access);
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(event.Option); New_State: constant State_Access := new Global_State(event.Option);
New_Hash : Hash_Type; New_Hash : Hash_Type;
begin begin
New_State.event := event; New_State.event := event;
New_State.context := ctxt; New_State.context := Process_Ctxt;
New_Hash := State_Hash(New_State); New_Hash := State_Hash(New_State);
if not Grafset.Contains(Key => New_Hash) then if not Grafset.Contains(Key => New_Hash) then
Grafset.Insert(Key => New_Hash, New_Item => New_State); Grafset.Insert(Key => New_Hash, New_Item => New_State);
...@@ -111,6 +100,8 @@ procedure test is ...@@ -111,6 +100,8 @@ procedure test is
return New_Hash; return New_Hash;
end; end;
-- To count the number of calls to the function's provided interfaces
count : natural := 0;
-- Vector of hashes (integers) used for the model checking -- Vector of hashes (integers) used for the model checking
subtype Vect_Count is Positive range 1 .. 1000; subtype Vect_Count is Positive range 1 .. 1000;
...@@ -159,18 +150,15 @@ procedure test is ...@@ -159,18 +150,15 @@ procedure test is
-- One function per PI to exhaust the interface parameters -- One function per PI to exhaust the interface parameters
procedure exhaust_pulse is procedure exhaust_pulse is
pulse_it : T_Int_pkg.Instance; pulse_it : T_Int_pkg.Instance;
asn1_p : aliased asn1SccT_Int;
event : Event_ty (pulse_pi); event : Event_ty (pulse_pi);
S_Hash : Hash_Type; S_Hash : Hash_Type;
begin begin
save_context; save_context;
for each of pulse_it loop for each of pulse_it loop
event.pulse_param := asn1SccT_Int(each); event.pulse_param := each;
asn1_p := asn1SccT_Int'(event.pulse_param); orchestrator.pulse(event.pulse_param'access);
orchestrator.pulse(asn1_p'access);
count := count + 1; count := count + 1;
S_Hash := Add_to_graph(event => event, S_Hash := Add_to_graph(event => event);
ctxt => orchestrator_ctxt);
check_and_report(S_Hash); check_and_report(S_Hash);
restore_context; restore_context;
end loop; end loop;
...@@ -178,21 +166,18 @@ procedure test is ...@@ -178,21 +166,18 @@ procedure test is
procedure exhaust_arr is procedure exhaust_arr is
arr_it : T_SeqOf_pkg.Instance; arr_it : T_SeqOf_pkg.Instance;
asn1_p : aliased asn1SccT_SeqOf;
event : Event_ty (arr_pi); event : Event_ty (arr_pi);
S_Hash : Hash_Type; S_Hash : Hash_Type;
begin begin
save_context; save_context;
for each of arr_it loop for each of arr_it loop
asn1_p.Length := each.Length; event.arr_param.length := each.length; -- only variable-sized arrays
for idx in 1..asn1_p.Length loop for idx in 1..each.length loop
asn1_p.Data(idx) := asn1SccT_Int'(asn1SccT_Int(each.Data(idx))); event.arr_param.data(idx) := each.data(idx);
end loop; end loop;
event.Arr_Param := asn1_p; orchestrator.arr(event.arr_param'access);
orchestrator.arr(asn1_p'access);
count := count + 1; count := count + 1;
S_Hash := Add_to_graph(event => event, S_Hash := Add_to_graph(event => event);
ctxt => orchestrator_ctxt);
check_and_report(S_Hash); check_and_report(S_Hash);
restore_context; restore_context;
end loop; end loop;
...@@ -205,8 +190,7 @@ procedure test is ...@@ -205,8 +190,7 @@ procedure test is
save_context; save_context;
orchestrator.paramless; orchestrator.paramless;
count := count + 1; count := count + 1;
S_Hash := Add_to_graph(event => event, S_Hash := Add_to_graph(event => event);
ctxt => orchestrator_ctxt);
check_and_report(S_Hash); check_and_report(S_Hash);
restore_context; restore_context;
end; end;
...@@ -224,13 +208,12 @@ procedure test is ...@@ -224,13 +208,12 @@ procedure test is
begin begin
put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long..."); put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
orchestrator.startup; orchestrator.startup;
S_Hash := Add_to_graph(event => event, S_Hash := Add_to_graph(event => event);
ctxt => orchestrator_ctxt);
check_and_report(S_Hash); check_and_report(S_Hash);
queue.append(S_Hash); queue.append(S_Hash);
visited.append(S_Hash); visited.append(S_Hash);
while queue.Length > 0 loop while queue.Length > 0 loop
orchestrator_ctxt := Grafset.Element(Key => queue.Last_Element).Context; Process_Ctxt := Grafset.Element(Key => queue.Last_Element).Context;
exhaustive_simulation; exhaustive_simulation;
queue.delete_last; queue.delete_last;
end loop; end loop;
......
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