From 34f1601b9ba566f18c7ee4e7e9552c258fce1a87 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Jan 2015 23:09:24 +0100 Subject: [PATCH] ltl: rename is_X_free() into is_syntactic_stutter_invariant() and adjust it to detect siPSL formulas, as in the paper of Dax et al. (ATVA'09). For issue #51. * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc: Rename the property, and adjust its computation on siSERE. * src/ltlvisit/remove_x.cc, src/ltlvisit/simplify.cc, src/tgbaalgos/stutter.cc: Adjust to new names. * src/bin/ltlfilt.cc: Add option --syntactic-sutter-invariant. * src/ltltest/kind.test: Update tests and add some new. --- src/bin/ltlfilt.cc | 16 ++++--- src/ltlast/atomic_prop.cc | 7 ++- src/ltlast/binop.cc | 8 +++- src/ltlast/bunop.cc | 18 ++++++- src/ltlast/constant.cc | 8 ++-- src/ltlast/formula.cc | 5 +- src/ltlast/formula.hh | 12 ++--- src/ltlast/multop.cc | 99 ++++++++++++++++++++++++++++++--------- src/ltlast/unop.cc | 9 ++-- src/ltltest/kind.test | 77 ++++++++++++++++++------------ src/ltlvisit/remove_x.cc | 2 +- src/ltlvisit/simplify.cc | 8 ++-- src/tgbaalgos/stutter.cc | 2 +- 13 files changed, 185 insertions(+), 86 deletions(-) diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 286619583..f66339214 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -58,7 +58,7 @@ Exit status:\n\ #define OPT_DROP_ERRORS 2 #define OPT_NNF 3 #define OPT_LTL 4 -#define OPT_NOX 5 +#define OPT_SYNTACTIC_SI 5 #define OPT_BOOLEAN 6 #define OPT_EVENTUAL 7 #define OPT_UNIVERSAL 8 @@ -121,7 +121,6 @@ static const argp_option options[] = { 0, 0, 0, 0, "Filtering options (matching is done after transformation):", 5 }, { "ltl", OPT_LTL, 0, 0, "match only LTL formulas (no PSL operator)", 0 }, - { "nox", OPT_NOX, 0, 0, "match X-free formulas", 0 }, { "boolean", OPT_BOOLEAN, 0, 0, "match Boolean formulas", 0 }, { "eventual", OPT_EVENTUAL, 0, 0, "match pure eventualities", 0 }, { "universal", OPT_UNIVERSAL, 0, 0, "match purely universal formulas", 0 }, @@ -135,6 +134,9 @@ static const argp_option options[] = "match syntactic-recurrence formulas", 0 }, { "syntactic-persistence", OPT_SYNTACTIC_PERSISTENCE, 0, 0, "match syntactic-persistence formulas", 0 }, + { "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, 0, 0, + "match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 }, + { "nox", 0, 0, OPTION_ALIAS, 0, 0 }, { "safety", OPT_SAFETY, 0, 0, "match safety formulas (even pathological)", 0 }, { "guarantee", OPT_GUARANTEE, 0, 0, @@ -206,7 +208,6 @@ static bool boolean_to_isop = false; static bool unique = false; static bool psl = false; static bool ltl = false; -static bool nox = false; static bool invert = false; static bool boolean = false; static bool universal = false; @@ -216,6 +217,7 @@ static bool syntactic_guarantee = false; static bool syntactic_obligation = false; static bool syntactic_recurrence = false; static bool syntactic_persistence = false; +static bool syntactic_si = false; static bool safety = false; static bool guarantee = false; static bool obligation = false; @@ -349,9 +351,6 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_NNF: nnf = true; break; - case OPT_NOX: - nox = true; - break; case OPT_OBLIGATION: obligation = true; break; @@ -407,6 +406,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_SYNTACTIC_PERSISTENCE: syntactic_persistence = true; break; + case OPT_SYNTACTIC_SI: + syntactic_si = true; + break; case OPT_UNIVERSAL: universal = true; break; @@ -558,7 +560,6 @@ namespace matched &= !ltl || f->is_ltl_formula(); matched &= !psl || f->is_psl_formula(); - matched &= !nox || f->is_X_free(); matched &= !boolean || f->is_boolean(); matched &= !universal || f->is_universal(); matched &= !eventual || f->is_eventual(); @@ -567,6 +568,7 @@ namespace matched &= !syntactic_obligation || f->is_syntactic_obligation(); matched &= !syntactic_recurrence || f->is_syntactic_recurrence(); matched &= !syntactic_persistence || f->is_syntactic_persistence(); + matched &= !syntactic_si || f->is_syntactic_stutter_invariant(); matched &= !ap || atomic_prop_collect(f)->size() == ap_n; if (matched && (size_min > 0 || size_max >= 0)) diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 8c8775bf4..c4ad4b034 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -38,7 +38,10 @@ namespace spot is.boolean = true; is.sugar_free_boolean = true; is.in_nenoform = true; - is.X_free = 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.sugar_free_ltl = true; is.ltl_formula = true; is.eltl_formula = true; diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 3e6723172..30edb26c8 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -132,6 +132,8 @@ namespace spot } assert(first->is_sere_formula()); assert(second->is_psl_formula()); + if (first->is_boolean()) + is.syntactic_si = false; break; case UConcat: is.not_marked = true; @@ -158,6 +160,8 @@ namespace spot } assert(first->is_sere_formula()); assert(second->is_psl_formula()); + if (first->is_boolean()) + is.syntactic_si = false; break; case U: is.not_marked = true; diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 1c147c0e4..fb6b724d4 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -57,14 +57,28 @@ namespace spot { case Star: if (max_ == unbounded) - is.finite = false; + { + is.finite = false; + is.syntactic_si = min_ == 1 && child->is_boolean(); + } + else + { + is.syntactic_si = false; + } if (min_ == 0) is.accepting_eword = true; break; case FStar: is.accepting_eword = false; if (max_ == unbounded) - is.finite = false; + { + is.finite = false; + is.syntactic_si &= !child->is_boolean(); + } + else + { + is.syntactic_si = false; + } break; } } diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index a74ee08a1..57fde76e6 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -43,7 +43,7 @@ namespace spot is.boolean = true; is.sugar_free_boolean = true; is.in_nenoform = true; - is.X_free = true; + is.syntactic_si = true; // for LTL (not PSL) is.sugar_free_ltl = true; is.ltl_formula = true; is.eltl_formula = true; @@ -64,7 +64,7 @@ namespace spot is.boolean = false; is.sugar_free_boolean = false; is.in_nenoform = true; - is.X_free = true; + is.syntactic_si = true; is.sugar_free_ltl = true; is.ltl_formula = false; is.eltl_formula = false; diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index fbae5fe01..52ab7b8b4 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -39,7 +39,8 @@ namespace spot proprint(is_boolean, "B", "Boolean formula"); \ proprint(is_sugar_free_boolean, "&", "without Boolean sugar"); \ proprint(is_in_nenoform, "!", "in negative normal form"); \ - proprint(is_X_free, "x", "without X operator"); \ + proprint(is_syntactic_stutter_invariant, "x", \ + "syntactic stutter invariant"); \ proprint(is_sugar_free_ltl, "f", "without LTL sugar"); \ proprint(is_ltl_formula, "L", "LTL formula"); \ proprint(is_eltl_formula, "E", "ELTL formula"); \ diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 943f7ac3b..b7903e193 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // // This file is part of Spot, a model checking library. @@ -153,10 +153,10 @@ namespace spot return is.in_nenoform; } - /// Whether the formula avoids the X operator. - bool is_X_free() const + /// Whether the formula is syntactically stutter_invariant + bool is_syntactic_stutter_invariant() const { - return is.X_free; + return is.syntactic_si; } /// Whether the formula avoids the F and G operators. @@ -337,7 +337,7 @@ namespace spot bool boolean:1; // No temporal operators. bool sugar_free_boolean:1; // Only AND, OR, and NOT operators. bool in_nenoform:1; // Negative Normal Form. - bool X_free:1; // No X operators. + bool syntactic_si:1; // LTL-X or siPSL bool sugar_free_ltl:1; // No F and G operators. bool ltl_formula:1; // Only LTL operators. bool eltl_formula:1; // Only ELTL operators. diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index ae63baa5c..4c3f80b4b 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -50,34 +50,61 @@ namespace spot case Concat: case AndNLM: case AndRat: - // Note: AndNLM(p1,p2) and AndRat(p1,p2) are Boolean - // formulae, but there are actually rewritten as And(p1,p2) - // by trivial identities before this constructor is called. - // So at this point, AndNLM/AndRat are always used with at - // most one Boolean argument, and the result is therefore - // NOT Boolean. - is.boolean = false; - is.ltl_formula = false; - is.eltl_formula = false; - is.psl_formula = false; - is.eventual = false; - is.universal = false; + { + bool syntactic_si = is.syntactic_si && !is.boolean; + // Note: AndNLM(p1,p2) and AndRat(p1,p2) are Boolean + // formulae, but they are actually rewritten as And(p1,p2) + // by trivial identities before this constructor is called. + // So at this point, AndNLM/AndRat are always used with at + // most one Boolean argument, and the result is therefore + // NOT Boolean. + is.boolean = false; + is.ltl_formula = false; + is.eltl_formula = false; + is.psl_formula = false; + is.eventual = false; + is.universal = false; + + for (unsigned i = 1; i < s; ++i) + { + syntactic_si &= (*v)[i]->is_syntactic_stutter_invariant() + && !(*v)[i]->is_boolean(); + props &= (*v)[i]->get_props(); + } + is.syntactic_si = syntactic_si; + break; + } case And: for (unsigned i = 1; i < s; ++i) props &= (*v)[i]->get_props(); break; case OrRat: - // Note: OrRat(p1,p2) is a Boolean formula, but its is - // actually rewritten as Or(p1,p2) by trivial identities - // before this constructor is called. So at this point, - // AndNLM is always used with at most one Boolean argument, - // and the result is therefore NOT Boolean. - is.boolean = false; - is.ltl_formula = false; - is.eltl_formula = false; - is.psl_formula = false; - is.eventual = false; - is.universal = false; + { + bool syntactic_si = is.syntactic_si && !is.boolean; + // Note: OrRat(p1,p2) is a Boolean formula, but its is + // actually rewritten as Or(p1,p2) by trivial identities + // before this constructor is called. So at this point, + // AndNLM is always used with at most one Boolean argument, + // and the result is therefore NOT Boolean. + is.boolean = false; + is.ltl_formula = false; + is.eltl_formula = false; + is.psl_formula = false; + is.eventual = false; + is.universal = false; + + bool ew = (*v)[0]->accepts_eword(); + for (unsigned i = 1; i < s; ++i) + { + ew |= (*v)[i]->accepts_eword(); + syntactic_si &= (*v)[i]->is_syntactic_stutter_invariant() + && !(*v)[i]->is_boolean(); + props &= (*v)[i]->get_props(); + } + is.accepting_eword = ew; + is.syntactic_si = syntactic_si; + break; + } case Or: { bool ew = (*v)[0]->accepts_eword(); @@ -90,6 +117,32 @@ namespace spot break; } } + // 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 + // !is_boolean()); + if (op == Concat) + { + unsigned sb = 0; // stared Boolean formulas seen + for (unsigned i = 0; i < s; ++i) + { + if ((*v)[i]->is_syntactic_stutter_invariant() + && !(*v)[i]->is_boolean()) + continue; + if (const bunop* b = is_Star((*v)[i])) + { + sb += b->child()->is_boolean(); + if (sb > 1) + break; + } + else + { + sb = 0; + break; + } + } + is.syntactic_si = sb == 1; + } } multop::~multop() diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index f2b46e877..208916b0b 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -58,7 +58,7 @@ namespace spot case X: is.not_marked = true; is.boolean = false; - is.X_free = false; + is.syntactic_si = false; is.eltl_formula = false; is.sere_formula = false; // is.syntactic_safety inherited @@ -112,6 +112,8 @@ namespace spot is.syntactic_recurrence = true; is.syntactic_persistence = true; is.accepting_eword = false; + assert(child->is_sere_formula()); + assert(!child->is_boolean()); break; case Closure: is.not_marked = true; @@ -127,6 +129,7 @@ namespace spot is.syntactic_persistence = true; is.accepting_eword = false; assert(child->is_sere_formula()); + assert(!child->is_boolean()); break; } } diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index 241589971..8d1d78812 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -59,32 +59,47 @@ check '(Ga|Fc) -> Fb' 'xLPopr' check '(Ga|Fa) -> Gb' 'xLPopr' check '{a;c*;b}|->!Xb' '&fPsopr' check '{a;c*;b}|->X!b' '&!fPsopr' -check '{a;c*;b}|->!Fb' '&xPsopr' -check '{a;c*;b}|->G!b' '&!xPsopr' -check '{a;c*;b}|->!Gb' '&xPr' -check '{a;c*;b}|->F!b' '&!xPr' -check '{a;c*;b}|->GFa' '&!xPr' -check '{a;c*;b}|->FGa' '&!xP' +check '{a;c*;b}|->!Fb' '&Psopr' +check '{a;c*;b}|->G!b' '&!Psopr' +check '{a;c*;b}|->!Gb' '&Pr' +check '{a;c*;b}|->F!b' '&!Pr' +check '{a;c*;b}|->GFa' '&!Pr' +check '{a;c*;b}|->FGa' '&!P' +check '{a[+];c[+];b*}|->!Fb' '&xPsopr' +check '{a[+];c*;b[+]}|->G!b' '&!xPsopr' +check '{a*;c[+];b[+]}|->!Gb' '&xPr' +check '{a[+];c*;b[+]}|->F!b' '&!xPr' +check '{a[+];c[+];b*}|->GFa' '&!xPr' +check '{a*;c[+];b[+]}|->FGa' '&!xP' check '{a;c;b|(d;e)}|->!Xb' '&fPFsgopr' check '{a;c;b|(d;e)}|->X!b' '&!fPFsgopr' -check '{a;c;b|(d;e)}|->!Fb' '&xPsopr' -check '{a;c;b|(d;e)}|->G!b' '&!xPsopr' -check '{a;c;b|(d;e)}|->!Gb' '&xPgopr' -check '{a;c;b|(d;e)}|->F!b' '&!xPgopr' -check '{a;c;b|(d;e)}|->GFa' '&!xPr' -check '{a;c;b|(d;e)}|->FGa' '&!xPp' -check '{a;c*;b}<>->!Gb' '&xPgopr' -check '{a;c*;b}<>->F!b' '&!xPgopr' -check '{a;c*;b}<>->FGb' '&!xPp' -check '{a;c*;b}<>->!GFb' '&xPp' -check '{a;c*;b}<>->GFb' '&!xP' -check '{a;c*;b}<>->!FGb' '&xP' -check '{a;c|d;b}<>->!Gb' '&xPgopr' -check '{a;c|d;b}<>->G!b' '&!xPsopr' -check '{a;c|d;b}<>->FGb' '&!xPp' -check '{a;c|d;b}<>->!GFb' '&xPp' -check '{a;c|d;b}<>->GFb' '&!xPr' -check '{a;c|d;b}<>->!FGb' '&xPr' +check '{a;c;b|(d;e)}|->!Fb' '&Psopr' +check '{a;c;b|(d;e)}|->G!b' '&!Psopr' +check '{a;c;b|(d;e)}|->!Gb' '&Pgopr' +check '{a;c;b|(d;e)}|->F!b' '&!Pgopr' +check '{a;c;b|(d;e)}|->GFa' '&!Pr' +check '{a;c;b|(d;e)}|->FGa' '&!Pp' +check '{a[+] && c[+]}|->!Xb' '&fPsopr' +check '{a[+] && c[+]}|->X!b' '&!fPsopr' +check '{a[+] && c[+]}|->!Fb' '&xPsopr' +check '{a[+] && c[+]}|->G!b' '&!xPsopr' +check '{a[+] && c[+]}|->!Gb' '&xPr' +check '{a[+] && c[+]}|->F!b' '&!xPr' +check '{a[+] && c[+]}|->GFa' '&!xPr' +check '{a[+] && c[+]}|->FGa' '&!xP' +check '{a;c*;b}<>->!Gb' '&Pgopr' +check '{a;c*;b}<>->F!b' '&!Pgopr' +check '{a;c*;b}<>->FGb' '&!Pp' +check '{a;c*;b}<>->!GFb' '&Pp' +check '{a;c*;b}<>->GFb' '&!P' +check '{a;c*;b}<>->!FGb' '&P' +check '{a*;c[+];b[+]}<>->!FGb' '&xP' +check '{a;c|d;b}<>->!Gb' '&Pgopr' +check '{a;c|d;b}<>->G!b' '&!Psopr' +check '{a;c|d;b}<>->FGb' '&!Pp' +check '{a;c|d;b}<>->!GFb' '&Pp' +check '{a;c|d;b}<>->GFb' '&!Pr' +check '{a;c|d;b}<>->!FGb' '&Pr' check '{a:b:c:d}!' 'B&!xfLEPSFsgopr' # Equivalent to a&b&c&d check 'a&b&c&d' 'B&!xfLEPSFsgopr' check '(Xa <-> XXXc) U (b & Fe)' 'LPgopr' @@ -110,11 +125,15 @@ check 'FGa W FGb' '&!xLPeu' check 'Ga W FGb' '&!xLPup' check 'Ga W b' '&!xLPsopr' check 'Fa M b' '&!xLPgopr' -check '{a;b*;c}' '&!xfPsopr' -check '{a;b*;c}!' '&!xfPgopr' -check '!{a;b*;c}!' '&xfPsopr' # The negative normal form is {a;b*;c}[]->0 -check '{a;b*;c}[]->0' '&!xfPsopr' -check '!{a;b*;c}' '&!xfPgopr' +check '{a;b*;c}' '&!fPsopr' +check '{a;b*;c}!' '&!fPgopr' +check '!{a;b*;c}!' '&fPsopr' # The negative normal form is {a;b*;c}[]->0 +check '{a;b*;c}[]->0' '&!fPsopr' +check '!{a;b*;c}' '&!fPgopr' +check '!{a[+];b*;c[+]}' '&!xfPgopr' +check '{a[+];b*;c[+]}' '&!xfPsopr' +check '{a[+] && b || c[+]}' '&!fPsopr' +check '{a[+] && b[+] || c[+]}' '&!xfPsopr' run 0 ../consterm '1' run 0 ../consterm '0' diff --git a/src/ltlvisit/remove_x.cc b/src/ltlvisit/remove_x.cc index 6b1c6221c..4ce91c6da 100644 --- a/src/ltlvisit/remove_x.cc +++ b/src/ltlvisit/remove_x.cc @@ -104,7 +104,7 @@ namespace spot virtual const formula* recurse(const formula* f) { - if (f->is_X_free()) + if (f->is_syntactic_stutter_invariant()) return f->clone(); f->accept(*this); return this->result(); diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index d9945599b..a3e24042a 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -2805,7 +2805,7 @@ namespace spot // a & (Xa U b) = b M a // a & (b | X(b R a)) = b R a // a & (b | X(b M a)) = b M a - if (!mo->is_X_free()) + if (!mo->is_syntactic_stutter_invariant()) // Skip if no X. { typedef std::unordered_set> fset_t; @@ -2825,7 +2825,7 @@ namespace spot { if (!(*res)[n]) continue; - if ((*res)[n]->is_X_free()) + if ((*res)[n]->is_syntactic_stutter_invariant()) continue; const formula* xarg = is_XWU((*res)[n]); @@ -3530,7 +3530,7 @@ namespace spot // a | (Xa M b) = b U a // a | (b & X(b W a)) = b W a // a | (b & X(b U a)) = b U a - if (!mo->is_X_free()) + if (!mo->is_syntactic_stutter_invariant()) // Skip if no X { typedef std::unordered_set> fset_t; @@ -3551,7 +3551,7 @@ namespace spot { if (!(*res)[n]) continue; - if ((*res)[n]->is_X_free()) + if ((*res)[n]->is_syntactic_stutter_invariant()) continue; const formula* xarg = is_XRM((*res)[n]); diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc index 0ba0593fb..d92227fbc 100644 --- a/src/tgbaalgos/stutter.cc +++ b/src/tgbaalgos/stutter.cc @@ -517,7 +517,7 @@ namespace spot bool is_stutter_invariant(const ltl::formula* f) { - if (f->is_ltl_formula() && f->is_X_free()) + if (f->is_ltl_formula() && f->is_syntactic_stutter_invariant()) return true; int algo = default_stutter_check_algorithm();