-- PSL - NFA builder. -- Copyright (C) 2002-2016 Tristan Gingold -- -- This program is free software: you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation, either version 2 of the License, or -- (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program. If not, see . with Tables; with Ada.Text_IO; use Ada.Text_IO; with Types; use Types; with PSL.Types; use PSL.Types; with PSL.Errors; use PSL.Errors; with PSL.CSE; use PSL.CSE; with PSL.QM; with PSL.Disp_NFAs; use PSL.Disp_NFAs; with PSL.Optimize; use PSL.Optimize; with PSL.NFAs.Utils; with PSL.Prints; with PSL.NFAs; use PSL.NFAs; package body PSL.Build is package Intersection is function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA; end Intersection; package body Intersection is type Stack_Entry_Id is new Natural; No_Stack_Entry : constant Stack_Entry_Id := 0; type Stack_Entry is record L, R : NFA_State; Res : NFA_State; Next_Unhandled : Stack_Entry_Id; end record; package Stackt is new Tables (Table_Component_Type => Stack_Entry, Table_Index_Type => Stack_Entry_Id, Table_Low_Bound => 1, Table_Initial => 128); First_Unhandled : Stack_Entry_Id; procedure Init_Stack is begin Stackt.Init; First_Unhandled := No_Stack_Entry; end Init_Stack; function Not_Empty return Boolean is begin return First_Unhandled /= No_Stack_Entry; end Not_Empty; procedure Pop_State (L, R : out NFA_State) is begin L := Stackt.Table (First_Unhandled).L; R := Stackt.Table (First_Unhandled).R; First_Unhandled := Stackt.Table (First_Unhandled).Next_Unhandled; end Pop_State; function Get_State (N : NFA; L, R : NFA_State) return NFA_State is Res : NFA_State; begin for I in Stackt.First .. Stackt.Last loop if Stackt.Table (I).L = L and then Stackt.Table (I).R = R then return Stackt.Table (I).Res; end if; end loop; Res := Add_State (N); Stackt.Append ((L => L, R => R, Res => Res, Next_Unhandled => First_Unhandled)); First_Unhandled := Stackt.Last; return Res; end Get_State; function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA is Start_L, Start_R : NFA_State; Final_L, Final_R : NFA_State; S_L, S_R : NFA_State; E_L, E_R : NFA_Edge; Res : NFA; Start : NFA_State; Extra_L, Extra_R : NFA_Edge; T : Node; begin Start_L := Get_Start_State (L); Start_R := Get_Start_State (R); Final_R := Get_Final_State (R); Final_L := Get_Final_State (L); if False then Disp_Body (L); Disp_Body (R); Put ("//start state: "); Disp_State (Start_L); Put (","); Disp_State (Start_R); New_Line; end if; if Match_Len then Extra_L := No_Edge; Extra_R := No_Edge; else Extra_L := Add_Edge (Final_L, Final_L, True_Node); Extra_R := Add_Edge (Final_R, Final_R, True_Node); end if; Res := Create_NFA; Init_Stack; Start := Get_State (Res, Start_L, Start_R); Set_Start_State (Res, Start); while Not_Empty loop Pop_State (S_L, S_R); if False then Put ("//poped state: "); Disp_State (S_L); Put (","); Disp_State (S_R); New_Line; end if; E_L := Get_First_Src_Edge (S_L); while E_L /= No_Edge loop E_R := Get_First_Src_Edge (S_R); while E_R /= No_Edge loop if not (E_L = Extra_L and E_R = Extra_R) then T := Build_Bool_And (Get_Edge_Expr (E_L), Get_Edge_Expr (E_R)); Add_Edge (Get_State (Res, S_L, S_R), Get_State (Res, Get_Edge_Dest (E_L), Get_Edge_Dest (E_R)), T); end if; E_R := Get_Next_Src_Edge (E_R); end loop; E_L := Get_Next_Src_Edge (E_L); end loop; end loop; Set_Final_State (Res, Get_State (Res, Final_L, Final_R)); Remove_Unreachable_States (Res); if not Match_Len then Remove_Edge (Extra_L); Remove_Edge (Extra_R); end if; -- FIXME: free L and R. return Res; end Build_Inter; end Intersection; -- All edges from A are duplicated using B as a source. -- Handle epsilon-edges. procedure Duplicate_Src_Edges (N : NFA; A, B : NFA_State) is pragma Unreferenced (N); E : NFA_Edge; Expr : Node; Dest : NFA_State; begin pragma Assert (A /= B); E := Get_First_Src_Edge (A); while E /= No_Edge loop Expr := Get_Edge_Expr (E); Dest := Get_Edge_Dest (E); if Expr /= Null_Node then Add_Edge (B, Dest, Expr); end if; E := Get_Next_Src_Edge (E); end loop; end Duplicate_Src_Edges; -- All edges to A are duplicated using B as a destination. -- Handle epsilon-edges. procedure Duplicate_Dest_Edges (N : NFA; A, B : NFA_State) is pragma Unreferenced (N); E : NFA_Edge; Expr : Node; Src : NFA_State; begin pragma Assert (A /= B); E := Get_First_Dest_Edge (A); while E /= No_Edge loop Expr := Get_Edge_Expr (E); Src := Get_Edge_Src (E); if Expr /= Null_Node then Add_Edge (Src, B, Expr); end if; E := Get_Next_Dest_Edge (E); end loop; end Duplicate_Dest_Edges; procedure Remove_Epsilon_Edge (N : NFA; S, D : NFA_State) is begin if Get_First_Src_Edge (S) = No_Edge then -- No edge from S. -- Move edges to S to D. Redest_Edges (S, D); Remove_Unconnected_State (N, S); if Get_Start_State (N) = S then Set_Start_State (N, D); end if; elsif Get_First_Dest_Edge (D) = No_Edge then -- No edge to D. -- Move edges from D to S. Resource_Edges (D, S); Remove_Unconnected_State (N, D); if Get_Final_State (N) = D then Set_Final_State (N, S); end if; else Duplicate_Dest_Edges (N, S, D); Duplicate_Src_Edges (N, D, S); Remove_Identical_Src_Edges (S); end if; end Remove_Epsilon_Edge; procedure Remove_Epsilon (N : NFA; E : NFA_Edge) is S : constant NFA_State := Get_Edge_Src (E); D : constant NFA_State := Get_Edge_Dest (E); begin Remove_Edge (E); Remove_Epsilon_Edge (N, S, D); end Remove_Epsilon; function Build_Concat (L, R : NFA) return NFA is Start_L, Start_R : NFA_State; Final_L, Final_R : NFA_State; Eps_L, Eps_R : Boolean; E_L, E_R : NFA_Edge; begin Start_L := Get_Start_State (L); Start_R := Get_Start_State (R); Final_R := Get_Final_State (R); Final_L := Get_Final_State (L); Eps_L := Get_Epsilon_NFA (L); Eps_R := Get_Epsilon_NFA (R); Merge_NFA (L, R); Set_Start_State (L, Start_L); Set_Final_State (L, Final_R); Set_Epsilon_NFA (L, False); if Eps_L then E_L := Add_Edge (Start_L, Final_L, Null_Node); end if; if Eps_R then E_R := Add_Edge (Start_R, Final_R, Null_Node); end if; Remove_Epsilon_Edge (L, Final_L, Start_R); if Eps_L then Remove_Epsilon (L, E_L); end if; if Eps_R then Remove_Epsilon (L, E_R); end if; if (Start_L = Final_L or else Eps_L) and then (Start_R = Final_R or else Eps_R) then Set_Epsilon_NFA (L, True); end if; Remove_Identical_Src_Edges (Final_L); Remove_Identical_Dest_Edges (Start_R); return L; end Build_Concat; function Build_Or (L, R : NFA) return NFA is Start_L, Start_R : NFA_State; Final_L, Final_R : NFA_State; Eps : Boolean; Start, Final : NFA_State; E_S_L, E_S_R, E_L_F, E_R_F : NFA_Edge; begin Start_L := Get_Start_State (L); Start_R := Get_Start_State (R); Final_R := Get_Final_State (R); Final_L := Get_Final_State (L); Eps := Get_Epsilon_NFA (L) or Get_Epsilon_NFA (R); -- Optimize [*0] | R. -- TODO: this was not valid if there is an edge from Start(R) -- to Start(R), like: {[*0] | {d[*]; e}} if False and then Start_L = Final_L and then Get_First_Src_Edge (Start_L) = No_Edge then if Start_R /= Final_R then Set_Epsilon_NFA (R, True); end if; -- FIXME -- delete_NFA (L); return R; end if; Merge_NFA (L, R); -- Use Thompson construction. Start := Add_State (L); Set_Start_State (L, Start); E_S_L := Add_Edge (Start, Start_L, Null_Node); E_S_R := Add_Edge (Start, Start_R, Null_Node); Final := Add_State (L); Set_Final_State (L, Final); E_L_F := Add_Edge (Final_L, Final, Null_Node); E_R_F := Add_Edge (Final_R, Final, Null_Node); Set_Epsilon_NFA (L, Eps); Remove_Epsilon (L, E_S_L); Remove_Epsilon (L, E_S_R); Remove_Epsilon (L, E_L_F); Remove_Epsilon (L, E_R_F); return L; end Build_Or; function Build_Fusion (L, R : NFA) return NFA is Start_R : NFA_State; Final_L, Final_R, S_L : NFA_State; E_L : NFA_Edge; E_R : NFA_Edge; N_L, Expr : Node; begin Start_R := Get_Start_State (R); Final_R := Get_Final_State (R); Final_L := Get_Final_State (L); Merge_NFA (L, R); E_L := Get_First_Dest_Edge (Final_L); while E_L /= No_Edge loop S_L := Get_Edge_Src (E_L); N_L := Get_Edge_Expr (E_L); E_R := Get_First_Src_Edge (Start_R); while E_R /= No_Edge loop Expr := Build_Bool_And (N_L, Get_Edge_Expr (E_R)); Expr := PSL.QM.Reduce (Expr); if Expr /= False_Node then Add_Edge (S_L, Get_Edge_Dest (E_R), Expr); end if; E_R := Get_Next_Src_Edge (E_R); end loop; Remove_Identical_Src_Edges (S_L); E_L := Get_Next_Dest_Edge (E_L); end loop; Set_Final_State (L, Final_R); Set_Epsilon_NFA (L, False); if Get_First_Src_Edge (Final_L) = No_Edge and then Final_L /= Get_Active_State (L) then Remove_State (L, Final_L); end if; if Get_First_Dest_Edge (Start_R) = No_Edge then Remove_State (L, Start_R); end if; return L; end Build_Fusion; function Build_Star_Repeat (N : Node) return NFA is Res : NFA; Start, Final, S : NFA_State; Seq : Node; begin Seq := Get_Sequence (N); if Seq = Null_Node then -- Epsilon. Res := Create_NFA; S := Add_State (Res); Set_Start_State (Res, S); Set_Final_State (Res, S); Set_Epsilon_NFA (Res, True); return Res; end if; Res := Build_SERE_FA (Seq); Start := Get_Start_State (Res); Final := Get_Final_State (Res); Redest_Edges (Final, Start); Set_Final_State (Res, Start); Remove_Unconnected_State (Res, Final); Set_Epsilon_NFA (Res, False); return Res; end Build_Star_Repeat; function Build_Plus_Repeat (N : Node) return NFA is Res : NFA; Start, Final, Src : NFA_State; T : NFA_Edge; begin Res := Build_SERE_FA (Get_Sequence (N)); Start := Get_Start_State (Res); Final := Get_Final_State (Res); -- Create edges from pre-final to start. T := Get_First_Dest_Edge (Final); while T /= No_Edge loop Src := Get_Edge_Src (T); if Src /= Start then -- Normal before-final to start. Add_Edge (Src, Start, Get_Edge_Expr (T)); else -- Do not create edges from start to start, as this is not the -- correct sequence (it will accept words like 001, while -- the first letter must be 1). Add_Edge (Final, Final, Get_Edge_Expr (T)); end if; T := Get_Next_Src_Edge (T); end loop; return Res; end Build_Plus_Repeat; -- Association actual to formals, so that when a formal is referenced, the -- actual can be used instead. procedure Assoc_Instance (Decl : Node; Instance : Node) is Formal : Node; Actual : Node; begin -- Temporary associates actuals to formals. Formal := Get_Parameter_List (Decl); Actual := Get_Association_Chain (Instance); while Formal /= Null_Node loop if Actual = Null_Node then -- Not enough actual. raise Internal_Error; end if; if Get_Actual (Formal) /= Null_Node then -- Recursion raise Internal_Error; end if; Set_Actual (Formal, Get_Actual (Actual)); Formal := Get_Chain (Formal); Actual := Get_Chain (Actual); end loop; if Actual /= Null_Node then -- Too many actual. raise Internal_Error; end if; end Assoc_Instance; procedure Unassoc_Instance (Decl : Node) is Formal : Node; begin -- Remove temporary association. Formal := Get_Parameter_List (Decl); while Formal /= Null_Node loop Set_Actual (Formal, Null_Node); Formal := Get_Chain (Formal); end loop; end Unassoc_Instance; function Build_SERE_FA (N : Node) return NFA is Res : NFA; S1, S2 : NFA_State; begin case Get_Kind (N) is when N_Booleans => Res := Create_NFA; S1 := Add_State (Res); S2 := Add_State (Res); Set_Start_State (Res, S1); Set_Final_State (Res, S2); if N /= False_Node then Add_Edge (S1, S2, N); end if; return Res; when N_Braced_SERE => return Build_SERE_FA (Get_SERE (N)); when N_Concat_SERE => return Build_Concat (Build_SERE_FA (Get_Left (N)), Build_SERE_FA (Get_Right (N))); when N_Fusion_SERE => return Build_Fusion (Build_SERE_FA (Get_Left (N)), Build_SERE_FA (Get_Right (N))); when N_Match_And_Seq => return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), Build_SERE_FA (Get_Right (N)), True); when N_And_Seq => return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), Build_SERE_FA (Get_Right (N)), False); when N_Or_Prop | N_Or_Seq => return Build_Or (Build_SERE_FA (Get_Left (N)), Build_SERE_FA (Get_Right (N))); when N_Star_Repeat_Seq => return Build_Star_Repeat (N); when N_Plus_Repeat_Seq => return Build_Plus_Repeat (N); when N_Sequence_Instance | N_Endpoint_Instance => declare Decl : Node; begin Decl := Get_Declaration (N); Assoc_Instance (Decl, N); Res := Build_SERE_FA (Get_Sequence (Decl)); Unassoc_Instance (Decl); return Res; end; when N_Boolean_Parameter | N_Sequence_Parameter => declare Actual : constant Node := Get_Actual (N); begin if Actual = Null_Node then raise Internal_Error; end if; return Build_SERE_FA (Actual); end; when others => Error_Kind ("build_sere_fa", N); end case; end Build_SERE_FA; function Count_Edges (S : NFA_State) return Natural is Res : Natural; E : NFA_Edge; begin Res := 0; E := Get_First_Src_Edge (S); while E /= No_Edge loop Res := Res + 1; E := Get_Next_Src_Edge (E); end loop; return Res; end Count_Edges; type Count_Vector is array (Natural range <>) of Natural; procedure Count_All_Edges (N : NFA; Res : out Count_Vector) is S : NFA_State; begin S := Get_First_State (N); while S /= No_State loop Res (Natural (Get_State_Label (S))) := Count_Edges (S); S := Get_Next_State (S); end loop; end Count_All_Edges; pragma Unreferenced (Count_All_Edges); package Determinize is -- Create a new NFA that reaches its final state only when N fails -- (ie when the final state is not reached). function Determinize (N : NFA) return NFA; end Determinize; package body Determinize is -- In all the comments N stands for the initial NFA (ie the NFA to -- determinize). use Prints; Flag_Trace : constant Boolean := False; Last_Label : Int32 := 0; -- The tree associates a set of states in N to *an* uniq set in the -- result NFA. -- -- As the NFA is labelized, each node represent a state in N, and has -- two branches: one for state is present and one for state is absent. -- -- The leaves contain the state in the result NFA. -- -- The leaves are chained to create a stack of state to handle. -- -- The root of the tree is node Start_Tree_Id and represent the start -- state of N. type Deter_Tree_Id is new Natural; No_Tree_Id : constant Deter_Tree_Id := 0; Start_Tree_Id : constant Deter_Tree_Id := 1; -- List of unhanded leaves. Deter_Head : Deter_Tree_Id; type Deter_Tree_Id_Bool_Array is array (Boolean) of Deter_Tree_Id; -- Node in the tree. type Deter_Tree_Entry is record Parent : Deter_Tree_Id; -- For non-leaf: Child : Deter_Tree_Id_Bool_Array; -- For leaf: Link : Deter_Tree_Id; State : NFA_State; -- + value ? end record; package Detert is new Tables (Table_Component_Type => Deter_Tree_Entry, Table_Index_Type => Deter_Tree_Id, Table_Low_Bound => 1, Table_Initial => 128); type Bool_Vector is array (Natural range <>) of Boolean; pragma Pack (Bool_Vector); -- Convert a set of states in N to a state in the result NFA. -- The set is represented by a vector of boolean. An element of the -- vector is true iff the corresponding state is present. function Add_Vector (V : Bool_Vector; N : NFA) return NFA_State is E : Deter_Tree_Id; Added : Boolean; Res : NFA_State; begin E := Start_Tree_Id; Added := False; for I in V'Range loop if Detert.Table (E).Child (V (I)) = No_Tree_Id then Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), Parent => E, Link => No_Tree_Id, State => No_State)); Detert.Table (E).Child (V (I)) := Detert.Last; E := Detert.Last; Added := True; else E := Detert.Table (E).Child (V (I)); Added := False; end if; end loop; if Added then -- Create the new state. Res := Add_State (N); Detert.Table (E).State := Res; if Flag_Trace then Set_State_Label (Res, Last_Label); Put ("Result state" & Int32'Image (Last_Label) & " for"); for I in V'Range loop if V (I) then Put (Natural'Image (I)); end if; end loop; New_Line; Last_Label := Last_Label + 1; end if; -- Put it to the list of states to be handled. Detert.Table (E).Link := Deter_Head; Deter_Head := E; return Res; else return Detert.Table (E).State; end if; end Add_Vector; -- Return true iff the stack is empty (ie all the states have been -- handled). function Stack_Empty return Boolean is begin return Deter_Head = No_Tree_Id; end Stack_Empty; -- Get an element from the stack. -- Extract the state in the result NFA. -- Rebuild the set of states in N (ie rebuild the vector of states). procedure Stack_Pop (V : out Bool_Vector; S : out NFA_State) is L, P : Deter_Tree_Id; begin L := Deter_Head; pragma Assert (L /= No_Tree_Id); S := Detert.Table (L).State; Deter_Head := Detert.Table (L).Link; for I in reverse V'Range loop pragma Assert (L /= Start_Tree_Id); P := Detert.Table (L).Parent; if L = Detert.Table (P).Child (True) then V (I) := True; elsif L = Detert.Table (P).Child (False) then V (I) := False; else raise Program_Error; end if; L := P; end loop; pragma Assert (L = Start_Tree_Id); end Stack_Pop; type State_Vector is array (Natural range <>) of Natural; type Expr_Vector is array (Natural range <>) of Node; procedure Build_Arcs (N : NFA; State : NFA_State; States : State_Vector; Exprs : Expr_Vector; Expr : Node; V : Bool_Vector) is T : Node; begin if Expr = False_Node then return; end if; if States'Length = 0 then declare Reduced_Expr : constant Node := PSL.QM.Reduce (Expr); --Reduced_Expr : constant Node := Expr; S : NFA_State; begin if Reduced_Expr = False_Node then return; end if; S := Add_Vector (V, N); Add_Edge (State, S, Reduced_Expr); if Flag_Trace then Put (" Add edge"); Put (Int32'Image (Get_State_Label (State))); Put (" to"); Put (Int32'Image (Get_State_Label (S))); Put (", expr="); Dump_Expr (Expr); Put (", reduced="); Dump_Expr (Reduced_Expr); New_Line; end if; end; else declare N_States : State_Vector renames States (States'First + 1 .. States'Last); N_V : Bool_Vector (V'Range) := V; S : constant Natural := States (States'First); E : constant Node := Exprs (S); begin N_V (S) := True; if Expr = Null_Node then Build_Arcs (N, State, N_States, Exprs, E, N_V); T := Build_Bool_Not (E); Build_Arcs (N, State, N_States, Exprs, T, V); else T := Build_Bool_And (E, Expr); Build_Arcs (N, State, N_States, Exprs, T, N_V); T := Build_Bool_Not (E); T := Build_Bool_And (T, Expr); Build_Arcs (N, State, N_States, Exprs, T, V); end if; end; end if; end Build_Arcs; function Determinize_1 (N : NFA; Nbr_States : Natural) return NFA is Final : Natural; V : Bool_Vector (0 .. Nbr_States - 1); Exprs : Expr_Vector (0 .. Nbr_States - 1); S : NFA_State; E : NFA_Edge; D : Natural; Edge_Expr : Node; Expr : Node; Nbr_Dest : Natural; States : State_Vector (0 .. Nbr_States - 1); Res : NFA; State : NFA_State; R : Node; begin Final := Natural (Get_State_Label (Get_Final_State (N))); -- FIXME: handle epsilon or final = start -> create an empty NFA. -- Initialize the tree. Res := Create_NFA; Detert.Init; Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), Parent => No_Tree_Id, Link => No_Tree_Id, State => No_State)); pragma Assert (Detert.Last = Start_Tree_Id); Deter_Head := No_Tree_Id; -- Put the initial state in the tree and in the stack. -- FIXME: ok, we know that its label is 0. V := (0 => True, others => False); State := Add_Vector (V, Res); Set_Start_State (Res, State); -- The failure state. As there is nothing to do with this -- state, remove it from the stack. V := (others => False); State := Add_Vector (V, Res); Set_Final_State (Res, State); Stack_Pop (V, State); -- Iterate on states in the result NFA that haven't yet been handled. while not Stack_Empty loop Stack_Pop (V, State); if Flag_Trace then Put_Line ("Handle result state" & Int32'Image (Get_State_Label (State))); end if; -- Build edges vector. Exprs := (others => Null_Node); Expr := Null_Node; S := Get_First_State (N); Nbr_Dest := 0; while S /= No_State loop if V (Natural (Get_State_Label (S))) then E := Get_First_Src_Edge (S); while E /= No_Edge loop D := Natural (Get_State_Label (Get_Edge_Dest (E))); Edge_Expr := Get_Edge_Expr (E); if False and Flag_Trace then Put_Line (" edge" & Int32'Image (Get_State_Label (S)) & " to" & Natural'Image (D)); end if; if D = Final then R := Build_Bool_Not (Edge_Expr); if Expr = Null_Node then Expr := R; else Expr := Build_Bool_And (Expr, R); end if; else if Exprs (D) = Null_Node then Exprs (D) := Edge_Expr; States (Nbr_Dest) := D; Nbr_Dest := Nbr_Dest + 1; else Exprs (D) := Build_Bool_Or (Exprs (D), Edge_Expr); end if; end if; E := Get_Next_Src_Edge (E); end loop; end if; S := Get_Next_State (S); end loop; if Flag_Trace then Put (" Final: expr="); Print_Expr (Expr); New_Line; for I in 0 .. Nbr_Dest - 1 loop Put (" Dest"); Put (Natural'Image (States (I))); Put (" expr="); Print_Expr (Exprs (States (I))); New_Line; end loop; end if; -- Build arcs. if not (Nbr_Dest = 0 and Expr = Null_Node) then Build_Arcs (Res, State, States (0 .. Nbr_Dest - 1), Exprs, Expr, Bool_Vector'(0 .. Nbr_States - 1 => False)); end if; end loop; --Remove_Unreachable_States (Res); return Res; end Determinize_1; function Determinize (N : NFA) return NFA is Nbr_States : Natural; begin Labelize_States (N, Nbr_States); if Flag_Trace then Put_Line ("NFA to determinize:"); Disp_NFA (N); Last_Label := 0; end if; return Determinize_1 (N, Nbr_States); end Determinize; end Determinize; function Build_Initial_Rep (N : NFA) return NFA is S : constant NFA_State := Get_Start_State (N); begin Add_Edge (S, S, True_Node); return N; end Build_Initial_Rep; procedure Build_Strong (N : NFA) is S : NFA_State; Final : constant NFA_State := Get_Final_State (N); begin S := Get_First_State (N); while S /= No_State loop -- FIXME. if S /= Final then Add_Edge (S, Final, EOS_Node); end if; S := Get_Next_State (S); end loop; end Build_Strong; procedure Build_Abort (N : NFA; Expr : Node) is S : NFA_State; E : NFA_Edge; Not_Expr : Node; begin Not_Expr := Build_Bool_Not (Expr); S := Get_First_State (N); while S /= No_State loop E := Get_First_Src_Edge (S); while E /= No_Edge loop Set_Edge_Expr (E, Build_Bool_And (Not_Expr, Get_Edge_Expr (E))); E := Get_Next_Src_Edge (E); end loop; S := Get_Next_State (S); end loop; end Build_Abort; function Build_Property_FA (N : Node; With_Active : Boolean) return NFA; function Build_Overlap_Imp (Left, Right : Node; With_Active : Boolean) return NFA is L, R : NFA; Res : NFA; begin L := Build_SERE_FA (Left); R := Build_Property_FA (Right, False); if With_Active then Set_Active_State (L, Get_Final_State (L)); end if; Res := Build_Fusion (L, R); -- Ensure the active state is kept. pragma Assert (Res = L); return Res; end Build_Overlap_Imp; function Build_Property_FA (N : Node; With_Active : Boolean) return NFA is L, R : NFA; begin case Get_Kind (N) is when N_Sequences | N_Booleans | N_Sequence_Instance => -- Build A(S) or A(B) R := Build_SERE_FA (N); return Determinize.Determinize (R); when N_Strong => R := Build_Property_FA (Get_Property (N), False); Build_Strong (R); return R; when N_Imp_Seq => -- R |=> P --> {R; TRUE} |-> P L := Build_SERE_FA (Get_Sequence (N)); R := Build_Property_FA (Get_Property (N), False); if With_Active then declare A : NFA_State; begin A := Add_State (L); Duplicate_Dest_Edges (L, Get_Final_State (L), A); Set_Active_State (L, A); end; end if; return Build_Concat (L, R); when N_Overlap_Imp_Seq => -- S |-> P is defined as Ac(S) : A(P) return Build_Overlap_Imp (Get_Sequence (N), Get_Property (N), With_Active); when N_Log_Imp_Prop => -- B -> P --> {B} |-> P --> Ac(B) : A(P) return Build_Overlap_Imp (Get_Left (N), Get_Right (N), With_Active); when N_And_Prop => -- P1 && P2 --> A(P1) | A(P2) L := Build_Property_FA (Get_Left (N), False); R := Build_Property_FA (Get_Right (N), False); return Build_Or (L, R); when N_Never => R := Build_SERE_FA (Get_Property (N)); return Build_Initial_Rep (R); when N_Always => R := Build_Property_FA (Get_Property (N), With_Active); return Build_Initial_Rep (R); when N_Abort | N_Sync_Abort => R := Build_Property_FA (Get_Property (N), With_Active); Build_Abort (R, Get_Boolean (N)); return R; when N_Property_Instance => declare Decl : Node; begin Decl := Get_Declaration (N); Assoc_Instance (Decl, N); R := Build_Property_FA (Get_Property (Decl), With_Active); Unassoc_Instance (Decl); return R; end; when others => Error_Kind ("build_property_fa", N); end case; end Build_Property_FA; function Build_FA (N : Node) return NFA is use PSL.NFAs.Utils; Res : NFA; begin Res := Build_Property_FA (N, True); if Optimize_Final then pragma Debug (Check_NFA (Res)); Remove_Unreachable_States (Res); if Has_Loop_On_Start (Res) then Remove_Simple_Prefix (Res); end if; Merge_Identical_States (Res); Merge_Edges (Res); end if; -- Clear the QM table. PSL.QM.Reset; return Res; end Build_FA; end PSL.Build;