From 474fe803aaf12ccc03099f616de142038a88adce Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Wed, 15 Mar 2023 07:44:06 +0100 Subject: psl: remove start loops only in case of always. For #2392 --- src/psl/psl-build.adb | 4 +++- src/psl/psl-optimize.adb | 17 +++++++++++++++++ src/psl/psl-optimize.ads | 4 ++++ 3 files changed, 24 insertions(+), 1 deletion(-) (limited to 'src') 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. -- cgit v1.2.3