tl: new PSL trivial simplifications

Always rewrite {[*]}[]->0 as 0, and {[*]}<>->1 = 1.  Fixes #572.

* spot/tl/formula.cc: Implement them.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/equals.test: Test those.

NEWS

@@ -89,6 +89,11 @@ New in spot 2.11.6.dev  (not yet released)
     - b:b[*i..j] = b[*max(i,1)..j]
     - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1, j+l-1]
 
+  - The following new trivial simplifications have been implemented
+    for PSL operators:
+    - {[*]}[]->0 = 0
+    - {[*]}<>->1 = 1
+
   - The HOA parser is a bit smarter when merging multiple initial
     states into a single initial state (Spot's automaton class
     supports only one): it now reuses the edges leaving initial states

doc/tl/tl.tex

@@ -998,6 +998,8 @@ formula $b$, the following rewritings are systematically performed
 & \nsere{b} &\equiv \NOT b\\
   \sere{r}\Asuffix \1&\equiv \1
 & \sere{r}\Esuffix \0&\equiv \0  \\
+  \sere{\STAR{}} \Asuffix \0 &\equiv \0
+& \sere{\STAR{}} \Esuffix \1 &\equiv \1 \\
 \end{align*}
 
 \chapter{Grammar}

spot/tl/formula.cc

@@ -1163,6 +1163,7 @@ namespace spot
         //   - 1 <>-> Exp = Exp
         //   - [*0] <>-> Exp = 0
         //   - Exp <>-> 0 = 0
+        //   - [*] <>-> 1 = 1
         //   - boolExp <>-> Exp = boolExp & Exp
         if (first->is_tt())
           return second;
@@ -1172,7 +1173,7 @@ namespace spot
             second->destroy();
             return ff();
           }
-        if (second->is_ff())
+        if (second->is_ff() || (second->is_tt() && first == one_star()))
           {
             first->destroy();
             return second;
@@ -1185,6 +1186,7 @@ namespace spot
         //   - 1 []-> Exp = Exp
         //   - [*0] []-> Exp = 1
         //   - Exp []-> 1 = 1
+        //   - [*] []-> 0 = 0
         //   - boolExp []-> Exp = !boolExp | Exp
         if (first->is_tt())
           return second;
@@ -1194,7 +1196,7 @@ namespace spot
             second->destroy();
             return tt();
           }
-        if (second->is_tt())
+        if (second->is_tt() || (second->is_ff() && first == one_star()))
           {
             first->destroy();
             return second;

tests/core/equals.test

@@ -55,6 +55,8 @@ GGGGGx, Gx
 !!!!!x, !x
 {[*0];x}<>->1, {x}<>->1
 {x;[*0]}<>->1, {x}<>-> 1
+{[*]}[]->0, 0
+{[*]}<>->1, 1
 {[*0];x;[*0];[*0]}<>->1, {x}<>->1
 {[*0];x;[*0];x;[*0]}<>->1, {x;x}<>->1
 {x;x;x;[*0];x;x}<>->1, {x;x;x;x;x}<>->1