diff --git a/spot/tl/ltlf.cc b/spot/tl/ltlf.cc index 7a07a3b2b..8e9d3d64c 100644 --- a/spot/tl/ltlf.cc +++ b/spot/tl/ltlf.cc @@ -30,6 +30,8 @@ namespace spot switch (auto o = f.kind()) { case op::strong_X: + o = op::X; + SPOT_FALLTHROUGH; case op::F: return formula::unop(o, formula::And({alive, t(f[0])})); case op::X: // weak diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index dd8f85a65..3d79695c7 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -335,7 +335,7 @@ al & X(a | !al) & (al U G!al) al & F(a & al & !X(a | !al) & X(!al | b)) & (al U G!al) a & al & (b | c) & (al U G!al) 0 -al & ((a & b) U (al & !X[!]al)) & (al U G!al) +al & ((a & b) U (al & !Xal)) & (al U G!al) EOF checkopt --ltl --from-ltlf='!dead' <in <