formula: fix syntactic-SI detection for ; operator

Reported by Victor Khomenko.

* spot/tl/formula.cc: Rewrite the siPSL detection for ";".
* tests/core/ltlfilt.test: Add more tests.
* tests/core/kind.test: Adjust.
* NEWS: Mention the bug.

NEWS

@@ -10,6 +10,10 @@ New in spot 2.7.3.dev (not yet released)
     was fixed by teaching simulation-based reductions how to deal
     with such cases.
 
+  - The code for detecting syntactically stutter-invariant PSL
+    formulas was incorrectly handling the ";" operator, causing some
+    stutter-sensitive formulas to be flagged a stutter-invariant.
+
 New in spot 2.7.3 (2019-04-19)
 
   Bugs fixed:

spot/tl/formula.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -1125,10 +1125,9 @@ namespace spot
         is_.boolean = true;
         is_.sugar_free_boolean = true;
         is_.in_nenoform = true;
-        is_.syntactic_si = true;        // Assuming LTL (for PSL a Boolean
+        is_.syntactic_si = true;        // Assuming LTL (for PSL, a Boolean
-        // term is not stared will be regarded
+        // term that is not stared will be regarded as non-SI where
-        // as not stuttering were this
+        // this matters.)
-        // matters.)
         is_.sugar_free_ltl = true;
         is_.ltl_formula = true;
         is_.psl_formula = true;
@@ -1544,9 +1543,12 @@ namespace spot
           is_.syntactic_si = syntactic_si;
           if (op_ == op::Fusion)
             is_.accepting_eword = false;
-          // A concatenation is an siSERE if it contains one stared
+          // A concatenation is an siSERE if looks like
-          // Boolean, and the other operands are siSERE (i.e.,
+          //    r;b*  or  b*;r
-          // sub-formulas that verify is_syntactic_stutter_invariant() and
+          // where b is Boolean and r is siSERE.  generalized to n-ary
+          // concatenation, it means all arguments should be of the
+          // form b*, except one that is siSERE (i.e., a sub-formula
+          // that verify is_syntactic_stutter_invariant() and
           // !is_boolean());
           if (op_ == op::Concat)
             {
@@ -1554,22 +1556,18 @@ namespace spot
               for (unsigned i = 0; i < s; ++i)
                 {
                   auto ci = children[i];
-                  if (ci->is_syntactic_stutter_invariant()
+                  if (ci->is_Kleene_star())
-                      && !ci->is_boolean())
-                    continue;
-                  if (ci->is(op::Star))
                     {
                       sb += ci->nth(0)->is_boolean();
-                      if (sb > 1)
-                        break;
                     }
-                  else
+                  else if (!ci->is_syntactic_stutter_invariant()
+                           || ci->is_boolean())
                     {
                       sb = 0;
                       break;
                     }
                 }
-              is_.syntactic_si = sb == 1;
+              is_.syntactic_si = sb == s - 1;
             }
           break;
         }

tests/core/kind.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2010, 2011, 2012, 2015, 2017 Laboratoire de Recherche
+# Copyright (C) 2010-2012, 2015, 2017, 2019 Laboratoire de Recherche
 # et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -59,12 +59,13 @@ Fa -> Gb,xLPsopra
 {a;c*;b}|->F!b,&!Pra
 {a;c*;b}|->GFa,&!Pra
 {a;c*;b}|->FGa,&!Pa
-{a[+];c[+];b*}|->!Fb,&xPsopra
+{a[+];c[+];b*}|->!Fb,&Psopra
-{a[+];c*;b[+]}|->G!b,&!xPsopra
+{a*;c[+];b*}|->!Fb,&xPsopra
-{a*;c[+];b[+]}|->!Gb,&xPra
+{a[+];c*;b[+]}|->G!b,&!Psopra
-{a[+];c*;b[+]}|->F!b,&!xPra
+{a*;c[+];b[+]}|->!Gb,&Pra
-{a[+];c[+];b*}|->GFa,&!xPra
+{a[+];c*;b[+]}|->F!b,&!Pra
-{a*;c[+];b[+]}|->FGa,&!xPa
+{a[+];c[+];b*}|->GFa,&!Pra
+{a*;c[+];b[+]}|->FGa,&!Pa
 {a;c;b|(d;e)}|->!Xb,&fPFsgopra
 {a;c;b|(d;e)}|->X!b,&!fPFsgopra
 {a;c;b|(d;e)}|->!Fb,&Psopra
@@ -87,7 +88,7 @@ Fa -> Gb,xLPsopra
 {a;c*;b}<>->!GFb,&Ppa
 {a;c*;b}<>->GFb,&!Pa
 {a;c*;b}<>->!FGb,&Pa
-{a*;c[+];b[+]}<>->!FGb,&xPa
+{a*;c[+];b[+]}<>->!FGb,&Pa
 {a;c|d;b}<>->!Gb,&Pgopra
 {a;c|d;b}<>->G!b,&!Psopra
 {a;c|d;b}<>->FGb,&!Ppa
@@ -126,8 +127,9 @@ Fa  M b,&!xLPgopra
 !{a;b*;c}!,&fPsopra
 {a;b*;p112}[]->0,&!fPsopra
 !{a;b*;c.2},&!fPgopr
-!{a[+];b*;c[+]},&!xfPgopra
+!{a[+];b*;c[+]},&!fPgopra
-{a[+];b*;c[+]},&!xfPsopra
+!{a[+];b*;c*},&!xfPgopra
+{a[+];b*;c[+]},&!fPsopra
 {a[+] && b || c[+]},&!fPsopra
 {a[+] && b[+] || c[+]},&!xfPsopra
 {p[+]:p[+]},&!xfPsoprla

tests/core/ltlfilt.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013-2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2013-2019 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -29,7 +29,7 @@ checkopt()
 {
   cat >exp
   run 0 ltlfilt "$@" formulas > out
-  diff exp out
+  diff -u exp out
 }
 
 # The empty lines in the file are meant, we want to make sure that
@@ -48,6 +48,16 @@ G(a & Xb)
 Xa
 F(a & !Xa & Xb)
 {a & {b|c} }
+
+{a[=2:3]}|->b
+{a[->2:3]}|->b
+{a[->1];a*}|->b  /* becomes {(!a)*;a[+]}|->b */
+{a*;(!a)*;a*}|->b
+{a*;(!a)[+];a*}|->b
+{a[+];(!a)*;a*}|->b
+{a*;(!a)*;a[+]}|->b
+{a*;(!a)[+];a[+]}|->b
+{a*;(!c)[+];a[+]}|->b
 EOF
 
 checkopt --boolean <<EOF
@@ -99,10 +109,30 @@ b W GFa
 a U Fb
 F(a & !Xa & Xb)
 a & (b | c)
+{{!a}[*];a[+]}[]-> b
+{a[*];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[+];a[*]}[]-> b
+{a[+];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[*];a[+]}[]-> b
+{a[*];{!a}[+];a[+]}[]-> b
 EOF
 
 checkopt -c --stutter-invariant <<EOF
-9
+15
+EOF
+
+checkopt --syntactic-stutter-invariant <<EOF
+GFa | FGb
+F(GFa | Gb)
+F(b W GFa)
+GFa | Gb
+b W GFa
+a U Fb
+a & (b | c)
+{{!a}[*];a[+]}[]-> b
+{a[*];{!a}[+];a[*]}[]-> b
+{a[+];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[*];a[+]}[]-> b
 EOF
 
 checkopt --simplify <<EOF
@@ -118,6 +148,15 @@ G(a & Xb)
 Xa
 F(a & X(!a & b))
 a & (b | c)
+a R (!a | X({a[->1..2]}[]-> (b & X(b W a))))
+a R (!a | X({a[->1..2]}[]-> b))
+a R (b W !a)
+{a[*];{!a}[*];a[*]}[]-> b
+!a R ((b & X(b W !a)) W a)
+(b & X((b W !a) & ((b & X(b W !a)) W a))) W !a
+!a R (a R (b W !a))
+!a R (a | X(a R (b W !a)))
+!a R (c | X(c R (b W !a)))
 EOF
 
 checkopt --simplify --eventual --unique <<EOF
@@ -142,6 +181,15 @@ checkopt --safety <<EOF
 G(a & Xb)
 Xa
 a & (b | c)
+{a[=2..3]}[]-> b
+{a[->2..3]}[]-> b
+{{!a}[*];a[+]}[]-> b
+{a[*];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[+];a[*]}[]-> b
+{a[+];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[*];a[+]}[]-> b
+{a[*];{!a}[+];a[+]}[]-> b
+{a[*];{!c}[+];a[+]}[]-> b
 EOF
 
 checkopt --obligation <<EOF
@@ -152,6 +200,15 @@ G(a & Xb)
 Xa
 F(a & !Xa & Xb)
 a & (b | c)
+{a[=2..3]}[]-> b
+{a[->2..3]}[]-> b
+{{!a}[*];a[+]}[]-> b
+{a[*];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[+];a[*]}[]-> b
+{a[+];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[*];a[+]}[]-> b
+{a[*];{!a}[+];a[+]}[]-> b
+{a[*];{!c}[+];a[+]}[]-> b
 EOF
 
 checkopt --guarantee <<EOF
@@ -165,6 +222,15 @@ EOF
 checkopt -v --ltl <<EOF
 !({a;b[*];c}!)
 !{a:b[*]:c}
+{a[=2..3]}[]-> b
+{a[->2..3]}[]-> b
+{{!a}[*];a[+]}[]-> b
+{a[*];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[+];a[*]}[]-> b
+{a[+];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[*];a[+]}[]-> b
+{a[*];{!a}[+];a[+]}[]-> b
+{a[*];{!c}[+];a[+]}[]-> b
 EOF
 
 checkopt -v --ap=3 <<EOF
@@ -177,6 +243,14 @@ a U Fb
 G(a & Xb)
 Xa
 F(a & !Xa & Xb)
+{a[=2..3]}[]-> b
+{a[->2..3]}[]-> b
+{{!a}[*];a[+]}[]-> b
+{a[*];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[+];a[*]}[]-> b
+{a[+];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[*];a[+]}[]-> b
+{a[*];{!a}[+];a[+]}[]-> b
 EOF
 
 checkopt --ap=2..3 <<EOF
@@ -191,12 +265,24 @@ a U Fb
 G(a & Xb)
 F(a & !Xa & Xb)
 a & (b | c)
+{a[=2..3]}[]-> b
+{a[->2..3]}[]-> b
+{{!a}[*];a[+]}[]-> b
+{a[*];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[+];a[*]}[]-> b
+{a[+];{!a}[*];a[*]}[]-> b
+{a[*];{!a}[*];a[+]}[]-> b
+{a[*];{!a}[+];a[+]}[]-> b
+{a[*];{!c}[+];a[+]}[]-> b
 EOF
 
 checkopt -v --stutter-invariant <<EOF
 !({a;b[*];c}!)
 G(a & Xb)
 Xa
+{a[=2..3]}[]-> b
+{a[->2..3]}[]-> b
+{a[*];{!c}[+];a[+]}[]-> b
 EOF
 
 checkopt --equivalent-to 'GFa | FGb' <<EOF