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

* bench/ltl2tgba/formulae.ltl: Fix three formulae to match the

Browse source 
original paper by Somenzi and Bloem.  Reported by Ruediger Ehlers.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-06 10:48:35 +01:00
parent 975045a4e6
commit cc66aff634
2 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2010-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* bench/ltl2tgba/formulae.ltl: Fix three formulae to match the
original paper by Somenzi and Bloem. Reported by Ruediger Ehlers.
2010-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix memory leak introduced in yesterday's change.

6
bench/ltl2tgba/formulae.ltl
View file

@ -6,7 +6,7 @@ U U t p0 V f p1
U V f p0 p1
& & U t U t p0 V f ! p0 & U t p0 V f V f ! p0
& V f U t p0 U t V f ! p1
& & V f U t p0 U t V f ! p1 & V f U t p1 U t V f ! p0
| & V f U t p0 U t V f ! p1 & V f U t p1 U t V f ! p0
V p0 | p0 p1
| U X p0 X p1 X V ! p0 ! p1
| U X p0 p1 X V ! p0 | ! p0 ! p1
@ -20,8 +20,8 @@ V f & U t p0 U t p1
V & X p1 p2 X U V U p3 p0 p2 V p3 p2
| | & V f | p1 V f U t p0 V f | p2 V f U t ! p0 V f p1 V f p2
| | & V f | p1 U t V f p0 V f | p2 U t V f ! p0 V f p1 V f p2
& & | U t & ! p1 U t V f ! p0 U t & ! p2 U t V f p0 U t p1 U t p2
& & | U t & ! p1 V f U t ! p0 U t & ! p2 V f U t p0 U t p1 U t p2
& & | U t & ! p1 U t V f ! p0 U t & ! p2 U t V f p0 U t ! p1 U t ! p2
& & | U t & ! p1 V f U t ! p0 U t & ! p2 V f U t p0 U t ! p1 U t ! p2
& V f | p1 X V f p0 V f | p2 X V f ! p0
V f | p1 & X p0 X ! p0
| U p0 p0 U p1 p0