From 9c4519e0c72187f95b6a91e95564ee6a1f45efc7 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Mon, 21 Oct 2019 20:09:18 +0200 Subject: psl: add active state. --- src/psl/psl-build.adb | 60 +++++++++++++++++++++++++++++++++++------------- src/psl/psl-nfas.adb | 14 ++++++++++- src/psl/psl-nfas.ads | 4 ++++ src/psl/psl-optimize.adb | 13 ++++++++--- 4 files changed, 71 insertions(+), 20 deletions(-) (limited to 'src/psl') diff --git a/src/psl/psl-build.adb b/src/psl/psl-build.adb index 5c317d711..18262f32e 100644 --- a/src/psl/psl-build.adb +++ b/src/psl/psl-build.adb @@ -378,7 +378,9 @@ package body PSL.Build is Set_Epsilon_NFA (L, False); - if Get_First_Src_Edge (Final_L) = No_Edge then + 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 @@ -943,7 +945,26 @@ package body PSL.Build is end loop; end Build_Abort; - function Build_Property_FA (N : Node) return NFA + 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 @@ -954,37 +975,44 @@ package body PSL.Build is R := Build_SERE_FA (N); return Determinize.Determinize (R); when N_Strong => - R := Build_Property_FA (Get_Property (N)); + 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)); + 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) - L := Build_SERE_FA (Get_Sequence (N)); - R := Build_Property_FA (Get_Property (N)); - return Build_Fusion (L, R); + 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) - L := Build_SERE_FA (Get_Left (N)); - R := Build_Property_FA (Get_Right (N)); - return Build_Fusion (L, R); + 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)); - R := Build_Property_FA (Get_Right (N)); + 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)); + R := Build_Property_FA (Get_Property (N), With_Active); return Build_Initial_Rep (R); when N_Abort => - R := Build_Property_FA (Get_Property (N)); + R := Build_Property_FA (Get_Property (N), With_Active); Build_Abort (R, Get_Boolean (N)); return R; when N_Property_Instance => @@ -993,7 +1021,7 @@ package body PSL.Build is begin Decl := Get_Declaration (N); Assoc_Instance (Decl, N); - R := Build_Property_FA (Get_Property (Decl)); + R := Build_Property_FA (Get_Property (Decl), With_Active); Unassoc_Instance (Decl); return R; end; @@ -1007,7 +1035,7 @@ package body PSL.Build is use PSL.NFAs.Utils; Res : NFA; begin - Res := Build_Property_FA (N); + Res := Build_Property_FA (N, True); if Optimize_Final then pragma Debug (Check_NFA (Res)); diff --git a/src/psl/psl-nfas.adb b/src/psl/psl-nfas.adb index 1e3f55ba7..5327f993a 100644 --- a/src/psl/psl-nfas.adb +++ b/src/psl/psl-nfas.adb @@ -30,6 +30,8 @@ package body PSL.NFAs is Start : NFA_State; Final : NFA_State; + Active : NFA_State; + -- If true there is an epsilon transition between the start and -- the final state. Epsilon : Boolean; @@ -208,7 +210,7 @@ package body PSL.NFAs is -- Fill it. Nfat.Table (Res) := (First_State => No_State, Last_State => No_State, - Start => No_State, Final => No_State, + Start | Final | Active => No_State, Epsilon => False); return Res; end Create_NFA; @@ -315,6 +317,16 @@ package body PSL.NFAs is Nfat.Table (N).Final := S; end Set_Final_State; + function Get_Active_State (N : NFA) return NFA_State is + begin + return Nfat.Table (N).Active; + end Get_Active_State; + + procedure Set_Active_State (N : NFA; S : NFA_State) is + begin + Nfat.Table (N).Active := S; + end Set_Active_State; + function Get_Next_Src_Edge (N : NFA_Edge) return NFA_Edge is begin return Transt.Table (N).Next_Src; diff --git a/src/psl/psl-nfas.ads b/src/psl/psl-nfas.ads index ffcf6fd1f..ff1d53b66 100644 --- a/src/psl/psl-nfas.ads +++ b/src/psl/psl-nfas.ads @@ -59,6 +59,10 @@ package PSL.NFAs is procedure Set_Final_State (N : NFA; S : NFA_State); function Get_Final_State (N : NFA) return NFA_State; + -- Each NFA also can have an active state. + procedure Set_Active_State (N : NFA; S : NFA_State); + function Get_Active_State (N : NFA) return NFA_State; + -- Iterate on all states. function Get_First_State (N : NFA) return NFA_State; function Get_Next_State (S : NFA_State) return NFA_State; diff --git a/src/psl/psl-optimize.adb b/src/psl/psl-optimize.adb index a9391d5ae..792aaacf9 100644 --- a/src/psl/psl-optimize.adb +++ b/src/psl/psl-optimize.adb @@ -36,15 +36,15 @@ package body PSL.Optimize is procedure Remove_Unreachable_States (N : NFA) is + Start : constant NFA_State := Get_Start_State (N); + Final : constant NFA_State := Get_Final_State (N); + Active : constant NFA_State := Get_Active_State (N); Head : NFA_State; - Start, Final : NFA_State; E : NFA_Edge; S, N_S : NFA_State; begin -- Remove unreachable states, ie states that can't be reached from -- start state. - Start := Get_Start_State (N); - Final := Get_Final_State (N); Head := No_State; @@ -77,6 +77,10 @@ package body PSL.Optimize is -- Do not remove final state! -- FIXME: deconnect state? null; + elsif S = Active then + -- Do not remove the active state, so that user can see that's + -- vacuous. + null; else Remove_State (N, S); end if; @@ -115,6 +119,9 @@ package body PSL.Optimize is -- Do not remove start state! -- FIXME: deconnect state? null; + elsif S = Active then + -- The active state is not expected to be reach the final state. + null; else Remove_State (N, S); end if; -- cgit v1.2.3