9cbaae7b66
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.
5166 lines
176 KiB
Text
5166 lines
176 KiB
Text
\input texinfo @c -*-texinfo-*-
|
|
@c %**start of header
|
|
@setfilename lbtt.info
|
|
@settitle @command{lbtt}
|
|
@afourpaper
|
|
@c %**end of header
|
|
|
|
@smallbook
|
|
|
|
@ifnottex
|
|
@ifhtml
|
|
@section @command{lbtt}
|
|
@end ifhtml
|
|
This file documents how to use the LTL-to-B@"uchi
|
|
translator testbench @command{lbtt}.
|
|
|
|
Copyright @copyright{} 2005 Heikki Tauriainen
|
|
@ifinfo
|
|
@email{heikki.tauriainen@@tkk.fi}
|
|
@end ifinfo
|
|
@ifnotinfo
|
|
@ifnothtml
|
|
<@email{heikki.tauriainen@@tkk.fi}>
|
|
@end ifnothtml
|
|
@end ifnotinfo
|
|
|
|
@ifhtml
|
|
@html
|
|
<blockquote>
|
|
@end html
|
|
@end ifhtml
|
|
Permission is granted to make and distribute verbatim
|
|
copies of this manual provided the copyright notice and
|
|
this permission notice are preserved on all copies.
|
|
|
|
@ignore
|
|
Permission is granted to process this file through TeX
|
|
and print the results, provided the printed document
|
|
carries a copying permission notice identical to this
|
|
one except for the removal of this paragraph (this
|
|
paragraph not being relevant to the printed manual).
|
|
|
|
@end ignore
|
|
Permission is granted to copy and distribute modified
|
|
versions of this manual under the conditions for
|
|
verbatim copying, provided also that the section
|
|
entitled ``GNU General Public License'' is included exactly
|
|
as in the original, and provided that the entire resulting
|
|
derived work is distributed under the terms of a
|
|
permission notice identical to this one.
|
|
|
|
Permission is granted to copy and distribute
|
|
translations of this manual into another language,
|
|
under the above conditions for modified versions.
|
|
@ifhtml
|
|
@html
|
|
</blockquote>
|
|
@end html
|
|
@end ifhtml
|
|
@end ifnottex
|
|
|
|
@iftex
|
|
@titlepage
|
|
@title @command{lbtt}
|
|
|
|
@subtitle LTL-to-B@"uchi Translator Testbench
|
|
@subtitle @today, @command{lbtt} Versions 1.2.x
|
|
@author Heikki Tauriainen <@email{heikki.tauriainen@@tkk.fi}>
|
|
@page
|
|
@vskip 0pt plus 1filll
|
|
Copyright @copyright{} 2005 Heikki Tauriainen
|
|
<@email{heikki.tauriainen@@tkk.fi}>
|
|
|
|
The latest version of this manual can be obtained from@*
|
|
<@url{http://www.tcs.hut.fi/Software/lbtt/}>.
|
|
|
|
Permission is granted to make and distribute verbatim
|
|
copies of this manual provided the copyright notice and
|
|
this permission notice are preserved on all copies.
|
|
|
|
Permission is granted to copy and distribute modified
|
|
versions of this manual under the conditions for
|
|
verbatim copying, provided also that the section
|
|
entitled ``GNU General Public License''
|
|
is included exactly as in the original, and provided
|
|
that the entire resulting derived work is distributed
|
|
under the terms of a permission notice identical to this
|
|
one.
|
|
|
|
Permission is granted to copy and distribute
|
|
translations of this manual into another language,
|
|
under the above conditions for modified versions.
|
|
@end titlepage
|
|
|
|
@contents
|
|
@end iftex
|
|
|
|
@ifnottex
|
|
@node Top, Copying, , (dir)
|
|
@top @command{lbtt}
|
|
|
|
@command{lbtt} is a tool for testing implementations of algorithms
|
|
for translating propositional linear temporal logic formulas into
|
|
B@"uchi automata.
|
|
|
|
This is edition 1.2.0 of the @command{lbtt} documentation. This edition
|
|
applies to @command{lbtt} versions 1.2.x.
|
|
|
|
@command{lbtt} is free software, you may change and redistribute it
|
|
under the terms of the GNU General Public License. @command{lbtt}
|
|
comes with NO WARRANTY. See @ref{Copying} for details.
|
|
|
|
@menu
|
|
* Copying:: GNU General Public License.
|
|
|
|
* Overview:: A short introduction to @command{lbtt}.
|
|
* Test methods:: Description of the tests @command{lbtt}
|
|
performs.
|
|
|
|
* Invocation:: How to run the program.
|
|
* Interpreting the output:: Explanation of @command{lbtt}'s output messages.
|
|
* Analyzing test results:: Working with @command{lbtt}'s internal
|
|
commands.
|
|
|
|
* Interfacing with lbtt:: Interfacing LTL-to-B@"uchi translators
|
|
with @command{lbtt}.
|
|
|
|
* References:: List of references.
|
|
|
|
* Definitions:: A reference of the formal definitions of
|
|
the various objects that @command{lbtt}
|
|
manipulates.
|
|
|
|
* Configuration file option index::
|
|
* Command line option index::
|
|
* User command index::
|
|
* Concept index::
|
|
@end menu
|
|
@end ifnottex
|
|
|
|
|
|
@node Copying, Overview, Top, Top
|
|
@include gpl.texi
|
|
|
|
|
|
|
|
@node Overview, Test methods, Copying, Top
|
|
@chapter Overview
|
|
|
|
@cindex model checking
|
|
@command{lbtt} is a tool for testing programs that translate
|
|
formulas expressed in propositional linear temporal logic (@dfn{LTL}) into
|
|
B@"uchi automata. These finite-state automata over infinite words are
|
|
used e.g.@: in automata-theoretic model checking
|
|
@ifnottex
|
|
@ref{[VW86]},
|
|
@ref{[Var96]},
|
|
@end ifnottex
|
|
@iftex
|
|
[VW86, Var96],
|
|
@end iftex
|
|
where they can help in detecting errors in the specifications of finite-state
|
|
hardware or software systems. Usually the model checking procedure involves
|
|
first composing an
|
|
automaton with a formal model of a given system, and the result of the
|
|
composition reveals whether any computation path of the system violates
|
|
some property that the automaton represents.
|
|
(For an introduction to model checking techniques in general, see,
|
|
for example,
|
|
@ifnottex
|
|
@ref{[CGP99]}.)
|
|
@end ifnottex
|
|
@iftex
|
|
[CGP99].)
|
|
@end iftex
|
|
|
|
The property to be model checked can be specified as an
|
|
LTL formula, and the B@"uchi automaton used for model checking is obtained
|
|
automatically from the formula with a translation algorithm.
|
|
(For descriptions and optimization techniques for such algorithms, see the
|
|
references, for example,
|
|
@ifnottex
|
|
@ref{[VW86]},
|
|
@ref{[Isl94]},
|
|
@ref{[GPVW95]},
|
|
@ref{[Cou99]}
|
|
@ref{[DGV99]},
|
|
@ref{[Ete99]},
|
|
@ref{[SB00]},
|
|
@ref{[EH00]},
|
|
@ref{[EWS01]},
|
|
@ref{[GO01]},
|
|
@ref{[Gei01]},
|
|
@ref{[Sch01]},
|
|
@ref{[Wol01]},
|
|
@ref{[Ete02]},
|
|
@ref{[GL02]},
|
|
@ref{[GSB02]},
|
|
@ref{[Thi02]},
|
|
@ref{[Fri03]},
|
|
@ref{[GO03]},
|
|
@ref{[Lat03]},
|
|
@ref{[ST03]}.)
|
|
@end ifnottex
|
|
@iftex
|
|
[VW86, Isl94, GPVW95, Cou99, DGV99, Ete99, SB00, EH00, EWS01, GO01,
|
|
Gei01, Sch01, Wol01, Ete02, GL02, GSB02, Thi02, Fri03, GO03, Lat03, ST03].)
|
|
@end iftex
|
|
In practice, ensuring the correctness of the implementation of such a
|
|
translation algorithm is crucial to guarantee the soundness of the
|
|
implementation of a model checking procedure.
|
|
|
|
The goal of @command{lbtt} is to assist implementing LTL-to-B@"uchi
|
|
translation algorithms correctly by providing an automated
|
|
testing environment for LTL-to-B@"uchi translators. Testing consists of running
|
|
LTL-to-B@"uchi translators on randomly generated (or user-specified) LTL
|
|
formulas as input and then performing simple consistency checks on the
|
|
resulting automata to test whether the translators seem to function correctly
|
|
in practice. (See
|
|
@ifnottex
|
|
@ref{[TH02]}
|
|
@end ifnottex
|
|
@iftex
|
|
[TH02]
|
|
@end iftex
|
|
for more information on the theory behind the testing methods.) If the test
|
|
results suggest that there is an error in an implementation,
|
|
@command{lbtt} can generate sample data which causes
|
|
a test failure and which may also be useful for debugging the
|
|
implementation.
|
|
|
|
Additionally, the testing environment can be used for very basic profiling of
|
|
different LTL-to-B@"uchi translators to evaluate their performance.
|
|
|
|
@noindent
|
|
@emph{Note: although @command{lbtt} might be able to detect inconsistent
|
|
behavior in an LTL-to-B@"uchi translator, it is only a testing tool and is
|
|
therefore incapable of formally proving any translation algorithm
|
|
implementation to be correct. Therefore, the test results should never be used
|
|
as the sole basis for any formal conclusions about the correctness of an
|
|
implementation.
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
@node Test methods, Invocation, Overview, Top
|
|
@chapter Test methods
|
|
|
|
This chapter describes the algorithms @command{lbtt} uses for generating
|
|
input for the tests and introduces some terminology.
|
|
A short description of each test is also included
|
|
together with the outline of @command{lbtt}'s testing procedure. However, the
|
|
chapter is not intended to be a thorough introduction to the theoretical
|
|
background of the different tests; see, for example,
|
|
@ifnottex
|
|
@ref{[TH02]}
|
|
@end ifnottex
|
|
@iftex
|
|
[TH02]
|
|
@end iftex
|
|
or
|
|
@ifnottex
|
|
@ref{[Tau00]}
|
|
@end ifnottex
|
|
@iftex
|
|
[Tau00]
|
|
@end iftex
|
|
for more information.
|
|
|
|
@menu
|
|
* Random input generation:: How @command{lbtt} generates input for the
|
|
tests.
|
|
* Testing procedure:: Outline of @command{lbtt}'s testing
|
|
procedure.
|
|
* Model checking result cross-comparison test::
|
|
Model checking the same LTL formula in
|
|
a fixed state space using different
|
|
LTL-to-B@"uchi translators should
|
|
give the same model checking result.
|
|
* Model checking result consistency check::
|
|
Model checking two complementary LTL
|
|
formulas in the same state space using
|
|
an LTL-to-B@"uchi translator should
|
|
give consistent results.
|
|
* Automata intersection emptiness check::
|
|
The intersection of the languages
|
|
accepted by two B@"uchi automata
|
|
constructed from two complementary
|
|
LTL formulas should be empty.
|
|
@end menu
|
|
|
|
|
|
|
|
@node Random input generation, Testing procedure, Test methods, Test methods
|
|
@section Random input generation
|
|
|
|
By default, all tests @command{lbtt} makes are based on randomly generated
|
|
input. However, the LTL formulas used as input for the LTL-to-B@"uchi
|
|
translators can be optionally given by the user by telling @command{lbtt} to
|
|
read LTL formulas from a file or from standard input
|
|
(@pxref{--formulafile,,@samp{--formulafile} command line option}).
|
|
|
|
@cindex state space
|
|
Additionally, some of the tests make use of randomly generated
|
|
``state spaces'', which are basically directed labeled graphs with labels on
|
|
nodes with the additional requirement of having at least one arc leaving
|
|
each node. The label of each node is a subset of a finite collection of atomic
|
|
propositions
|
|
@cindex atomic proposition
|
|
(an uninterpreted set of assertions which may or may not hold in a
|
|
state), which occur also in the LTL formulas used in the tests.
|
|
|
|
The following sections describe how @command{lbtt} generates input for the
|
|
tests and list the parameters which can be used to adjust the behavior of
|
|
the input generation algorithms.
|
|
|
|
@menu
|
|
* Random LTL formulas:: How @command{lbtt} generates random
|
|
LTL formulas.
|
|
* Random state spaces:: How @command{lbtt} generates random
|
|
state spaces.
|
|
@end menu
|
|
|
|
|
|
|
|
@node Random LTL formulas, Random state spaces, Random input generation, Random input generation
|
|
@subsection Random LTL formulas
|
|
|
|
@cindex random LTL formula
|
|
@cindex LTL formula, random
|
|
|
|
The LTL formulas used by @command{lbtt} are built from
|
|
atomic propositions (with names of the form
|
|
@ifhtml
|
|
@samp{p}@var{n}
|
|
@end ifhtml
|
|
@ifnothtml
|
|
@samp{p@var{n}}
|
|
@end ifnothtml
|
|
for some nonnegative integer @var{n}), the Boolean constants
|
|
@ifnottex
|
|
@samp{true} and @samp{false},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\sc{True}
|
|
@end tex
|
|
and
|
|
@tex
|
|
\sc{False},
|
|
@end tex
|
|
@end iftex
|
|
and logical or temporal operators. @command{lbtt} supports the
|
|
following logical operators:
|
|
|
|
@cindex supported LTL formula operators
|
|
@cindex LTL formula operators, supported
|
|
@itemize @bullet
|
|
@item
|
|
@cindex @samp{\/} (LTL formula operator)
|
|
@cindex @emph{or} (LTL formula operator)
|
|
@cindex disjunction (LTL formula operator)
|
|
logical disjunction
|
|
@iftex
|
|
(@tex
|
|
$\vee$
|
|
@end tex
|
|
--- @samp{\/} as shown in output messages),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{\/} as shown in output messages),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{/\} (LTL formula operator)
|
|
@cindex @emph{and} (LTL formula operator)
|
|
@cindex conjunction (LTL formula operator)
|
|
logical conjunction
|
|
@iftex
|
|
(@tex
|
|
$\wedge$
|
|
@end tex
|
|
--- @samp{/\}),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{/\}),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{!} (LTL formula operator)
|
|
@cindex @emph{not} (LTL formula operator)
|
|
@cindex negation (LTL formula operator)
|
|
logical negation
|
|
@iftex
|
|
(@tex
|
|
$\neg$
|
|
@end tex
|
|
--- @samp{!}),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{!}),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{->} (LTL formula operator)
|
|
@cindex implication (LTL formula operator)
|
|
logical implication
|
|
@iftex
|
|
(@tex
|
|
$\rightarrow$
|
|
@end tex
|
|
--- @samp{->})
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{->})
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{<->} (LTL formula operator)
|
|
@cindex equivalence (LTL formula operator)
|
|
logical equivalence
|
|
@iftex
|
|
(@tex
|
|
$\leftrightarrow$
|
|
@end tex
|
|
--- @samp{<->})
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{<->})
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{xor} (LTL formula operator)
|
|
@cindex exclusive or (LTL formula operator)
|
|
logical ``exclusive or''
|
|
@iftex
|
|
(@tex
|
|
$\oplus$
|
|
@end tex
|
|
--- @samp{xor})
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{xor})
|
|
@end ifnottex
|
|
|
|
@end itemize
|
|
|
|
@noindent
|
|
and the following temporal operators:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
@cindex @samp{X} (LTL formula operator)
|
|
@cindex next time (LTL formula operator)
|
|
``Next time''
|
|
@iftex
|
|
(@tex
|
|
$\bf{X}$
|
|
@end tex
|
|
--- @samp{X}),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{X}),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{U} (LTL formula operator)
|
|
@cindex until (LTL formula operator)
|
|
@cindex strong until (LTL formula operator)
|
|
``(Strong) Until''
|
|
@iftex
|
|
(@tex
|
|
$\bf{U}$
|
|
@end tex
|
|
--- @samp{U}),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{U}),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{W} (LTL formula operator)
|
|
@cindex weak until (LTL formula operator)
|
|
@cindex unless (LTL formula operator)
|
|
``Weak Until'' (also known as ``Unless'')
|
|
@iftex
|
|
(@tex
|
|
$\bf{W}$
|
|
@end tex
|
|
--- @samp{W}),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{W}),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{F} (LTL formula operator)
|
|
@cindex finally (LTL formula operator)
|
|
@cindex eventually (LTL formula operator)
|
|
``Finally'' (``Eventually'')
|
|
@iftex
|
|
(@tex
|
|
$\bf{F}$
|
|
@end tex
|
|
--- @samp{<>})
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{<>})
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{B} (LTL formula operator)
|
|
@cindex before (LTL formula operator)
|
|
``Before''
|
|
@iftex
|
|
(@tex
|
|
$\bf{B}$
|
|
@end tex
|
|
--- @samp{B})
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{B})
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{V} (LTL formula operator)
|
|
@cindex release (LTL formula operator)
|
|
@cindex weak release (LTL formula operator)
|
|
``(Weak) Release'', the dual of ``(Strong) Until''
|
|
@iftex
|
|
(@tex
|
|
$\bf{V}$
|
|
@end tex
|
|
--- @samp{V}),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{V}),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{M} (LTL formula operator)
|
|
@cindex strong release (LTL formula operator)
|
|
``Strong Release'', the dual of ``Weak Until''
|
|
@iftex
|
|
(@tex
|
|
$\bf{M}$
|
|
@end tex
|
|
--- @samp{M}),
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{M}),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{G} (LTL formula operator)
|
|
@cindex globally (LTL formula operator)
|
|
@cindex always (LTL formula operator)
|
|
@cindex henceforth (LTL formula operator)
|
|
``Globally'' (``Always'', ``Henceforth'')
|
|
@iftex
|
|
(@tex
|
|
$\bf{G}$
|
|
@end tex
|
|
--- @samp{[]}).
|
|
@end iftex
|
|
@ifnottex
|
|
(@samp{[]}).
|
|
@end ifnottex
|
|
|
|
@end itemize
|
|
|
|
@noindent
|
|
See @ref{LTL formulas}, for a reference on the exact semantics of these
|
|
operators.
|
|
|
|
@cindex parameters for random LTL formula generation algorithm
|
|
@cindex random LTL formula, parameters for generation algorithm
|
|
@cindex LTL formula, parameters for generation algorithm
|
|
The behavior of @command{lbtt}'s random formula generation algorithm can be
|
|
adjusted with the following parameters:
|
|
|
|
@itemize @bullet
|
|
|
|
@item
|
|
@cindex LTL formula, size
|
|
@cindex formula size
|
|
@cindex random LTL formula, size
|
|
Number of nodes in the parse tree of a formula (i.e., the total number of
|
|
occurrences of propositions, Boolean constants and operators in the formula).
|
|
|
|
@item
|
|
Number of different atomic propositions that can be used for generating a
|
|
formula. (Note that this does not restrict the total number of atomic
|
|
propositions in the formula, nor the number of occurrences of any individual
|
|
proposition. However, none of the generated formulas will have more than this
|
|
number of @emph{different} atomic propositions.)
|
|
|
|
@item
|
|
@cindex priorities for formula constants, atomic propositions and operators
|
|
@cindex constants, priorities for
|
|
@cindex atomic propositions, priorities for
|
|
@cindex operators, priorities for
|
|
Priorities for the Boolean constants and atomic propositions. The priority of
|
|
a symbol determines the relative likelihood of its occurrence in a generated
|
|
formula. The higher the priority of a symbol, the more likely it is that the
|
|
symbol will occur (with respect to the other symbols) in a generated formula; a
|
|
zero priority will exclude the symbol altogether.
|
|
|
|
@item
|
|
Priorities for the logical and temporal operators.
|
|
|
|
@end itemize
|
|
|
|
@noindent
|
|
Note that the priorities for atomic symbols (Boolean constants and atomic
|
|
propositions) and the priorities of the logical and temporal operators are
|
|
independent, i.e., changing the priority of an atomic symbol does not affect
|
|
the likelihood of the occurrence of any logical or temporal operator and vice
|
|
versa.
|
|
|
|
@ifnottex
|
|
For further details, see @ref{The formula generation algorithm} for a
|
|
pseudocode description of the algorithm used for generating random LTL
|
|
formulas.
|
|
@end ifnottex
|
|
|
|
@node The formula generation algorithm, , Random LTL formulas, Random LTL formulas
|
|
|
|
@subsubsection The formula generation algorithm
|
|
@cindex random LTL formula, generation algorithm
|
|
@cindex LTL formula, generation algorithm
|
|
|
|
@command{lbtt} uses an algorithm similar to the one outlined in
|
|
@ifnottex
|
|
@ref{[DGV99]}
|
|
@end ifnottex
|
|
@iftex
|
|
[DGV99]
|
|
@end iftex
|
|
for generating random LTL formulas. The algorithm can be described in
|
|
pseudocode as follows:
|
|
|
|
@smallexample
|
|
@r{1} function RandomFormula(@var{n} : Integer) : LtlFormula;
|
|
@r{2} if @var{n} = 1 then begin
|
|
@r{3} @var{p} := @r{random atomic proposition or} @r{TRUE} @r{or} @r{FALSE};
|
|
@r{4} return @var{p};
|
|
@r{5} end
|
|
@r{6} else if @var{n} = 2 then begin
|
|
@r{7} @var{op} := @r{random unary operator};
|
|
@r{8} @var{f} := RandomFormula(1);
|
|
@r{9} return @var{op} @var{f};
|
|
@r{10} end
|
|
@r{11} else begin
|
|
@r{12} @var{op} := @r{random unary or binary operator};
|
|
@r{13} if @var{op} @r{is a unary operator} then begin
|
|
@r{14} @var{f} := RandomFormula(@var{n}-1);
|
|
@r{15} return @var{op} @var{f};
|
|
@r{16} end
|
|
@r{17} else begin
|
|
@r{18} @var{x} := @r{random integer in the interval} [1,@var{n}-2];
|
|
@r{19} @var{f1} := RandomFormula(@var{x});
|
|
@r{20} @var{f2} := RandomFormula(@var{n}-@var{x}-1);
|
|
@r{21} return (@var{f1} @var{op} @var{f2});
|
|
@r{22} end;
|
|
@r{23} end;
|
|
@r{24} end;
|
|
@end smallexample
|
|
|
|
Each invocation of the algorithm returns an LTL formula with @var{n}
|
|
nodes in the formula parse tree. The behavior of the algorithm can be adjusted
|
|
by giving values for the parameters @var{n} (the number of nodes in the
|
|
formula parse tree),
|
|
@iftex
|
|
@tex
|
|
$|\it{AP}|$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{|AP|}
|
|
@end ifnottex
|
|
(the number of different atomic propositions), and
|
|
@iftex
|
|
@tex
|
|
$\it{pri}(\it{SYMBOL})$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
pri(@var{symbol})
|
|
@end ifnottex
|
|
(the priorities for the different symbols).
|
|
|
|
@cindex priorities for formula constants, atomic propositions and operators
|
|
@cindex constants, priorities for
|
|
@cindex probabilities for formula constants and atomic propositions
|
|
@cindex constants, computing probabilities for
|
|
In @command{lbtt}'s implementation of the above algorithm, the priority of a
|
|
symbol determines the probability with which the symbol is chosen
|
|
into a generated formula each time line 3, 7 or 12 of the algorithm is
|
|
executed. For Boolean constants
|
|
@ifnottex
|
|
@samp{true} and @samp{false}
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\sc{True}
|
|
@end tex
|
|
and
|
|
@tex
|
|
\sc{False}
|
|
@end tex
|
|
@end iftex
|
|
(line 3 of the algorithm), the probability is given by the equation
|
|
|
|
@ifnottex
|
|
@math{pri(@var{CONSTANT}) / (pri(AP) + pri(@samp{true}) + pri(@samp{false}))}
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\smallskip
|
|
\center{$\it{pri}(\it{CONSTANT}) / \big(\it{pri}(\it{AP}) + \it{pri}($\sc{True}$) + \it{pri}($\sc{False}$)\big)$}
|
|
\smallskip
|
|
@end tex
|
|
@end iftex
|
|
|
|
@noindent
|
|
where @var{CONSTANT} is either
|
|
@ifnottex
|
|
@samp{true} or @samp{false},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\sc{True}
|
|
@end tex
|
|
or
|
|
@tex
|
|
\sc{False},
|
|
@end tex
|
|
@end iftex
|
|
and
|
|
@ifnottex
|
|
pri(@math{AP})
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$\it{pri}(\it{AP})$
|
|
@end tex
|
|
@end iftex
|
|
is the total priority of all atomic propositions.
|
|
|
|
@cindex priorities for formula constants, atomic propositions and operators
|
|
@cindex atomic propositions, priorities for
|
|
@cindex probabilities for formula constants and atomic propositions
|
|
@cindex atomic propositions, computing probabilities for
|
|
The probability of choosing a particular atomic proposition into a formula
|
|
(line 3) is
|
|
|
|
@ifnottex
|
|
@math{pri(AP) / (|AP| * (pri(AP) + pri(@samp{true}) + pri(@samp{false})))},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\smallskip
|
|
\center{$\it{pri}(\it{AP}) / \Big(|\it{AP}|\times\big(\it{pri}(\it{AP}) + \it{pri}($\sc{True}$) + \it{pri}($\sc{False}$)\big)\Big)$}
|
|
\smallskip
|
|
@end tex
|
|
@end iftex
|
|
|
|
@noindent
|
|
where
|
|
@ifnottex
|
|
@math{|AP|}
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$|AP|$
|
|
@end tex
|
|
@end iftex
|
|
and
|
|
@ifnottex
|
|
pri(@math{AP})
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$\it{pri}(\it{AP})$
|
|
@end tex
|
|
@end iftex
|
|
are as defined above.
|
|
|
|
@cindex priorities for formula constants, atomic propositions and operators
|
|
@cindex operators, priorities for
|
|
@cindex probabilities for formula operators
|
|
@cindex operators, computing probabilities for
|
|
Line 7 of the algorithm concerns choosing a unary operator
|
|
@ifnottex
|
|
(@samp{!}, @samp{X}, @samp{<>} or @samp{[]})
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
($\neg$, $\bf{X}$, $\bf{F}$ or $\bf{G}$)
|
|
@end tex
|
|
@end iftex
|
|
into a formula. Here the probability of choosing the unary operator
|
|
@iftex
|
|
@tex
|
|
$\it{op}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@var{op}
|
|
@end ifnottex
|
|
is given by the equation
|
|
|
|
@iftex
|
|
@tex
|
|
$$
|
|
\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
|
|
@ifnottex
|
|
@math{pri(@var{op}) / Sum (pri(@var{op'}))},
|
|
@end ifnottex
|
|
|
|
@noindent
|
|
where
|
|
@iftex
|
|
@tex
|
|
$\it{op}^\prime$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@var{op'}
|
|
@end ifnottex
|
|
ranges over all unary operators.
|
|
|
|
Finally, at line 12 of the algorithm, the probability of choosing the (unary or
|
|
binary) operator
|
|
@iftex
|
|
@tex
|
|
$\it{op}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@var{op}
|
|
@end ifnottex
|
|
into the formula is
|
|
|
|
@iftex
|
|
@tex
|
|
$$
|
|
\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
|
|
@ifnottex
|
|
@math{pri(@var{op}) / Sum (pri(@var{op'}))},
|
|
@end ifnottex
|
|
|
|
@noindent
|
|
where
|
|
@iftex
|
|
@tex
|
|
$\it{op}^\prime$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@var{op'}
|
|
@end ifnottex
|
|
ranges over all unary and binary
|
|
@ifnottex
|
|
operators (@samp{!}, @samp{\/}, @samp{/\}, @samp{->}, @samp{<->}, @samp{xor},
|
|
@samp{X}, @samp{U}, @samp{W}, @samp{<>}, @samp{B}, @samp{V}, @samp{M},
|
|
@samp{[]}).
|
|
@end ifnottex
|
|
@iftex
|
|
operators.
|
|
@end iftex
|
|
|
|
An analysis of this algorithm is included in an appendix of
|
|
@ifnottex
|
|
@ref{[Tau00]}.
|
|
@end ifnottex
|
|
@iftex
|
|
[Tau00].
|
|
@end iftex
|
|
The analysis shows how to use the operator priorities to calculate the
|
|
expected number of occurrences of an operator in a randomly generated
|
|
formula. @command{lbtt} can optionally compute the expected operator
|
|
distribution for a given combination of operator priorities; see the
|
|
@samp{--showoperatordistribution} command line option
|
|
(@pxref{--showoperatordistribution,,@samp{--showoperatordistribution} command line option})
|
|
for more information.
|
|
|
|
See also the web page@*
|
|
@ifinfo
|
|
@url{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php}
|
|
@end ifinfo
|
|
@ifnotinfo
|
|
<@uref{http://www.tcs.hut.fi/Software/lbtt/formulaoptions.php}>
|
|
@end ifnotinfo
|
|
for an interface to a small database for adjusting the operator priorities
|
|
towards certain simple distributions.
|
|
|
|
|
|
|
|
@node Random state spaces, , Random LTL formulas, Random input generation
|
|
@subsection Random state spaces
|
|
|
|
@cindex state space
|
|
@cindex state space, random
|
|
@cindex random state space
|
|
State spaces are needed as input for tests only in the
|
|
model checking result cross comparison test
|
|
(@pxref{Model checking result cross-comparison test}) and the
|
|
model checking result consistency check
|
|
(@pxref{Model checking result consistency check}).
|
|
The state spaces are directed labeled graphs, each node of which is labeled
|
|
with a randomly chosen set of atomic propositions (the propositions that
|
|
hold in the state corresponding to the graph node). In addition, each state of
|
|
the state space always has at least one successor.
|
|
|
|
@command{lbtt} provides three different random state space generation
|
|
algorithms that differ in the structure of the generated state spaces. The
|
|
common parameters for each of these algorithms are:
|
|
|
|
@cindex state space, generation parameters
|
|
@cindex random state space, generation parameters
|
|
@cindex parameters for random state space generation algorithm
|
|
@itemize @bullet
|
|
|
|
@item
|
|
Number of states in the state space.
|
|
|
|
@item
|
|
Maximum number of different atomic propositions allowed in the label of any
|
|
state of the state space.
|
|
|
|
@item
|
|
The probability with which each atomic proposition should hold in a state of
|
|
the state space (which is, for simplicity, common to all atomic propositions).
|
|
|
|
@end itemize
|
|
|
|
@noindent
|
|
The different types of random state spaces that can be generated are:
|
|
@cindex state space, generation modes
|
|
|
|
@enumerate
|
|
|
|
@item
|
|
@cindex random connected graph
|
|
@cindex graph density
|
|
@cindex density (of a state space)
|
|
@cindex state space, density
|
|
@cindex random state space, density
|
|
Random connected graphs. These state spaces are guaranteed to have at least
|
|
one state such that every other state of the state space is reachable from
|
|
this state. In addition to the three above parameters, the behavior of the
|
|
algorithm generating these state spaces can be adjusted by specifying a
|
|
probability which approximates the @dfn{density} of the graph, i.e., the
|
|
probability that there is a directed edge from a state @var{x} to another
|
|
state @var{y}, where @var{x} and @var{y} are any two states in the state
|
|
space. For more details, see @ref{Algorithm for generating connected graphs}.
|
|
|
|
@item
|
|
@cindex random graph
|
|
Random graphs. These state spaces are constructed simply by taking all
|
|
pairs (@var{x}, @var{y}) of states in the state space and connecting state
|
|
@var{x} to state @var{y} with a user-specified probability that approximates
|
|
the graph density.
|
|
|
|
@item
|
|
@cindex random path
|
|
Random paths. A random path is simply a non-branching sequence of states,
|
|
where the last state of the sequence is connected to a randomly chosen state
|
|
earlier in the sequence.
|
|
|
|
@end enumerate
|
|
|
|
@cindex enumerated path
|
|
@command{lbtt} also includes a state space generation algorithm which
|
|
systematically enumerates all ``paths'' (see above) of a given size with a
|
|
given number of atomic propositions in each state. If
|
|
@iftex
|
|
@tex
|
|
$|S|$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{|S|}
|
|
@end ifnottex
|
|
is the number of states in the path and
|
|
@iftex
|
|
@tex
|
|
$|\it{AP}|$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{|AP|}
|
|
@end ifnottex
|
|
is the number of atomic propositions in each state of the path, it is easy to
|
|
see that the number of different paths having these parameters is
|
|
|
|
@iftex
|
|
@tex
|
|
$$|S|\cdot 2^{|S|\cdot|AP|},$$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{|S| * 2^(|S| * |AP|)},
|
|
@end ifnottex
|
|
|
|
@noindent
|
|
a number which grows exponentially in the product of the two parameters.
|
|
Obviously, this makes the exhaustive enumeration of all paths of a given size
|
|
practicable only for very small values of
|
|
@iftex
|
|
@tex
|
|
$|S|$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{|S|}
|
|
@end ifnottex
|
|
and
|
|
@iftex
|
|
@tex
|
|
$|\it{AP}|$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{|AP|}.
|
|
@end ifnottex
|
|
|
|
In practice, testing should be started using only very small state spaces
|
|
(say, with only 10--50 states and a small density) regardless of the particular
|
|
algorithm chosen for generating the state spaces. The size of the state spaces
|
|
can then be increased if @command{lbtt}'s memory consumption and the time spent
|
|
running the tests stay within acceptable limits.
|
|
|
|
|
|
|
|
@node Algorithm for generating connected graphs, , Random state spaces, Random state spaces
|
|
|
|
@subsubsection Algorithm for generating connected graphs
|
|
@cindex random connected graph, generation algorithm
|
|
@cindex random state space, algorithm for generating random connected graphs
|
|
@cindex state space, algorithm for generating random connected graphs
|
|
|
|
@command{lbtt} uses the following algorithm for generating random connected
|
|
graphs:
|
|
|
|
@smallexample
|
|
@r{1} function RandomGraph(@var{n} : Integer; @var{d} : Real in [0.0,1.0];
|
|
@var{t} : Real in [0.0,1.0]) : Graph;
|
|
@r{2} @var{S} := @{s1, s2, ..., sn@};
|
|
@r{3} @var{NodesToProcess} := @{s1@};
|
|
@r{4} @var{UnreachableNodes} := @{s2, s3, ..., sn@};
|
|
@r{5} @var{Edges} := @{@};
|
|
@r{6} while @var{NodesToProcess} @r{is not empty} do begin
|
|
@r{7} @var{state} := @r{a random node in} @var{NodesToProcess};
|
|
@r{8} @r{remove} @var{state} @r{from} @var{NodesToProcess};
|
|
@r{9} @var{Label}(@var{state}) := @{@};
|
|
@r{10} for @r{all} @var{p} @r{in} @var{AP} do
|
|
@r{11} if RandomNumber(0.0, 1.0) < @var{t} then
|
|
@r{12} @r{insert} @var{p} @r{into} @var{Label}(@var{state});
|
|
@r{13} if @var{UnreachableNodes} @r{is not empty} then begin
|
|
@r{14} @var{state'} := @r{a random node in} @var{UnreachableNodes};
|
|
@r{15} @r{remove} @var{state'} @r{from} @var{UnreachableNodes};
|
|
@r{16} @r{insert} @var{state'} @r{into} @var{NodesToProcess};
|
|
@r{17} @r{insert} (@var{state},@var{state'}) @r{into} @var{Edges};
|
|
@r{18} end;
|
|
@r{19} for @r{all} @var{state'} @r{in} @var{S} do
|
|
@r{20} if RandomNumber(0.0, 1.0) < @var{d} then begin
|
|
@r{21} @r{insert} (@var{state},@var{state'}) @r{into} @var{Edges};
|
|
@r{22} if @var{state'} @r{is in} @var{UnreachableNodes} then begin
|
|
@r{23} @r{remove} @var{state'} @r{from} @var{UnreachableNodes};
|
|
@r{24} @r{insert} @var{state'} @r{into} @var{NodesToProcess};
|
|
@r{25} end;
|
|
@r{26} end;
|
|
@r{27} if @r{there is no edge} (@var{state},@var{state'}) @r{in} @var{Edges}
|
|
@r{for any} @var{state'} @r{in} @var{S} then
|
|
@r{28} @r{insert} (@var{state},@var{state}) @r{into} @var{Edges};
|
|
@r{29} end;
|
|
@r{30} return <@var{S}, @var{Edges}, s1, @var{Label}>;
|
|
@r{31} end;
|
|
@end smallexample
|
|
|
|
The algorithm receives the parameters @var{n} (number of states in the
|
|
state spaces), @var{d} (approximate density of the generated graph) and
|
|
@var{t} (the probability with which each of the propositions in @math{AP}
|
|
should hold in a state) and returns the generated state space as a quadruple
|
|
<@var{S}, @var{Edges}, s1, @var{Label}>. Here @var{S} is the set of
|
|
states, @var{Edges} is the set of directed edges between the states, @math{s1}
|
|
is a state from which every state of the state space can be reached, and
|
|
@var{Label} is a function which maps each state to its label (a subset of
|
|
@var{AP}).
|
|
|
|
|
|
|
|
@node Testing procedure, Model checking result cross-comparison test, Random input generation, Test methods
|
|
@section Testing procedure
|
|
|
|
@cindex testing procedure
|
|
The following figure illustrates the first two tests in @command{lbtt}'s
|
|
testing procedure:
|
|
@ifhtml
|
|
@*
|
|
@end ifhtml
|
|
|
|
@image{testprocedure,6.5cm}
|
|
|
|
@noindent
|
|
After obtaining an LTL formula
|
|
@ifnottex
|
|
@math{f}
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$f$
|
|
@end tex
|
|
@end iftex
|
|
(either by reading it from a file or by calling the random formula generation
|
|
algorithm),
|
|
@command{lbtt} invokes each LTL-to-B@"uchi translator participating in
|
|
the tests in turn to construct a collection of B@"uchi automata for the formula
|
|
@ifnottex
|
|
@math{f}
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$f$
|
|
@end tex
|
|
@end iftex
|
|
@emph{and} the negated formula
|
|
@ifnottex
|
|
@math{! f}.
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$\neg f$.
|
|
@end tex
|
|
@end iftex
|
|
Each of these automata is then composed with the
|
|
randomly generated state space, whereafter @command{lbtt} performs the
|
|
model checking result cross-comparison test
|
|
(@pxref{Model checking result cross-comparison test})
|
|
and the model checking result consistency check
|
|
(@pxref{Model checking result consistency check})
|
|
on the model checking results, and reports all detected failures.
|
|
|
|
The B@"uchi automata intersection emptiness check
|
|
(@pxref{Automata intersection emptiness check}) operates as follows (note that
|
|
the LTL-to-B@"uchi translation phase is repeated in this figure only for
|
|
completeness; in reality, @command{lbtt} performs this phase only once):
|
|
@ifhtml
|
|
@*
|
|
@end ifhtml
|
|
|
|
@image{intersectioncheck,6.5cm}
|
|
|
|
The test procedure can then be repeated using a different LTL formula
|
|
and/or a different state space.
|
|
|
|
|
|
|
|
|
|
|
|
@node Model checking result cross-comparison test, Model checking result consistency check, Testing procedure, Test methods
|
|
@section Model checking result cross-comparison test
|
|
|
|
@cindex model checking result cross-comparison test
|
|
@cindex tests, model checking result cross-comparison test
|
|
|
|
LTL model checking can be used to test whether any of the infinite paths
|
|
starting from some state of a state space satisfies a given LTL
|
|
formula. For a fixed LTL formula, this question may have a different answer in
|
|
different states of the state space, but the answer should be independent
|
|
of the details of any (correct) implementation of the LTL model checking
|
|
procedure.
|
|
|
|
Therefore, it is possible to test LTL-to-B@"uchi translators by comparing
|
|
the results obtained by model checking an LTL formula in a fixed state space
|
|
several times, using each time a different translator for constructing a
|
|
B@"uchi automaton from the LTL formula. Differences in the model checking
|
|
results then suggest that at least one of the translators failed to translate
|
|
the LTL formula correctly into an automaton.
|
|
|
|
@cindex model checking modes
|
|
@cindex local model checking
|
|
@cindex global model checking
|
|
To extract as much test data as possible from a state space,
|
|
@command{lbtt} will by default make the model checking result comparison
|
|
``globally'' in the state space, which means using each LTL-to-B@"uchi
|
|
translator to find @emph{all} states in the state space with an infinite
|
|
path supposedly satisfying some LTL formula and then comparing the resulting
|
|
state sets for equality. Alternatively, the test can be performed only
|
|
``locally'' in a single state of each state space (i.e., by choosing some
|
|
state of the state space and checking that all B@"uchi automata constructed
|
|
using the different translators give the same model checking result in
|
|
that state), which may speed up testing, but
|
|
will reduce the number of comparison tests. In addition, @command{lbtt} repeats
|
|
the result
|
|
cross-comparison test for the negation of each LTL formula, since model
|
|
checking also the negated formula permits making an additional consistency
|
|
check (see below) on the results computed using each implementation.
|
|
|
|
@cindex internal model checking algorithm
|
|
@cindex using the internal model checking algorithm
|
|
@cindex tests, against internal model checking algorithm
|
|
Note: If the generated state spaces are paths (either random or
|
|
systematically enumerated, @pxref{Random state spaces}), @command{lbtt}
|
|
will then include its internal LTL model checking algorithm (a restricted model
|
|
checking algorithm used normally in test failure analysis,
|
|
@pxref{Analyzing test results}) into the model
|
|
checking result cross-comparison test. This is especially useful if there is
|
|
only one translation algorithm implementation available for testing
|
|
(in which case normal model checking result cross-comparison is obviously
|
|
redundant) but may be of advantage also in other cases by
|
|
providing an additional implementation to include in the tests.
|
|
|
|
|
|
|
|
@node Model checking result consistency check, Automata intersection emptiness check, Model checking result cross-comparison test, Test methods
|
|
@section Model checking result consistency check
|
|
|
|
@cindex model checking result consistency check
|
|
@cindex tests, model checking result consistency check
|
|
|
|
LTL model checking tells whether any of the infinite paths starting from some
|
|
state of a state space satisfies a given LTL formula. If there
|
|
are no such paths beginning from the state, it follows that all infinite paths
|
|
beginning from the state must then satisfy the @emph{negation} of the same
|
|
formula. Since all state spaces used by @command{lbtt} always have at least
|
|
one path beginning from each state of the state space (guaranteed by the
|
|
state space generation algorithms), at least
|
|
one path beginning from any state must satisfy either the formula or its
|
|
negation, i.e., it cannot be the case that none of the paths is a model of
|
|
either formula.
|
|
|
|
However, implementation errors in an LTL-to-B@"uchi translator used for model
|
|
checking may actually lead to this inconsistent model checking result if the
|
|
translation of either of the formulas results in an incorrect automaton, in
|
|
which case @command{lbtt} will report an error.
|
|
|
|
@cindex model checking modes
|
|
@cindex local model checking
|
|
@cindex global model checking
|
|
Similarly to the model checking result cross-comparison test, the
|
|
model checking result consistency check can be performed either in all states
|
|
of the state space (``globally'') or only in a single state of the state
|
|
space (``locally''), with the same trade-offs between testing speed and
|
|
number of tests as described in the previous
|
|
@ifnottex
|
|
section (@pxref{Model checking result cross-comparison test}).
|
|
@end ifnottex
|
|
@iftex
|
|
section.
|
|
@end iftex
|
|
|
|
|
|
@node Automata intersection emptiness check, , Model checking result consistency check, Test methods
|
|
@section Automata intersection emptiness check
|
|
|
|
@cindex B@"uchi automata intersection emptiness check
|
|
@cindex tests, B@"uchi automata intersection emptiness check
|
|
|
|
The semantics of LTL guarantees that no model of an LTL formula
|
|
can be the model of the negation of the same formula. In terms of
|
|
B@"uchi automata, this implies that the languages accepted by automata
|
|
constructed from two complementary LTL formulas should be disjoint.
|
|
This can be confirmed by intersecting the automata (i.e., by composing the
|
|
automata to construct a third B@"uchi automaton that accepts precisely
|
|
those inputs accepted by both of the original automata) and checking the
|
|
result for emptiness. If the intersection is found to be nonempty, however,
|
|
at least one of the LTL-to-B@"uchi translator(s) used for constructing the
|
|
original automata must have failed to perform the translation of either
|
|
formula correctly.
|
|
|
|
|
|
|
|
@node Invocation, Interpreting the output, Test methods, Top
|
|
@chapter Invocation
|
|
|
|
@cindex invoking @command{lbtt}
|
|
@cindex starting @command{lbtt}
|
|
@cindex tests, starting
|
|
@cindex @command{lbtt} (executable file)
|
|
@command{lbtt} is started with the command @command{lbtt} with optional
|
|
command line parameters. Before starting the program, however, you need
|
|
to create a configuration file which lists the LTL-to-B@"uchi translators
|
|
to be tested and defines additional testing parameters.
|
|
@xref{Configuration file}. If no suitable configuration file is found or
|
|
if the configuration file cannot be processed successfully, @command{lbtt}
|
|
exits with an error message.
|
|
|
|
After reading the configuration file, @command{lbtt} starts tests on the
|
|
LTL-to-B@"uchi translators listed in the configuration file (for
|
|
details about the testing procedure, see @ref{Test methods}). The program
|
|
exits after a predetermined number of test rounds.
|
|
|
|
@cindex exiting @command{lbtt}
|
|
@cindex quitting @command{lbtt}
|
|
@cindex tests, aborting
|
|
If the program is started in any of its interactive modes
|
|
(see @ref{Interactivity modes}), the program
|
|
may occasionally pause to wait for user input between test rounds. Type
|
|
@samp{quit @key{ENTER}} at the prompt to exit @command{lbtt} at this
|
|
point (or see @ref{Analyzing test results}, for more information on
|
|
how to use @command{lbtt}'s internal commands).
|
|
|
|
@menu
|
|
* Configuration file:: Description of the configuration file
|
|
format.
|
|
* Command line options:: List of command line options.
|
|
@end menu
|
|
|
|
|
|
|
|
@node Configuration file, Command line options, Invocation, Invocation
|
|
@section Configuration file
|
|
|
|
@cindex configuration file, formatting
|
|
@cindex conventions for writing configuration files
|
|
|
|
The configuration file of @command{lbtt} contains a list of the
|
|
LTL-to-B@"uchi translators to be tested along with other options
|
|
which affect the way the tests are performed. The configuration
|
|
file is processed before starting the tests. By default, @command{lbtt}
|
|
will try to read the configuration from the file @file{config} in the
|
|
current working directory; a different file name can be specified with the
|
|
@option{--configfile=@var{filename}} command line option.
|
|
|
|
The configuration file consists of one or more sections, each of which
|
|
provides a collection of interrelated configuration options. The general
|
|
format of the configuration file is
|
|
|
|
@smallexample
|
|
@var{section-name}
|
|
@{
|
|
@var{option-name} = @var{value}
|
|
@var{option-name} = @var{value}
|
|
@dots{}
|
|
@}
|
|
|
|
@dots{}
|
|
@end smallexample
|
|
|
|
@cindex configuration file, option values
|
|
@cindex truth values in configuration file
|
|
@cindex string values in configuration file
|
|
@cindex numeric values in configuration file
|
|
|
|
@noindent
|
|
Section and option names are case-insensitive. Values can be numbers,
|
|
strings or truth values (@samp{yes} and @samp{no}, or equivalently,
|
|
@samp{true} and @samp{false}). String values are case-sensitive and are subject
|
|
to common quoting and escaping rules (i.e., string values containing white
|
|
space should be enclosed in quotes, or the white space characters should be
|
|
escaped with @samp{\}).
|
|
|
|
@cindex comments in configuration file
|
|
@cindex configuration file, comments
|
|
|
|
Comments can be included by putting a @samp{#} symbol before them; the end of
|
|
any line containing the @samp{#} character will be ignored when processing the
|
|
configuration file.
|
|
|
|
@cindex configuration file, minimal requirements
|
|
@cindex minimal requirements for configuration files
|
|
|
|
The configuration file must contain at least one @samp{Translator}
|
|
section specifying an LTL-to-B@"uchi translator. The other sections
|
|
are optional and can be used to override the default testing parameters.
|
|
|
|
@menu
|
|
* Translator section:: Each LTL-to-B@"uchi translator to be
|
|
tested requires a separate
|
|
@samp{Translator} section in the
|
|
configuration file.
|
|
* GlobalOptions section:: Options for changing the general
|
|
behavior of @command{lbtt}.
|
|
* FormulaOptions section:: Options controlling the way random
|
|
LTL formulas are generated.
|
|
* StateSpaceOptions section:: Options controlling the way random
|
|
state spaces are generated.
|
|
* Sample configuration file:: An example of a configuration file.
|
|
@end menu
|
|
|
|
|
|
@node Translator section, GlobalOptions section, Configuration file, Configuration file
|
|
@subsection The @samp{Translator} section
|
|
|
|
@cindex configuration file, @samp{Algorithm} section
|
|
@cindex configuration file, @samp{Implementation} section
|
|
@cindex configuration file, @samp{Translator} section
|
|
@cindex @samp{Algorithm} section (configuration file)
|
|
@cindex @samp{Implementation} section (configuration file)
|
|
@cindex @samp{Translator} section (configuration file)
|
|
@cindex configuration file, minimal requirements
|
|
|
|
Each LTL-to-B@"uchi translator to be tested requires a separate
|
|
@samp{Translator}
|
|
section@footnote{The @samp{Algorithm} and @samp{Implementation} keywords are
|
|
recognized as aliases of the @samp{Translator} keyword.} in the configuration
|
|
file; there must be at least one such section in the file.
|
|
|
|
The translators are assumed to be accessible
|
|
through external executable files. Therefore, this section must at a minimum
|
|
specify the full file name of the executable to run in order to invoke
|
|
the translator; see @ref{Translator interface}, for information about the
|
|
conventions @command{lbtt} uses to communicate with the
|
|
LTL-to-B@"uchi translators.
|
|
|
|
@cindex LTL-to-B@"uchi translators, identifiers
|
|
@cindex identifiers for LTL-to-B@"uchi translators
|
|
Translators specified in the configuration file are given unique
|
|
integer identifiers in the order they are listed in the file,
|
|
starting from zero. These numbers can be used when referring to the
|
|
different translators when using @command{lbtt}'s internal commands
|
|
(@pxref{Analyzing test results}). Alternatively, the translators can be
|
|
referred to using the names specified in the configuration file.
|
|
|
|
The following options (in alphabetical order) are available within this
|
|
section:
|
|
|
|
@table @samp
|
|
@item Enabled = @var{TRUTH-VALUE}
|
|
@cindex enabling LTL-to-B@"uchi translators
|
|
@cindex LTL-to-B@"uchi translators, enabling
|
|
@cindex disabling LTL-to-B@"uchi translators
|
|
@cindex LTL-to-B@"uchi translators, disabling
|
|
@findex Enabled @r{[}Translator@r{]}
|
|
This option determines whether the translator should be initially included in
|
|
or excluded from the tests. The default value is @samp{Yes}. The translator
|
|
can be enabled or disabled during testing with @command{lbtt}'s
|
|
internal commands (@pxref{Test control commands}).
|
|
|
|
@item Name = @var{STRING}
|
|
@findex Name @r{[}Translator@r{]}
|
|
This option can be used to specify a unique textual identifier for the
|
|
LTL-to-B@"uchi translator. @command{lbtt} will use this identifier when
|
|
displaying various messages concerning the implementation; the identifier can
|
|
also be used to refer to the implementation when working with @command{lbtt}'s
|
|
internal commands (@pxref{Analyzing test results}). (If no name has been
|
|
explicitly given for the translator, @command{lbtt} assigns the translator a
|
|
name of the
|
|
form @samp{Algorithm @var{n}}, where @var{n} is the running integer identifier
|
|
for the translators.)
|
|
|
|
The identifier @samp{lbtt} is reserved for @command{lbtt}'s internal model
|
|
checking algorithm (@pxref{Model checking result cross-comparison test}).
|
|
|
|
@item Parameters = @var{STRING}
|
|
@findex Parameters @r{[}Translator@r{]}
|
|
This option can be used to specify any additional parameters that should
|
|
be passed to the translator executable whenever running it. (The parameter
|
|
string defaults to the empty string if the option is not used.)
|
|
|
|
@item Path = @var{STRING}
|
|
@findex Path @r{[}Translator@r{]}
|
|
This option must be given a value for each translator specified in the
|
|
configuration file. The value should be the complete file name of the program
|
|
which is used to run the translator.
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node GlobalOptions section, FormulaOptions section, Translator section, Configuration file
|
|
@subsection The @samp{GlobalOptions} section
|
|
|
|
@cindex configuration file, @samp{GlobalOption} section
|
|
@cindex @samp{GlobalOptions} section (configuration file)
|
|
|
|
The @samp{GlobalOptions} section includes options that affect the general
|
|
behavior of @command{lbtt}. Options available within this section are (in
|
|
alphabetical order):
|
|
|
|
@table @samp
|
|
@item ComparisonCheck = @var{TRUTH-VALUE}
|
|
@itemx ComparisonTest = @var{TRUTH-VALUE}
|
|
@cindex tests, enabling and disabling
|
|
@cindex enabling and disabling tests
|
|
@findex ComparisonCheck @r{[}GlobalOptions@r{]}
|
|
@findex ComparisonTest @r{[}GlobalOptions@r{]}
|
|
This option can be used to enable or disable the model checking result
|
|
cross-comparison test (@pxref{Model checking result cross-comparison test}).
|
|
The test is enabled by default.
|
|
|
|
@item ConsistencyCheck = @var{TRUTH-VALUE}
|
|
@itemx ConsistencyTest = @var{TRUTH-VALUE}
|
|
@cindex tests, enabling and disabling
|
|
@cindex enabling and disabling tests
|
|
@findex ConsistencyCheck @r{[}GlobalOptions@r{]}
|
|
@findex ConsistencyTest @r{[}GlobalOptions@r{]}
|
|
This option can be used to enable or disable the model checking result
|
|
consistency check (@pxref{Model checking result consistency check}). The test
|
|
is enabled by default.
|
|
|
|
@item @anchor{Interactivity modes}Interactive = @var{MODE-LIST}
|
|
@cindex interactivity modes
|
|
@findex Interactive @r{[}GlobalOptions@r{]}
|
|
This option determines when @command{lbtt} should pause to wait for user input
|
|
between test rounds. The @var{MODE-LIST} is a comma-separated list of the
|
|
following modes (with no spaces in between the modes):
|
|
@table @samp
|
|
@item Always
|
|
Pause unconditionally after each test round.
|
|
|
|
@item OnError
|
|
Pause testing only after failed test rounds.
|
|
|
|
@item Never
|
|
Run all tests without interruption.
|
|
|
|
@item OnBreak
|
|
Pause testing when requested by the user (for example, after receiving a break
|
|
signal from the keyboard). If this mode is not specified, @samp{lbtt} will
|
|
respond to break signals by aborting.
|
|
@end table
|
|
|
|
(Since the first three interactivity modes are mutually exclusive, it does not
|
|
make sense to combine these modes with each other.) The default mode list
|
|
consists of the value @samp{Always}, that is, testing is paused after
|
|
every test round, and signalling a break will abort testing.
|
|
|
|
@item IntersectionCheck = @var{TRUTH-VALUE}
|
|
@itemx IntersectionTest = @var{TRUTH-VALUE}
|
|
@cindex tests, enabling and disabling
|
|
@cindex enabling and disabling tests
|
|
@findex IntersectionCheck @r{[}GlobalOptions@r{]}
|
|
@findex IntersectionTest @r{[}GlobalOptions@r{]}
|
|
This option can be used to enable or disable the B@"uchi automata intersection
|
|
emptiness check (@pxref{Automata intersection emptiness check}). The test is
|
|
enabled by default.
|
|
|
|
@item ModelCheck = Local @r{|} Global
|
|
@findex ModelCheck @r{[}GlobalOptions@r{]}
|
|
@cindex model checking modes
|
|
@cindex local model checking
|
|
@cindex global model checking
|
|
This option determines whether @command{lbtt} should perform model checking
|
|
with respect to all states of each state space or only with respect
|
|
to a single state of each state space. This affects the number of tests that
|
|
@command{lbtt} makes during the model checking result cross-comparison test
|
|
(@pxref{Model checking result cross-comparison test}) and the model checking
|
|
result consistency check (@pxref{Model checking result consistency check}).
|
|
Global model checking (the default) maximizes the number of tests, but may
|
|
require more time and memory. (Note: This option has no effect if none of the
|
|
model checking tests is enabled.)
|
|
|
|
@item Rounds = @var{INTEGER}
|
|
@findex Rounds @r{[}GlobalOptions@r{]}
|
|
The @samp{Rounds} option can be used to specify the number of test rounds to
|
|
run; the default value is 10.
|
|
|
|
@item @anchor{Timeouts}TranslatorTimeout = @var{TIME-SPECIFICATION}
|
|
@findex TranslatorTimeout @r{[}GlobalOptions@r{]}
|
|
@cindex timeouts for translators
|
|
This option can be used to specify a time limit (in wall-clock time) after
|
|
which the execution of a translator is aborted if it fails to produce a
|
|
result within the given limit. A timeout is considered a test failure. The time
|
|
specification is of the form
|
|
@samp{@r{[}@var{hours}@r{]}h@r{[}@var{minutes}@r{]}min@r{[}@var{seconds}@r{]}s}
|
|
where @var{hours}, @var{minutes} and @var{seconds} specify the time limit in
|
|
the obvious way (time units having value 0 can be omitted). For example,
|
|
a limit of @samp{1h30min} sets the limit at one hour and thirty minutes.
|
|
|
|
@item Verbosity = @var{INTEGER}
|
|
@findex Verbosity @r{[}GlobalOptions@r{]}
|
|
@cindex verbosity, changing
|
|
@cindex changing verbosity of output
|
|
This option sets the verbosity level for output messages. The value
|
|
can be an integer between 0 and 5 (inclusive). A value of 0 will suppress all
|
|
messages (and is therefore useful only when storing test results into a log
|
|
file; @pxref{--logfile,,@samp{--logfile} command line option}); increasing
|
|
the value results in more output. The default value is 3.
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node FormulaOptions section, StateSpaceOptions section, GlobalOptions section, Configuration file
|
|
@subsection The @samp{FormulaOptions} section
|
|
|
|
@cindex configuration file, @samp{FormulaOptions} section
|
|
@cindex @samp{FormulaOptions} section (configuration file)
|
|
|
|
The @samp{FormulaOptions} section defines the parameters that affect the
|
|
algorithm @command{lbtt} uses for generating random LTL formulas
|
|
(for more information about the algorithm, see @ref{Random LTL formulas}).
|
|
This section provides the following options:
|
|
|
|
@cindex parameters for random LTL formula generation algorithm
|
|
@cindex random LTL formula, parameters for generation algorithm
|
|
@cindex LTL formula, parameters for generation algorithm
|
|
@cindex priorities for formula constants, atomic propositions and operators
|
|
@cindex atomic propositions, priorities for
|
|
@cindex constants, priorities for
|
|
@cindex operators, priorities for
|
|
|
|
@table @samp
|
|
@item AbbreviatedOperators = @var{TRUTH-VALUE}
|
|
@cindex abbreviated LTL formula operators
|
|
@cindex LTL formula operators, abbreviated
|
|
@cindex operators, abbreviated
|
|
@findex AbbreviatedOperators @r{[}FormulaOptions@r{]}
|
|
This option determines whether the generated formulas should be allowed to
|
|
include any of the operators @samp{->}, @samp{<->}, @samp{xor}, @samp{W},
|
|
@samp{<>}, @samp{B}, @samp{V}, @samp{M} or @samp{[]} (all of which can be
|
|
given definitions using only the operators @samp{!}, @samp{\/}, @samp{/\},
|
|
@samp{U} and @samp{V}). Setting this option to @samp{No} assigns each of the
|
|
abbreviated operators a zero priority, overriding any explicit priorities
|
|
defined for these operators in the program configuration. The default value
|
|
for the option is @samp{Yes}, so abbreviations are allowed by default.
|
|
|
|
@item AndPriority = @var{INTEGER}
|
|
@findex AndPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the logical conjunction operator (@samp{/\}).
|
|
|
|
@item BeforePriority = @var{INTEGER}
|
|
@findex BeforePriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal operator ``before'' (@samp{B}). (Note: This option
|
|
has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@item ChangeInterval = @var{INTEGER}
|
|
@findex ChangeInterval @r{[}FormulaOptions@r{]}
|
|
This option determines how often (in number of test rounds)
|
|
@command{lbtt} should generate a new random LTL formula (or read a new formula
|
|
from a user-specified file). A value of 0 forces
|
|
@command{lbtt} to use a fixed LTL formula for all tests. The default value
|
|
is 1, i.e.,@: a new formula will be generated at the beginning of each test
|
|
round.
|
|
|
|
@item DefaultOperatorPriority = @var{INTEGER}
|
|
@cindex default operator priority
|
|
@findex DefaultOperatorPriority @r{[}FormulaOptions@r{]}
|
|
This option sets the priority for all formula operators for which
|
|
no priority has been given explicitly in the program configuration (i.e.,
|
|
it can be used as a shorthand to initialize the priority of all operators).
|
|
The default value of this option is 0, so all operators with no explicitly
|
|
given priorities are disabled by default.
|
|
|
|
@item EquivalencePriority = @var{INTEGER}
|
|
@findex EquivalencePriority @r{[}FormulaOptions@r{]}
|
|
Priority of the logical equivalence operator (@samp{<->}). (Note: This
|
|
option has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@item FalsePriority = @var{INTEGER}
|
|
@findex FalsePriority @r{[}FormulaOptions@r{]}
|
|
Priority of the Boolean constant
|
|
@iftex
|
|
@tex
|
|
\sc{False}
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{false}
|
|
@end ifnottex
|
|
(with respect to priorities of the constant
|
|
@iftex
|
|
@tex
|
|
\sc{True}
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{true}
|
|
@end ifnottex
|
|
and the atomic propositions).
|
|
|
|
@item FinallyPriority = @var{INTEGER}
|
|
@findex FinallyPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal operator ``finally'' (@samp{<>}). (Note: This
|
|
option has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@item GenerateMode = Normal @r{|} NNF
|
|
@cindex random LTL formula, generation modes
|
|
@cindex negation normal form
|
|
@findex GenerateMode @r{[}FormulaOptions@r{]}
|
|
This option determines whether @command{lbtt} should generate random formulas
|
|
directly into (a weakened version of) negation normal form in which the
|
|
negation operator may only precede atomic propositions. Note that the
|
|
formulas may still contain ``abbreviated'' operators if they have nonzero
|
|
priorities---use @samp{AbbreviatedOperators=No} or @samp{OutputMode=NNF} if you
|
|
wish to prevent this. The default value for this option is @samp{Normal}.
|
|
(See the @samp{OutputMode} option below for an example about the differences
|
|
in the effects of the @samp{GenerateMode} and @samp{OutputMode} options.)
|
|
|
|
@item GloballyPriority = @var{INTEGER}
|
|
@findex GloballyPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal operator ``globally'' (@samp{[]}). (Note: This
|
|
option has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@item ImplicationPriority = @var{INTEGER}
|
|
@findex ImplicationPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the logical implication operator (@samp{->}). (Note: This
|
|
option has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@item NextPriority = @var{INTEGER}
|
|
@findex NextPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal operator ``next time'' (@samp{X}).
|
|
|
|
@item NotPriority = @var{INTEGER}
|
|
@findex NotPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the logical negation operator (@samp{!}).
|
|
|
|
@item OrPriority = @var{INTEGER}
|
|
@findex OrPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the logical disjunction operator (@samp{\/}).
|
|
|
|
@item OutputMode = Normal @r{|} NNF
|
|
@findex OutputMode @r{[}FormulaOptions@r{]}
|
|
@cindex random LTL formula, output modes
|
|
@cindex LTL formula, output modes
|
|
@cindex negation normal form
|
|
This option determines whether @command{lbtt} should transform each generated
|
|
LTL formula into (strict) negation normal form before passing it to
|
|
LTL-to-B@"uchi translators. If the value is set to @samp{NNF}, @command{lbtt}
|
|
will rewrite each generated formula into a form consisting of the
|
|
operators @samp{!}, @samp{\/}, @samp{/\}, @samp{U} and @samp{V} such that all
|
|
negations in the formula (if any) precede atomic propositions. The default
|
|
value is @samp{Normal}. (See also the @samp{GenerateMode} option that can be
|
|
used to force formulas to be generated directly into negation normal
|
|
form.)
|
|
|
|
The option is probably useful only if you have a translator which does not
|
|
support the ``abbreviated'' operators directly, but you still wish to test it
|
|
with formulas which describe properties expressed using these operators.
|
|
Note, however, that rewriting may change the size of the formula.
|
|
|
|
The following table illustrates the effects of the
|
|
@samp{GenerateMode} and the @samp{OutputMode} options.
|
|
@smallformat
|
|
@t{
|
|
@r{LTL formula} @r{Can} f @r{be} OutputMode@r{'s effect on the}
|
|
f @r{generated if} @r{formula passed to the}
|
|
GenerateMode @r{LTL-to-B@"uchi translators}
|
|
=NNF @r{?}
|
|
-------------------------------------------------------------
|
|
(p1 V ! p0) @r{Yes} Normal@r{/}NNF@r{:} (p1 V ! p0)
|
|
|
|
[] p0 -> <> p1 @r{Yes*} Nor@r{:} [] p0 -> <> p1
|
|
NNF@r{:} (true U ! p0) \/ (true U p1)
|
|
|
|
! <> p0 @r{No} Nor@r{:} ! <> p0
|
|
NNF@r{:} (false V ! p0)
|
|
|
|
@r{* only if} AbbreviatedOperators=Yes}
|
|
@end smallformat
|
|
|
|
@item PropositionPriority = @var{INTEGER}
|
|
@cindex atomic propositions, priorities for
|
|
@findex PropositionPriority @r{[}FormulaOptions@r{]}
|
|
Priority for atomic propositions with respect to the priority of Boolean
|
|
constants. This priority is the common priority of @emph{all} atomic
|
|
propositions.
|
|
|
|
@item Propositions = @var{INTEGER}
|
|
@findex Propositions @r{[}FormulaOptions@r{]}
|
|
This option sets the maximum number of different atomic propositions in
|
|
each generated LTL formula. No generated formula will have more than this
|
|
number of different atomic propositions. A value of 0 will generate random
|
|
formulas with only Boolean
|
|
constants (one of which must in this case have a nonzero priority). The
|
|
default value is 5. The names of the propositions are of the form
|
|
@ifhtml
|
|
@samp{p}@var{n},
|
|
@end ifhtml
|
|
@ifnothtml
|
|
@samp{p@var{n}},
|
|
@end ifnothtml
|
|
where @var{n} is a nonnegative integer less than the maximum number of
|
|
propositions.
|
|
|
|
@item RandomSeed = @var{INTEGER}
|
|
@cindex random LTL formula, random seed for generation algorithm
|
|
@cindex random seed, LTL formula generation algorithm
|
|
@findex RandomSeed @r{[}FormulaOptions@r{]}
|
|
This option specifies a seed value for generating random numbers for the
|
|
random LTL formula generation algorithm. If this option is not present, the
|
|
seed defaults to 1. See the next section for information on how to change the
|
|
default seed for the random state space generation algorithm.
|
|
|
|
(The reason for having two separate random seeds is to make the sequences of
|
|
random formulas and state spaces independent of each other. For example,
|
|
this makes it easy to repeat tests using the same batch of random LTL formulas,
|
|
but with state spaces of different size.)
|
|
|
|
@item ReleasePriority = @var{INTEGER}
|
|
@findex ReleasePriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal ``(weak) release'' operator (@samp{V}).
|
|
|
|
@item Size = @var{INTEGER}
|
|
@itemx Size = @var{MINIMUM-SIZE}-@var{MAXIMUM-SIZE}
|
|
@itemx Size = @var{MINIMUM-SIZE}...@var{MAXIMUM-SIZE}
|
|
@findex Size @r{[}FormulaOptions@r{]}
|
|
This option defines how many nodes are allowed in the parse tree of each
|
|
randomly generated LTL formula. If the size is given as an interval (by
|
|
separating the bounds with @samp{-} or @samp{...} with no white space in
|
|
between),
|
|
@command{lbtt} chooses the size of each formula randomly in the interval
|
|
using a uniform random distribution. The default size is 5.
|
|
|
|
@item StrongReleasePriority = @var{INTEGER}
|
|
@findex StrongReleasePriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal ``strong release'' operator (@samp{M}). (Note: This
|
|
option has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@item UntilPriority = @var{INTEGER}
|
|
@findex UntilPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal ``(strong) until'' operator (@samp{U}).
|
|
|
|
@item TruePriority = @var{INTEGER}
|
|
@findex TruePriority @r{[}FormulaOptions@r{]}
|
|
Priority of the Boolean constant
|
|
@iftex
|
|
@tex
|
|
\sc{True}
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{true}
|
|
@end ifnottex
|
|
(with respect to the priorities of the constant
|
|
@iftex
|
|
@tex
|
|
\sc{False}
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{false}
|
|
@end ifnottex
|
|
and the atomic propositions).
|
|
|
|
@item WeakUntilPriority = @var{INTEGER}
|
|
@findex WeakUntilPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the temporal ``weak until'' operator (@samp{W}). (Note: This
|
|
option has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@item XorPriority = @var{INTEGER}
|
|
@findex XorPriority @r{[}FormulaOptions@r{]}
|
|
Priority of the logical ``exclusive or'' operator (@samp{xor}). (Note: This
|
|
option has no effect if @samp{AbbreviatedOperators} is set to @samp{No}.)
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node StateSpaceOptions section, Sample configuration file, FormulaOptions section, Configuration file
|
|
@subsection The @samp{StateSpaceOptions} section
|
|
|
|
@cindex configuration file, @samp{StateSpaceOptions} section
|
|
@cindex @samp{StateSpaceOptions} section (configuration file)
|
|
|
|
The @samp{StateSpaceOptions} section defines the parameters that affect the
|
|
way @command{lbtt} generates random state spaces for the
|
|
model checking result cross-comparison test
|
|
(@pxref{Model checking result cross-comparison test})
|
|
and the model checking result consistency check
|
|
(@pxref{Model checking result consistency check}).
|
|
See also @ref{Random state spaces}, for more information about the different
|
|
types of available state spaces and the algorithms used for constructing them.
|
|
The options available within this section are:
|
|
|
|
@cindex parameters for random state space generation algorithm
|
|
@cindex state space, generation parameters
|
|
@cindex random state space, generation parameters
|
|
|
|
@table @samp
|
|
@item ChangeInterval = @var{INTEGER}
|
|
@findex ChangeInterval @r{[}StateSpaceOptions@r{]}
|
|
This option determines how often (in number of test rounds)
|
|
@command{lbtt} should generate a new random state space. A value of 0 forces
|
|
@command{lbtt} to use a fixed state space for all tests. The default behavior
|
|
is to generate a new state space at the beginning of each test round.
|
|
|
|
@item EdgeProbability = @var{PROBABILITY}
|
|
@cindex graph density
|
|
@cindex density (of a state space)
|
|
@cindex state space, density
|
|
@cindex random state space, density
|
|
@findex EdgeProbability @r{[}StateSpaceOptions@r{]}
|
|
This option sets the approximate probability (between 0.0 and 1.0) of adding a
|
|
transition from any state @var{x} to some other state @var{y} when generating
|
|
random graphs as state spaces. The default value is 0.2. The probability is
|
|
approximate because
|
|
@command{lbtt} still has
|
|
to ensure that all states of each generated state spaces have at least one
|
|
successor, which might require adding extra transitions to the graph.
|
|
Note: This option has no effect if @samp{GenerateMode} is set to
|
|
@samp{RandomPath} or @samp{EnumeratedPath}.
|
|
|
|
@item GenerateMode = RandomConnectedGraph @r{|} RandomGraph @r{|} RandomPath @r{|} EnumeratedPath
|
|
@cindex state space, generation modes
|
|
@cindex random connected graph
|
|
@cindex random graph
|
|
@cindex random path
|
|
@cindex enumerated path
|
|
@findex GenerateMode @r{[}StateSpaceOptions@r{]}
|
|
This option selects the type of generated state spaces from the four available
|
|
types. The default value is @samp{RandomConnectedGraph}. See
|
|
@ref{Random state spaces}, for more information on the different state space
|
|
types.
|
|
|
|
@cindex internal model checking algorithm
|
|
@cindex using the internal model checking algorithm
|
|
@cindex tests, against internal model checking algorithm
|
|
Note: Using the @samp{RandomPath} or the @samp{EnumeratedPath} setting includes
|
|
@command{lbtt}'s internal model checking algorithm into the various model
|
|
checking tests if they are enabled. For more information, see
|
|
@ref{Model checking result cross-comparison test}.
|
|
|
|
@item Propositions = @var{INTEGER}
|
|
@findex Propositions @r{[}StateSpaceOptions@r{]}
|
|
This option sets the number of atomic propositions attached to each state of
|
|
the generated state spaces. The default value is 5.
|
|
|
|
Usually this should probably be the same as the maximum number of
|
|
different atomic propositions in the generated formulas
|
|
(@pxref{FormulaOptions section}).
|
|
If the number of propositions attached to each state of
|
|
the state spaces is less than the maximum number of different propositions that
|
|
may occur in the generated formulas, all ``extra'' propositions in the formulas
|
|
are considered to be false in every state of the state space.
|
|
|
|
@item RandomSeed = @var{INTEGER}
|
|
@cindex random state space, random seed for generation algorithm
|
|
@cindex random seed, state space generation algorithm
|
|
@findex RandomSeed @r{[}StateSpaceOptions@r{]}
|
|
This option specifies a seed value for generating random numbers required by
|
|
the random state space generation algorithm. If this option is not present, the
|
|
seed defaults to 1. See the previous section for how to change the random seed
|
|
used to initialize the random number generator for the random LTL formula
|
|
generation algorithm.
|
|
|
|
@item Size = @var{INTEGER}
|
|
@itemx Size = @var{MINIMUM-SIZE}-@var{MAXIMUM-SIZE}
|
|
@itemx Size = @var{MINIMUM-SIZE}...@var{MAXIMUM-SIZE}
|
|
@findex Size @r{[}StateSpaceOptions@r{]}
|
|
This option sets the number of states in the generated state spaces. If the
|
|
size is given as an interval, @command{lbtt} either chooses a random size in
|
|
the interval (including its endpoints) each time a new state space is
|
|
generated, or, if @samp{GenerateMode} is set to @samp{EnumeratedPath},
|
|
enumerates all state spaces in the specified range systematically, starting
|
|
from the minimum size. The default size is 20.
|
|
|
|
@item TruthProbability = @var{PROBABILITY}
|
|
@findex TruthProbability @r{[}StateSpaceOptions@r{]}
|
|
Probability (between 0.0 and 1.0) with which each individual atomic proposition
|
|
has the value
|
|
@ifnottex
|
|
@samp{true}
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\sc{True}
|
|
@end tex
|
|
@end iftex
|
|
in any state of the state space. Note: This option has no effect if
|
|
@samp{GenerateMode} is set to @samp{EnumeratedPath}. The default value is 0.5.
|
|
|
|
@end table
|
|
|
|
|
|
@node Sample configuration file, , StateSpaceOptions section, Configuration file
|
|
@subsection Sample configuration file
|
|
|
|
@cindex configuration file, example
|
|
|
|
The following configuration file sets @command{lbtt} up for testing two
|
|
imaginary LTL-to-B@"uchi translators.
|
|
|
|
@smallexample
|
|
# Sample configuration file for lbtt
|
|
|
|
Translator
|
|
@{
|
|
Name = Translator\ 1
|
|
Path = /home/lbtt-user/bin/t-1 # location of the translator
|
|
# executable
|
|
Enabled = Yes
|
|
@}
|
|
|
|
Translator
|
|
@{
|
|
Name = "Translator 2"
|
|
Path = /home/lbtt-user/bin/t-2
|
|
Parameters = "-x -y 3 -v 0" # parameters to be passed to the
|
|
# executable
|
|
Enabled = Yes
|
|
@}
|
|
|
|
GlobalOptions
|
|
@{
|
|
Rounds = 100 # 100 test rounds
|
|
|
|
Interactive = OnError,OnBreak # pause testing in case of an error
|
|
# or when receiving a break signal
|
|
|
|
Verbosity = 1 # show only numeric statistics
|
|
|
|
ComparisonTest = Yes # enable all tests except the
|
|
ConsistencyTest = Yes # B@"uchi automata intersection
|
|
IntersectionTest = No # emptiness test
|
|
|
|
ModelCheck = Local # perform the tests only in a
|
|
# single state of each state
|
|
# space
|
|
|
|
TranslatorTimeout = 30s # abort the execution of a
|
|
# translator if it fails to give
|
|
# a result in 30 seconds
|
|
@}
|
|
|
|
FormulaOptions
|
|
@{
|
|
AbbreviatedOperators = Yes # formula generation mode
|
|
GenerateMode = Normal
|
|
OutputMode = NNF # rewrite formulas in negation
|
|
# normal form before passing
|
|
# them to the translators
|
|
|
|
ChangeInterval = 1 # new formula after each round
|
|
|
|
RandomSeed = 4632912 # random seed
|
|
|
|
Size = 5-15 # 5 to 15 nodes in the parse
|
|
# tree of each formula
|
|
|
|
Propositions = 3 # allow at most three different
|
|
# propositions in each LTL formula
|
|
|
|
PropositionPriority = 50 # priorities for propositional
|
|
TruePriority = 1 # symbols
|
|
FalsePriority = 1
|
|
|
|
AndPriority = 10 # priorities for some logical
|
|
OrPriority = 10 # operators
|
|
NotPriority = 10
|
|
EquivalencePriority = 5
|
|
|
|
NextPriority = 5 # priorities for some temporal
|
|
UntilPriority = 5 # operators
|
|
ReleasePriority = 5
|
|
FinallyPriority = 2
|
|
|
|
DefaultOperatorPriority = 0 # disable all the remaining
|
|
# operators
|
|
@}
|
|
|
|
StatespaceOptions
|
|
@{
|
|
GenerateMode = RandomGraph # generate random (not
|
|
# necessarily connected) graphs
|
|
# as state spaces
|
|
|
|
ChangeInterval = 10 # new state space after every
|
|
# 10th test round
|
|
|
|
RandomSeed = 37620 # random seed
|
|
|
|
Size = 50 # 50 states in each state space
|
|
|
|
Propositions = 3 # three propositions in each
|
|
# state of each state space
|
|
|
|
EdgeProbability = 0.1 # approximate probability of
|
|
# having a transition between
|
|
# any two states
|
|
|
|
TruthProbability = 0.5 # probability with which any
|
|
# atomic proposition is true in
|
|
# a state
|
|
@}
|
|
@end smallexample
|
|
|
|
|
|
@node Command line options, , Configuration file, Invocation
|
|
@section Command line options
|
|
|
|
This section lists the command line options that may be used when
|
|
invoking @command{lbtt}. The command line options are processed only
|
|
after reading the configuration file, so they can be used to override the
|
|
settings given in the file. There are also a few options for which
|
|
there is no direct equivalent in the configuration file options.
|
|
|
|
@menu
|
|
* Special options:: Options available only as command line
|
|
parameters.
|
|
* Global options:: Options corresponding to the
|
|
@samp{GlobalOptions} section of the
|
|
configuration file.
|
|
* LTL formula options:: Options corresponding to the
|
|
@samp{FormulaOptions} section of the
|
|
configuration file.
|
|
* State space options:: Options corresponding to the
|
|
@samp{StateSpaceOptions} section of the
|
|
configuration file.
|
|
@end menu
|
|
|
|
|
|
|
|
@node Special options, Global options, Command line options, Command line options
|
|
@subsection Special options
|
|
|
|
The following list presents all command line options for which there is
|
|
no (directly) corresponding option that may be set in the program
|
|
configuration file.
|
|
|
|
@table @samp
|
|
@item --configfile=@var{FILE-NAME}
|
|
@cindex configuration file, changing the name of
|
|
@vindex --configfile
|
|
This option can be used to instruct @command{lbtt} to read program
|
|
configuration from another file instead of the default configuration
|
|
file @samp{config} in the current working directory.
|
|
|
|
@item @anchor{--formulafile}--formulafile=@var{FILE-NAME}
|
|
@vindex --formulafile
|
|
@cindex LTL formula, reading from a file or standard input
|
|
@cindex file formats, formula input file for @command{lbtt}
|
|
This option instructs @command{lbtt} to read the LTL formulas used in the tests
|
|
from a file (or standard input) instead of generating them randomly. The
|
|
special filename @samp{-} refers to standard input. Each
|
|
input formula should be followed by a newline. The formulas can be specified
|
|
either in @command{lbtt}'s own prefix notation
|
|
(@pxref{Format for LTL formulas}; also the infix notation used in output
|
|
messages is supported) or in a variety of formats found in
|
|
some LTL-to-B@"uchi translator implementations (Spin, LTL2BA, LTL2AUT,
|
|
Temporal Massage Parlor, Wring, Spot, LBT), however with the restriction that
|
|
all atomic propositions should have names of the form
|
|
@samp{p@var{N}} for some nonnegative integer @var{N}.
|
|
|
|
@cindex operators, precedence in input files
|
|
(When using one of the alternative
|
|
formats, it is recommended to use parentheses to avoid possible ambiguities in
|
|
the precedence and associativity of the various operators; in @command{lbtt},
|
|
the unary operators have the highest precedence, @samp{/\} has higher
|
|
precedence than @samp{\/}, which in turn has higher precedence than any of
|
|
@samp{->}, @samp{<->} or @samp{xor}, and the binary temporal operators have
|
|
the lowest precedence. All binary logical operators are left-associative;
|
|
all binary temporal operators are nonassociative.)
|
|
|
|
If this option is used, all command line or configuration file parameters
|
|
affecting the generation of random LTL formulas (excluding their mode of
|
|
output) are ignored.
|
|
|
|
@item --h
|
|
@itemx --help
|
|
@vindex -h
|
|
@vindex --help
|
|
These options list all the available command line parameters.
|
|
|
|
@item @anchor{--logfile}--logfile=@var{FILE-NAME}
|
|
@vindex --logfile
|
|
@cindex log file for test failures
|
|
@cindex using a test failure log file
|
|
This option instructs @command{lbtt} to create a log of all errors
|
|
encountered during testing. By default no log will be created.
|
|
|
|
@item --profile
|
|
@vindex --profile
|
|
@cindex tests, enabling and disabling
|
|
@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.
|
|
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.
|
|
|
|
@item --quiet
|
|
@itemx --silent
|
|
@vindex --quiet
|
|
@vindex --silent
|
|
@cindex suppressing output
|
|
These options suppress any messages that are normally displayed during
|
|
testing. Use the @samp{--logfile} option (see
|
|
above) with these options to save a test failure report into a log file.
|
|
|
|
@item @anchor{--showconfig}--showconfig
|
|
@vindex --showconfig
|
|
If this option is present on the command line, @command{lbtt} will
|
|
write the current configuration to standard output
|
|
(@pxref{Configuration information}) and then exit.
|
|
This option can be used together with the @samp{--configfile} option to
|
|
test the settings defined in a configuration file without actually performing
|
|
any tests.
|
|
|
|
@item @anchor{--showoperatordistribution}--showoperatordistribution
|
|
@vindex --showoperatordistribution
|
|
@cindex operators, computing distribution for
|
|
@cindex random LTL formula, computing operator distribution
|
|
With this option @command{lbtt} uses the priorities defined for the
|
|
LTL formula operators available for random LTL formula generation to compute
|
|
the expected number of occurrences of each operator in a single randomly
|
|
generated formula. The distribution is then displayed along with other
|
|
configuration information when the program starts.
|
|
|
|
@item @anchor{--skip}--skip=@var{NUMBER-OF-ROUNDS}
|
|
@vindex --skip
|
|
@cindex tests, skipping test rounds
|
|
@cindex skipping test rounds
|
|
This option can be used to skip the first @var{NUMBER-OF-ROUNDS} test rounds,
|
|
i.e., begin testing from round @var{NUMBER-OF-ROUNDS}+1.
|
|
|
|
@item -V
|
|
@itemx --version
|
|
@vindex -V
|
|
@vindex --version
|
|
This option displays the version of the @command{lbtt} executable.
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node Global options, LTL formula options, Special options, Command line options
|
|
@subsection Global options
|
|
|
|
The following list presents the options that can be used to override the
|
|
values specified in the @samp{GlobalOptions} section of the configuration
|
|
file.
|
|
|
|
@table @samp
|
|
@item --comparisontest@r{[}=yes | no@r{]}
|
|
@itemx --nocomparisontest
|
|
@cindex tests, enabling and disabling
|
|
@cindex enabling and disabling tests
|
|
@vindex --comparisontest
|
|
@vindex --nocomparisontest
|
|
These options enable or disable the model checking result cross-comparison
|
|
test (@pxref{Model checking result cross-comparison test}).
|
|
|
|
@item --consistencytest@r{[}=yes | no@r{]}
|
|
@itemx --noconsistencytest
|
|
@cindex tests, enabling and disabling
|
|
@cindex enabling and disabling tests
|
|
@vindex --consistencytest
|
|
@vindex --noconsistencytest
|
|
These options enable or disable the model checking result consistency check
|
|
(@pxref{Model checking result consistency check}).
|
|
|
|
@item --disable=@var{IMPLEMENTATION-ID}@r{[},@var{IMPLEMENTATION-ID}@r{...]}
|
|
@cindex disabling LTL-to-B@"uchi translators
|
|
@cindex LTL-to-B@"uchi translators, disabling
|
|
@vindex --disable
|
|
This option can be used to exclude some implementations from the tests by
|
|
specifying a comma-separated list of implementation names or their numeric
|
|
identifiers. (The implementations are numbered in the order in which they
|
|
appear in the configuration file, starting from zero. Use the
|
|
@samp{--showconfig} option, see @ref{Special options}, to obtain a list of the
|
|
implementations specified in the configuration file, together with their
|
|
identifiers.)
|
|
|
|
@item --enable=@var{IMPLEMENTATION-ID}@r{[},@var{IMPLEMENTATION-ID}@r{...]}
|
|
@cindex enabling LTL-to-B@"uchi translators
|
|
@cindex LTL-to-B@"uchi translators, enabling
|
|
@vindex --enable
|
|
This option can be used to include implementations into the tests (in the
|
|
case they are initially disabled in the configuration file).
|
|
|
|
@item --globalmodelcheck
|
|
@vindex --globalmodelcheck
|
|
@cindex model checking modes
|
|
@cindex global model checking
|
|
This option instructs @command{lbtt} to perform model checking globally
|
|
(with respect to all states of each random state space) in the model
|
|
checking result cross-comparison test and the model checking result
|
|
consistency check. Using a global check increases the number of possible
|
|
tests.
|
|
|
|
@item --interactive@r{[}=@var{MODE-LIST}@r{]}
|
|
@itemx --pause@r{[}=@var{MODE-LIST}@r{]}
|
|
@vindex --interactive
|
|
@cindex interactivity modes
|
|
These options can be used to override whether @command{lbtt} should pause
|
|
between test rounds to wait for user input. The optional @var{MODE-LIST} is a
|
|
comma-separated list of interactivity modes (@samp{Always}, @samp{OnError},
|
|
@samp{Never}, @samp{OnBreak}) with no spaces in between
|
|
(@pxref{Interactivity modes}, for the mode descriptions). If omitted, the
|
|
mode list defaults to @samp{Always}.
|
|
|
|
@item --intersectiontest@r{[}=yes | no@r{]}
|
|
@itemx --nointersectiontest
|
|
@cindex tests, enabling and disabling
|
|
@cindex enabling and disabling tests
|
|
@vindex --intersectiontest
|
|
@vindex --nointersectiontest
|
|
These options enable or disable the B@"uchi automata intersection emptiness
|
|
check (@pxref{Automata intersection emptiness check}).
|
|
|
|
@item --localmodelcheck
|
|
@vindex --localmodelcheck
|
|
@cindex model checking modes
|
|
@cindex local model checking
|
|
This option instructs @command{lbtt} to perform model checking only with
|
|
respect to a single state of each random state space in the model checking
|
|
result cross-comparison test and the model checking result consistency
|
|
check.
|
|
|
|
@item --modelcheck=global | local
|
|
@vindex --modelcheck
|
|
@cindex model checking modes
|
|
@cindex local model checking
|
|
@cindex global model checking
|
|
This option can be used to select the model checking mode.
|
|
|
|
@item --pause@r{[}=@var{MODE-LIST}@r{]}
|
|
@vindex --pause
|
|
See @samp{--interactive}.
|
|
|
|
@item --rounds=@var{NUMBER-OF-ROUNDS}
|
|
@vindex --rounds
|
|
This option can be used to override the number of test rounds to run.
|
|
|
|
@item --translatortimeout=@var{TIME-SPECIFICATION}
|
|
@vindex --translatortimeout
|
|
This option can be used to override the running time limit (in wall-clock
|
|
time) for translators (@pxref{Timeouts}, for more information).
|
|
|
|
@item --verbosity=@var{INTEGER}
|
|
@vindex --verbosity
|
|
@cindex verbosity, changing
|
|
@cindex changing verbosity of output
|
|
This option sets the verbosity of output messages. The value must be
|
|
between 0 and 5 (inclusive).
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node LTL formula options, State space options, Global options, Command line options
|
|
@subsection LTL formula options
|
|
|
|
The following command line options can be used to control the behavior of
|
|
@command{lbtt}'s random LTL formula generation algorithm. They correspond
|
|
to the options available in the @samp{FormulaOptions} section of the
|
|
configuration file.
|
|
|
|
@cindex parameters for random LTL formula generation algorithm
|
|
@cindex random LTL formula, parameters for generation algorithm
|
|
@cindex LTL formula, parameters for generation algorithm
|
|
@cindex priorities for formula constants, atomic propositions and operators
|
|
@cindex atomic propositions, priorities for
|
|
@cindex constants, priorities for
|
|
@cindex operators, priorities for
|
|
|
|
@table @samp
|
|
@item --abbreviatedoperators@r{[}=yes | no@r{]}
|
|
@itemx --noabbreviatedoperators
|
|
@vindex --abbreviatedoperators
|
|
@vindex --noabbreviatedoperators
|
|
@cindex abbreviated LTL formula operators
|
|
@cindex LTL formula operators, abbreviated
|
|
@cindex operators, abbreviated
|
|
These options can be used to allow or prevent @command{lbtt} from using any of
|
|
the ``abbreviated'' operators (@samp{->}, @samp{<->}, @samp{xor}, @samp{W},
|
|
@samp{<>}, @samp{B}, @samp{M} and @samp{[]}) when generating random LTL
|
|
formulas.
|
|
|
|
@item --andpriority
|
|
@vindex --andpriority
|
|
This option sets the priority for logical conjunction (the @samp{/\} operator).
|
|
|
|
@item --beforepriority
|
|
@vindex --beforepriority
|
|
This option sets the priority for the temporal ``before'' operator
|
|
(@samp{B}).
|
|
|
|
@item --defaultoperatorpriority
|
|
@vindex --defaultoperatorpriority
|
|
@cindex default operator priority
|
|
This option sets the default priority for all logical and temporal operators.
|
|
|
|
@item --equivalencepriority
|
|
@vindex --equivalencepriority
|
|
This option sets the priority for logical equivalence (the @samp{<->}
|
|
operator).
|
|
|
|
@item --falsepriority
|
|
@vindex --falsepriority
|
|
This option sets the priority for the Boolean constant @samp{false}.
|
|
|
|
@item --finallypriority
|
|
@vindex --finallypriority
|
|
This option sets the priority for the temporal ``finally'' operator
|
|
(@samp{<>}).
|
|
|
|
@item --formulachangeinterval=@var{NUMBER-OF-ROUNDS}
|
|
@vindex --formulachangeinterval
|
|
This option determines how often (in number of test rounds)
|
|
@command{lbtt} should generate a new random LTL formula. A value of 0 forces
|
|
@command{lbtt} to use a fixed LTL formula for all tests.
|
|
|
|
@item --formulageneratemode=normal | nnf
|
|
@vindex --formulageneratemode
|
|
@cindex random LTL formula, generation modes
|
|
@cindex negation normal form
|
|
This option can be used to choose how @command{lbtt} should generate random
|
|
LTL formulas. With the option @samp{--formulageneratemode=nnf}, all generated
|
|
formulas will be in (a weakened) negation normal form in which all negations in
|
|
the formula (if any) precede atomic propositions. (Note that the formulas may
|
|
still contain some of the ``abbreviated'' operators if their priorities are
|
|
not explicitly set to zero.)
|
|
|
|
@item --formulaoutputmode=normal | nnf
|
|
@vindex --formulaoutputmode
|
|
@cindex random LTL formula, output modes
|
|
@cindex LTL formula, output modes
|
|
@cindex negation normal form
|
|
This option can be used to force or prevent @command{lbtt} from converting each
|
|
LTL formula into (strict) negation normal form (i.e., rewriting it with the
|
|
operators @samp{!}, @samp{/\}, @samp{\/}, @samp{U} and @samp{V}) before passing
|
|
it to the LTL-to-B@"uchi translators.
|
|
|
|
@item --formulapropositions
|
|
@vindex --formulapropositions
|
|
This option sets the maximum number of different atomic propositions that
|
|
@command{lbtt} may use for generating random LTL formulas.
|
|
|
|
@item --formularandomseed=@var{INTEGER}
|
|
@cindex random seed, LTL formula generation algorithm
|
|
@vindex --formularandomseed
|
|
This option gives a seed value for generating random numbers used by the
|
|
random LTL formula generation algorithm.
|
|
|
|
@item --formulasize=@var{INTEGER}
|
|
@itemx --formulasize=@var{MINIMUM-SIZE}-@var{MAXIMUM-SIZE}
|
|
@itemx --formulasize=@var{MINIMUM-SIZE}...@var{MAXIMUM-SIZE}
|
|
@vindex --formulasize
|
|
This option sets the size of the random LTL formulas generated for the tests.
|
|
The size can be given either as a fixed integer or as an interval, in which
|
|
case the size of each generated formula will be chosen randomly in the
|
|
interval using a uniform random distribution.
|
|
|
|
@item --generatennf
|
|
@itemx --nogeneratennf
|
|
@vindex --generatennf
|
|
@vindex --nogeneratennf
|
|
@cindex random LTL formula, generation modes
|
|
@cindex negation normal form
|
|
These options can be used instead of the @samp{--formulageneratemode} option
|
|
to select the random formula generation mode.
|
|
|
|
@item --globallypriority
|
|
@vindex --globallypriority
|
|
This option sets the priority for the temporal ``globally'' operator
|
|
(@samp{[]}).
|
|
|
|
@item --implicationpriority
|
|
@vindex --implicationpriority
|
|
This option sets the priority for logical implication (the @samp{->} operator).
|
|
|
|
@item --nextpriority
|
|
@vindex --nextpriority
|
|
This option sets the priority for the temporal ``next time'' operator
|
|
(@samp{X}).
|
|
|
|
@item --notpriority
|
|
@vindex --notpriority
|
|
This option sets the priority for logical negation (the @samp{!} operator).
|
|
|
|
@item --orpriority
|
|
@vindex --orpriority
|
|
This option sets the priority for logical disjunction (the @samp{\/} operator).
|
|
|
|
@item --outputnnf
|
|
@itemx --nooutputnnf
|
|
@vindex --outputnnf
|
|
@vindex --nooutputnnf
|
|
@cindex random LTL formula, output modes
|
|
@cindex LTL formula, output modes
|
|
@cindex negation normal form
|
|
These options can be used instead of the @samp{--formulaoutputmode} option to
|
|
choose the format in which @command{lbtt} passes LTL formulas to LTL-to-B@"uchi
|
|
translators.
|
|
|
|
@item --propositionpriority
|
|
@vindex --propositionpriority
|
|
This option sets the priority for atomic propositions.
|
|
|
|
@item --releasepriority
|
|
@vindex --releasepriority
|
|
This option sets the priority for the temporal ``(weak) release'' operator
|
|
(@samp{V}).
|
|
|
|
@item --strongreleasepriority
|
|
@vindex --strongreleasepriority
|
|
This option sets the priority for the temporal ``strong release'' operator
|
|
(@samp{M}).
|
|
|
|
@item --truepriority
|
|
@vindex --truepriority
|
|
This option sets the priority for the Boolean constant
|
|
@iftex
|
|
@tex
|
|
\sc{True}.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{true}.
|
|
@end ifnottex
|
|
|
|
@item --untilpriority
|
|
@vindex --untilpriority
|
|
This option sets the priority for the temporal ``(strong) until'' operator
|
|
(@samp{U}).
|
|
|
|
@item --weakuntilpriority
|
|
@vindex --weakuntilpriority
|
|
This option sets the priority for the temporal ``weak until'' operator
|
|
(@samp{W}).
|
|
|
|
@item --xorpriority
|
|
@vindex --xorpriority
|
|
This option sets the priority for the logical ``exclusive or'' operator.
|
|
|
|
@end table
|
|
|
|
Note also the @samp{--formulafile=@var{FILE-NAME}} option
|
|
(@pxref{--formulafile,,@samp{--formulafile} option}), which can be used to
|
|
instruct @command{lbtt} to read LTL formulas from a file (or standard input)
|
|
instead of generating them randomly.
|
|
|
|
|
|
|
|
@node State space options, , LTL formula options, Command line options
|
|
@subsection State space options
|
|
|
|
The following command line options affect the way in which @command{lbtt}
|
|
generates state spaces that are then used in the model checking tests. They
|
|
correspond to options in the @samp{StateSpaceOptions} section of the
|
|
configuration file. See also @ref{Random state spaces}, for more information
|
|
about the graph generation modes.
|
|
|
|
@cindex parameters for random state space generation algorithm
|
|
@cindex state space, generation parameters
|
|
@cindex random state space, generation parameters
|
|
|
|
@table @samp
|
|
@item --edgeprobability=@var{PROBABILITY}
|
|
@vindex --edgeprobability
|
|
This option sets the approximate random edge probability for state spaces. (The
|
|
option has no effect if the generated state spaces are random or enumerated
|
|
paths.)
|
|
|
|
@item --enumeratedpath
|
|
@vindex --enumeratedpath
|
|
@cindex state space, generation modes
|
|
@cindex enumerated path
|
|
This option instructs @command{lbtt} to enumerate all paths of a given size
|
|
as state spaces instead of generating random state spaces for model checking
|
|
tests. The option also enables @command{lbtt}'s internal model checking
|
|
algorithm.
|
|
|
|
@item --randomconnectedgraph
|
|
@vindex --randomconnectedgraph
|
|
@cindex state space, generation modes
|
|
@cindex random connected graph
|
|
This option makes @command{lbtt} generate random connected graphs as state
|
|
spaces for model checking tests.
|
|
|
|
@item --randomgraph
|
|
@vindex --randomgraph
|
|
@cindex state space, generation modes
|
|
@cindex random graph
|
|
This option makes @command{lbtt} generate random graphs as state spaces for
|
|
model checking tests.
|
|
|
|
@item --randompath
|
|
@vindex --randompath
|
|
@cindex state space, generation modes
|
|
@cindex random path
|
|
This option forces @command{lbtt} to generate random paths as state spaces.
|
|
The option also enables @command{lbtt}'s internal model checking algorithm
|
|
in the model checking tests.
|
|
|
|
@item --statespacechangeinterval=@var{NUMBER-OF-ROUNDS}
|
|
@vindex --statespacechangeinterval
|
|
This option sets the frequency (in test rounds) in which new state spaces
|
|
are generated. A value of 0 forces @command{lbtt} to use a fixed state space
|
|
for all tests.
|
|
|
|
@item --statespacegeneratemode=randomconnectedgraph | randomgraph | randompath | enumeratedpath
|
|
@vindex --statespacegeneratemode
|
|
@cindex state space, generation modes
|
|
@cindex enumerated path
|
|
@cindex random connected graph
|
|
@cindex random graph
|
|
@cindex random path
|
|
This option can be used instead of one of the four options above to select
|
|
the state space generation mode.
|
|
|
|
@item --statespacerandomseed=@var{INTEGER}
|
|
@vindex --statespacerandomseed
|
|
@cindex random state space, random seed for generation algorithm
|
|
This option gives a seed value for generating random numbers required by the
|
|
random state space generation algorithm.
|
|
|
|
@item --statespacesize=@var{INTEGER}
|
|
@itemx --statespacesize=@var{MINIMUM-SIZE}-@var{MAXIMUM-SIZE}
|
|
@itemx --statespacesize=@var{MINIMUM-SIZE}...@var{MAXIMUM-SIZE}
|
|
@vindex --statespacesize
|
|
This option can be used to change the size of the generated state spaces.
|
|
|
|
@item --truthprobability=@var{PROBABILITY}
|
|
@vindex --truthprobability
|
|
This option sets the probability that @command{lbtt} uses for choosing the
|
|
valuation for each atomic proposition in each state of the randomly generated
|
|
state spaces. (This option has no effect if using enumerated paths as state
|
|
spaces.)
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node Interpreting the output, Analyzing test results, Invocation, Top
|
|
@chapter Interpreting the output
|
|
|
|
This chapter briefly introduces the most typical messages that
|
|
@command{lbtt} outputs during testing. Most of the examples in this section
|
|
illustrate the output when @command{lbtt} is running in its default output
|
|
verbosity mode (3). In lower verbosity modes some (or in verbosity mode 0, all)
|
|
of these messages will be suppressed; in higher verbosity modes, some
|
|
additional information about @command{lbtt}'s internal behavior is shown.
|
|
|
|
@menu
|
|
* Configuration information:: The current configuration is shown
|
|
before starting tests.
|
|
* Test round messages:: Conventions for reporting test
|
|
results and test failures.
|
|
* Test statistics:: Shown at the end of testing.
|
|
@end menu
|
|
|
|
|
|
@node Configuration information, Test round messages, Interpreting the output, Interpreting the output
|
|
@section Configuration information
|
|
|
|
@cindex configuration information
|
|
|
|
Before starting tests, @command{lbtt} outputs (in verbosity modes 2 and above)
|
|
a summary of the current
|
|
program configuration as obtained by reading the program configuration file
|
|
and interpreting the command line parameters. The same summary can be
|
|
obtained without running any tests by using the
|
|
@samp{--showconfig} command line option
|
|
(@pxref{--showconfig,,@samp{--showconfig} option}). The information will be
|
|
written also to the error log file if one was specified in the command line
|
|
with the @samp{--logfile} option
|
|
(@pxref{--logfile,,@samp{--logfile} option}).
|
|
The summary consists of the following information:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
LTL-to-B@"uchi translator implementations enabled for testing.
|
|
|
|
@item
|
|
List of enabled tests.
|
|
|
|
@item
|
|
Random state space generation parameters.
|
|
|
|
@item
|
|
Random LTL formula generation parameters (unless reading LTL formulas from
|
|
an external source; @pxref{--formulafile,,@samp{--formulafile} command line
|
|
option}). This includes information about all enabled formula operators and
|
|
their priorities. When using the command line option
|
|
@samp{--showoperatordistribution}
|
|
(@pxref{--showoperatordistribution,,@samp{--showoperatordistribution} option}),
|
|
@command{lbtt} shows also the expected number of occurrence of each
|
|
operator in each randomly generated formula.
|
|
|
|
@end itemize
|
|
|
|
@noindent
|
|
Example:
|
|
|
|
@smallexample
|
|
Program configuration:
|
|
----------------------
|
|
|
|
1000 test rounds.
|
|
Testing will be interrupted in case of an error.
|
|
Signalling a break will interrupt testing.
|
|
Using global model checking for tests.
|
|
Writing error log to `error.log'.
|
|
|
|
Implementations:
|
|
0: `Implementation 0'
|
|
1: `Implementation 1'
|
|
|
|
Timeout for translators is set to 30 seconds.
|
|
|
|
Enabled tests:
|
|
Model checking result cross-comparison test
|
|
Model checking result consistency check
|
|
B@"uchi automata intersection emptiness check
|
|
|
|
Random state spaces:
|
|
Random graphs (50 states, 5 atomic propositions)
|
|
New state space will be generated after every 5th round.
|
|
Random seed: 98
|
|
Random edge probability: 0.10
|
|
Propositional truth probability: 0.50
|
|
|
|
Random LTL formulas:
|
|
5 parse tree nodes, 5 atomic propositions
|
|
New LTL formula will be generated after every round.
|
|
Random seed: 17991
|
|
Atomic symbols in use (priority):
|
|
false (5); propositions (90); true (5)
|
|
Operators used for random LTL formula generation:
|
|
operator ! /\ U V X \/
|
|
priority 10 10 20 20 10 20
|
|
|
|
@end smallexample
|
|
|
|
@node Test round messages, Test statistics, Configuration information, Interpreting the output
|
|
@section Test round messages
|
|
|
|
In verbosity modes 1 and 2, @command{lbtt} reports numeric statistics on the
|
|
generated automata in tabular form. Each row of this table contains the
|
|
following information (in this order):
|
|
@itemize
|
|
@item
|
|
number of the current test round (verbosity mode 1 only);
|
|
@item
|
|
numeric identifier of an implementation;
|
|
@item
|
|
formula identifier (@samp{+} or @samp{-});
|
|
@item
|
|
time consumed when generating an automaton from the formula using the
|
|
implementation;
|
|
@item
|
|
number of states, transitions and acceptance conditions in the automaton;
|
|
@item
|
|
number of states and transitions in the product automaton
|
|
@item
|
|
number of accepting cycles in the state space (see below), and
|
|
@item
|
|
result of the consistency check (verbosity mode 2 only).
|
|
@end itemize
|
|
|
|
The following example shows a fragment of the output that @command{lbtt} might
|
|
produce during a test round when running in the default verbosity mode 3.
|
|
|
|
@cindex tests, output example
|
|
|
|
@smallformat
|
|
1. @t{Round 6 of 10}
|
|
|
|
2. @t{ Generating random state space}
|
|
|
|
3. @t{ Random LTL formula:}
|
|
@r{ }@t{ formula: ((p1 <-> p0) U (p0 \/ ! p3))}
|
|
@r{ }@t{ negated formula: ! ((p1 <-> p0) U (p0 \/ ! p3))}
|
|
|
|
@r{ }@t{ 0: `Implementation 0'}
|
|
@r{ }@t{ Positive formula:}
|
|
4. @t{ B@"uchi automaton:}
|
|
@r{ }@t{ number of states: 6}
|
|
@r{ }@t{ number of transitions: 15}
|
|
@r{ }@t{ acceptance sets: 1}
|
|
@r{ }@t{ computation time: 0.03 seconds (user time)}
|
|
5. @t{ Product automaton:}
|
|
@r{ }@t{ number of states: 582 [97.00% of worst case (600)]}
|
|
@r{ }@t{ number of transitions: 7188}
|
|
6. @t{ Accepting cycles:}
|
|
@r{ }@t{ cycle reachable from 0 states}
|
|
@r{ }@t{ not reachable from 100 states}
|
|
7. @t{ Negated formula:}
|
|
@r{ }@t{ B@"uchi automaton:}
|
|
@r{ }@t{ number of states: 4}
|
|
@r{ }@t{ number of transitions: 6}
|
|
@r{ }@t{ acceptance sets: 0}
|
|
@r{ }@t{ computation time: 0.04 seconds (user time)}
|
|
@r{ }@t{ Product automaton:}
|
|
@r{ }@t{ number of states: 363 [90.75% of worst case (400)]}
|
|
@r{ }@t{ number of transitions: 2581}
|
|
@r{ }@t{ Accepting cycles:}
|
|
@r{ }@t{ cycle reachable from 25 states}
|
|
@r{ }@t{ not reachable from 75 states}
|
|
8. @t{ Result consistency check:}
|
|
@r{ }@t{ result: failed [75 (75.00%) of 100 test cases]}
|
|
@end smallformat
|
|
|
|
@noindent
|
|
The numbered parts of the output are:
|
|
|
|
@enumerate
|
|
@item
|
|
Number of the test round.
|
|
|
|
@item
|
|
@command{lbtt} generates a new random state space for model
|
|
checking tests. (In this case the size of the state spaces was fixed in the
|
|
configuration; if the state space size is allowed to vary in an interval,
|
|
@command{lbtt} would also show here the actual size of the generated state
|
|
space.)
|
|
|
|
@item
|
|
@cindex operators, precedence in output messages
|
|
Information about a random LTL formula and its negation. To simplify the
|
|
notation, it is assumed that all unary formula operators have higher
|
|
precedence than binary operators.
|
|
|
|
@item
|
|
Information about the B@"uchi automaton that `Implementation 0' generated
|
|
from the positive LTL formula (number of states, transitions and acceptance
|
|
conditions, and the amount of user time elapsed in generating the automaton).
|
|
|
|
@item
|
|
Information about the synchronous product of the state space and the
|
|
B@"uchi automaton constructed from the positive formula.
|
|
|
|
@item
|
|
Model checking result information. In this case, the automaton cannot reach
|
|
an ``accepting cycle'' regardless of the state of the state space in which
|
|
the automaton could begin its execution. In other words, the random state
|
|
space contains no states with an infinite path beginning from the state such
|
|
that the B@"uchi automaton accepts the temporal interpretation of the path
|
|
(the infinite sequence of state labels on the path).
|
|
|
|
@item
|
|
The model checking process is repeated using the negated formula as
|
|
input for the LTL-to-B@"uchi translator `Implementation 0'.
|
|
|
|
@item
|
|
@command{lbtt} performs the model checking result consistency check
|
|
(@pxref{Model checking result consistency check}) using the model checking
|
|
results computed for the positive and the negative formula. In this example,
|
|
the result consistency check fails in 75 states of the state space. This
|
|
implies that `Implementation 0' failed to translate one (or both)
|
|
of the formulas into a B@"uchi automaton correctly.
|
|
|
|
@end enumerate
|
|
|
|
The output of phases 4---8 will be repeated for each implementation included in
|
|
the tests. After this @command{lbtt} proceeds to the model checking result
|
|
cross-comparison test (@pxref{Model checking result cross-comparison test}) and
|
|
the B@"uchi automata intersection emptiness test
|
|
(@pxref{Automata intersection emptiness check}).
|
|
|
|
The model checking result cross-comparison test might result in the following
|
|
output (shown in verbosity modes greater than 1):
|
|
|
|
@smallformat
|
|
@t{ Model checking result cross-comparison:}
|
|
@t{ result:}
|
|
@t{ failed (+) 0: `Implementation 0', 1: `Implementation 1'}
|
|
@end smallformat
|
|
|
|
@cindex tests, failure report format
|
|
Throughout all test failure reports, @command{lbtt} refers to the positive and
|
|
negated formulas with the symbols @samp{+} and @samp{-}, respectively.
|
|
Therefore, the above message indicates that the model checking results obtained
|
|
using `Implementation 0' and `Implementation 1' for the positive formula do not
|
|
agree. A similar line will be shown for all pairs of implementations for which
|
|
the test failed.
|
|
|
|
@command{lbtt} also reports if the model checking result cross-comparison could
|
|
not be performed between a pair of implementations (for example, if one of the
|
|
implementations failed to generate an automaton); in this case, the result of
|
|
the test is @samp{N/A}.
|
|
|
|
@cindex internal model checking algorithm
|
|
@cindex tests, against internal model checking algorithm
|
|
If using enumerated or randomly generated paths as state spaces, the model
|
|
checking results are also compared against those given by
|
|
@command{lbtt}'s internal model checking algorithm.
|
|
|
|
A similar convention is used to report failures in the B@"uchi automata
|
|
intersection emptiness check. However, because this test is always performed
|
|
on B@"uchi automata constructed from two complementary LTL formulas, a test
|
|
failure report shows LTL formula information beside the name of the
|
|
implementation used for generating the B@"uchi automaton from that formula.
|
|
Note that the B@"uchi automata intersection emptiness check may fail on the
|
|
automata constructed by the same implementation; in the following example,
|
|
the check failed between the automata constructed by `Implementation 0', and
|
|
the automata constructed by `Implementation 0' and `Implementation 1' from
|
|
the positive and negative formulas, respectively.
|
|
|
|
@smallformat
|
|
@t{ B@"uchi automata intersection emptiness check:}
|
|
@t{ result:}
|
|
@t{ failed 0: `Implementation 0'}
|
|
@t{ failed (+) 0: `Implementation 0', (-) 1: `Implementation 1'}
|
|
@end smallformat
|
|
|
|
If using a log file (@pxref{--logfile,,@samp{--logfile} command line option}),
|
|
a summary of all testing errors will be written to the file using the output
|
|
format specified above.
|
|
|
|
|
|
|
|
|
|
|
|
@node Test statistics, , Test round messages, Interpreting the output
|
|
@section Test statistics
|
|
|
|
@cindex tests, statistics
|
|
|
|
At the end of testing, @command{lbtt} outputs some simple statistics computed
|
|
over all tests in verbosity modes 2 and above. If using an error log file
|
|
(@pxref{--logfile,,@samp{--logfile} command line option}), the statistics
|
|
will be stored also in the log file. These statistics can be also accessed
|
|
during interactive testing by using the internal command @samp{statistics}
|
|
(@pxref{statistics,,@samp{statistics} command}).
|
|
In brief, the statistics include:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
Number of generated state spaces and the total number of states and
|
|
transitions in them.
|
|
|
|
@item
|
|
@cindex operators, computing distribution for
|
|
Number of processed LTL formulas (not counting the negations of each
|
|
formula). If using random formulas, @command{lbtt} also shows the overall
|
|
distribution of each individual proposition, Boolean constant and logical
|
|
or temporal operator in the sample of randomly generated formulas.
|
|
Theoretically, in a large sample of random formulas, this distribution
|
|
should correspond to the one that can be computed before testing by using the
|
|
@samp{--showoperatordistribution} command line option
|
|
(@pxref{--showoperatordistribution,,@samp{--showoperatordistribution} command line option}).
|
|
|
|
@item
|
|
Automata statistics for each implementation:
|
|
|
|
@itemize @minus
|
|
@item
|
|
number of generated B@"uchi automata and product automata
|
|
|
|
@item
|
|
total and average numbers of states, transitions and acceptance sets in the
|
|
generated B@"uchi/product automata, and
|
|
|
|
@item
|
|
total and average time consumed in generating the B@"uchi automata.
|
|
@end itemize
|
|
|
|
@item
|
|
Number of times that each implementation failed to generate an acceptable
|
|
automaton from an input formula.
|
|
|
|
@item
|
|
Number of failures in the model checking result consistency check
|
|
(@pxref{Model checking result consistency check}) for each implementation.
|
|
|
|
@item
|
|
Number of result inconsistencies detected in pairwise comparison of the
|
|
B@"uchi automata generated by different implementations. Depending on
|
|
the model checking mode and which correctness tests are enabled, the
|
|
output may include none, some or all of the following information:
|
|
|
|
@itemize @minus
|
|
@item
|
|
Overall number of failures in the model checking result cross-comparison test
|
|
(@pxref{Model checking result cross-comparison test}) for each pair of
|
|
implementations.
|
|
|
|
@item
|
|
Number of failures in the model checking result cross-comparison test in
|
|
a single fixed state of each generated state space (called the ``initial''
|
|
state of the state space).
|
|
|
|
@item
|
|
Number of failures in the B@"uchi automata intersection emptiness check
|
|
(@pxref{Automata intersection emptiness check}) for each pair of
|
|
implementations.
|
|
@end itemize
|
|
|
|
Note that the pairwise inconsistency results form a symmetric matrix (possibly
|
|
shown in several parts), which means that
|
|
the same information is repeated on both sides of the matrix diagonal.
|
|
|
|
@end itemize
|
|
|
|
@noindent
|
|
Where applicable, the statistics are shown separately for positive, negative
|
|
and all LTL formulas used in the tests.
|
|
|
|
|
|
|
|
|
|
@node Analyzing test results, Interfacing with lbtt, Interpreting the output, Top
|
|
@chapter Analyzing test results
|
|
|
|
This chapter documents how to use @command{lbtt}'s internal commands to
|
|
analyze test results.
|
|
|
|
To use the internal commands, @command{lbtt} must be started in one of its
|
|
interactive modes (@pxref{Interactivity modes}). Depending on the mode,
|
|
@command{lbtt} may occasionally pause (for example, after each test round, or
|
|
when a test failure is detected) between test rounds to wait for user input by
|
|
showing a prompt of the form
|
|
|
|
@smallexample
|
|
** [Round 22 of 1000] >>
|
|
@end smallexample
|
|
|
|
@menu
|
|
* Command conventions:: Conventions for entering commands.
|
|
* Getting help:: Use the @samp{help} command to access
|
|
on-line help.
|
|
* Test control commands:: Commands for continuing testing,
|
|
skipping tests or enabling or disabling
|
|
implementations.
|
|
* Data display commands:: Commands for displaying information
|
|
about B@"uchi automata, state spaces,
|
|
and LTL formulas.
|
|
* Failure analysis commands:: Commands for analyzing test failures.
|
|
@end menu
|
|
|
|
|
|
|
|
@node Command conventions, Getting help, Analyzing test results, Analyzing test results
|
|
@section Command conventions
|
|
|
|
@cindex commands, conventions for entering
|
|
@cindex conventions for entering commands
|
|
|
|
Commands are entered by typing a command name followed by any parameters for
|
|
the command and then pressing @key{ENTER}.
|
|
The command names are case-sensitive. Each parameter should be separated from
|
|
the command name and other parameters with white space.
|
|
|
|
@cindex commands, abbreviating
|
|
Command names can be abbreviated to the shortest prefix that identifies the
|
|
command unambiguously (for example, @samp{h} could be used in place of the
|
|
@samp{help} command).
|
|
|
|
@cindex commands, entering lists of numbers
|
|
Some of the commands expect lists of implementation or state
|
|
identifiers as parameters. The lists can be specified as comma-separated
|
|
numbers (for example, @samp{8}) or intervals (for example, @samp{3-11})
|
|
with no white space between the commas and the numbers or intervals that
|
|
belong to the same list. For example, assuming that the state space used in
|
|
the current test round has at least 23 states, the command
|
|
@samp{statespace -5,8,14-18,22-} would
|
|
display information about all state space states with an identifier less than
|
|
or equal to 5, together with information about state 8, states 14 to 18
|
|
(inclusive) and all states with an identifier greater than or equal to 22. The
|
|
@samp{*} symbol can be used as a shorthand for all identifiers in the
|
|
available range.
|
|
|
|
@command{lbtt} also recognizes the symbolic names of implementations (defined
|
|
in the configuration file) in implementation identifier lists. The names can be
|
|
used in place of the numeric identifiers. Quotes or the escape character
|
|
(@samp{\}) should be used to handle white space in identifiers.
|
|
|
|
@cindex LTL formula, identifiers in commands
|
|
@cindex commands, LTL formula identifiers
|
|
Some of the commands require a formula identifier as a parameter for choosing
|
|
between a positive and a negative LTL formula. The formula identifier
|
|
(@samp{+} for positive formula, @samp{-} for negative formula) must follow
|
|
the command name as the first parameter for the command. If the formula
|
|
identifier is omitted, the positive formula is assumed.
|
|
|
|
@cindex redirecting command output
|
|
@cindex commands, redirecting output
|
|
The output of most commands (excluding the test control commands,
|
|
@pxref{Test control commands}) can be redirected or appended to a file
|
|
by ending the command line with @samp{>filename} or @samp{>>filename},
|
|
respectively.
|
|
|
|
@cindex commands, invoking external programs
|
|
@cindex commands, writing output to a pipe
|
|
Optionally, the output can be handed over to an external program by ending the
|
|
command line with @samp{| @var{command}}, where @var{command} is the command
|
|
line used for invoking the external program.
|
|
For example, the output of the (@command{lbtt}'s internal) command can be piped
|
|
to a pager application if the entire output does not fit on the screen by
|
|
itself. Using the pipe construct without specifying any internal command
|
|
will simply invoke the external program.
|
|
|
|
|
|
|
|
@node Getting help, Test control commands, Command conventions, Analyzing test results
|
|
@section Getting help
|
|
|
|
@cindex commands, getting help
|
|
@kindex help
|
|
Use the @samp{help} command to access on-line help. Typing @samp{help} with
|
|
no parameters shows a list of all available commands, together with
|
|
general conventions for using the commands. The @samp{help} command can be
|
|
optionally given a command name as a parameter to access command-specific
|
|
help.
|
|
|
|
In command-specific help, arguments in angle brackets (@r{<}, @r{>})
|
|
denote obligatory command parameters, while arguments in square brackets
|
|
(@r{[}, @r{]}) are optional. A vertical bar (@r{|}) denotes
|
|
selection between several alternatives. Arguments in double quotes should
|
|
be entered literally (without the quotes themselves).
|
|
|
|
|
|
|
|
@node Test control commands, Data display commands, Getting help, Analyzing test results
|
|
@section Test control commands
|
|
|
|
@cindex commands, test control
|
|
@cindex tests, controlling with user commands
|
|
The following commands can be used to continue or abort testing, skip a number
|
|
of test rounds, enable or disable implementations for testing, and change the
|
|
verbosity of @command{lbtt}'s output messages.
|
|
|
|
@table @samp
|
|
@item continue @r{[}@var{number-of-rounds}@r{]}
|
|
@kindex continue
|
|
Continue testing. If no argument is given, testing will be interrupted again
|
|
when mandated by the current interactivity mode
|
|
(@pxref{Interactivity modes}). The optional argument @var{number-of-rounds}
|
|
can be used to specify a number of rounds to run; testing is then interrupted
|
|
again after the given number of test rounds (or in case of a new
|
|
test failure if mandated by the current interactivity mode).
|
|
|
|
@item disable @r{[}@var{implementation-id-list}@r{]}
|
|
@kindex disable
|
|
@cindex disabling LTL-to-B@"uchi translators
|
|
@cindex LTL-to-B@"uchi translators, disabling
|
|
Disable testing of a list of implementations (all implementations if
|
|
no list of implementations is specified). @command{lbtt} will not include these
|
|
implementations in the tests in subsequent test rounds. (See
|
|
@ref{Command conventions}, for the syntax used for the list of
|
|
implementations.)
|
|
|
|
@item enable @r{[}@var{implementation-id-list}@r{]}
|
|
@kindex enable
|
|
@cindex enabling LTL-to-B@"uchi translators
|
|
@cindex LTL-to-B@"uchi translators, enabling
|
|
Enable testing of a list of implementations.
|
|
|
|
@item quit
|
|
@kindex quit
|
|
@cindex quitting @command{lbtt}
|
|
Display test statistics (@pxref{Test statistics}) over the test rounds
|
|
performed and then abort testing.
|
|
|
|
@item skip @r{[}@var{number-of-rounds}@r{]}
|
|
@kindex skip
|
|
@cindex tests, skipping test rounds
|
|
@cindex skipping test rounds
|
|
Skip a number of test rounds and then return to wait for further user input.
|
|
If not explicitly specified, the number of rounds to skip defaults to 1.
|
|
Use the @samp{--skip} command line option
|
|
(@pxref{--skip,,The @samp{--skip} command line option}) to begin
|
|
testing from another test round than 1.
|
|
|
|
@item verbosity @r{[}@var{verbosity-level}@r{]}
|
|
@kindex verbosity
|
|
@cindex verbosity, changing
|
|
@cindex changing verbosity of output
|
|
Display or change the verbosity of @command{lbtt}'s output messages. If no
|
|
argument is given, show the current verbosity level, otherwise change the
|
|
verbosity setting to the given value. The argument must be an integer between
|
|
0 and 5 (inclusive). (The new value will take effect when testing is resumed.)
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node Data display commands, Failure analysis commands, Test control commands, Analyzing test results
|
|
@section Data display commands
|
|
|
|
The following commands can be used to access test result information and to
|
|
inspect the LTL formulas, B@"uchi automata and the state space used in the
|
|
current test round.
|
|
|
|
@table @samp
|
|
@item algorithms
|
|
@itemx implementations
|
|
@itemx translators
|
|
@kindex algorithms
|
|
@kindex implementations
|
|
@kindex translators
|
|
Show a list of implementations declared in the program configuration file and
|
|
tell whether they are currently enabled for testing. The list also shows the
|
|
numeric identifiers of the implementations.
|
|
|
|
@item buchi @r{[``}+@r{''} @r{|} @r{``}-@r{'']} @r{<}@var{implementation-id}@r{>} @r{[}@var{state-id-list} | @r{``}dot@r{'']}
|
|
@kindex buchi
|
|
Display information about the structure of the B@"uchi automaton generated by
|
|
the implementation @var{implementation-id} from the positive (@samp{+}) or
|
|
negative (@samp{-}) LTL formula used in the current test round. The
|
|
implementation identifier may be optionally followed by a list of state
|
|
identifiers to display specific states of the automaton (see
|
|
@ref{Command conventions}, for details on how the list should be formatted),
|
|
or the keyword @samp{dot} to display the automaton in a format that can be
|
|
given as input for the @samp{dot} tool of the
|
|
@cindex GraphViz
|
|
GraphViz graph visualization package
|
|
@ifnottex
|
|
@ref{[GViz]}
|
|
@end ifnottex
|
|
@iftex
|
|
[GViz]
|
|
@end iftex
|
|
to obtain a graphical representation of the automaton.
|
|
|
|
@item evaluate @r{[``}+@r{''} @r{|} @r{``}-@r{'']} @r{[}@var{implementation-id-list}@r{]} @r{[}@var{state-id-list}@r{]}
|
|
@kindex evaluate
|
|
Display the model checking results for the positive (@samp{+}) or the negative
|
|
(@samp{-}) formula computed using a given set of implementations for
|
|
constructing a B@"uchi automaton from the formula. If no implementation list
|
|
is specified, show the results for all implementations. The implementation
|
|
identifier list may optionally be followed by a list of (state space) state
|
|
identifiers to restrict the output to only a subset of all states. (See
|
|
@ref{Command conventions}, for more information about the format used for the
|
|
lists.)
|
|
|
|
This command can be used to look for states in which the model checking result
|
|
cross-comparison test (@pxref{Model checking result cross-comparison test})
|
|
failed for a pair of implementations. These state identifiers can then be used
|
|
as input for the @samp{resultanalysis} command
|
|
(@pxref{Failure analysis commands}).
|
|
|
|
Note 1: Observe that the model checking results shown do not follow the
|
|
``universal'' semantics of LTL (common in model checking), by which a formula
|
|
is usually considered to
|
|
hold in a set of infinite paths beginning from a state only if @emph{all}
|
|
paths in the set are accepted by the B@"uchi automaton constructed from the
|
|
formula to be model checked. Instead, @command{lbtt} will mark the result
|
|
true if @emph{any} of these paths is accepted by the automaton.
|
|
|
|
Note 2: If using random or enumerated paths as state spaces, @command{lbtt}
|
|
accepts also the identifier @samp{lbtt} in the implementation identifier list.
|
|
This identifier can be used for accessing the model checking results computed
|
|
using @command{lbtt}'s internal model checking algorithm for paths.
|
|
|
|
@item formula @r{[``}+@r{''} @r{|} @r{``}-@r{'']} @r{[``}normal@r{''} @r{|} @r{``}nnf@r{'']}
|
|
@kindex formula
|
|
@cindex LTL formula, displaying with user command
|
|
Display the positive (@samp{+}) or the negative (@samp{-}) LTL formula used
|
|
for tests in the current test round either in the form in which it was
|
|
generated (@samp{normal} -- the default) or in negation normal form
|
|
(@samp{nnf}).
|
|
|
|
@item inconsistencies @r{[}@var{implementation-id-list}@r{]}
|
|
@kindex inconsistencies
|
|
List the state space states in which the model checking result consistency
|
|
check (@pxref{Model checking result consistency check}) failed for each
|
|
implementation in the list (or all implementations if the list is omitted).
|
|
See @ref{Command conventions}, for information on formatting the list.
|
|
The state identifiers can then be used as input for the
|
|
@samp{consistencyanalysis} command (@pxref{Failure analysis commands}).
|
|
|
|
@item results @r{[}@var{implementation-id-list}@r{]}
|
|
@kindex results
|
|
Display test results (in the current test round) for each implementation in the
|
|
list (or all
|
|
implementations if the list is omitted).
|
|
For more information about the output, see @ref{Test round messages}; see
|
|
@ref{Command conventions}, for information on how to specify the
|
|
implementations.
|
|
|
|
@item statespace @r{[}@var{state-id-list} @r{|} @r{``}dot@r{'']}
|
|
@kindex statespace
|
|
@cindex state space, displaying with an user command
|
|
Display information about the structure of the state space used for model
|
|
checking tests in the current test round. The optional @var{state-id-list}
|
|
can be used to display only a part of the whole state space (see
|
|
@ref{Command conventions}, for information on formatting the state list).
|
|
Alternatively, the @samp{dot} keyword can be used to output the state space
|
|
description in a format recognized by the @samp{dot} tool of
|
|
@cindex GraphViz
|
|
the GraphViz graph visualization package
|
|
@ifnottex
|
|
@ref{[GViz]}
|
|
@end ifnottex
|
|
@iftex
|
|
[GViz]
|
|
@end iftex
|
|
that can be used to obtain a graphical representation of the state space.
|
|
|
|
@item @anchor{statistics}statistics
|
|
@kindex statistics
|
|
Display statistics computed over all test rounds performed since the program
|
|
was started. This is the same information that @command{lbtt} normally outputs
|
|
at the end of testing; see @ref{Test statistics}, for more information about
|
|
the output that is displayed.
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node Failure analysis commands, , Data display commands, Analyzing test results
|
|
@section Failure analysis commands
|
|
|
|
The first part of this section introduces the commands available for
|
|
identifying an LTL-to-B@"uchi translator that caused a failure in one of the
|
|
automata correctness tests. The second part describes the conventions that
|
|
@command{lbtt} uses for justifying the result of the analysis.
|
|
|
|
@subsection Alphabetical list of failure analysis commands
|
|
|
|
@table @samp
|
|
@item buchianalysis @r{<}@var{implementation-id}@r{>} @r{<}@var{implementation-id}@r{>}
|
|
@kindex buchianalysis
|
|
@cindex B@"uchi automata intersection emptiness check, failure analysis
|
|
@cindex tests, failure analysis
|
|
@cindex failure analysis, B@"uchi automata intersection check
|
|
@cindex analyzing test failures, B@"uchi automata intersection emptiness check
|
|
Analyze a failure in the B@"uchi automata intersection emptiness check
|
|
(@pxref{Automata intersection emptiness check}).
|
|
The two implementation identifiers select the B@"uchi automata for which
|
|
to perform the analysis. The B@"uchi automata intersection emptiness
|
|
check always involves automata constructed from the positive and the negative
|
|
formulas used in the current test round. The first implementation identifier
|
|
chooses an implementation that constructed an automaton from the positive
|
|
formula, and the second identifier selects an implementation used for
|
|
translating the negative formula into an automaton. (The identifiers can also
|
|
be equal if one of the tested implementations failed the check against itself.)
|
|
|
|
@cindex witness
|
|
A failure in the B@"uchi automata intersection emptiness check implies that
|
|
there exists an input sequence over subsets of atomic propositions that is
|
|
accepted by both automata included in the analysis. @command{lbtt} examines the
|
|
intersection of the automata to find a witness of such an input, checks whether
|
|
this witness is a model of the positive formula, and tells which one of the
|
|
automata is likely to be incorrect according to the following rules:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
If the positive formula is found to hold in the witness, the automaton
|
|
constructed from the negative formula is likely to contain an error.
|
|
|
|
@item
|
|
If the witness is not a model for the positive formula, then the automaton
|
|
constructed from the positive formula probably accepts the witness incorrectly.
|
|
@end itemize
|
|
|
|
@item consistencyanalysis @r{<}@var{implementation-id}@r{>} @r{[}@var{state-id}@r{]}
|
|
@kindex consistencyanalysis
|
|
@cindex model checking result consistency check, failure analysis
|
|
@cindex tests, failure analysis
|
|
@cindex failure analysis, model checking result consistency check
|
|
@cindex analyzing test failures, model checking result consistency check
|
|
Analyze a failure in the model checking result consistency check
|
|
(@pxref{Model checking result consistency check}). The
|
|
@var{implementation-id} parameter chooses the implementation to analyze.
|
|
In addition, the optional @var{state-id} parameter can be used to specify a
|
|
state (in the state space) in which to perform the analysis (use the
|
|
@samp{inconsistencies} command, @ref{Data display commands}, to see a list
|
|
of all states in which the check failed). If the state identifier
|
|
is omitted, @command{lbtt} will try to find a state where
|
|
the check failed.
|
|
|
|
@cindex witness
|
|
A failure in the model checking result consistency check implies the existence
|
|
of a witness (i.e., a path in the state space used for the tests in the
|
|
current test round) whose temporal interpretation is not accepted by either of
|
|
two automata constructed from two complementary LTL formulas. In the analysis,
|
|
@command{lbtt} finds such a witness, checks separately whether it is a model of
|
|
the positive formula, and then tells which one of the automata seems to reject
|
|
the witness incorrectly.
|
|
|
|
@item resultanalysis @r{[``}+@r{''} @r{|} @r{``}-@r{'']} @r{<}@var{implementation-id}@r{>} @r{<}@var{implementation-id}@r{>} @r{[}@var{state-id}@r{]}
|
|
@kindex resultanalysis
|
|
@cindex model checking result cross-comparison test, failure analysis
|
|
@cindex tests, failure analysis
|
|
@cindex failure analysis, model checking result cross-comparison test
|
|
@cindex analyzing test failures, model checking result cross-comparison test
|
|
Analyze a failure in the model checking result cross-comparison test
|
|
(@pxref{Model checking result cross-comparison test}) between two
|
|
implementations on either the positive (@samp{+}) or the negative
|
|
(@samp{-}) LTL formula used in the current test round. The implementation
|
|
identifiers can be optionally followed by an identifier of a state in the
|
|
state space to specify a state in which the analysis should be performed.
|
|
(Suitable
|
|
state identifiers can be found by looking for inconsistencies in the model
|
|
checking results accessible with the @samp{evaluate} command,
|
|
@ref{Data display commands}; by omitting the state identifier,
|
|
@command{lbtt} will try to find a state in which the model
|
|
checking result comparison failed between the implementations.)
|
|
|
|
If using randomly generated or enumerated paths as state spaces, @command{lbtt}
|
|
also accepts the identifier @samp{lbtt} in place of either of the
|
|
implementation identifiers. This instructs @command{lbtt} to perform the
|
|
analysis against @command{lbtt}'s internal model checking algorithm.
|
|
|
|
@cindex witness
|
|
A failure in the model checking result cross-comparison test suggests that
|
|
the state space used in the current test round contains a path which is
|
|
accepted by one, but rejected by another automaton constructed from the same
|
|
LTL formula. To determine which one of these automata accepts or rejects the
|
|
input incorrectly, @command{lbtt} finds a witness path giving contradictory
|
|
model checking results, model checks the formula separately in the witness,
|
|
and tells which one of the automata seems to accept or reject the witness
|
|
incorrectly.
|
|
|
|
@end table
|
|
|
|
@subsection Witnesses, proofs and refutations
|
|
|
|
@cindex witness
|
|
All of the above analysis commands use @command{lbtt}'s internal model
|
|
checking algorithm to determine which one of the two automata involved in
|
|
each test is incorrect by checking whether an LTL formula holds in a witness
|
|
path extracted from the state space used in the current test round or from the
|
|
intersection of two B@"uchi automata. The witness path is a sequence of
|
|
consecutive states that ends in a loop, and is represented in two parts as an
|
|
initial
|
|
``prefix'' (which may be empty) and a ``cycle'' that is considered to repeat
|
|
itself indefinitely. The witness might, for example, look as follows:
|
|
|
|
@smallexample
|
|
Execution M:
|
|
prefix:
|
|
s3 @{p0,p2,p4@} --> s4
|
|
cycle:
|
|
s4 @{p1,p3@} --> s5
|
|
s5 @{p3@} --> s6
|
|
s6 @{p1,p2,p3@} --> s7
|
|
s7 @{p3,p4@} --> s8
|
|
s8 @{p1@} --> s9
|
|
s9 @{@} --> s2
|
|
s2 @{@} --> s3
|
|
s3 @{p0,p2,p4@} --> s4
|
|
@end smallexample
|
|
|
|
@noindent
|
|
In this case, the witness (or ``execution'' as displayed in the output)
|
|
@math{M} consists of a single-state prefix followed by a cycle of eight
|
|
states. The atomic propositions that hold in each state are also shown in
|
|
the output.
|
|
|
|
(The witness can be considered a small state space
|
|
@iftex
|
|
@tex
|
|
$M = \langle S, \rho, {\cal L} \rangle$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{M = <S, R, L>}
|
|
@end ifnottex
|
|
following the definition in @ref{State spaces}; in the example above,
|
|
@iftex
|
|
@tex
|
|
$S = \{s_2, s_3, s_4, s_5, s_6, s_7, s_8, s_9\}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{S = @{s2, s3, s4, s5, s6, s7, s8, s9@}},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$\rho = \{(s_2, s_3), (s_3, s_4), (s_4, s_5), (s_5, s_6), (s_6, s_7),
|
|
(s_7, s_8), (s_8, s_9), (s_9, s_2)\}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{R = @{(s2, s3), (s3, s4), (s4, s5), (s5, s6), (s6, s7), (s7, s8), (s8, s9), (s9, s2)@}},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
${\cal L}(s_2) = {\cal L}(s_9) = \emptyset$,
|
|
${\cal L}(s_3) = \{p_0, p_2, p_4\}$,
|
|
${\cal L}(s_4) = \{p_1, p_3\}$,
|
|
${\cal L}(s_5) = \{p_3\}$,
|
|
${\cal L}(s_6) = \{p_1, p_2, p_3\}$,
|
|
${\cal L}(s_7) = \{p_3, p_4\}$, and
|
|
${\cal L}(s_8) = \{p_1\}$.)
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{L(s2) = L(s_9) = @{@}, L(s3) = @{p0, p2, p4@}, L(s4) = @{p1, p3@}, L(s5) = @{p3@}, L(s6) = @{p1, p2, p3@}, L(s7) = @{p3, p4@},} and @math{L(s8) = @{p1@}}.)
|
|
@end ifnottex
|
|
|
|
|
|
In the model checking result cross-comparison test and the model checking
|
|
result consistency check, the witness is an actual path extracted from the
|
|
state space used for the tests in the current test round. In this case, the
|
|
state identifiers correspond to the states of the state space, and can be
|
|
accessed with the @samp{statespace @r{[}@var{state-id}@r{]}} command
|
|
(@pxref{Data display commands}).
|
|
|
|
@cindex proof for an LTL formula
|
|
@cindex refutation for an LTL formula
|
|
To justify the result of the analysis, @command{lbtt} also displays a proof
|
|
or a refutation for the LTL formula in the witness. The proof or refutation is
|
|
constructed by a recursive examination of the subformulas of the (positive or
|
|
negative) formula used in the current test round according to the semantics of
|
|
LTL and might look as follows:
|
|
|
|
@smallexample
|
|
Analysis of the formula in the execution:
|
|
M,<s3, ...> |/= ((X p0 U ! p4) <-> p0) :
|
|
+-> M,<s3, ...> |/= (X p0 U ! p4) :
|
|
| +-> M,<s3, ...> |/= X p0 :
|
|
| | +-> s3 --> s4
|
|
| | +-> M,<s4, ...> |/= p0
|
|
| +-> M,<s3, ...> |/= ! p4 :
|
|
| +-> M,<s3, ...> |== p4
|
|
+-> M,<s3, ...> |== p0
|
|
@end smallexample
|
|
|
|
@noindent
|
|
The proof (or refutation) can be considered a tree of statements of the form
|
|
@samp{M,<s, ...> |== @var{subformula}} or
|
|
@samp{M,<s, ...> |/= @var{subformula}}. Here, the symbol @samp{|==} is used
|
|
to denote that the formula @var{subformula} holds in the (infinite)
|
|
subsequence beginning at state @samp{s} of the witness, and the relational
|
|
symbol @samp{|/=} denotes the opposite. The children of each proof tree node
|
|
give justification for the claim in their parent node; the children might be
|
|
further expanded if the claims in them do not directly follow from the
|
|
definition of
|
|
@iftex
|
|
@tex
|
|
${\cal L}$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{L}.
|
|
@end ifnottex
|
|
In the presence of temporal operators, the proofs may
|
|
need to be based also on the structural properties of @math{M}. These are
|
|
shown as statements of the form @samp{sn --> sm} to indicate that @math{M}
|
|
contains a transition from the state @samp{sn} to the state @samp{sm} (and,
|
|
since the states in @math{M} are connected into a non-branching sequence, that
|
|
this is the @emph{only} transition originating from @samp{sn}).
|
|
|
|
In the above example, @command{lbtt} claims that the formula
|
|
@samp{((X p0 U ! p4) <-> p0)} does not hold in the witness presented earlier
|
|
in this section, and that this follows (by the semantics of logical
|
|
equivalence) from the claims that the subformula @samp{(X p0 U ! p4)} does not
|
|
hold, but the subformula @samp{p0} holds in this witness.
|
|
@samp{(X p0 U ! p4)} does not hold in the witness, because neither
|
|
@samp{X p0} nor @samp{! p4} holds in the first state of the witness
|
|
@iftex
|
|
@tex
|
|
($p_4 \in {\cal L}(s_3)$, and $p_0 \notin {\cal L}(s_4)$, where $s_4$ is the
|
|
only successor of $s_3$).
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
(@math{p4} is included in @math{L(s3)}, and @math{p0} is not included in
|
|
@math{L(s4)}, where @math{s4} is the only successor of @math{s3}).
|
|
@end ifnottex
|
|
On the other hand,
|
|
@samp{p0} holds in the witness because of the fact that
|
|
@iftex
|
|
@tex
|
|
$p_0 \in {\cal L}(s_3)$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{p0} is included in @math{L(s3)}.
|
|
@end ifnottex
|
|
|
|
|
|
|
|
@node Interfacing with lbtt, References, Analyzing test results, Top
|
|
@chapter Interfacing with @command{lbtt}
|
|
|
|
@cindex LTL-to-B@"uchi translators, interfacing with
|
|
@cindex interfacing LTL-to-B@"uchi translators with @command{lbtt}
|
|
|
|
The output generated by @command{lbtt} consists of textual messages
|
|
and an optional error log file (@pxref{--logfile,,@samp{--logfile} command line
|
|
option}). The format of the output messages is determined by the verbosity
|
|
mode;
|
|
for more information, see @ref{Interpreting the output}. In addition,
|
|
@command{lbtt} returns one of the following three values as its exit
|
|
status upon normal termination:
|
|
@itemize
|
|
@item 0:
|
|
@command{lbtt} exited successfully; no errors were detected during testing.
|
|
|
|
@item 1:
|
|
@command{lbtt} exited successfully; errors were detected during testing.
|
|
|
|
@item 2:
|
|
An error was found when reading the program configuration or when processing
|
|
the command line options.
|
|
|
|
@item 3:
|
|
@command{lbtt} exited due to an unrecoverable internal error.
|
|
@end itemize
|
|
|
|
The rest of this chapter gives the details on how to use @command{lbtt} for
|
|
testing LTL-to-B@"uchi translation algorithm implementations that are not
|
|
supported by the basic distribution. (See
|
|
@ref{The lbtt-translate utility}
|
|
for information on how to connect several publicly available
|
|
LTL-to-B@"uchi translator implementations to @command{lbtt}.)
|
|
|
|
@menu
|
|
* Translator interface:: @command{lbtt}'s requirements for an
|
|
LTL-to-B@"uchi translator.
|
|
* Format for LTL formulas:: How @command{lbtt} passes LTL formulas
|
|
to the translators.
|
|
* Format for automata:: How @command{lbtt} expects the translators
|
|
to present their output.
|
|
* The lbtt-translate utility:: An interface for two LTL-to-B@"uchi
|
|
translators.
|
|
@end menu
|
|
|
|
|
|
|
|
@node Translator interface, Format for LTL formulas, , Interfacing with lbtt
|
|
@section Requirements for translator executables
|
|
|
|
@cindex LTL-to-B@"uchi translators, interface requirements
|
|
@command{lbtt} assumes each tested LTL-to-B@"uchi translator to be
|
|
accessible by running an executable file which should read in an LTL
|
|
formula from a file, convert it into a B@"uchi automaton and then
|
|
write the automaton into another file. For this purpose, the executable
|
|
should support the following command line interface:
|
|
|
|
@example
|
|
@var{path-to-program} @var{parameters} @var{input-file} @var{output-file}
|
|
@end example
|
|
|
|
@noindent
|
|
where @var{path-to-program} is the full name (and location) of the
|
|
executable, @var{parameters} are any optional parameters that might be needed
|
|
for running the executable, and @var{input-file} and
|
|
@var{output-file} are two file names.
|
|
The translator executable should read its input (an LTL formula) from
|
|
@var{input-file} and write its output (a B@"uchi automaton) into
|
|
@var{output-file} (without removing the input file); see
|
|
@ifnottex
|
|
@ref{Format for LTL formulas} and @ref{Format for automata}
|
|
@end ifnottex
|
|
@iftex
|
|
the following two sections
|
|
@end iftex
|
|
for a description on how these files should be formatted.
|
|
|
|
The translator executable should always create an output file and then return
|
|
with a zero exit status in case no errors occur during the translation.
|
|
@command{lbtt} interprets a missing output file or a nonzero exit status as
|
|
an error and will not in this case try to run any tests, even if
|
|
an automaton were successfully saved in an output file.
|
|
|
|
To start testing the translator, add a new @samp{Translator} section for it
|
|
into
|
|
@command{lbtt}'s configuration file (@pxref{Configuration file}), for example
|
|
|
|
@smallexample
|
|
Translator
|
|
@{
|
|
Name = "LTL-to-B@"uchi translator"
|
|
Path = /home/lbtt-user/bin/ltl-to-buchi-translator
|
|
Parameters = "-x -y -z"
|
|
Enabled = Yes
|
|
@}
|
|
@end smallexample
|
|
|
|
|
|
|
|
@node Format for LTL formulas, Format for automata, Translator interface, Interfacing with lbtt
|
|
@section Input file format for LTL formulas
|
|
|
|
@cindex LTL-to-B@"uchi translators, LTL formula input file format
|
|
@cindex LTL formula, LTL-to-B@"uchi translator input file format
|
|
@cindex file formats, LTL-to-B@"uchi translator input file
|
|
@command{lbtt} passes each LTL formula to each LTL-to-B@"uchi translator
|
|
in a file containing an LTL formula in a prefix notation followed by a
|
|
single newline. The precise grammar for the LTL formulas (in a BNF-style
|
|
notation) is as follows:
|
|
|
|
@smallexample
|
|
@var{formula} @r{::=} `t'
|
|
@r{// ``true''}
|
|
@r{|} `f'
|
|
@r{// ``false''}
|
|
@r{|} `p'@r{[}0@r{---}9@r{]+}
|
|
@r{// atomic proposition with}
|
|
@r{// a nonnegative integer}
|
|
@r{// identifier}
|
|
@r{|} `!' @var{sp} @var{formula}
|
|
@r{// negation}
|
|
@r{|} `X' @var{sp} @var{formula}
|
|
@r{// ``next time''}
|
|
@r{|} `F' @var{sp} @var{formula}
|
|
@r{// ``finally''}
|
|
@r{|} `G' @var{sp} @var{formula}
|
|
@r{// ``globally''}
|
|
@r{|} `&' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// conjunction}
|
|
@r{|} `|' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// disjunction}
|
|
@r{|} `i' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// implication}
|
|
@r{|} `e' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// equivalence}
|
|
@r{|} `^' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// exclusive or}
|
|
@r{|} `U' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// ``(strong) until''}
|
|
@r{|} `V' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// ``(weak) release''}
|
|
@r{|} `W' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// ``weak until''}
|
|
@r{|} `M' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// ``strong release''}
|
|
@r{|} `B' @var{sp} @var{formula} @var{sp} @var{formula}
|
|
@r{// ``before''}
|
|
|
|
@end smallexample
|
|
@noindent
|
|
(The quoted characters denote the characters themselves; @var{sp} denotes
|
|
any nonempty string of white space. Lines containing a // are comments and
|
|
are not part of the grammar. All atomic propositions in the formula have a
|
|
nonnegative numeric identifier.)
|
|
|
|
@noindent
|
|
For example, the LTL formula
|
|
@iftex
|
|
@tex
|
|
$(p_0\;{\bf U}\;p_1)\rightarrow({\bf F}\;{\bf G}(\neg p_2\leftrightarrow p_3))$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
(in @command{lbtt}'s infix syntax)
|
|
@example
|
|
(p0 U p1) -> (<> [] (! p2 <-> p3))
|
|
@end example
|
|
@end ifnottex
|
|
@noindent
|
|
would be expressed in the form
|
|
@example
|
|
i U p0 p1 F G e ! p2 p3
|
|
@end example
|
|
@noindent
|
|
in an output file.
|
|
|
|
If your translator does not support all of the above operators, edit
|
|
the configuration file (@pxref{Configuration file}) or use the command
|
|
line options (@pxref{Command line options}) to prevent
|
|
@command{lbtt} from generating random LTL formulas with these operators.
|
|
|
|
|
|
|
|
@node Format for automata, The lbtt-translate utility, Format for LTL formulas, Interfacing with lbtt
|
|
@section Output file format for automata
|
|
|
|
@cindex file formats, LTL-to-B@"uchi translator output file
|
|
@cindex LTL-to-B@"uchi translators, automaton output file format
|
|
@cindex B@"uchi automata, LTL-to-B@"uchi translator output file format
|
|
@cindex generalized B@"uchi automata, LTL-to-B@"uchi translator output file format
|
|
@command{lbtt} expects the B@"uchi automata generated by each LTL-to-B@"uchi
|
|
translator implementation to be in the format specified below. The format
|
|
encodes a generalized B@"uchi automaton (a B@"uchi automaton with zero or
|
|
more acceptance conditions) with a single initial state and labels (guards) on
|
|
transitions. For the full formal definition and examples on how
|
|
to reduce other definitions into the one used by @command{lbtt}, see
|
|
@ref{Definitions}.
|
|
|
|
The output file generated by the translator should contain an @var{automaton}
|
|
described using the following grammar
|
|
(as before, quoted characters denote the characters themselves, @var{sp}
|
|
denotes any nonempty string of white space, lines containing a // are
|
|
comments that are not part of the grammar, and @samp{\n} corresponds to the
|
|
newline character).
|
|
|
|
@smallexample
|
|
@var{automaton} @r{::=} @var{num-states} @var{sp} @var{cond-specifier} @var{state-list}
|
|
|
|
@var{num-states} @r{::=} @r{[}0@r{---}9@r{]+}
|
|
|
|
@var{cond-specifier} @r{::=} @r{[}0@r{---}9@r{]+}@r{[}st@r{]}*
|
|
|
|
@var{state-list} @r{::=} @var{state-list} @var{sp} @var{state}
|
|
@r{|} @r{// empty}
|
|
@end smallexample
|
|
|
|
@noindent
|
|
The automaton description begins with a nonnegative number that gives the
|
|
number of states in the automaton. If the number of
|
|
states is 0, the automaton will not accept any input. If the number is
|
|
positive, it should be followed by a @var{cond-specifier} that determines the
|
|
number
|
|
and placement of acceptance conditions in the automaton. If the number of
|
|
acceptance conditions is 0, the automaton accepts an input word if and only if
|
|
it has a run on that word according to the definition given in the
|
|
Appendix (@pxref{Definitions}).
|
|
|
|
The placement of acceptance conditions is specified by concatenating a
|
|
string formed from the symbols @samp{s} and @samp{t} to the number of
|
|
acceptance conditions (with no white space in between). The interpretation of
|
|
this string is as follows:
|
|
@itemize
|
|
@item
|
|
If the string is empty or does not include the symbol @samp{t}, the acceptance
|
|
conditions of the automaton are placed exclusively on its states. (This
|
|
alternative corresponds to the definition supported by @command{lbtt} 1.0.x.)
|
|
|
|
@item
|
|
If the string is nonempty but does not include the symbol @samp{s}, the
|
|
automaton has acceptance conditions exclusively on its transitions.
|
|
|
|
@item
|
|
Otherwise, the automaton has acceptance conditions on both states and
|
|
transitions.
|
|
@end itemize
|
|
|
|
The @var{cond-specifier} is followed by a list of the descriptions of states in
|
|
the automaton. The format of this list is affected by the choice of the
|
|
placement of the acceptance conditions.
|
|
More precisely, the choice affects the interpretation of the
|
|
@var{cond-list} nonterminal symbol in the following fragment of the grammar: we
|
|
indicate this by prefixing the nonterminal with either ``<s>'' or
|
|
``<t>'' to denote that the list (together with its terminating @samp{-1})
|
|
should be
|
|
omitted in automata that do not associate acceptance conditions with states or
|
|
transitions, respectively.
|
|
|
|
@smallexample
|
|
@var{state} @r{::=} @var{state-id} @var{sp} @var{initial?} @r{<s>}@var{cond-list} @var{transition-list}
|
|
|
|
@var{state-id} @r{::=} @r{[}0@r{---}9@r{]+}
|
|
|
|
@var{initial?} @r{::=} `0' @r{|} `1'
|
|
|
|
@var{cond-list} @r{::=} @var{sp} @var{acceptance-condition-id} @var{cond-list}
|
|
@r{|} @var{sp} `-1'
|
|
|
|
@var{acceptance-condition-id} @r{::=} @r{[}0@r{---}9@r{]+}
|
|
|
|
@var{transition-list} @r{::=} @var{sp} @var{transition} @var{transition-list}
|
|
@r{|} @var{sp} `-1'
|
|
|
|
@var{transition} @r{::=} @var{state-id} @r{<t>}@var{cond-list} @var{sp} @var{guard-formula} `\n'
|
|
|
|
@var{guard-formula} @r{::=} `t'
|
|
@r{// ``true''}
|
|
@r{|} `f'
|
|
@r{// ``false''}
|
|
@r{|} `p'@r{[}0@r{---}9@r{]+}
|
|
@r{// atomic proposition}
|
|
@r{|} `!' @var{sp} @var{guard-formula}
|
|
@r{// negation}
|
|
@r{|} `&' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula}
|
|
@r{// conjunction}
|
|
@r{|} `|' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula}
|
|
@r{// disjunction}
|
|
@r{|} `i' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula}
|
|
@r{// implication}
|
|
@r{|} `e' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula}
|
|
@r{// equivalence}
|
|
@r{|} `^' @var{sp} @var{guard-formula} @var{sp} @var{guard-formula}
|
|
@r{// exclusive or}
|
|
@end smallexample
|
|
@noindent
|
|
|
|
The description of each state begins with a numeric state identifier, which can
|
|
be any nonnegative integer. The state identifier should be followed by a number
|
|
telling whether the state is initial (@samp{1} if yes). The automaton should
|
|
have exactly one initial state. If the automaton has acceptance conditions
|
|
associated with its states, this number should then be followed by a list of
|
|
acceptance condition identifiers separated by white space. This list should be
|
|
terminated with @samp{-1}.
|
|
|
|
The state description should be followed by the list of transitions starting
|
|
from the state (terminated again by @samp{-1}). Each transition consists of a
|
|
state identifier (the target state of the transition), a list of acceptance
|
|
condition identifiers (if the automaton has acceptance conditions on
|
|
transitions), and a propositional formula @footnote{Although not described
|
|
formally in the grammar, the guard formulas can be specified in any
|
|
of the formats @command{lbtt} supports in its formula input files
|
|
(@pxref{--formulafile,,@samp{--formulafile} command line option}). Note that
|
|
the formula always needs to be terminated with a newline, though.} that encodes
|
|
the symbols of the alphabet
|
|
@iftex
|
|
@tex
|
|
$2^{AP}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{2^AP}
|
|
@end ifnottex
|
|
(where @var{AP} is a finite set of atomic propositions) on which the
|
|
automaton is allowed to take the transition. The propositional formula should
|
|
be terminated with a newline.
|
|
|
|
The state and acceptance condition identifiers need not be successive, and the
|
|
states or acceptance conditions can be listed in any order. The only
|
|
restrictions are that the identifiers of different states and acceptance
|
|
conditions should be unique and that the total number of different identifiers
|
|
should equal @var{num-states} or @var{num-conds},
|
|
respectively. (The same identifiers can be shared between states and acceptance
|
|
conditions, however.)
|
|
|
|
|
|
Note that the output file should always contain a valid automaton description
|
|
if the LTL-to-B@"uchi translation was successful, even in the case that the
|
|
resulting automaton is empty (@command{lbtt} interprets a missing automaton
|
|
description file as an error).
|
|
|
|
The following examples illustrate the file format. The first example
|
|
gives the description of an automaton with acceptance conditions on
|
|
states. Note that in this case the @samp{s} is optional for describing the
|
|
placement of acceptance conditions; therefore, the automaton files used with
|
|
@command{lbtt} 1.0.x are upwards compatible with newer versions of the tool
|
|
(provided that each guard of a transition is terminated by a newline).
|
|
|
|
@smallexample
|
|
6 2s @r{// an automaton with six states and two acc.@ conditions on states}
|
|
0 1 -1 @r{// state 0: initial state, no acceptance conditions}
|
|
2 p1 @r{// transition to state 2, guard} @samp{p1}
|
|
5 p2 @r{// transition to state 5, guard} @samp{p2}
|
|
15 p3 @r{// transition to state 15, guard} @samp{p3}
|
|
-1 @r{// end of state 0}
|
|
2 0 1 -1 @r{// state 2: non-initial state, acceptance condition 1}
|
|
2 p1 @r{// transition to state 2, guard} @samp{p1}
|
|
5 p2 @r{// transition to state 5, guard} @samp{p2}
|
|
15 p3 @r{// transition to state 15, guard} @samp{p3}
|
|
-1 @r{// end of state 2}
|
|
5 0 0 -1 @r{// state 5: non-initial state, acceptance condition 0}
|
|
5 p2 @r{// transition to state 5, guard} @samp{p2}
|
|
8 & p1 p2 @r{// transition to state 8, guard} @samp{p1 /\ p2}
|
|
12 & p1 p3 @r{// transition to state 12, guard} @samp{p1 /\ p3}
|
|
15 p3 @r{// transition to state 15, guard} @samp{p3}
|
|
-1 @r{// end of state 5}
|
|
8 0 0 -1 @r{// state 8: non-initial state, acceptance condition 0}
|
|
5 p2 @r{// transition to state 5, guard} @samp{p2}
|
|
8 & p1 p2 @r{// transition to state 8, guard} @samp{p1 /\ p2}
|
|
12 & p1 p3 @r{// transition to state 12, guard} @samp{p1 /\ p3}
|
|
15 p3 @r{// transition to state 15, guard} @samp{p3}
|
|
-1 @r{// end of state 8}
|
|
15 0 1 0 -1 @r{// state 15: non-initial state, acceptance conditions 1 and 0}
|
|
2 p1 @r{// transition to state 2, guard} @samp{p1}
|
|
5 p2 @r{// transition to state 5, guard} @samp{p2}
|
|
15 p3 @r{// transition to state 15, guard} @samp{p3}
|
|
-1 @r{// end of state 15}
|
|
12 0 1 0 -1 @r{// state 12: non-initial state, acceptance conditions 1 and 0}
|
|
2 p1 @r{// transition to state 2, guard} @samp{p1}
|
|
5 p2 @r{// transition to state 5, guard} @samp{p2}
|
|
15 p3 @r{// transition to state 15, guard} @samp{p3}
|
|
-1 @r{// end of state 12}
|
|
@end smallexample
|
|
|
|
@noindent
|
|
The following example illustrates an automaton in which acceptance conditions
|
|
are placed on transitions.
|
|
|
|
@smallexample
|
|
4 3t @r{// four states, three acceptance conditions on transitions}
|
|
5 0 @r{// state 5: non-initial state}
|
|
84 0 -1 p1 @r{// transition to state 84, condition 0, guard} @samp{p1}
|
|
27 0 -1 & p1 ! p2 @r{// tr. to state 27, condition 0, guard} @samp{p1 /\ ! p2}
|
|
5 -1 t @r{// transition to state 5, no conditions, guard} @samp{true}
|
|
-1 @r{// end of state 5}
|
|
84 1 @r{// state 84: initial state}
|
|
5 1 -1 t @r{// transition to state 5, condition 1, guard} @samp{true}
|
|
27 0 -1 p1 @r{// transition to state 27, condition 0, guard} @samp{p1}
|
|
-1 @r{// end of state 84}
|
|
49 0 @r{// state 49: non-initial state}
|
|
5 -1 t @r{// transition to state 5, no conditions, guard} @samp{true}
|
|
49 1 4 -1 & p1 ! p2 @r{// tr.@ to state 49, conds.@ 1 and 4, guard} @samp{p1 /\ ! p2}
|
|
84 -1 p1 @r{// transition to state 84, no conditions, guard} @samp{p1}
|
|
-1 @r{// end of state 49}
|
|
27 0 @r{// state 27: non-initial state}
|
|
49 -1 & p1 p3 @r{// transition to state 49, no conds., guard} @samp{p1 /\ p3}
|
|
-1 @r{// end of state 27}
|
|
@end smallexample
|
|
|
|
@noindent
|
|
Automata with acceptance conditions on both states and transitions can be
|
|
specified using a combination of the above two formats, that is, by using
|
|
@samp{st} as the acceptance condition placement specifier and including a list
|
|
of acceptance conditions both after the value determining the initialness of a
|
|
state, and after the identifier of the target state of each transition.
|
|
|
|
@node The lbtt-translate utility, , Format for automata, Interfacing with lbtt
|
|
@section The @command{lbtt-translate} utility
|
|
|
|
@cindex @command{lbtt-translate} (executable file)
|
|
@cindex LTL-to-B@"uchi translators, interfacing with
|
|
@cindex interfacing LTL-to-B@"uchi translators with @command{lbtt}
|
|
The @command{lbtt} source distribution includes a small utility which can be
|
|
used as a common interface for the following publicly available LTL-to-B@"uchi
|
|
translator algorithm implementations:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
@cindex @command{lbt}
|
|
@command{lbt} --- an LTL-to-B@"uchi translation algorithm implementation
|
|
based on the algorithm described in
|
|
@ifnottex
|
|
@ref{[GPVW95]}.
|
|
@end ifnottex
|
|
@iftex
|
|
[GPVW95].
|
|
@end iftex
|
|
See
|
|
@ifinfo
|
|
@url{http://www.tcs.hut.fi/Software/maria/tools/lbt/}
|
|
@end ifinfo
|
|
@ifnotinfo
|
|
<@uref{http://www.tcs.hut.fi/Software/maria/tools/lbt/}>
|
|
@end ifnotinfo
|
|
for more information, including the source code of the implementation.
|
|
|
|
@item
|
|
@cindex SPIN
|
|
@ifnottex
|
|
SPIN @ref{[Hol97]}
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\sc{Spin}
|
|
@end tex
|
|
[Hol97]
|
|
@end iftex
|
|
--- a model checking tool
|
|
that includes a module for translating LTL formulas into B@"uchi automata
|
|
originally based on the algorithm presented in
|
|
@ifnottex
|
|
@ref{[GPVW95]}.
|
|
@end ifnottex
|
|
@iftex
|
|
[GPVW95].
|
|
@end iftex
|
|
See
|
|
@ifinfo
|
|
@url{http://spinroot.com/spin/whatispin.html}
|
|
@end ifinfo
|
|
@ifnotinfo
|
|
<@uref{http://spinroot.com/spin/whatispin.html}>
|
|
@end ifnotinfo
|
|
for more information.
|
|
|
|
@item
|
|
@cindex Spot
|
|
@ifnottex
|
|
Spot @ref{[DP04]}
|
|
@end ifnottex
|
|
@iftex
|
|
Spot [DP04]
|
|
@end iftex
|
|
--- a model checking library that includes a module for translating LTL
|
|
formulas into B@"uchi automata incorporating optimization techniques from
|
|
several different sources. See
|
|
@ifinfo
|
|
@url{http://spot.lip6.fr/}
|
|
@end ifinfo
|
|
@ifnotinfo
|
|
<@uref{http://spot.lip6.fr/}>
|
|
@end ifnotinfo
|
|
for more information.
|
|
@end itemize
|
|
|
|
To use @command{lbtt} for testing the LTL-to-B@"uchi translators included in
|
|
these tools, you should first install the tool normally by following its
|
|
installation instructions. Then add the following @samp{Translator} section in
|
|
@command{lbtt}'s configuration file:
|
|
|
|
@smallexample
|
|
Translator
|
|
@{
|
|
Name = "@r{[@var{name for the implementation}]}"
|
|
Path = "@r{[@var{path to @command{lbtt-translate}}]}"
|
|
Parameters = "@r{[@var{implementation selector}]} @r{[@var{path to executable}]}"
|
|
Enabled = Yes
|
|
@}
|
|
@end smallexample
|
|
|
|
@noindent
|
|
where [@var{path to @command{lbtt-translate}}] contains the complete path and
|
|
file name of the @command{lbtt-translate} tool executable,
|
|
[@var{implementation selector}] is either of the options @samp{--lbt} or
|
|
@samp{--spin}, and [@var{path to executable}] is the full path
|
|
of the tool executable. The names of these executables are usually (assuming
|
|
a normal installation) @command{lbt} and @command{spin}, respectively.
|
|
|
|
Note: These implementations may not have built-in support for all of the
|
|
LTL formula operators available for generating random LTL formulas with
|
|
@command{lbtt}. See the documentation of each translator for information
|
|
about which operators are supported, and then change the parameters in
|
|
@command{lbtt}'s configuration file accordingly to disable the unsupported
|
|
operators (or instruct @command{lbtt} to read the formulas from an external
|
|
source by invoking @command{lbtt} with the
|
|
@ref{--formulafile,,@samp{--formulafile} command line option}).
|
|
|
|
The @command{lbtt-translate} utility can also be invoked directly from the
|
|
shell to translate an LTL formula into a B@"uchi automaton using either of the
|
|
above translators. Use the command @command{lbtt-translate --help} to
|
|
see a short summary of available options.
|
|
|
|
|
|
|
|
@node References, Definitions, Interfacing with lbtt, Top
|
|
@unnumbered References
|
|
|
|
@table @asis
|
|
@item @anchor{[CGP99]} [CGP99]
|
|
E.@: Clarke Jr., O.@: Grumberg and D.@: Peled. Model checking. The MIT Press,
|
|
1999.
|
|
|
|
@item @anchor{[Cou99]} [Cou99]
|
|
J.-M.@: Couvreur. On-the-fly verification of linear temporal logic. In
|
|
@i{Proceedings of the World Congress on Formal Methods in the Development of
|
|
Computing Systems (FM'99), volume I}, volume 1708 of
|
|
@i{Lecture Notes in Computer Science}, pages 253---271. Springer-Verlag, 1999.
|
|
|
|
@item @anchor{[DGV99]} [DGV99]
|
|
M.@: Daniele, F.@: Giunchiglia and M.@: Y.@: Vardi. Improved automata
|
|
generation for linear temporal logic. In @i{Proceedings of the 11th
|
|
International Conference on Computer Aided Verification (CAV'99)}, volume 1633
|
|
of @i{Lecture Notes in Computer Science}, pages 249---260. Springer-Verlag,
|
|
1999.
|
|
|
|
@item @anchor{[DP04]} [DP04]
|
|
A.@: Duret-Lutz and D.@: Poitrenaud. SPOT: An Extensible Model Checking Library
|
|
Using Transition-Based Generalized B@"uchi Automata. In
|
|
@i{Proceedings of the 12th IEEE/ACM International Symposium on Modeling,
|
|
Analysis, and Simulation of Computer and Telecommunication Systems
|
|
(MASCOTS 2004)}, pages 76--83. IEEE Computer Society Press, 2004.
|
|
|
|
@item @anchor{[EH00]} [EH00]
|
|
K.@: Etessami and G.@: Holzmann. Optimizing B@"uchi automata. In
|
|
@i{Proceedings of the 11th International Conference on Concurrency Theory
|
|
(CONCUR 2000)}, volume 1877 of @i{Lecture Notes in Computer Science},
|
|
pages 153---167. Springer-Verlag, 2000.
|
|
|
|
@item @anchor{[Ete99]} [Ete99]
|
|
K.@: Etessami. Stutter-invariant languages, omega-automata, and temporal
|
|
logic. In @i{Proceedings of the 11th International Conference on Computer Aided
|
|
Verification (CAV'99)}, volume 1633 of @i{Lecture Notes in Computer Science},
|
|
pages 236---248. Springer-Verlag, 1999.
|
|
|
|
@item @anchor{[Ete02]} [Ete02]
|
|
K.@: Etessami. A hierarchy of polynomial-time computable simulations for
|
|
automata. In @i{Proceedings of the 13th International Conference on
|
|
Concurrency Theory (CONCUR 2002)}, volume 2421 of
|
|
@i{Lecture Notes in Computer Science}, pages 131---144. Springer-Verlag, 2002.
|
|
|
|
@item @anchor{[EWS01]} [EWS01]
|
|
K.@: Etessami, Th.@: Wilke and R.@: Schuller. Fair simulation relations,
|
|
parity games, and state space reduction for B@"uchi automata. In
|
|
@i{Proceedings of the 28th International Colloquium on Automata, Languages and
|
|
Programming (ICALP 2001)}, volume 2076 of
|
|
@i{Lecture Notes in Computer Science}, pages 694---707. Springer-Verlag, 2001.
|
|
|
|
@item @anchor{[Fri03]} [Fri03]
|
|
C.@: Fritz. Constructing B@"uchi automata from linear temporal logic using
|
|
simulation relations for alternating B@"uchi automata. In
|
|
@i{Proceedings of the 8th International Conference on Implementation and
|
|
Application of Automata (CIAA 2003)}, volume 2759 of
|
|
@i{Lecture Notes in Computer Science}, pages 35---48. Springer-Verlag, 2003.
|
|
|
|
@item @anchor{[GO01]} [GO01]
|
|
P.@: Gastin and D.@: Oddoux. Fast LTL to B@"uchi automata translation.
|
|
In @i{Proceedings of the 13th International Conference on Computer
|
|
Aided Verification (CAV 2001)}, volume 2102 of @i{Lecture Notes in Computer
|
|
Science}, pages 53---65. Springer-Verlag, 2001.
|
|
|
|
@item @anchor{[GO03]} [GO03]
|
|
P.@: Gastin and D.@: Oddoux. LTL with past and two-way weak alternating
|
|
automata. In @i{Proceedings of the 28th International Symposium on Mathematical
|
|
Foundations of Computer Science (MFCS 2003)}, volume 2747 of
|
|
@i{Lecture Notes in Computer Science}, pages 439---448. Springer-Verlag, 2003.
|
|
|
|
@item @anchor{[Gei01]} [Gei01]
|
|
M.@: C.@: W.@: Geilen. On the construction of monitors for temporal logic
|
|
properties. @i{Electronic Notes for Theoretical Computer Science}, 55(2), 2001.
|
|
|
|
@item @anchor{[GPVW95]} [GPVW95]
|
|
R.@: Gerth, D.@: Peled, M.@: Y.@: Vardi and P.@: Wolper. Simple on-the-fly
|
|
automatic verification of linear temporal logic. In
|
|
@i{Proceedings of 15th IFIP WG6.1 International Symposium on Protocol
|
|
Specification, Testing, and Verification (PSTV'95)}, pages 3---18.
|
|
Chapman & Hall, 1995.
|
|
|
|
@item @anchor{[GL02]} [GL02]
|
|
D.@: Giannakopoulou and F.@: Lerda. From states to transitions: Improving
|
|
translation of LTL formulae to B@"uchi automata. In
|
|
@i{Proceedings of the 22nd IFIP WG6.1 International Conference on Formal
|
|
Techniques for Networked and Distributed Systems (FORTE 2002)}, volume 2529 of
|
|
@i{Lecture Notes in Computer Science}, pages 308---326. Springer-Verlag, 2002.
|
|
|
|
@item @anchor{[GSB02]} [GSB02]
|
|
S.@: Gurumurthy, F.@: Somenzi and R.@: Bloem. Fair simulation minimization.
|
|
In @i{Proceedings of the 14th International Conference on Computer Aided
|
|
Verification (CAV 2002)}, volume 2404 of @i{Lecture Notes in Computer Science},
|
|
pages 610---624. Springer-Verlag, 2002.
|
|
|
|
@item @anchor{[GViz]} [GViz]
|
|
GraphViz - open source graph drawing software. See
|
|
@ifinfo
|
|
@url{http://www.research.att.com/sw/tools/graphviz/}.
|
|
@end ifinfo
|
|
@ifnotinfo
|
|
<@uref{http://www.research.att.com/sw/tools/graphviz/}>.
|
|
@end ifnotinfo
|
|
|
|
@item @anchor{[Hol97]} [Hol97]
|
|
G.@: J.@: Holzmann. The model checker
|
|
@ifnottex
|
|
SPIN.
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
\sc{Spin}.
|
|
@end tex
|
|
@end iftex
|
|
@i{IEEE Transactions on Software Engineering}, 23(5):279---295, 1997.
|
|
|
|
@item @anchor{[Isl94]} [Isl94]
|
|
A.@: Isli. Mapping an LPTL formula into a B@"uchi alternating automaton
|
|
accepting its models. In @i{Temporal Logic: Proceedings of the ICTL Workshop},
|
|
pages 85---90. Research Report MPI-I-94-230, Max-Planck-Institut f@"ur
|
|
Informatik, 1994.
|
|
|
|
@item @anchor{[Lat03]} [Lat03]
|
|
T.@: Latvala. Efficient model checking of safety properties. In
|
|
@i{Proceedings of the 10th Spin Workshop on Model Checking of Software
|
|
(SPIN 2003)}, volume 2648 of @i{Lecture Notes in Computer Science}, pages
|
|
74---88. Springer-Verlag, 2003.
|
|
|
|
@item @anchor{[Sch01]} [Sch01]
|
|
K.@: Schneider. Improving automata generation for linear temporal logic by
|
|
considering the automaton hierarchy. In @i{Proceedings of the 8th International
|
|
Conference on Logic for Programming, Artificial Intelligence and Reasoning
|
|
(LPAR 2001)}, volume 2250 of @i{Lecture Notes in Computer Science}, pages
|
|
39---54. Springer-Verlag, 2001.
|
|
|
|
@item @anchor{[ST03]} [ST03]
|
|
R.@: Sebastiani and S.@: Tonetta. ``More deterministic'' vs.@: ``smaller''
|
|
B@"uchi automata for efficient LTL model checking. In
|
|
@i{Proceedings of the 12th Advanced Research Working Conference on Correct
|
|
Hardware Design and Verification Methods (CHARME 2003)}, volume 2860 of
|
|
@i{Lecture Notes in Computer Science}, pages 126---140. Springer-Verlag, 2003.
|
|
|
|
@item @anchor{[SB00]} [SB00]
|
|
F.@: Somenzi and R.@: Bloem. Efficient B@"uchi automata from LTL formulae.
|
|
In @i{Proceedings of the 12th International Conference on Computer Aided
|
|
Verification (CAV 2000)}, volume 1855 of @i{Lecture Notes in Computer Science},
|
|
pages 247---263. Springer-Verlag, 2000.
|
|
|
|
@item @anchor{[Tau00]} [Tau00]
|
|
H.@: Tauriainen. Automated testing of B@"uchi automata translators
|
|
for linear temporal logic. Research report A66, Laboratory for Theoretical
|
|
Computer Science, Helsinki University of Technology, Espoo, Finland,
|
|
2000. Available on the WWW at
|
|
@ifinfo
|
|
@url{http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A66.shtml}
|
|
@end ifinfo
|
|
@ifhtml
|
|
<@uref{http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A66.shtml}>.
|
|
@end ifhtml
|
|
@iftex
|
|
<@url{http://www.tcs.hut.fi/Publications/info/ bibdb.HUT-TCS-A66.shtml}>.
|
|
@end iftex
|
|
|
|
@item @anchor{[TH02]} [TH02]
|
|
H.@: Tauriainen and K.@: Heljanko. Testing LTL formula translation into B@"uchi
|
|
automata.
|
|
@i{International Journal on Software Tools for Technology Transfer (STTT)}
|
|
4(1):57---70, 2002.
|
|
|
|
@item @anchor{[Thi02]} [Thi02]
|
|
X.@: Thirioux. Simple and efficient translation from LTL formulas to B"uchi
|
|
automata. @i{Electronic Notes in Theoretical Computer Science}, 66(2), 2002.
|
|
|
|
@item @anchor{[Var96]} [Var96]
|
|
M.@: Y.@: Vardi. An automata-theoretic approach to linear temporal logic.
|
|
In @i{Logics for Concurrency: Structure versus Automata}, volume 1043 of
|
|
@i{Lecture Notes in Computer Science}, pages 238---265. Springer-Verlag,
|
|
1996.
|
|
|
|
@item @anchor{[VW86]} [VW86]
|
|
M.@: Y.@: Vardi and P.@: Wolper. An automata-theoretic approach to
|
|
automatic program verification. In @i{Proceedings of the First IEEE
|
|
Symposium on Logic in Computer Science (LICS'86)}, pages 332---344. IEEE
|
|
Computer Society Press, 1986.
|
|
|
|
@item @anchor{[Wol01]} [Wol01]
|
|
P.@: Wolper. Constructing automata from temporal logic formulas: A tutorial.
|
|
In @i{Lectures on Formal Methods and Performance Analysis: First EEF/Euro
|
|
Summer School on Trends in Computer Science, Revised Lectures}, volume 2090
|
|
of @i{Lecture Notes in Computer Science}, pages 261---277. Springer-Verlag,
|
|
2001.
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node Definitions, Configuration file option index, References, Top
|
|
@appendix Definitions
|
|
|
|
This appendix reviews the formal definitions of the objects that @command{lbtt}
|
|
manipulates.
|
|
|
|
@menu
|
|
* LTL formulas:: @command{lbtt} uses traditional semantics
|
|
for propositional linear temporal
|
|
logic.
|
|
* Generalized automata:: The B@"uchi automata used by @command{lbtt}
|
|
have one initial state, labels on
|
|
transitions and zero or more
|
|
acceptance conditions.
|
|
* State spaces:: State spaces are Kripke structures
|
|
with a total transition relation.
|
|
@end menu
|
|
|
|
|
|
@node LTL formulas, Generalized automata, Definitions, Definitions
|
|
@appendixsec LTL formulas
|
|
|
|
@command{lbtt} uses the traditional definition for propositional linear
|
|
temporal logic. Let @math{AP} be a finite set of atomic propositions.
|
|
The set of propositional linear temporal logic formulas is defined inductively
|
|
as follows:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
@cindex @samp{t} (Boolean constant semantics in LTL)
|
|
@cindex true (Boolean constant semantics in LTL)
|
|
All atomic propositions in @math{AP} and the Boolean constant
|
|
@iftex
|
|
@tex
|
|
\sc{True}
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{true}
|
|
@end ifnottex
|
|
are LTL formulas.
|
|
|
|
@item
|
|
If
|
|
@iftex
|
|
@tex
|
|
$\varphi$ and $\psi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{f1} and @samp{f2}
|
|
@end ifnottex
|
|
are LTL formulas, then
|
|
@iftex
|
|
@tex
|
|
$\neg\varphi, {\bf X}\varphi, (\varphi\vee\psi)$ and $(\varphi\;{\bf U}\;\psi)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{! f1}, @samp{X f1}, @samp{(f1 \/ f2)} and @samp{(f1 U f2)}
|
|
@end ifnottex
|
|
are LTL formulas.
|
|
|
|
@end itemize
|
|
|
|
The semantics of linear temporal logic
|
|
(i.e., a satisfiability
|
|
@iftex
|
|
relation, denoted by
|
|
@tex
|
|
$\models$)
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
relation)
|
|
@end ifnottex
|
|
is defined over infinite sequences
|
|
@iftex
|
|
@tex
|
|
$\xi = \langle y_0, y_1, y_2, \ldots \rangle \in (2^{AP})^\omega$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x = <y(0), y(1), y(2), ...>}
|
|
@end ifnottex
|
|
over subsets of @math{AP} as follows:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\xi \models$ \sc{True} for all sequences $\xi$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{true} for all sequences @math{x}.
|
|
@end ifnottex
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\xi \models p \in {\it AP}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies an atomic proposition @samp{p}
|
|
@end ifnottex
|
|
if and only if
|
|
@iftex
|
|
@tex
|
|
$p \in y_0$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{p} belongs to @math{y(0)},
|
|
@end ifnottex
|
|
the first element of the sequence
|
|
@iftex
|
|
@tex
|
|
$\xi$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x}.
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{!} (operator semantics in LTL)
|
|
@cindex negation (operator semantics in LTL)
|
|
@iftex
|
|
@tex
|
|
$\xi \models \neg\varphi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{! f}
|
|
@end ifnottex
|
|
if and only if it is not the case that
|
|
@iftex
|
|
@tex
|
|
$\xi \models \varphi$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{f}.
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{\/} (operator semantics in LTL)
|
|
@cindex @emph{or} (operator semantics in LTL)
|
|
@cindex disjunction (operator semantics in LTL)
|
|
@iftex
|
|
@tex
|
|
$\xi \models \varphi\vee\psi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{f1 \/ f2}
|
|
@end ifnottex
|
|
if and only if
|
|
@iftex
|
|
@tex
|
|
$\xi \models \varphi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{f1}
|
|
@end ifnottex
|
|
or
|
|
@iftex
|
|
@tex
|
|
$\xi \models \psi$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{f2}.
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{X} (operator semantics in LTL)
|
|
@cindex next time (operator semantics in LTL)
|
|
@iftex
|
|
@tex
|
|
$\xi \models {\bf X}\varphi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{X f}
|
|
@end ifnottex
|
|
if and only if
|
|
@iftex
|
|
@tex
|
|
$\langle y_1, y_2, y_3, \ldots\rangle \models \varphi$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<y(1), y(2), y(3), ...>} satisfies @samp{f}.
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{U} (operator semantics in LTL)
|
|
@cindex strong until (operator semantics in LTL)
|
|
@cindex until (operator semantics in LTL)
|
|
@iftex
|
|
@tex
|
|
$\xi \models \varphi\;{\bf U}\;\psi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x} satisfies @samp{f1 U f2}
|
|
@end ifnottex
|
|
if and only if there exists an
|
|
@iftex
|
|
@tex
|
|
$i \geq 0$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{i >= 0}
|
|
@end ifnottex
|
|
such that
|
|
@iftex
|
|
@tex
|
|
$\langle y_i, y_{i+1},$ $y_{i+2}, \ldots\rangle \models \psi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<y(i), y(i+1), y(i+2), ...>} satisfies @samp{f2}
|
|
@end ifnottex
|
|
and for all
|
|
@iftex
|
|
@tex
|
|
$0 \leq j < i, \langle y_j, y_{j+1}, y_{j+2}, \ldots \rangle \models \varphi$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{0 <= j < i}, @math{<y(j), y(j+1), y(j+2), ...>} satisfies @samp{f1}.
|
|
@end ifnottex
|
|
|
|
@end itemize
|
|
|
|
@command{lbtt} also supports the following operators and Boolean constants,
|
|
the definitions of which can be given in terms of the previously defined
|
|
operators:
|
|
|
|
@itemize @bullet
|
|
@item
|
|
@cindex @samp{f} (Boolean constant semantics in LTL)
|
|
@cindex false (Boolean constant semantics in LTL)
|
|
``false'':
|
|
@iftex
|
|
@tex
|
|
\sc{False} $\equiv_{\rm def} \neg\!$ \sc{True}
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{false} := @samp{! true}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{/\} (operator semantics in LTL)
|
|
@cindex @emph{and} (operator semantics in LTL)
|
|
@cindex conjunction (operator semantics in LTL)
|
|
logical conjunction:
|
|
@iftex
|
|
@tex
|
|
$(\varphi \wedge \psi) \equiv_{\rm def} \neg(\neg\varphi \vee \neg\psi)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 /\ f2)} := @samp{! (! f1 \/ ! f2)}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{->} (operator semantics in LTL)
|
|
@cindex implication (operator semantics in LTL)
|
|
logical implication:
|
|
@iftex
|
|
@tex
|
|
$(\varphi \rightarrow \psi) \equiv_{\rm def} (\neg\varphi \vee \psi)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 -> f2)} := @samp{(! f1 \/ f2)}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{<->} (operator semantics in LTL)
|
|
@cindex equivalence (operator semantics in LTL)
|
|
logical equivalence:
|
|
@iftex
|
|
@tex
|
|
$(\varphi \leftrightarrow \psi) \equiv_{\rm def} ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 <-> f2)} := @samp{((f1 -> f2) /\ (f2 -> f1))}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{xor} (operator semantics in LTL)
|
|
@cindex exclusive or (operator semantics in LTL)
|
|
logical ``exclusive or'':
|
|
@iftex
|
|
@tex
|
|
$(\varphi \oplus \psi) \equiv_{\rm def} \neg(\varphi \leftrightarrow \psi)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 xor f2)} := @samp{! (f1 <-> f2)}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{F} (operator semantics in LTL)
|
|
@cindex finally (operator semantics in LTL)
|
|
@cindex eventually (operator semantics in LTL)
|
|
temporal ``finally'':
|
|
@iftex
|
|
@tex
|
|
${\bf F} \varphi \equiv_{\rm def} ($\sc{True}$\;{\bf U}\;\varphi)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{<> f} := @samp{(true U f)}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{G} (operator semantics in LTL)
|
|
@cindex globally (operator semantics in LTL)
|
|
@cindex always (operator semantics in LTL)
|
|
@cindex henceforth (operator semantics in LTL)
|
|
temporal ``globally'':
|
|
@iftex
|
|
@tex
|
|
${\bf G} \varphi \equiv_{\rm def} \neg{\bf F}\neg\varphi$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{[] f} := @samp{! <> ! f}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{V} (operator semantics in LTL)
|
|
@cindex weak release (operator semantics in LTL)
|
|
@cindex release (operator semantics in LTL)
|
|
temporal ``(weak) release'':
|
|
@iftex
|
|
@tex
|
|
$(\varphi\;{\bf V}\;\psi) \equiv_{\rm def} \neg(\neg\varphi\;{\bf U}\;\neg\psi)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 V f2)} := @samp{! (! f1 U ! f2)}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{W} (operator semantics in LTL)
|
|
@cindex weak until (operator semantics in LTL)
|
|
@cindex unless (operator semantics in LTL)
|
|
temporal ``weak until'':
|
|
@iftex
|
|
@tex
|
|
$(\varphi\;{\bf W}\;\psi) \equiv_{\rm def} \big((\varphi\;{\bf U}\;\psi) \vee {\bf G}\varphi\big)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 W f2)} := @samp{((f1 U f2) \/ [] f1)}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{M} (operator semantics in LTL)
|
|
@cindex strong release (operator semantics in LTL)
|
|
temporal ``strong release'':
|
|
@iftex
|
|
@tex
|
|
$(\varphi\;{\bf M}\;\psi) \equiv_{\rm def} \big((\varphi\;{\bf V}\;\psi) \wedge {\bf F}\varphi\big)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 M f2)} := @samp{((f1 V f2) /\ <> f1)}
|
|
@end ifnottex
|
|
|
|
@item
|
|
@cindex @samp{B} (operator semantics in LTL)
|
|
@cindex before (operator semantics in LTL)
|
|
temporal ``before'':
|
|
@iftex
|
|
@tex
|
|
$(\varphi\;{\bf B}\;\psi) \equiv_{\rm def} \neg(\neg\varphi\;\bf{U}\;\psi)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@samp{(f1 B f2)} := @samp{! (! f1 U f2)}
|
|
@end ifnottex
|
|
|
|
@end itemize
|
|
|
|
|
|
|
|
@node Generalized automata, State spaces, LTL formulas, Definitions
|
|
@appendixsec Generalized automata
|
|
|
|
@cindex B@"uchi automata, formal definition
|
|
@cindex generalized B@"uchi automata, formal definition
|
|
|
|
@command{lbtt} uses internally finite-state automata on infinite words
|
|
(B@"uchi automata) over the alphabet
|
|
@iftex
|
|
@tex
|
|
$2^{AP}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{2^AP}
|
|
@end ifnottex
|
|
(where @math{AP} is a finite set of atomic propositions)
|
|
with one initial state, labels on transitions and zero or more acceptance
|
|
conditions.
|
|
|
|
@appendixsubsec Formal definition of generalized automata
|
|
|
|
Formally, a generalized B@"uchi automaton can be represented as a
|
|
tuple@footnote{This definition differs from those commonly found in
|
|
the literature by specifying the acceptance conditions in terms of a separate
|
|
set that is independent of the other components of the automaton, together with
|
|
an
|
|
explicit labeling function for the states. This is to allow the definition to
|
|
correspond more accurately to the automata that can be described in
|
|
input files.}
|
|
@iftex
|
|
@tex
|
|
$\langle \Sigma, Q, \Delta, q_I, \cal{F}, \lambda\rangle$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<S, Q, R, q, F, L>},
|
|
@end ifnottex
|
|
where
|
|
|
|
@itemize @bullet
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\Sigma$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{S}
|
|
@end ifnottex
|
|
is the finite @emph{alphabet}
|
|
@iftex
|
|
@tex
|
|
($\Sigma = 2^{AP}$ in this case),
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
(@math{S = 2^AP} in this case),
|
|
@end ifnottex
|
|
|
|
@item
|
|
@math{Q} is the finite set of @emph{states},
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\Delta \subseteq Q \times 2^\Sigma \times 2^{\cal{F}} \times Q$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{R} (a subset of @math{Q x 2^S x 2^F x Q})
|
|
@end ifnottex
|
|
is the set of @emph{transitions} (each of which consists of four components
|
|
called the @emph{start state}, the @emph{guard}, the
|
|
@emph{acceptance component}, and the @emph{target state}, respectively),
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$q_I$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{q}
|
|
@end ifnottex
|
|
is the @emph{initial state},
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
${\cal F} = \{f_1,f_2,\ldots,f_n\}$ (for some finite $n$)
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{F = @{f1, f2, ..., fn@} (for some finite @math{n})}
|
|
@end ifnottex
|
|
is the set of @emph{acceptance conditions} (a ``nongeneralized''
|
|
B@"uchi automaton has exactly one acceptance condition), and
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\lambda: Q \rightarrow 2^{\cal F}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{L: Q -> 2^F}
|
|
@end ifnottex
|
|
is a @emph{labeling function} that associates each state of the automaton
|
|
with a set of acceptance conditions.
|
|
|
|
@end itemize
|
|
|
|
A @emph{run} of a B@"uchi automaton on an infinite sequence
|
|
@iftex
|
|
@tex
|
|
$\langle x_0, x_1, x_2, \ldots \rangle \in (2^{AP})^\omega$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<x(0), x(1), x(2), ...>}
|
|
@end ifnottex
|
|
over the alphabet
|
|
@iftex
|
|
@tex
|
|
$2^{AP}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{2^AP}
|
|
@end ifnottex
|
|
is an infinite sequence of pairs of states and transitions
|
|
@iftex
|
|
@tex
|
|
$\langle (q_0, t_0), (q_1, t_1), (q_2, t_2), \ldots \rangle \in
|
|
(Q\times\Delta)^\omega$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<(q(0),t(0)), (q(1),t(1)), (q(2),t(2)) ...>}
|
|
(where each @math{q(i)} is a state in @math{Q} and each @math{t(i)} is a
|
|
transition in @math{R})
|
|
@end ifnottex
|
|
such that
|
|
@iftex
|
|
@tex
|
|
$q_0 = q_I$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{q(0) = q}
|
|
@end ifnottex
|
|
and for all
|
|
@iftex
|
|
@tex
|
|
$i \geq 0$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{i >= 0},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$t_i = \langle q_i, X_i, Y_i, q_{i+1}\rangle \in \Delta$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{t(i) = <q(i), X(i), Y(i), q(i+1)>} in @math{R}
|
|
@end ifnottex
|
|
such that
|
|
@iftex
|
|
@tex
|
|
$x_i \in X_i$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x(i)} belongs to @math{X(i)}.
|
|
@end ifnottex
|
|
(Because the relation
|
|
@iftex
|
|
@tex
|
|
$\Delta$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{R}
|
|
@end ifnottex
|
|
is not necessarily a function from
|
|
@iftex
|
|
@tex
|
|
$Q \times 2^\Sigma \times 2^{\cal{F}}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{Q x 2^S x 2^F}
|
|
@end ifnottex
|
|
to
|
|
@iftex
|
|
@tex
|
|
$Q$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{Q},
|
|
@end ifnottex
|
|
the automaton may have many runs on the same input.)
|
|
|
|
A run
|
|
@iftex
|
|
@tex
|
|
$\langle (q_0,t_0), (q_1,t_1), (q_2,t_2), \ldots\rangle$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<(q(0),t(0)), (q(1),t(1)), (q(2),t(2)), ...>}
|
|
@end ifnottex
|
|
(where
|
|
@iftex
|
|
@tex
|
|
$t_i = \langle q_i,X_i,Y_i,q_{i+1}\rangle\in\Delta$ for all $i$)
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{t(i) = < q(i), X(i), Y(i), q(i+1) >} for all @math{i})
|
|
@end ifnottex
|
|
is @emph{accepting} if and only if additionally, for each acceptance condition
|
|
@iftex
|
|
@tex
|
|
$f \in {@cal F}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{f} in @math{F},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$f \in \lambda(q_i)$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{f} is in @math{L(q(i))}
|
|
@end ifnottex
|
|
or
|
|
@iftex
|
|
@tex
|
|
$f \in Y_i$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{f} is in @math{Y(i)}
|
|
@end ifnottex
|
|
for infinitely many
|
|
@iftex
|
|
@tex
|
|
$i$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{i}.
|
|
@end ifnottex
|
|
|
|
The automaton @emph{accepts} an infinite sequence
|
|
@iftex
|
|
@tex
|
|
$\langle x_0, x_1, x_2, \ldots\rangle \in 2^{AP}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<x(0), x(1), x(2), ...>} over the alphabet @math{2^AP}
|
|
@end ifnottex
|
|
if and only if the automaton has at least one accepting run on this sequence.
|
|
|
|
@appendixsubsec Transition label encoding
|
|
|
|
When working with automata on words over the alphabet
|
|
@iftex
|
|
@tex
|
|
$2^{AP}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{2^AP},
|
|
@end ifnottex
|
|
the guards of transitions can be expressed as propositional formulas by
|
|
identifying a set of symbols from this alphabet with the set of models of a
|
|
propositional formula. A transition can then be seen as a rule ``if in state
|
|
@iftex
|
|
@tex
|
|
$q_i$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{q(i)}
|
|
@end ifnottex
|
|
and the next input symbol
|
|
@iftex
|
|
@tex
|
|
$x_i$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x(i)}
|
|
@end ifnottex
|
|
is a model of the propositional formula guarding the transition, the automaton
|
|
can move to state
|
|
@iftex
|
|
@tex
|
|
$q_{i+1}$''.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{q(i+1)}''.
|
|
@end ifnottex
|
|
In the context of B@"uchi automata constructed from LTL formulas, this
|
|
often allows for a compact representation for the transitions.
|
|
|
|
@appendixsubsec Converting between equivalent definitions
|
|
|
|
Many LTL-to-B@"uchi translation algorithms presented in the literature
|
|
(for example,
|
|
@ifnottex
|
|
@ref{[GPVW95]})
|
|
@end ifnottex
|
|
@iftex
|
|
[GPVW95])
|
|
@end iftex
|
|
are based on a slightly different definition for generalized B@"uchi automata,
|
|
where the automata can have several initial states, acceptance is determined
|
|
using a family of sets of states, and the guards of transitions are replaced
|
|
with an additional state labeling that associates a set of LTL
|
|
formulas with each state. These automata can easily be described using the
|
|
above definition through the following steps:
|
|
|
|
@enumerate
|
|
@item
|
|
Add a new state (associated with an empty set of LTL formulas) into the
|
|
automaton and add transitions from it to each initial state of the original
|
|
automaton. Make the new state the (only) initial state of the automaton.
|
|
|
|
@item
|
|
For each state of the (modified) automaton, construct a conjunction of all
|
|
propositional constraints (all formulas with no temporal operators)
|
|
associated with the state and make the conjunction the guard of each transition
|
|
coming into the state (the acceptance component of each transition remains
|
|
empty). Then remove the association between states and sets of formulas.
|
|
|
|
@item
|
|
If
|
|
@iftex
|
|
@tex
|
|
$Q_1,Q_2,\ldots,Q_k \in 2^Q$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{Q1, Q2, ..., Qk} (subsets of @math{Q})
|
|
@end ifnottex
|
|
are the sets of states determining acceptance in the original automaton,
|
|
let
|
|
@iftex
|
|
@tex
|
|
$f_i = Q_i$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{fi = Qi}
|
|
@end ifnottex
|
|
for all
|
|
@iftex
|
|
@tex
|
|
$1 \leq i \leq k$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{1 <= 1 <= k},
|
|
@end ifnottex
|
|
and let
|
|
@iftex
|
|
@tex
|
|
$\lambda(q) = \{f_i\mid q \in f_i\}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{L(q) = @{fi | q is a member of fi@}}
|
|
@end ifnottex
|
|
for all states
|
|
@iftex
|
|
@tex
|
|
$q$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{q}.
|
|
@end ifnottex
|
|
@end enumerate
|
|
|
|
|
|
|
|
@node State spaces, , Generalized automata, Definitions
|
|
@appendixsec State spaces
|
|
|
|
@cindex state space, formal definition
|
|
@command{lbtt} uses randomly generated state spaces in the
|
|
model checking result cross-comparison test
|
|
(@pxref{Model checking result cross-comparison test}) and
|
|
the model checking result consistency check
|
|
(@pxref{Model checking result consistency check}). Formally,
|
|
the state spaces are (finite) Kripke structures with a total transition
|
|
relation, i.e., directed graphs with a set of atomic propositions
|
|
attached to each state, with each state having at least one
|
|
immediate successor (which may be the state itself). The precise
|
|
definition is as follows (as before, let @math{AP} be a
|
|
finite set of atomic propositions).
|
|
|
|
A state space can be represented as a tuple
|
|
@iftex
|
|
@tex
|
|
$\langle S, \rho, {\cal L}\rangle$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<S, R, L>},
|
|
@end ifnottex
|
|
where
|
|
|
|
@itemize @bullet
|
|
|
|
@item
|
|
@math{S} is the finite set of @emph{states},
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\rho \subseteq S \times S$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{R} (a subset of @math{S x S})
|
|
@end ifnottex
|
|
is the @emph{transition relation}, and
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
${\cal L}: S \rightarrow 2^{AP}$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{L: S -> 2^AP}
|
|
@end ifnottex
|
|
is the @emph{labeling function} which maps each state to a set of atomic
|
|
propositions that hold in the state.
|
|
|
|
@end itemize
|
|
|
|
|
|
|
|
@node Configuration file option index, Command line option index, Definitions, Top
|
|
@unnumbered Configuration file option index
|
|
|
|
@printindex fn
|
|
|
|
|
|
|
|
@node Command line option index, User command index, Configuration file option index, Top
|
|
@unnumbered Command line option index
|
|
|
|
@printindex vr
|
|
|
|
|
|
|
|
@node User command index, Concept index, Command line option index, Top
|
|
@unnumbered User command index
|
|
|
|
@printindex ky
|
|
|
|
|
|
@node Concept index, , User command index, Top
|
|
@unnumbered Concept index
|
|
|
|
@printindex cp
|
|
|
|
@bye
|