psl: remove start loops only in case of always.

For #2392

3 files changed, 24 insertions, 1 deletions

diff --git a/src/psl/psl-build.adb b/src/psl/psl-build.adb
index 02c4961ff..41d9a4d79 100644
--- a/src/psl/psl-build.adb
+++ b/src/psl/psl-build.adb
@@ -1061,7 +1061,9 @@ package body PSL.Build is
          pragma Debug (Check_NFA (Res));
 
          Remove_Unreachable_States (Res);
-         Remove_Simple_Prefix (Res);
+         if Has_Loop_On_Start (Res) then
+            Remove_Simple_Prefix (Res);
+         end if;
          Merge_Identical_States (Res);
          Merge_Edges (Res);
       end if;
diff --git a/src/psl/psl-optimize.adb b/src/psl/psl-optimize.adb
index a2b5fbd9e..eb9b93579 100644
--- a/src/psl/psl-optimize.adb
+++ b/src/psl/psl-optimize.adb
@@ -127,6 +127,23 @@ package body PSL.Optimize is
       end loop;
    end Remove_Unreachable_States;
 
+   function Has_Loop_On_Start (N : NFA) return Boolean
+   is
+      Start : constant NFA_State := Get_Start_State (N);
+      E : NFA_Edge;
+   begin
+      E := Get_First_Src_Edge (Start);
+      while E /= No_Edge loop
+         if Get_Edge_Dest (E) = Start
+           and then Get_Edge_Expr (E) = True_Node
+         then
+            return True;
+         end if;
+         E := Get_Next_Src_Edge (E);
+      end loop;
+      return False;
+   end Has_Loop_On_Start;
+
    procedure Remove_Simple_Prefix (N : NFA)
    is
       Start : NFA_State;
diff --git a/src/psl/psl-optimize.ads b/src/psl/psl-optimize.ads
index 819e3690b..e841ce04a 100644
--- a/src/psl/psl-optimize.ads
+++ b/src/psl/psl-optimize.ads
@@ -24,6 +24,10 @@ package PSL.Optimize is
    --  O(N) algorithm.
    procedure Remove_Unreachable_States (N : NFA);
 
+   --  Return true iff there is an edge from start to start (a loop) with
+   --  the true expression.
+   function Has_Loop_On_Start (N : NFA) return Boolean;
+
    --  Remove single prefix, ie edges to a state S that is also from start
    --  to S.
    --  O(M) algorithm.