alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

from-ltlf: never output strong_X

Browse source 
* spot/tl/ltlf.cc: Here.
* tests/core/ltlfilt.test: Adjust test case.
This commit is contained in:
Alexandre Duret-Lutz 2019-09-24 10:34:04 +02:00
parent 98a8b891a1
commit 4378745458
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/tl/ltlf.cc
View file

@ -30,6 +30,8 @@ namespace spot
switch (auto o = f.kind()) switch (auto o = f.kind())
{ {
case op::strong_X: case op::strong_X:
o = op::X;
SPOT_FALLTHROUGH;
case op::F: case op::F:
return formula::unop(o, formula::And({alive, t(f[0])})); return formula::unop(o, formula::And({alive, t(f[0])}));
case op::X: // weak case op::X: // weak

4
tests/core/ltlfilt.test
View file

@ -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) al & F(a & al & !X(a | !al) & X(!al | b)) & (al U G!al)
a & al & (b | c) & (al U G!al) a & al & (b | c) & (al U G!al)
0 0
al & ((a & b) U (al & !X[!]al)) & (al U G!al) al & ((a & b) U (al & !Xal)) & (al U G!al)
EOF EOF
checkopt --ltl --from-ltlf='!dead' <<EOF checkopt --ltl --from-ltlf='!dead' <<EOF
@ -350,7 +350,7 @@ checkopt --ltl --from-ltlf='!dead' <<EOF
!dead & F(a & !dead & !X(a | dead) & X(b | dead)) & (!dead U Gdead) !dead & F(a & !dead & !X(a | dead) & X(b | dead)) & (!dead U Gdead)
a & !dead & (b | c) & (!dead U Gdead) a & !dead & (b | c) & (!dead U Gdead)
0 0
!dead & ((a & b) U (!dead & !X[!]!dead)) & (!dead U Gdead) !dead & ((a & b) U (!dead & !X!dead)) & (!dead U Gdead)
EOF EOF
cat >in <<EOF cat >in <<EOF