1-- PSL - NFA builder. 2-- Copyright (C) 2002-2016 Tristan Gingold 3-- 4-- This program is free software: you can redistribute it and/or modify 5-- it under the terms of the GNU General Public License as published by 6-- the Free Software Foundation, either version 2 of the License, or 7-- (at your option) any later version. 8-- 9-- This program is distributed in the hope that it will be useful, 10-- but WITHOUT ANY WARRANTY; without even the implied warranty of 11-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 12-- GNU General Public License for more details. 13-- 14-- You should have received a copy of the GNU General Public License 15-- along with this program. If not, see <gnu.org/licenses>. 16 17with Tables; 18with Ada.Text_IO; use Ada.Text_IO; 19with Types; use Types; 20with PSL.Types; use PSL.Types; 21with PSL.Errors; use PSL.Errors; 22with PSL.CSE; use PSL.CSE; 23with PSL.QM; 24with PSL.Disp_NFAs; use PSL.Disp_NFAs; 25with PSL.Optimize; use PSL.Optimize; 26with PSL.NFAs.Utils; 27with PSL.Prints; 28with PSL.NFAs; use PSL.NFAs; 29 30package body PSL.Build is 31 package Intersection is 32 function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA; 33 end Intersection; 34 35 package body Intersection is 36 37 type Stack_Entry_Id is new Natural; 38 No_Stack_Entry : constant Stack_Entry_Id := 0; 39 type Stack_Entry is record 40 L, R : NFA_State; 41 Res : NFA_State; 42 Next_Unhandled : Stack_Entry_Id; 43 end record; 44 45 package Stackt is new Tables 46 (Table_Component_Type => Stack_Entry, 47 Table_Index_Type => Stack_Entry_Id, 48 Table_Low_Bound => 1, 49 Table_Initial => 128); 50 51 First_Unhandled : Stack_Entry_Id; 52 53 procedure Init_Stack is 54 begin 55 Stackt.Init; 56 First_Unhandled := No_Stack_Entry; 57 end Init_Stack; 58 59 function Not_Empty return Boolean is 60 begin 61 return First_Unhandled /= No_Stack_Entry; 62 end Not_Empty; 63 64 procedure Pop_State (L, R : out NFA_State) is 65 begin 66 L := Stackt.Table (First_Unhandled).L; 67 R := Stackt.Table (First_Unhandled).R; 68 First_Unhandled := Stackt.Table (First_Unhandled).Next_Unhandled; 69 end Pop_State; 70 71 function Get_State (N : NFA; L, R : NFA_State) return NFA_State 72 is 73 Res : NFA_State; 74 begin 75 for I in Stackt.First .. Stackt.Last loop 76 if Stackt.Table (I).L = L 77 and then Stackt.Table (I).R = R 78 then 79 return Stackt.Table (I).Res; 80 end if; 81 end loop; 82 Res := Add_State (N); 83 Stackt.Append ((L => L, R => R, Res => Res, 84 Next_Unhandled => First_Unhandled)); 85 First_Unhandled := Stackt.Last; 86 return Res; 87 end Get_State; 88 89 function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA 90 is 91 Start_L, Start_R : NFA_State; 92 Final_L, Final_R : NFA_State; 93 S_L, S_R : NFA_State; 94 E_L, E_R : NFA_Edge; 95 Res : NFA; 96 Start : NFA_State; 97 Extra_L, Extra_R : NFA_Edge; 98 T : Node; 99 begin 100 Start_L := Get_Start_State (L); 101 Start_R := Get_Start_State (R); 102 Final_R := Get_Final_State (R); 103 Final_L := Get_Final_State (L); 104 105 if False then 106 Disp_Body (L); 107 Disp_Body (R); 108 Put ("//start state: "); 109 Disp_State (Start_L); 110 Put (","); 111 Disp_State (Start_R); 112 New_Line; 113 end if; 114 115 if Match_Len then 116 Extra_L := No_Edge; 117 Extra_R := No_Edge; 118 else 119 Extra_L := Add_Edge (Final_L, Final_L, True_Node); 120 Extra_R := Add_Edge (Final_R, Final_R, True_Node); 121 end if; 122 123 Res := Create_NFA; 124 Init_Stack; 125 Start := Get_State (Res, Start_L, Start_R); 126 Set_Start_State (Res, Start); 127 128 while Not_Empty loop 129 Pop_State (S_L, S_R); 130 131 if False then 132 Put ("//poped state: "); 133 Disp_State (S_L); 134 Put (","); 135 Disp_State (S_R); 136 New_Line; 137 end if; 138 139 E_L := Get_First_Src_Edge (S_L); 140 while E_L /= No_Edge loop 141 E_R := Get_First_Src_Edge (S_R); 142 while E_R /= No_Edge loop 143 if not (E_L = Extra_L and E_R = Extra_R) then 144 T := Build_Bool_And (Get_Edge_Expr (E_L), 145 Get_Edge_Expr (E_R)); 146 Add_Edge (Get_State (Res, S_L, S_R), 147 Get_State (Res, 148 Get_Edge_Dest (E_L), 149 Get_Edge_Dest (E_R)), 150 T); 151 end if; 152 E_R := Get_Next_Src_Edge (E_R); 153 end loop; 154 E_L := Get_Next_Src_Edge (E_L); 155 end loop; 156 end loop; 157 Set_Final_State (Res, Get_State (Res, Final_L, Final_R)); 158 Remove_Unreachable_States (Res); 159 160 if not Match_Len then 161 Remove_Edge (Extra_L); 162 Remove_Edge (Extra_R); 163 end if; 164 165 -- FIXME: free L and R. 166 return Res; 167 end Build_Inter; 168 end Intersection; 169 170 -- All edges from A are duplicated using B as a source. 171 -- Handle epsilon-edges. 172 procedure Duplicate_Src_Edges (N : NFA; A, B : NFA_State) 173 is 174 pragma Unreferenced (N); 175 E : NFA_Edge; 176 Expr : Node; 177 Dest : NFA_State; 178 begin 179 pragma Assert (A /= B); 180 E := Get_First_Src_Edge (A); 181 while E /= No_Edge loop 182 Expr := Get_Edge_Expr (E); 183 Dest := Get_Edge_Dest (E); 184 if Expr /= Null_Node then 185 Add_Edge (B, Dest, Expr); 186 end if; 187 E := Get_Next_Src_Edge (E); 188 end loop; 189 end Duplicate_Src_Edges; 190 191 -- All edges to A are duplicated using B as a destination. 192 -- Handle epsilon-edges. 193 procedure Duplicate_Dest_Edges (N : NFA; A, B : NFA_State) 194 is 195 pragma Unreferenced (N); 196 E : NFA_Edge; 197 Expr : Node; 198 Src : NFA_State; 199 begin 200 pragma Assert (A /= B); 201 E := Get_First_Dest_Edge (A); 202 while E /= No_Edge loop 203 Expr := Get_Edge_Expr (E); 204 Src := Get_Edge_Src (E); 205 if Expr /= Null_Node then 206 Add_Edge (Src, B, Expr); 207 end if; 208 E := Get_Next_Dest_Edge (E); 209 end loop; 210 end Duplicate_Dest_Edges; 211 212 procedure Remove_Epsilon_Edge (N : NFA; S, D : NFA_State) is 213 begin 214 if Get_First_Src_Edge (S) = No_Edge then 215 -- No edge from S. 216 -- Move edges to S to D. 217 Redest_Edges (S, D); 218 Remove_Unconnected_State (N, S); 219 if Get_Start_State (N) = S then 220 Set_Start_State (N, D); 221 end if; 222 elsif Get_First_Dest_Edge (D) = No_Edge then 223 -- No edge to D. 224 -- Move edges from D to S. 225 Resource_Edges (D, S); 226 Remove_Unconnected_State (N, D); 227 if Get_Final_State (N) = D then 228 Set_Final_State (N, S); 229 end if; 230 else 231 Duplicate_Dest_Edges (N, S, D); 232 Duplicate_Src_Edges (N, D, S); 233 Remove_Identical_Src_Edges (S); 234 end if; 235 end Remove_Epsilon_Edge; 236 237 procedure Remove_Epsilon (N : NFA; 238 E : NFA_Edge) is 239 S : constant NFA_State := Get_Edge_Src (E); 240 D : constant NFA_State := Get_Edge_Dest (E); 241 begin 242 Remove_Edge (E); 243 244 Remove_Epsilon_Edge (N, S, D); 245 end Remove_Epsilon; 246 247 function Build_Concat (L, R : NFA) return NFA 248 is 249 Start_L, Start_R : NFA_State; 250 Final_L, Final_R : NFA_State; 251 Eps_L, Eps_R : Boolean; 252 E_L, E_R : NFA_Edge; 253 begin 254 Start_L := Get_Start_State (L); 255 Start_R := Get_Start_State (R); 256 Final_R := Get_Final_State (R); 257 Final_L := Get_Final_State (L); 258 Eps_L := Get_Epsilon_NFA (L); 259 Eps_R := Get_Epsilon_NFA (R); 260 261 Merge_NFA (L, R); 262 263 Set_Start_State (L, Start_L); 264 Set_Final_State (L, Final_R); 265 Set_Epsilon_NFA (L, False); 266 267 if Eps_L then 268 E_L := Add_Edge (Start_L, Final_L, Null_Node); 269 end if; 270 271 if Eps_R then 272 E_R := Add_Edge (Start_R, Final_R, Null_Node); 273 end if; 274 275 Remove_Epsilon_Edge (L, Final_L, Start_R); 276 277 if Eps_L then 278 Remove_Epsilon (L, E_L); 279 end if; 280 if Eps_R then 281 Remove_Epsilon (L, E_R); 282 end if; 283 284 if (Start_L = Final_L or else Eps_L) 285 and then (Start_R = Final_R or else Eps_R) 286 then 287 Set_Epsilon_NFA (L, True); 288 end if; 289 290 Remove_Identical_Src_Edges (Final_L); 291 Remove_Identical_Dest_Edges (Start_R); 292 293 return L; 294 end Build_Concat; 295 296 function Build_Or (L, R : NFA) return NFA 297 is 298 Start_L, Start_R : NFA_State; 299 Final_L, Final_R : NFA_State; 300 Eps : Boolean; 301 Start, Final : NFA_State; 302 E_S_L, E_S_R, E_L_F, E_R_F : NFA_Edge; 303 begin 304 Start_L := Get_Start_State (L); 305 Start_R := Get_Start_State (R); 306 Final_R := Get_Final_State (R); 307 Final_L := Get_Final_State (L); 308 Eps := Get_Epsilon_NFA (L) or Get_Epsilon_NFA (R); 309 310 -- Optimize [*0] | R. 311 if Start_L = Final_L 312 and then Get_First_Src_Edge (Start_L) = No_Edge 313 then 314 if Start_R /= Final_R then 315 Set_Epsilon_NFA (R, True); 316 end if; 317 -- FIXME 318 -- delete_NFA (L); 319 return R; 320 end if; 321 322 Merge_NFA (L, R); 323 324 -- Use Thompson construction. 325 Start := Add_State (L); 326 Set_Start_State (L, Start); 327 E_S_L := Add_Edge (Start, Start_L, Null_Node); 328 E_S_R := Add_Edge (Start, Start_R, Null_Node); 329 330 Final := Add_State (L); 331 Set_Final_State (L, Final); 332 E_L_F := Add_Edge (Final_L, Final, Null_Node); 333 E_R_F := Add_Edge (Final_R, Final, Null_Node); 334 335 Set_Epsilon_NFA (L, Eps); 336 337 Remove_Epsilon (L, E_S_L); 338 Remove_Epsilon (L, E_S_R); 339 Remove_Epsilon (L, E_L_F); 340 Remove_Epsilon (L, E_R_F); 341 342 return L; 343 end Build_Or; 344 345 function Build_Fusion (L, R : NFA) return NFA 346 is 347 Start_R : NFA_State; 348 Final_L, Final_R, S_L : NFA_State; 349 E_L : NFA_Edge; 350 E_R : NFA_Edge; 351 N_L, Expr : Node; 352 begin 353 Start_R := Get_Start_State (R); 354 Final_R := Get_Final_State (R); 355 Final_L := Get_Final_State (L); 356 357 Merge_NFA (L, R); 358 359 E_L := Get_First_Dest_Edge (Final_L); 360 while E_L /= No_Edge loop 361 S_L := Get_Edge_Src (E_L); 362 N_L := Get_Edge_Expr (E_L); 363 364 E_R := Get_First_Src_Edge (Start_R); 365 while E_R /= No_Edge loop 366 Expr := Build_Bool_And (N_L, Get_Edge_Expr (E_R)); 367 Expr := PSL.QM.Reduce (Expr); 368 if Expr /= False_Node then 369 Add_Edge (S_L, Get_Edge_Dest (E_R), Expr); 370 end if; 371 E_R := Get_Next_Src_Edge (E_R); 372 end loop; 373 Remove_Identical_Src_Edges (S_L); 374 E_L := Get_Next_Dest_Edge (E_L); 375 end loop; 376 377 Set_Final_State (L, Final_R); 378 379 Set_Epsilon_NFA (L, False); 380 381 if Get_First_Src_Edge (Final_L) = No_Edge 382 and then Final_L /= Get_Active_State (L) 383 then 384 Remove_State (L, Final_L); 385 end if; 386 if Get_First_Dest_Edge (Start_R) = No_Edge then 387 Remove_State (L, Start_R); 388 end if; 389 390 return L; 391 end Build_Fusion; 392 393 function Build_Star_Repeat (N : Node) return NFA is 394 Res : NFA; 395 Start, Final, S : NFA_State; 396 Seq : Node; 397 begin 398 Seq := Get_Sequence (N); 399 if Seq = Null_Node then 400 -- Epsilon. 401 Res := Create_NFA; 402 S := Add_State (Res); 403 Set_Start_State (Res, S); 404 Set_Final_State (Res, S); 405 return Res; 406 end if; 407 Res := Build_SERE_FA (Seq); 408 Start := Get_Start_State (Res); 409 Final := Get_Final_State (Res); 410 Redest_Edges (Final, Start); 411 Set_Final_State (Res, Start); 412 Remove_Unconnected_State (Res, Final); 413 Set_Epsilon_NFA (Res, False); 414 return Res; 415 end Build_Star_Repeat; 416 417 function Build_Plus_Repeat (N : Node) return NFA is 418 Res : NFA; 419 Start, Final : NFA_State; 420 T : NFA_Edge; 421 begin 422 Res := Build_SERE_FA (Get_Sequence (N)); 423 Start := Get_Start_State (Res); 424 Final := Get_Final_State (Res); 425 T := Get_First_Dest_Edge (Final); 426 while T /= No_Edge loop 427 Add_Edge (Get_Edge_Src (T), Start, Get_Edge_Expr (T)); 428 T := Get_Next_Src_Edge (T); 429 end loop; 430 return Res; 431 end Build_Plus_Repeat; 432 433 -- Association actual to formals, so that when a formal is referenced, the 434 -- actual can be used instead. 435 procedure Assoc_Instance (Decl : Node; Instance : Node) 436 is 437 Formal : Node; 438 Actual : Node; 439 begin 440 -- Temporary associates actuals to formals. 441 Formal := Get_Parameter_List (Decl); 442 Actual := Get_Association_Chain (Instance); 443 while Formal /= Null_Node loop 444 if Actual = Null_Node then 445 -- Not enough actual. 446 raise Internal_Error; 447 end if; 448 if Get_Actual (Formal) /= Null_Node then 449 -- Recursion 450 raise Internal_Error; 451 end if; 452 Set_Actual (Formal, Get_Actual (Actual)); 453 Formal := Get_Chain (Formal); 454 Actual := Get_Chain (Actual); 455 end loop; 456 if Actual /= Null_Node then 457 -- Too many actual. 458 raise Internal_Error; 459 end if; 460 end Assoc_Instance; 461 462 procedure Unassoc_Instance (Decl : Node) 463 is 464 Formal : Node; 465 begin 466 -- Remove temporary association. 467 Formal := Get_Parameter_List (Decl); 468 while Formal /= Null_Node loop 469 Set_Actual (Formal, Null_Node); 470 Formal := Get_Chain (Formal); 471 end loop; 472 end Unassoc_Instance; 473 474 function Build_SERE_FA (N : Node) return NFA 475 is 476 Res : NFA; 477 S1, S2 : NFA_State; 478 begin 479 case Get_Kind (N) is 480 when N_Booleans => 481 Res := Create_NFA; 482 S1 := Add_State (Res); 483 S2 := Add_State (Res); 484 Set_Start_State (Res, S1); 485 Set_Final_State (Res, S2); 486 if N /= False_Node then 487 Add_Edge (S1, S2, N); 488 end if; 489 return Res; 490 when N_Braced_SERE => 491 return Build_SERE_FA (Get_SERE (N)); 492 when N_Concat_SERE => 493 return Build_Concat (Build_SERE_FA (Get_Left (N)), 494 Build_SERE_FA (Get_Right (N))); 495 when N_Fusion_SERE => 496 return Build_Fusion (Build_SERE_FA (Get_Left (N)), 497 Build_SERE_FA (Get_Right (N))); 498 when N_Match_And_Seq => 499 return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), 500 Build_SERE_FA (Get_Right (N)), 501 True); 502 when N_And_Seq => 503 return Intersection.Build_Inter (Build_SERE_FA (Get_Left (N)), 504 Build_SERE_FA (Get_Right (N)), 505 False); 506 when N_Or_Prop 507 | N_Or_Seq => 508 return Build_Or (Build_SERE_FA (Get_Left (N)), 509 Build_SERE_FA (Get_Right (N))); 510 when N_Star_Repeat_Seq => 511 return Build_Star_Repeat (N); 512 when N_Plus_Repeat_Seq => 513 return Build_Plus_Repeat (N); 514 when N_Sequence_Instance 515 | N_Endpoint_Instance => 516 declare 517 Decl : Node; 518 begin 519 Decl := Get_Declaration (N); 520 Assoc_Instance (Decl, N); 521 Res := Build_SERE_FA (Get_Sequence (Decl)); 522 Unassoc_Instance (Decl); 523 return Res; 524 end; 525 when N_Boolean_Parameter 526 | N_Sequence_Parameter => 527 declare 528 Actual : constant Node := Get_Actual (N); 529 begin 530 if Actual = Null_Node then 531 raise Internal_Error; 532 end if; 533 return Build_SERE_FA (Actual); 534 end; 535 when others => 536 Error_Kind ("build_sere_fa", N); 537 end case; 538 end Build_SERE_FA; 539 540 function Count_Edges (S : NFA_State) return Natural 541 is 542 Res : Natural; 543 E : NFA_Edge; 544 begin 545 Res := 0; 546 E := Get_First_Src_Edge (S); 547 while E /= No_Edge loop 548 Res := Res + 1; 549 E := Get_Next_Src_Edge (E); 550 end loop; 551 return Res; 552 end Count_Edges; 553 554 type Count_Vector is array (Natural range <>) of Natural; 555 556 procedure Count_All_Edges (N : NFA; Res : out Count_Vector) 557 is 558 S : NFA_State; 559 begin 560 S := Get_First_State (N); 561 while S /= No_State loop 562 Res (Natural (Get_State_Label (S))) := Count_Edges (S); 563 S := Get_Next_State (S); 564 end loop; 565 end Count_All_Edges; 566 567 pragma Unreferenced (Count_All_Edges); 568 569 package Determinize is 570 -- Create a new NFA that reaches its final state only when N fails 571 -- (ie when the final state is not reached). 572 function Determinize (N : NFA) return NFA; 573 end Determinize; 574 575 package body Determinize is 576 -- In all the comments N stands for the initial NFA (ie the NFA to 577 -- determinize). 578 579 use Prints; 580 581 Flag_Trace : constant Boolean := False; 582 Last_Label : Int32 := 0; 583 584 -- The tree associates a set of states in N to *an* uniq set in the 585 -- result NFA. 586 -- 587 -- As the NFA is labelized, each node represent a state in N, and has 588 -- two branches: one for state is present and one for state is absent. 589 -- 590 -- The leaves contain the state in the result NFA. 591 -- 592 -- The leaves are chained to create a stack of state to handle. 593 -- 594 -- The root of the tree is node Start_Tree_Id and represent the start 595 -- state of N. 596 type Deter_Tree_Id is new Natural; 597 No_Tree_Id : constant Deter_Tree_Id := 0; 598 Start_Tree_Id : constant Deter_Tree_Id := 1; 599 600 -- List of unhanded leaves. 601 Deter_Head : Deter_Tree_Id; 602 603 type Deter_Tree_Id_Bool_Array is array (Boolean) of Deter_Tree_Id; 604 605 -- Node in the tree. 606 type Deter_Tree_Entry is record 607 Parent : Deter_Tree_Id; 608 609 -- For non-leaf: 610 Child : Deter_Tree_Id_Bool_Array; 611 612 -- For leaf: 613 Link : Deter_Tree_Id; 614 State : NFA_State; 615 -- + value ? 616 end record; 617 618 package Detert is new Tables 619 (Table_Component_Type => Deter_Tree_Entry, 620 Table_Index_Type => Deter_Tree_Id, 621 Table_Low_Bound => 1, 622 Table_Initial => 128); 623 624 type Bool_Vector is array (Natural range <>) of Boolean; 625 pragma Pack (Bool_Vector); 626 627 -- Convert a set of states in N to a state in the result NFA. 628 -- The set is represented by a vector of boolean. An element of the 629 -- vector is true iff the corresponding state is present. 630 function Add_Vector (V : Bool_Vector; N : NFA) return NFA_State 631 is 632 E : Deter_Tree_Id; 633 Added : Boolean; 634 Res : NFA_State; 635 begin 636 E := Start_Tree_Id; 637 Added := False; 638 for I in V'Range loop 639 if Detert.Table (E).Child (V (I)) = No_Tree_Id then 640 Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), 641 Parent => E, 642 Link => No_Tree_Id, 643 State => No_State)); 644 Detert.Table (E).Child (V (I)) := Detert.Last; 645 E := Detert.Last; 646 Added := True; 647 else 648 E := Detert.Table (E).Child (V (I)); 649 Added := False; 650 end if; 651 end loop; 652 if Added then 653 -- Create the new state. 654 Res := Add_State (N); 655 Detert.Table (E).State := Res; 656 657 if Flag_Trace then 658 Set_State_Label (Res, Last_Label); 659 Put ("Result state" & Int32'Image (Last_Label) & " for"); 660 for I in V'Range loop 661 if V (I) then 662 Put (Natural'Image (I)); 663 end if; 664 end loop; 665 New_Line; 666 Last_Label := Last_Label + 1; 667 end if; 668 669 -- Put it to the list of states to be handled. 670 Detert.Table (E).Link := Deter_Head; 671 Deter_Head := E; 672 673 return Res; 674 else 675 return Detert.Table (E).State; 676 end if; 677 end Add_Vector; 678 679 -- Return true iff the stack is empty (ie all the states have been 680 -- handled). 681 function Stack_Empty return Boolean is 682 begin 683 return Deter_Head = No_Tree_Id; 684 end Stack_Empty; 685 686 -- Get an element from the stack. 687 -- Extract the state in the result NFA. 688 -- Rebuild the set of states in N (ie rebuild the vector of states). 689 procedure Stack_Pop (V : out Bool_Vector; S : out NFA_State) 690 is 691 L, P : Deter_Tree_Id; 692 begin 693 L := Deter_Head; 694 pragma Assert (L /= No_Tree_Id); 695 S := Detert.Table (L).State; 696 Deter_Head := Detert.Table (L).Link; 697 698 for I in reverse V'Range loop 699 pragma Assert (L /= Start_Tree_Id); 700 P := Detert.Table (L).Parent; 701 if L = Detert.Table (P).Child (True) then 702 V (I) := True; 703 elsif L = Detert.Table (P).Child (False) then 704 V (I) := False; 705 else 706 raise Program_Error; 707 end if; 708 L := P; 709 end loop; 710 pragma Assert (L = Start_Tree_Id); 711 end Stack_Pop; 712 713 type State_Vector is array (Natural range <>) of Natural; 714 type Expr_Vector is array (Natural range <>) of Node; 715 716 procedure Build_Arcs (N : NFA; 717 State : NFA_State; 718 States : State_Vector; 719 Exprs : Expr_Vector; 720 Expr : Node; 721 V : Bool_Vector) 722 is 723 T : Node; 724 begin 725 if Expr = False_Node then 726 return; 727 end if; 728 729 if States'Length = 0 then 730 declare 731 Reduced_Expr : constant Node := PSL.QM.Reduce (Expr); 732 --Reduced_Expr : constant Node := Expr; 733 S : NFA_State; 734 begin 735 if Reduced_Expr = False_Node then 736 return; 737 end if; 738 S := Add_Vector (V, N); 739 Add_Edge (State, S, Reduced_Expr); 740 if Flag_Trace then 741 Put (" Add edge"); 742 Put (Int32'Image (Get_State_Label (State))); 743 Put (" to"); 744 Put (Int32'Image (Get_State_Label (S))); 745 Put (", expr="); 746 Dump_Expr (Expr); 747 Put (", reduced="); 748 Dump_Expr (Reduced_Expr); 749 New_Line; 750 end if; 751 end; 752 else 753 declare 754 N_States : State_Vector renames 755 States (States'First + 1 .. States'Last); 756 N_V : Bool_Vector (V'Range) := V; 757 S : constant Natural := States (States'First); 758 E : constant Node := Exprs (S); 759 begin 760 N_V (S) := True; 761 if Expr = Null_Node then 762 Build_Arcs (N, State, N_States, Exprs, E, N_V); 763 T := Build_Bool_Not (E); 764 Build_Arcs (N, State, N_States, Exprs, T, V); 765 else 766 T := Build_Bool_And (E, Expr); 767 768 Build_Arcs (N, State, N_States, Exprs, T, N_V); 769 T := Build_Bool_Not (E); 770 T := Build_Bool_And (T, Expr); 771 Build_Arcs (N, State, N_States, Exprs, T, V); 772 end if; 773 end; 774 end if; 775 end Build_Arcs; 776 777 function Determinize_1 (N : NFA; Nbr_States : Natural) return NFA 778 is 779 Final : Natural; 780 V : Bool_Vector (0 .. Nbr_States - 1); 781 Exprs : Expr_Vector (0 .. Nbr_States - 1); 782 S : NFA_State; 783 E : NFA_Edge; 784 D : Natural; 785 Edge_Expr : Node; 786 Expr : Node; 787 Nbr_Dest : Natural; 788 States : State_Vector (0 .. Nbr_States - 1); 789 Res : NFA; 790 State : NFA_State; 791 R : Node; 792 begin 793 Final := Natural (Get_State_Label (Get_Final_State (N))); 794 795 -- FIXME: handle epsilon or final = start -> create an empty NFA. 796 797 -- Initialize the tree. 798 Res := Create_NFA; 799 Detert.Init; 800 Detert.Append ((Child => (No_Tree_Id, No_Tree_Id), 801 Parent => No_Tree_Id, 802 Link => No_Tree_Id, 803 State => No_State)); 804 pragma Assert (Detert.Last = Start_Tree_Id); 805 Deter_Head := No_Tree_Id; 806 807 -- Put the initial state in the tree and in the stack. 808 -- FIXME: ok, we know that its label is 0. 809 V := (0 => True, others => False); 810 State := Add_Vector (V, Res); 811 Set_Start_State (Res, State); 812 813 -- The failure state. As there is nothing to do with this 814 -- state, remove it from the stack. 815 V := (others => False); 816 State := Add_Vector (V, Res); 817 Set_Final_State (Res, State); 818 Stack_Pop (V, State); 819 820 -- Iterate on states in the result NFA that haven't yet been handled. 821 while not Stack_Empty loop 822 Stack_Pop (V, State); 823 824 if Flag_Trace then 825 Put_Line ("Handle result state" 826 & Int32'Image (Get_State_Label (State))); 827 end if; 828 829 -- Build edges vector. 830 Exprs := (others => Null_Node); 831 Expr := Null_Node; 832 833 S := Get_First_State (N); 834 Nbr_Dest := 0; 835 while S /= No_State loop 836 if V (Natural (Get_State_Label (S))) then 837 E := Get_First_Src_Edge (S); 838 while E /= No_Edge loop 839 D := Natural (Get_State_Label (Get_Edge_Dest (E))); 840 Edge_Expr := Get_Edge_Expr (E); 841 842 if False and Flag_Trace then 843 Put_Line (" edge" & Int32'Image (Get_State_Label (S)) 844 & " to" & Natural'Image (D)); 845 end if; 846 847 if D = Final then 848 R := Build_Bool_Not (Edge_Expr); 849 if Expr = Null_Node then 850 Expr := R; 851 else 852 Expr := Build_Bool_And (Expr, R); 853 end if; 854 else 855 if Exprs (D) = Null_Node then 856 Exprs (D) := Edge_Expr; 857 States (Nbr_Dest) := D; 858 Nbr_Dest := Nbr_Dest + 1; 859 else 860 Exprs (D) := Build_Bool_Or (Exprs (D), Edge_Expr); 861 end if; 862 end if; 863 E := Get_Next_Src_Edge (E); 864 end loop; 865 end if; 866 S := Get_Next_State (S); 867 end loop; 868 869 if Flag_Trace then 870 Put (" Final: expr="); 871 Print_Expr (Expr); 872 New_Line; 873 for I in 0 .. Nbr_Dest - 1 loop 874 Put (" Dest"); 875 Put (Natural'Image (States (I))); 876 Put (" expr="); 877 Print_Expr (Exprs (States (I))); 878 New_Line; 879 end loop; 880 end if; 881 882 -- Build arcs. 883 if not (Nbr_Dest = 0 and Expr = Null_Node) then 884 Build_Arcs (Res, State, 885 States (0 .. Nbr_Dest - 1), Exprs, Expr, 886 Bool_Vector'(0 .. Nbr_States - 1 => False)); 887 end if; 888 end loop; 889 890 --Remove_Unreachable_States (Res); 891 return Res; 892 end Determinize_1; 893 894 function Determinize (N : NFA) return NFA 895 is 896 Nbr_States : Natural; 897 begin 898 Labelize_States (N, Nbr_States); 899 900 if Flag_Trace then 901 Put_Line ("NFA to determinize:"); 902 Disp_NFA (N); 903 Last_Label := 0; 904 end if; 905 906 return Determinize_1 (N, Nbr_States); 907 end Determinize; 908 end Determinize; 909 910 function Build_Initial_Rep (N : NFA) return NFA 911 is 912 S : constant NFA_State := Get_Start_State (N); 913 begin 914 Add_Edge (S, S, True_Node); 915 return N; 916 end Build_Initial_Rep; 917 918 procedure Build_Strong (N : NFA) 919 is 920 S : NFA_State; 921 Final : constant NFA_State := Get_Final_State (N); 922 begin 923 S := Get_First_State (N); 924 while S /= No_State loop 925 -- FIXME. 926 if S /= Final then 927 Add_Edge (S, Final, EOS_Node); 928 end if; 929 S := Get_Next_State (S); 930 end loop; 931 end Build_Strong; 932 933 procedure Build_Abort (N : NFA; Expr : Node) 934 is 935 S : NFA_State; 936 E : NFA_Edge; 937 Not_Expr : Node; 938 begin 939 Not_Expr := Build_Bool_Not (Expr); 940 S := Get_First_State (N); 941 while S /= No_State loop 942 E := Get_First_Src_Edge (S); 943 while E /= No_Edge loop 944 Set_Edge_Expr (E, Build_Bool_And (Not_Expr, Get_Edge_Expr (E))); 945 E := Get_Next_Src_Edge (E); 946 end loop; 947 S := Get_Next_State (S); 948 end loop; 949 end Build_Abort; 950 951 function Build_Property_FA (N : Node; With_Active : Boolean) return NFA; 952 953 function Build_Overlap_Imp 954 (Left, Right : Node; With_Active : Boolean) return NFA 955 is 956 L, R : NFA; 957 Res : NFA; 958 begin 959 L := Build_SERE_FA (Left); 960 R := Build_Property_FA (Right, False); 961 if With_Active then 962 Set_Active_State (L, Get_Final_State (L)); 963 end if; 964 Res := Build_Fusion (L, R); 965 -- Ensure the active state is kept. 966 pragma Assert (Res = L); 967 return Res; 968 end Build_Overlap_Imp; 969 970 function Build_Property_FA (N : Node; With_Active : Boolean) return NFA 971 is 972 L, R : NFA; 973 begin 974 case Get_Kind (N) is 975 when N_Sequences 976 | N_Booleans => 977 -- Build A(S) or A(B) 978 R := Build_SERE_FA (N); 979 return Determinize.Determinize (R); 980 when N_Strong => 981 R := Build_Property_FA (Get_Property (N), False); 982 Build_Strong (R); 983 return R; 984 when N_Imp_Seq => 985 -- R |=> P --> {R; TRUE} |-> P 986 L := Build_SERE_FA (Get_Sequence (N)); 987 R := Build_Property_FA (Get_Property (N), False); 988 if With_Active then 989 declare 990 A : NFA_State; 991 begin 992 A := Add_State (L); 993 Duplicate_Dest_Edges (L, Get_Final_State (L), A); 994 Set_Active_State (L, A); 995 end; 996 end if; 997 return Build_Concat (L, R); 998 when N_Overlap_Imp_Seq => 999 -- S |-> P is defined as Ac(S) : A(P) 1000 return Build_Overlap_Imp 1001 (Get_Sequence (N), Get_Property (N), With_Active); 1002 when N_Log_Imp_Prop => 1003 -- B -> P --> {B} |-> P --> Ac(B) : A(P) 1004 return Build_Overlap_Imp 1005 (Get_Left (N), Get_Right (N), With_Active); 1006 when N_And_Prop => 1007 -- P1 && P2 --> A(P1) | A(P2) 1008 L := Build_Property_FA (Get_Left (N), False); 1009 R := Build_Property_FA (Get_Right (N), False); 1010 return Build_Or (L, R); 1011 when N_Never => 1012 R := Build_SERE_FA (Get_Property (N)); 1013 return Build_Initial_Rep (R); 1014 when N_Always => 1015 R := Build_Property_FA (Get_Property (N), With_Active); 1016 return Build_Initial_Rep (R); 1017 when N_Abort => 1018 R := Build_Property_FA (Get_Property (N), With_Active); 1019 Build_Abort (R, Get_Boolean (N)); 1020 return R; 1021 when N_Property_Instance => 1022 declare 1023 Decl : Node; 1024 begin 1025 Decl := Get_Declaration (N); 1026 Assoc_Instance (Decl, N); 1027 R := Build_Property_FA (Get_Property (Decl), With_Active); 1028 Unassoc_Instance (Decl); 1029 return R; 1030 end; 1031 when others => 1032 Error_Kind ("build_property_fa", N); 1033 end case; 1034 end Build_Property_FA; 1035 1036 function Build_FA (N : Node) return NFA 1037 is 1038 use PSL.NFAs.Utils; 1039 Res : NFA; 1040 begin 1041 Res := Build_Property_FA (N, True); 1042 if Optimize_Final then 1043 pragma Debug (Check_NFA (Res)); 1044 1045 Remove_Unreachable_States (Res); 1046 Remove_Simple_Prefix (Res); 1047 Merge_Identical_States (Res); 1048 Merge_Edges (Res); 1049 end if; 1050 -- Clear the QM table. 1051 PSL.QM.Reset; 1052 return Res; 1053 end Build_FA; 1054end PSL.Build; 1055