From 9cbaae7b669d84213837e216d46de23408367ae0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Jan 2010 13:14:48 +0100 Subject: [PATCH] [lbtt] Let "make dvi" work on Ubuntu. * doc/lbtt.texi (The formula generation algorithm): Use op^\prime instead of op', because etex on Ubuntu hangs (an infinite loop?) on the later when texi2dvi tries to compile a dvi. --- lbtt/ChangeLog | 8 ++++++++ lbtt/doc/lbtt.texi | 12 ++++++------ 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 749b0343e..cbdc950d8 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,11 @@ +2010-01-22 Alexandre Duret-Lutz + + Let "make dvi" work on Ubuntu. + + * doc/lbtt.texi (The formula generation algorithm): Use op^\prime + instead of op', because etex on Ubuntu hangs (an infinite loop?) + on the later when texi2dvi tries to compile a dvi. + 2010-01-21 Alexandre Duret-Lutz Kill some warnings on Ubuntu. diff --git a/lbtt/doc/lbtt.texi b/lbtt/doc/lbtt.texi index 06a9fd2f6..7427c0745 100644 --- a/lbtt/doc/lbtt.texi +++ b/lbtt/doc/lbtt.texi @@ -816,7 +816,7 @@ is given by the equation @iftex @tex $$ -\it{pri}(\it{op}) / \sum_{\rm{op}' \in \{\neg, \bf{X}, \bf{F}, \bf{G}\}}\it{pri}\it(op') +\it{pri}(\it{op}) / \sum_{\rm{op}^\prime \in \{\neg, \bf{X}, \bf{F}, \bf{G}\}}\it{pri}(\it{op}^\prime) $$ @end tex @end iftex @@ -828,7 +828,7 @@ $$ where @iftex @tex -$\it{op}'$ +$\it{op}^\prime$ @end tex @end iftex @ifnottex @@ -851,7 +851,7 @@ into the formula is @iftex @tex $$ -\it{pri}(\it{op}) / \sum_{\rm{op}' \in \{\neg, \vee, \wedge, \rightarrow, \leftrightarrow, \oplus, \bf{X}, \bf{U}, \bf{W}, \bf{F}, \bf{B}, \bf{V}, \bf{M}, \bf{G}\}}\it{pri}\it(op') +\it{pri}(\it{op}) / \sum_{\rm{op}^\prime \in \{\neg, \vee, \wedge, \rightarrow, \leftrightarrow, \oplus, \bf{X}, \bf{U}, \bf{W}, \bf{F}, \bf{B}, \bf{V}, \bf{M}, \bf{G}\}}\it{pri}(\it{op}^\prime) $$ @end tex @end iftex @@ -863,7 +863,7 @@ $$ where @iftex @tex -$\it{op}'$ +$\it{op}^\prime$ @end tex @end iftex @ifnottex @@ -1743,7 +1743,7 @@ The following table illustrates the effects of the ------------------------------------------------------------- (p1 V ! p0) @r{Yes} Normal@r{/}NNF@r{:} (p1 V ! p0) - [] p0 -> <> p1 @r{Yes*} Nor@r{:} [] p0 -> <> p1 + [] p0 -> <> p1 @r{Yes*} Nor@r{:} [] p0 -> <> p1 NNF@r{:} (true U ! p0) \/ (true U p1) ! <> p0 @r{No} Nor@r{:} ! <> p0 @@ -2168,7 +2168,7 @@ encountered during testing. By default no log will be created. @cindex enabling and disabling tests @cindex tests, profiling LTL-to-B@"uchi translators This option can be used as a shorthand for disabling all B@"uchi automata -correctness tests. +correctness tests. The test report generated at the end of testing then shows only the running times of each tested LTL-to-B@"uchi translator and the sizes of the generated automata.