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

Simplify the SDL model of demo-iterators

parent d1c553c9
......@@ -21,7 +21,7 @@ paramless;
CONNECT c AND r;
/* CIF PROCESS (465, 158), (265, 176) */
PROCESS orchestrator;
/* CIF TEXT (920, 71), (268, 140) */
/* CIF TEXT (964, 71), (268, 140) */
-- Text area for declarations and comments
dcl t t_int := 0;
......@@ -30,58 +30,68 @@ dcl counter t_int := 0;
dcl seqof t_seqof;
/* CIF ENDTEXT */
/* CIF START (444, 48), (70, 34) */
/* CIF START (434, 48), (70, 34) */
START;
/* CIF PROCEDURECALL (373, 102), (211, 35) */
/* CIF PROCEDURECALL (363, 102), (211, 35) */
CALL writeln( 'Orchestrator startup');
/* CIF NEXTSTATE (445, 152), (67, 35) */
/* CIF NEXTSTATE (435, 152), (67, 35) */
NEXTSTATE wait;
/* CIF STATE (733, 94), (70, 35) */
/* CIF STATE (825, 94), (70, 35) */
STATE running;
/* CIF INPUT (733, 149), (70, 35) */
/* CIF INPUT (825, 149), (70, 35) */
INPUT *;
/* CIF NEXTSTATE (733, 204), (70, 35) */
/* CIF NEXTSTATE (825, 204), (70, 35) */
NEXTSTATE wait;
ENDSTATE;
/* CIF STATE (445, 152), (67, 35) */
/* CIF STATE (435, 152), (67, 35) */
STATE wait;
/* CIF INPUT (120, 207), (70, 35) */
/* CIF INPUT (89, 207), (70, 35) */
INPUT pulse(t);
/* CIF DECISION (120, 262), (70, 50) */
/* CIF DECISION (89, 262), (70, 50) */
DECISION t;
/* CIF ANSWER (75, 332), (70, 23) */
/* CIF ANSWER (27, 332), (70, 23) */
(0):
/* CIF NEXTSTATE (75, 375), (70, 35) */
/* CIF TASK (0, 375), (124, 53) */
TASK seqof := {1,1,1,1},
counter := 0,
t := 0;
/* CIF NEXTSTATE (27, 443), (70, 35) */
NEXTSTATE wait;
/* CIF ANSWER (165, 332), (70, 23) */
/* CIF ANSWER (161, 332), (70, 23) */
else:
/* CIF NEXTSTATE (165, 375), (70, 35) */
/* CIF TASK (134, 375), (124, 53) */
TASK seqof := {1,1,1,1},
counter := 0,
t := 0;
/* CIF NEXTSTATE (161, 443), (70, 35) */
NEXTSTATE running;
ENDDECISION;
/* CIF INPUT (371, 207), (83, 35) */
/* CIF INPUT (405, 207), (83, 35) */
INPUT arr(seqof);
/* CIF TASK (312, 262), (202, 35) */
/* CIF TASK (345, 262), (202, 35) */
TASK counter := (counter + 1) mod 4;
/* CIF DECISION (353, 317), (121, 50) */
/* CIF DECISION (386, 317), (121, 50) */
DECISION seqof = {4,4,4,4}
and counter = 0;
/* CIF ANSWER (336, 387), (70, 23) */
/* CIF ANSWER (359, 387), (70, 23) */
(true):
/* CIF PROCEDURECALL (245, 430), (250, 35) */
/* CIF PROCEDURECALL (268, 430), (250, 35) */
CALL writeln( 'Property should be checked');
/* CIF ANSWER (522, 387), (70, 23) */
/* CIF ANSWER (556, 387), (70, 23) */
(false):
/* CIF TASK (506, 430), (103, 35) */
/* CIF TASK (540, 430), (103, 35) */
TASK seqof(1) := 1;
ENDDECISION;
/* CIF NEXTSTATE (378, 480), (70, 35) */
/* CIF NEXTSTATE (412, 480), (70, 35) */
NEXTSTATE -;
/* CIF INPUT (629, 207), (83, 35) */
/* CIF INPUT (684, 207), (83, 35) */
INPUT paramless;
/* CIF TASK (619, 262), (104, 38) */
/* CIF TASK (674, 262), (104, 38) */
TASK counter := 4,
t := 1;
/* CIF NEXTSTATE (636, 320), (70, 35) */
/* CIF TASK (663, 320), (124, 38) */
TASK seqof := {1,1,1,1};
/* CIF NEXTSTATE (691, 373), (70, 35) */
NEXTSTATE running;
ENDSTATE;
ENDPROCESS orchestrator;
......
......@@ -97,14 +97,14 @@ procedure test is
Grafset : State_graph.Set;
function Add_to_graph(event : Event_ty;
ctxt : orchestrator_ctxt_ty) return State_Access is
ctxt : orchestrator_ctxt_ty) return Hash_Type is
New_State: constant State_Access := new Global_State;
begin
New_State.event := new Event_ty (event.Option);
New_State.event.all := event;
New_State.context := ctxt;
Grafset.Insert(New_State);
return New_State;
return State_Hash(New_State);
end;
-- Build up a function to retrieve a state in the graph based on the hash
......@@ -146,8 +146,9 @@ procedure test is
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 => State_Access,
package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count);
use Lists;
......@@ -161,7 +162,7 @@ procedure test is
pulse_it : T_Int_pkg.Instance;
asn1_p : aliased asn1SccT_Int;
event : Event_ty (pulse_pi);
SA : State_Access;
S_Hash : Hash_Type;
done : boolean := false;
begin
for each of pulse_it loop
......@@ -172,23 +173,22 @@ procedure test is
event.pulse_param := asn1SccT_Int(each);
asn1_p := asn1SccT_Int'(event.pulse_param);
orchestrator.pulse(asn1_p'access);
SA := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
check_and_report;
restore_context;
for ctxt of visited loop
for each_hash of visited loop
-- We should check the hash, not the full value..
if ctxt.context = SA.context then
if each_hash = S_Hash then
done := true;
exit;
end if;
end loop;
--if visited.find(SA) = Lists.No_Element then
if not done then
visited.append(SA);
visited.append(S_Hash);
if stop_condition = false then
queue.append(SA);
queue.append(S_Hash);
end if;
end if;
end loop;
......@@ -198,7 +198,7 @@ procedure test is
arr_it : T_SeqOf_pkg.Instance;
asn1_p : aliased asn1SccT_SeqOf;
event : Event_ty (arr_pi);
SA : State_Access;
S_Hash : Hash_Type;
done : boolean := false;
begin
for each of arr_it loop
......@@ -212,21 +212,20 @@ procedure test is
end loop;
event.Arr_Param := asn1_p;
orchestrator.arr(asn1_p'access);
SA := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
check_and_report;
restore_context;
for ctxt of visited loop
-- We should check the hash, not the full value..
if ctxt.context = SA.context then
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(SA);
visited.append(S_Hash);
if stop_condition = false then
queue.append(SA);
queue.append(S_Hash);
end if;
end if;
......@@ -235,12 +234,12 @@ procedure test is
procedure exhaust_paramless is
event : Event_ty (paramless_pi);
SA : State_Access;
S_Hash : Hash_Type;
begin
save_context;
orchestrator.paramless;
SA := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
check_and_report;
restore_context;
end;
......@@ -252,18 +251,19 @@ procedure test is
exhaust_arr;
end;
event : Event_ty(start);
SA : State_Access;
event : Event_ty(start);
S_Hash : Hash_Type;
begin
put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
orchestrator.startup;
check_and_report;
SA := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
queue.append(SA);
visited.append(SA);
S_Hash := Add_to_graph(event => event,
ctxt => orchestrator_ctxt);
queue.append(S_Hash);
visited.append(S_Hash);
while queue.Length > 0 loop
orchestrator_ctxt := queue.Last_Element.context;
--put_line (queue.length'img);
orchestrator_ctxt := Retrieve_State(queue.Last_Element).Context;
exhaustive_simulation;
-- discard the event for now (needed to generate MSC)
queue.delete_last;
......
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