Commit a4bee08c authored by Maxime Perrotin's avatar Maxime Perrotin

Update model checker

parent c683f697
......@@ -29,67 +29,67 @@ def asn1_module (module: str) -> str:
'''
def provided_interface (interface: str) -> str:
return f'{interface}_pi'
return f'{interface}_PI'
def required_interface (interface: str) -> str:
return f'{interface}_ri'
return f'{interface}_RI'
def event (interface: str, sort: str, param: bool) -> str:
if param:
return f'''when {interface}_pi =>
{interface}_Param: aliased asn1Scc{sort};'''
return f'''when {interface}_PI =>
{interface}_Param : aliased asn1Scc{sort};'''
else:
return f'''when {interface}_pi =>
return f'''when {interface}_PI =>
null;'''
def print_event (interface: str, sort: str, param : bool) -> str:
if param:
return f'''when {interface}_pi =>
return f'''when {interface}_PI =>
Put_Line ("{interface}(" & {sort}_Pkg.Image(Event.{interface}_Param) & ")");'''
else:
return f'''when {interface}_pi =>
return f'''when {interface}_PI =>
Put_Line ("{interface}");'''
def check_ppty (num: int, model: str) -> str:
return f'''errno := {num};
res := {model}_stop_conditions.p\u00dcproperty_{num};
if res then
return res;
return f'''Errno := {num};
Res := {model}_Stop_Conditions.p\u00dcproperty_{num};
if Res then
return Res;
end if;
'''
def exhaust_procedure (interface: str, sort: str, model: str, param: bool) -> str:
if param:
return f'''procedure exhaust_{interface} is
{interface}_it : {sort}_pkg.Instance;
event : Event_ty({interface}_pi);
S_Hash : Hash_Type;
return f'''procedure Exhaust_{interface} is
{interface}_It : {sort}_pkg.Instance;
Event : Event_Ty ({interface}_PI);
S_Hash : Hash_Type;
begin
for each of {interface}_it loop
{sort}_pkg.To_ASN1(each, event.{interface}_param);
{model}.{interface}(event.{interface}_param'access);
ES.count := ES.count + 1;
S_Hash := Add_To_Graph(event => event);
Check_And_Report(S_Hash);
Process_Ctxt := backup_ctxt;
exit when properties.length >= 10;
for Each of {interface}_it loop
Event.{interface}_Param := {sort}_Pkg.To_ASN1 (Each);
{model}.{interface} (Event.{interface}_Param'access);
ES.Count := ES.Count + 1;
S_Hash := Add_To_Graph (Event => Event);
Check_And_Report (S_Hash);
Process_Ctxt := Backup_Ctxt;
exit when Properties.Length >= 10;
end loop;
end;'''
end Exhaust_{interface};'''
else:
return f'''procedure exhaust_{interface} is
event : Event_ty({interface}_pi);
S_Hash : Hash_Type;
return f'''procedure Exhaust_{interface} is
Event : Event_Ty ({interface}_PI);
S_Hash : Hash_Type;
begin
{model}.{interface};
ES.count := ES.count + 1;
S_Hash := Add_To_Graph(event => event);
Check_And_Report(S_Hash);
Process_Ctxt := Backup_Ctxt;
end;'''
{model}.{interface};
ES.Count := ES.Count + 1;
S_Hash := Add_To_Graph (Event => Event);
Check_And_Report (S_Hash);
Process_Ctxt := Backup_Ctxt;
end Exhaust_{interface};'''
def exhaust (states: List[str], interface : str) -> str:
return f'''if Process_Ctxt.State in {" | ".join(states)} then
exhaust_{interface};
Exhaust_{interface};
end if;'''
def checker_template (model: str,
......@@ -117,9 +117,8 @@ use Ada.Containers,
with ASN1_Iterators.Exhaustive_Simulation;
use ASN1_Iterators;
procedure Model_Checker is
subtype Context_ty is {model}_ctxt_ty;
subtype Context_ty is {model}_Ctxt_Ty;
Process_Ctxt : Context_ty renames {model}_Ctxt;
-- Type representing an event (input or output)
......@@ -127,18 +126,18 @@ procedure Model_Checker is
type Event_ty (Option: Interfaces := Start) is
record
case Option is
when start =>
when Start =>
null;
{indent(12, events)}
end case;
end record;
-- Display scenario (in the future: generate MSC)
procedure Print_Event(Event: Event_ty) is
procedure Print_Event (Event: Event_ty) is
begin
case Event.Option is
when start =>
Put_Line("START");
when Start =>
Put_Line ("START");
{indent(9, print_events)}
end case;
end;
......@@ -164,22 +163,22 @@ procedure Model_Checker is
procedure Exhaustive_Simulator is
begin
backup_ctxt := Process_Ctxt;
backup_hash := State_Hash(Backup_ctxt);
Backup_Ctxt := Process_Ctxt;
Backup_Hash := State_Hash (Backup_ctxt);
{indent(6, exhausts)}
end Exhaustive_Simulator;
Event : Event_ty(start);
Event : Event_ty (Start);
Start_Time : constant Time := Clock;
begin
Put_Line ("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
{model}.Startup;
Start_Hash := Add_to_graph (Event => Event);
Check_And_Report(Start_Hash);
ES.Queue.append(Start_Hash);
Visited.Include(Start_Hash);
Start_Hash := Add_To_Graph (Event => Event);
Check_And_Report (Start_Hash);
ES.Queue.append (Start_Hash);
Visited.Include (Start_Hash);
while ES.Queue.Length > 0 and Properties.Length <= 10 loop
Process_Ctxt := Grafset.Element(Key => ES.Queue.Last_Element).Context;
Process_Ctxt := Grafset.Element (Key => ES.Queue.Last_Element).Context;
Exhaustive_Simulator;
ES.Queue.Delete_Last;
end loop;
......
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