asn1_iterators-exhaustive_simulation.adb 4.12 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
-- (c) 2017 European Space Agency / TASTE Project
package body ASN1_Iterators.Exhaustive_Simulation is

    function State_Hash(Context: Context_Ty) return Hash_Type is
        (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
    function Add_to_graph(event : Event_ty) return Hash_Type is
        New_State: State_Access;
        New_Hash : Hash_Type;
        New_Edge : constant Edge_ty := (event => event, state => backup_hash);
    begin
        New_Hash := State_Hash(Process_Ctxt.all);
        if not Grafset.Contains(Key => New_Hash) then
            New_State := new Global_State;
            New_State.context := Process_Ctxt.all;
            Grafset.Insert(Key => New_Hash, New_Item => New_State);
        else
            New_State := Grafset.Element(Key => New_Hash);
        end if;
        New_State.edges.append(New_Edge);
        return New_Hash;
    end;

    -- Report the result of the property check to the user
    procedure Check_And_Report (S_Hash: Hash_Type) is
        errno: Natural := 0;
        stop_condition: boolean := false;
    begin
        count := count + 1;
        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);
            if stop_condition = false then
                queue.append(S_Hash);
            end if;
        end if;
    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;
end ASN1_Iterators.Exhaustive_Simulation;