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

ltlf: ensure alive holds initially

Browse source 
Reported by Shufang Zhu.

* spot/tl/ltlf.cc, spot/tl/ltlf.hh: Fix the transltion
and update the comments.
* tests/core/ltlfilt.test: Adjust test cases.
* NEWS: Mention the fix.
* THANKS: Add Shufang Zhu.
This commit is contained in:
Alexandre Duret-Lutz 2016-12-09 21:37:15 +01:00
parent 0ab8dc06c4
commit 413eab1d32
5 changed files with 31 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -28,6 +28,9 @@ New in spot 2.2.1.dev (Not yet released)
spot/misc/mspool.hh, spot/twaalgos/emptiness_stats.hh) were not
self-contained.
* ltlfilt --from-ltlf should ensure that "alive" holds initially in
order to reject empty traces.
New in spot 2.2.1 (2016-11-21)
Bug fix:

1
THANKS
View file

@ -29,6 +29,7 @@ Nikos Gorogiannis
Reuben Rowe
Rüdiger Ehlers
Silien Hong
Shufang Zhu
Sonali Dutta
Tomáš Babiak
Valentin Iovene

6
spot/tl/ltlf.cc
View file

@ -37,6 +37,10 @@ namespace spot
// the IJCAI'13 paper by De Giacomo & Vardi has a typo.
// t(a U b) should be equal to t(a) U t(b & alive).
// This typo is fixed in the Memocode'14 paper by Dutta & Vardi.
//
// (However beware that the translation given in the
// Memocode'14 paper forgets to ensure that alive holds
// initially, as required in the IJCAI'13 paper.)
case op::U:
return formula::U(t(f[0]), formula::And({alive, t(f[1])}));
case op::R:
@ -60,7 +64,7 @@ namespace spot
auto al = ((*alive == '!')
? formula::Not(formula::ap(alive + 1))
: formula::ap(alive));
return formula::And({from_ltlf_aux(f, al),
return formula::And({from_ltlf_aux(f, al), al,
formula::U(al, formula::G(formula::Not(al)))});
}
}

2
spot/tl/ltlf.hh
View file

@ -35,7 +35,7 @@ namespace spot
/// finite word. The formula is rewritten to ensure that the
/// eventualities occur during the "alive" portion. For instance
/// <code>a U b</code> becomes
/// <code>(a U (b & alive))&(alive U G!alive)</code>.
/// <code>alive&(a U (b & alive))&(alive U G!alive)</code>.
///
/// The \a alive argument can be used to change the name of the
/// atomic property used to introduce. Additionally if \a alive is

42
tests/core/ltlfilt.test
View file

@ -182,30 +182,30 @@ EOF
run 0 ltlfilt --ltl formulas > formulas2
mv formulas2 formulas
checkopt --ltl --from-ltlf <<EOF
(G(!alive | F(a & alive)) | F(alive & G(!alive | b))) & (alive U G!alive)
F(alive & (G(!alive | F(a & alive)) | G(!alive | b))) & (alive U G!alive)
F(alive & ((!alive | b) W G(!alive | F(a & alive)))) & (alive U G!alive)
(G(!alive | F(a & alive)) | G(!alive | b)) & (alive U G!alive)
((!alive | b) W G(!alive | F(a & alive))) & (alive U G!alive)
(a U (alive & F(alive & b))) & (alive U G!alive)
G(!alive | (a & X(alive & b))) & (alive U G!alive)
X(a & alive) & (alive U G!alive)
F(a & alive & !X(a & alive) & X(alive & b)) & (alive U G!alive)
a & (b | c) & (alive U G!alive)
checkopt --ltl --from-ltlf=al <<EOF
al & (G(!al | F(a & al)) | F(al & G(!al | b))) & (al U G!al)
al & F(al & (G(!al | F(a & al)) | G(!al | b))) & (al U G!al)
al & F(al & ((!al | b) W G(!al | F(a & al)))) & (al U G!al)
al & (G(!al | F(a & al)) | G(!al | b)) & (al U G!al)
al & ((!al | b) W G(!al | F(a & al))) & (al U G!al)
al & (a U (al & F(al & b))) & (al U G!al)
al & G(!al | (a & X(al & b))) & (al U G!al)
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)
EOF
checkopt --ltl --from-ltlf='!dead' <<EOF
(G(dead | F(a & !dead)) | F(!dead & G(b | dead))) & (!dead U Gdead)
F(!dead & (G(dead | F(a & !dead)) | G(b | dead))) & (!dead U Gdead)
F(!dead & ((b | dead) W G(dead | F(a & !dead)))) & (!dead U Gdead)
(G(dead | F(a & !dead)) | G(b | dead)) & (!dead U Gdead)
((b | dead) W G(dead | F(a & !dead))) & (!dead U Gdead)
(a U (!dead & F(b & !dead))) & (!dead U Gdead)
G(dead | (a & X(b & !dead))) & (!dead U Gdead)
X(a & !dead) & (!dead U Gdead)
F(a & !dead & !X(a & !dead) & X(b & !dead)) & (!dead U Gdead)
a & (b | c) & (!dead U Gdead)
!dead & (G(dead | F(a & !dead)) | F(!dead & G(b | dead))) & (!dead U Gdead)
!dead & F(!dead & (G(dead | F(a & !dead)) | G(b | dead))) & (!dead U Gdead)
!dead & F(!dead & ((b | dead) W G(dead | F(a & !dead)))) & (!dead U Gdead)
!dead & (G(dead | F(a & !dead)) | G(b | dead)) & (!dead U Gdead)
!dead & ((b | dead) W G(dead | F(a & !dead))) & (!dead U Gdead)
!dead & (a U (!dead & F(b & !dead))) & (!dead U Gdead)
!dead & G(dead | (a & X(b & !dead))) & (!dead U Gdead)
!dead & X(a & !dead) & (!dead U Gdead)
!dead & F(a & !dead & !X(a & !dead) & X(b & !dead)) & (!dead U Gdead)
a & !dead & (b | c) & (!dead U Gdead)
EOF
cat >in <<EOF