diff --git a/NEWS b/NEWS index dd6e6071f..2e796f6ff 100644 --- a/NEWS +++ b/NEWS @@ -56,6 +56,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: diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 5d2bba518..36397d2d4 100644 --- a/spot/tl/formula.cc +++ b/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 - // term is not stared will be regarded - // as not stuttering were this - // matters.) + is_.syntactic_si = true; // Assuming LTL (for PSL, a Boolean + // term that is not stared will be regarded as non-SI where + // this 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 - // Boolean, and the other operands are siSERE (i.e., - // sub-formulas that verify is_syntactic_stutter_invariant() and + // A concatenation is an siSERE if looks like + // r;b* or b*;r + // 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() - && !ci->is_boolean()) - continue; - if (ci->is(op::Star)) + if (ci->is_Kleene_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; } diff --git a/tests/core/kind.test b/tests/core/kind.test index 416eb0c1d..a7b859d97 100755 --- a/tests/core/kind.test +++ b/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[+]}|->G!b,&!xPsopra -{a*;c[+];b[+]}|->!Gb,&xPra -{a[+];c*;b[+]}|->F!b,&!xPra -{a[+];c[+];b*}|->GFa,&!xPra -{a*;c[+];b[+]}|->FGa,&!xPa +{a[+];c[+];b*}|->!Fb,&Psopra +{a*;c[+];b*}|->!Fb,&xPsopra +{a[+];c*;b[+]}|->G!b,&!Psopra +{a*;c[+];b[+]}|->!Gb,&Pra +{a[+];c*;b[+]}|->F!b,&!Pra +{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[+]},&!xfPsopra +!{a[+];b*;c[+]},&!fPgopra +!{a[+];b*;c*},&!xfPgopra +{a[+];b*;c[+]},&!fPsopra {a[+] && b || c[+]},&!fPsopra {a[+] && b[+] || c[+]},&!xfPsopra {p[+]:p[+]},&!xfPsoprla diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index d4d2092d5..998b5ab1a 100755 --- a/tests/core/ltlfilt.test +++ b/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 < 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 < b +{a[*];{!a}[+];a[*]}[]-> b +{a[+];{!a}[*];a[*]}[]-> b +{a[*];{!a}[*];a[+]}[]-> b EOF checkopt --simplify <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 < 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 < 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 < 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 < 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 < 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 < b +{a[->2..3]}[]-> b +{a[*];{!c}[+];a[+]}[]-> b EOF checkopt --equivalent-to 'GFa | FGb' <