diff options
Diffstat (limited to 'psl/psl-build.adb')
| -rw-r--r-- | psl/psl-build.adb | 1009 |
1 files changed, 0 insertions, 1009 deletions
diff --git a/psl/psl-build.adb b/psl/psl-build.adb deleted file mode 100644 index c3e47baa6..000000000 --- a/psl/psl-build.adb +++ /dev/null @@ -1,1009 +0,0 @@ -with GNAT.Table; -with Ada.Text_IO; use Ada.Text_IO; -with Types; use 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 - function Build_SERE_FA (N : Node) return NFA; - - - 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 GNAT.Table - (Table_Component_Type => Stack_Entry, - Table_Index_Type => Stack_Entry_Id, - Table_Low_Bound => 1, - Table_Initial => 128, - Table_Increment => 100); - - 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; - 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 - Add_Edge (Get_State (Res, S_L, S_R), - Get_State (Res, - Get_Edge_Dest (E_L), - Get_Edge_Dest (E_R)), - Build_Bool_And (Get_Edge_Expr (E_L), - Get_Edge_Expr (E_R))); - 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. - if 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 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); - 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 : NFA_State; - T : NFA_Edge; - begin - Res := Build_SERE_FA (Get_Sequence (N)); - Start := Get_Start_State (Res); - Final := Get_Final_State (Res); - T := Get_First_Dest_Edge (Final); - while T /= No_Edge loop - Add_Edge (Get_Edge_Src (T), Start, Get_Edge_Expr (T)); - 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 GNAT.Table - (Table_Component_Type => Deter_Tree_Entry, - Table_Index_Type => Deter_Tree_Id, - Table_Low_Bound => 1, - Table_Initial => 128, - Table_Increment => 100); - - 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 - 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); - Build_Arcs (N, State, N_States, Exprs, - Build_Bool_Not (E), V); - else - Build_Arcs (N, State, N_States, Exprs, - Build_Bool_And (E, Expr), N_V); - Build_Arcs (N, State, N_States, Exprs, - Build_Bool_And (Build_Bool_Not (E), Expr), 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; - 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 - Edge_Expr := Build_Bool_Not (Edge_Expr); - if Expr = Null_Node then - Expr := Edge_Expr; - else - Expr := Build_Bool_And (Expr, Edge_Expr); - 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) return NFA - is - L, R : NFA; - begin - case Get_Kind (N) is - when N_Sequences - | N_Booleans => - -- 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)); - 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)); - return Build_Concat (L, R); - when N_Overlap_Imp_Seq => - -- S |-> P is defined as Ac(S) : A(P) - L := Build_SERE_FA (Get_Sequence (N)); - R := Build_Property_FA (Get_Property (N)); - return Build_Fusion (L, R); - when N_Log_Imp_Prop => - -- B -> P --> {B} |-> P --> Ac(B) : A(P) - L := Build_SERE_FA (Get_Left (N)); - R := Build_Property_FA (Get_Right (N)); - return Build_Fusion (L, R); - when N_And_Prop => - -- P1 && P2 --> A(P1) | A(P2) - L := Build_Property_FA (Get_Left (N)); - R := Build_Property_FA (Get_Right (N)); - 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)); - return Build_Initial_Rep (R); - when N_Abort => - R := Build_Property_FA (Get_Property (N)); - 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)); - 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); - if Optimize_Final then - pragma Debug (Check_NFA (Res)); - - Remove_Unreachable_States (Res); - Remove_Simple_Prefix (Res); - Merge_Identical_States (Res); - Merge_Edges (Res); - end if; - -- Clear the QM table. - PSL.QM.Reset; - return Res; - end Build_FA; -end PSL.Build; |