diff --git a/NEWS b/NEWS index 3509f9e3c..7d026bea7 100644 --- a/NEWS +++ b/NEWS @@ -17,6 +17,8 @@ New in spot 1.2.3a (not yet released) - Fix three incorrect simplifications rules, all related to the factorization of Boolean subformulas in operands of the non-length-matching "&" SERE operator. + - Fix incorrect translation of the fusion operator (":") in SERE + such as {xx;1}:yy[*] where the left operand has 1 as tail. New in spot 1.2.3 (2014-02-11) diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 65338f1cd..cfa5de45c 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -348,6 +348,8 @@ for x in ../reduccmp ../reductaustr; do run 0 $x '{s[*]}<>->b' 'b M s' run 0 $x '{s[+]}<>->b' 'b M s' run 0 $x '{s[*2..]}<>->b' 's & X(b M s)' + run 0 $x '{1:a*}!' 'a' + run 0 $x '{(1;1):a*}!' 'Xa' run 0 $x '{a;b*;c;d*}<>->e' 'a & X(b U (c & (e | X(e M d))))' run 0 $x '{a:b*:c:d*}<>->e' 'a & ((c & (e M d)) M b)' run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)' diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index bde8ec011..a972cb12c 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // Coopératifs (SRC), Université Pierre et Marie Curie. @@ -912,11 +912,12 @@ namespace spot } - if (dest->kind() != formula::Constant) + // If the destination is not 0 or [*0], it means it + // can have successors. Fusion the tail and append + // anything to concatenate. + if (dest->kind() != formula::Constant + || dest == ltl::constant::true_instance()) { - // If the destination is not a constant, it - // means it can have successors. Fusion the - // tail and append anything to concatenate. const formula* dest2 = multop::instance(multop::Fusion, dest, tail->clone()); if (to_concat_)