Commit 89792597 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 653ffceb
......@@ -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:
......
// -*- 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;
}
......
#! /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
......
#! /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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment