psl: add active state.

4 files changed, 71 insertions, 20 deletions

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;