Commit 35412d34 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Create a full graph including edges

parent d73ce7d5
...@@ -38,7 +38,6 @@ exhaust_procedure = '''procedure exhaust_<interface> is ...@@ -38,7 +38,6 @@ exhaust_procedure = '''procedure exhaust_<interface> is
event : Event_ty(<interface>_pi); event : Event_ty(<interface>_pi);
S_Hash : Hash_Type; S_Hash : Hash_Type;
begin begin
backup_ctxt := Process_Ctxt;
<if(param)> <if(param)>
for each of <interface>_it loop for each of <interface>_it loop
<sort>_pkg.To_ASN1(each, event.<interface>_param); <sort>_pkg.To_ASN1(each, event.<interface>_param);
...@@ -53,6 +52,7 @@ begin ...@@ -53,6 +52,7 @@ begin
count := count + 1; count := count + 1;
S_Hash := Add_to_graph(event => event); S_Hash := Add_to_graph(event => event);
check_and_report(S_Hash); check_and_report(S_Hash);
Process_Ctxt := backup_ctxt;
<endif> <endif>
end;''' end;'''
...@@ -95,10 +95,14 @@ procedure model_checker is ...@@ -95,10 +95,14 @@ procedure model_checker is
-- To save/restore the context when calling a PI: -- To save/restore the context when calling a PI:
backup_ctxt : Context_ty; backup_ctxt : Context_ty;
backup_hash : Hash_Type;
-- Set a maximum size for vectors (set of states and edges)
subtype Vect_Count is Positive range 1 .. 1000000;
-- Type representing an event (input or output) -- Type representing an event (input or output)
type Interfaces is (start, <interfaces;separator=", ">); type Interfaces is (start, <interfaces;separator=", ">);
type Event_ty (Option: Interfaces) is type Event_ty (Option: Interfaces := start) is
record record
case Option is case Option is
when start => when start =>
...@@ -107,10 +111,20 @@ procedure model_checker is ...@@ -107,10 +111,20 @@ procedure model_checker is
end case; end case;
end record; end record;
-- Type representing an entry in the state graph -- An edge is made of a past state reference and an event to leave it
type Global_State (I: Interfaces) is type Edge is
record
event : Event_ty;
state : Hash_Type; -- Previous state reached by event
end record;
package Edges_Pkg is new Vectors (Element_Type => Edge,
Index_Type => Vect_Count);
-- A state is made of a context and a set of edges leading to it
type Global_State is
record record
event : Event_ty(I); edges : Edges_Pkg.Vector := Edges_Pkg.Empty_Vector;
context : Context_ty; context : Context_ty;
end record; end record;
...@@ -133,20 +147,24 @@ procedure model_checker is ...@@ -133,20 +147,24 @@ procedure model_checker is
function As_SEA_Ptr is function As_SEA_Ptr is
new Ada.Unchecked_Conversion (System.Address, SEA_Pointer); new Ada.Unchecked_Conversion (System.Address, SEA_Pointer);
function State_Hash(state: State_Access) return Hash_Type is function State_Hash(Context: Context_Ty) 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(Context'Address).all)));
-- Add a state to the graph: compute the hash (key) and store if not already there -- Add a state to the graph: compute the hash (key) and store if not already there
function Add_to_graph(event : Event_ty) return Hash_Type is function Add_to_graph(event : Event_ty) return Hash_Type is
New_State: constant State_Access := new Global_State(event.Option); New_State: State_Access;
New_Hash : Hash_Type; New_Hash : Hash_Type;
New_Edge : Edge := (event => event, state => backup_hash);
begin begin
New_State.event := event; New_Hash := State_Hash(Process_Ctxt);
New_State.context := Process_Ctxt;
New_Hash := State_Hash(New_State);
if not Grafset.Contains(Key => New_Hash) then if not Grafset.Contains(Key => New_Hash) then
New_State := new Global_State;
New_State.context := Process_Ctxt;
Grafset.Insert(Key => New_Hash, New_Item => New_State); Grafset.Insert(Key => New_Hash, New_Item => New_State);
else
New_State := Grafset.Element(Key => New_Hash);
end if; end if;
New_State.edges.append(New_Edge);
return New_Hash; return New_Hash;
end; end;
...@@ -154,7 +172,6 @@ procedure model_checker is ...@@ -154,7 +172,6 @@ procedure model_checker is
count : natural := 0; 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;
package Lists is new Vectors (Element_Type => Hash_Type, package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count); Index_type => Vect_Count);
use Lists; use Lists;
...@@ -195,6 +212,8 @@ procedure model_checker is ...@@ -195,6 +212,8 @@ procedure model_checker is
procedure exhaustive_simulation is procedure exhaustive_simulation is
begin begin
backup_ctxt := Process_Ctxt;
backup_hash := State_Hash(Backup_ctxt);
<exhausts;separator="\n"> <exhausts;separator="\n">
end; end;
......
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
''' Property parser for SDL systems ''' Property parser for SDL systems
Parse expressions such as: Parse expressions such as:
"stop if state=toto and x = 3" "stop if state=toto and x=3"
and generate code to verify the property and generate code to verify the property
...@@ -16,7 +16,7 @@ Author: Maxime.Perrotin@esa.int ...@@ -16,7 +16,7 @@ Author: Maxime.Perrotin@esa.int
__author__ = "Maxime Perrotin" __author__ = "Maxime Perrotin"
__license__ = "LGPL v3" __license__ = "LGPL v3"
__version__ = "1.1.0" __version__ = "1.1.1"
__url__ = "http://taste.tuxfamily.org" __url__ = "http://taste.tuxfamily.org"
import os 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