From cc66aff6342c52d14cfc1b38022888f5b3dc7499 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Mar 2010 10:48:35 +0100 Subject: [PATCH] * bench/ltl2tgba/formulae.ltl: Fix three formulae to match the original paper by Somenzi and Bloem. Reported by Ruediger Ehlers. --- ChangeLog | 5 +++++ bench/ltl2tgba/formulae.ltl | 6 +++--- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/ChangeLog b/ChangeLog index 18f3fbb66..a56f31706 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,8 @@ +2010-03-06 Alexandre Duret-Lutz + + * 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 Fix memory leak introduced in yesterday's change. diff --git a/bench/ltl2tgba/formulae.ltl b/bench/ltl2tgba/formulae.ltl index 59af12813..bd8036772 100644 --- a/bench/ltl2tgba/formulae.ltl +++ b/bench/ltl2tgba/formulae.ltl @@ -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