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

Add generation of scenario

parent 35412d34
......@@ -27,6 +27,13 @@ event = '''when <interface>_pi =>
null;
<endif>'''
print_event = '''when <interface>_pi =>
<if(param)>
Put_Line("<interface>(" & <sort>_Pkg.Image(Event.<interface>_Param) & ")");
<else>
Put_Line("<interface>");
<endif>'''
check_ppty = u'''errno := <num>;
res := <model>_stop_conditions.p\u00dcproperty_<num>;
if res then
......@@ -35,8 +42,8 @@ end if;'''
exhaust_procedure = '''procedure exhaust_<interface> is
<if(param)><interface>_it : <sort>_pkg.Instance;<endif>
event : Event_ty(<interface>_pi);
S_Hash : Hash_Type;
event : Event_ty(<interface>_pi);
S_Hash : Hash_Type;
begin
<if(param)>
for each of <interface>_it loop
......@@ -46,6 +53,7 @@ begin
S_Hash := Add_to_graph(event => event);
check_and_report(S_Hash);
Process_Ctxt := backup_ctxt;
exit when properties.length >= 10;
end loop;
<else>
<model>.<interface>;
......@@ -96,6 +104,7 @@ procedure model_checker is
-- To save/restore the context when calling a PI:
backup_ctxt : Context_ty;
backup_hash : Hash_Type;
start_hash : Hash_Type;
-- Set a maximum size for vectors (set of states and edges)
subtype Vect_Count is Positive range 1 .. 1000000;
......@@ -111,14 +120,24 @@ procedure model_checker is
end case;
end record;
-- Display scenario (in the future: generate MSC)
procedure Print_Event(Event: Event_ty) is
begin
case Event.Option is
when start =>
Put_Line("START");
<print_events;separator="\n">
end case;
end;
-- An edge is made of a past state reference and an event to leave it
type Edge is
type Edge_ty is
record
event : Event_ty;
state : Hash_Type; -- Previous state reached by event
state : Hash_Type;
end record;
package Edges_Pkg is new Vectors (Element_Type => Edge,
package Edges_Pkg is new Vectors (Element_Type => Edge_ty,
Index_Type => Vect_Count);
-- A state is made of a context and a set of edges leading to it
......@@ -154,7 +173,7 @@ procedure model_checker is
function Add_to_graph(event : Event_ty) return Hash_Type is
New_State: State_Access;
New_Hash : Hash_Type;
New_Edge : Edge := (event => event, state => backup_hash);
New_Edge : constant Edge_ty := (event => event, state => backup_hash);
begin
New_Hash := State_Hash(Process_Ctxt);
if not Grafset.Contains(Key => New_Hash) then
......@@ -174,12 +193,12 @@ procedure model_checker is
-- Vector of hashes (integers) used for the model checking
package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count);
use Lists;
package Sets is new Ordered_Sets(Element_Type => Hash_Type);
queue : Lists.Vector;
visited : Sets.Set;
properties: Sets.Set;
-- Check all properties in one go, and if one fails, set errno
function check_properties(errno: out natural) return boolean is
......@@ -197,6 +216,9 @@ procedure model_checker is
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);
......@@ -217,21 +239,79 @@ procedure model_checker is
<exhausts;separator="\n">
end;
procedure Generate_MSC is
package Loc_Maps is new Ordered_Maps(Key_Type => Hash_Type,
Element_Type => Boolean);
package Evt_Lists is new Vectors(Element_Type => Event_ty,
Index_Type => Vect_Count);
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
Loc_Q : Lists.Vector;
Loc_Visited : Loc_Maps.Map;
Next_Hash : Hash_Type;
State : State_Access;
Parent_Map : Parent_Maps.Map;
Curr : Hash_Type;
Edge : Edge_Ty;
Scenario : Evt_Lists.Vector;
begin
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);
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,
New_Item => True);
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);
Curr := Edge.State;
Scenario.Append(Edge.Event);
end loop;
return Scenario;
end;
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_evt of Scenario loop
Print_Event(each_evt);
end loop;
end loop;
end;
event : Event_ty(start);
S_Hash : Hash_Type;
Start_Time : Time := Clock;
Start_Time : constant Time := Clock;
begin
put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
orchestrator.startup;
S_Hash := Add_to_graph(event => event);
check_and_report(S_Hash);
queue.append(S_Hash);
visited.include(S_Hash);
while queue.Length > 0 loop
Start_Hash := Add_to_graph(event => event);
check_and_report(Start_Hash);
queue.append(Start_Hash);
visited.include(Start_Hash);
while queue.Length > 0 and properties.length \<= 10 loop
Process_Ctxt := Grafset.Element(Key => queue.Last_Element).Context;
exhaustive_simulation;
queue.delete_last;
end loop;
if properties.length > 0 then
Generate_MSC;
end if;
put_line("Executed" & count'img & " functions");
put_line("Visited" & Grafset.Length'img & " states");
Put_Line("Execution time:" & Duration'Image(Clock - Start_Time) & "s.");
......@@ -275,14 +355,17 @@ def generate(ast, stop_conditions):
required_interfaces.append(str(ri_tpl))
events = []
print_events = []
for name, sort in pis.viewitems():
event_tpl = StringTemplate(event, group=group)
event_tpl['interface'] = name
event_tpl['param'] = True if sort else False
event_tpl['sort'] = (opengeode.AdaGenerator.type_name(sort,
use_prefix=False)
if sort else "")
print_event_tpl = StringTemplate(print_event, group=group)
event_tpl['interface'] = print_event_tpl['interface'] = name
event_tpl['param'] = print_event_tpl['param'] = True if sort else False
event_tpl['sort'] = print_event_tpl['sort'] = \
(opengeode.AdaGenerator.type_name(sort, use_prefix=False)
if sort else "")
events.append(str(event_tpl))
print_events.append(str(print_event_tpl))
check_ppties = []
for idx in range(len(stop_conditions)):
......@@ -319,6 +402,7 @@ def generate(ast, stop_conditions):
complete['asn1_modules'] = asn1_modules
complete['interfaces'] = provided_interfaces
complete['events'] = events
complete['print_events'] = print_events
complete['check_properties'] = check_ppties
complete['exhaust_procedures'] = exhaust_procedures
complete['exhausts'] = exhausts
......
......@@ -16,7 +16,7 @@ Author: Maxime.Perrotin@esa.int
__author__ = "Maxime Perrotin"
__license__ = "LGPL v3"
__version__ = "1.1.1"
__version__ = "1.1.2"
__url__ = "http://taste.tuxfamily.org"
import os
......
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