4751 lines
156 KiB
Text
4751 lines
156 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{} 2003 Heikki Tauriainen
|
|
@ifinfo
|
|
@email{heikki.tauriainen@@hut.fi}
|
|
@end ifinfo
|
|
@ifnotinfo
|
|
@ifnothtml
|
|
<@email{heikki.tauriainen@@hut.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.0.x
|
|
@author Heikki Tauriainen <@email{heikki.tauriainen@@hut.fi}>
|
|
@page
|
|
@vskip 0pt plus 1filll
|
|
Copyright @copyright{} 2003 Heikki Tauriainen
|
|
<@email{heikki.tauriainen@@hut.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), (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.0.1 of the @command{lbtt} documentation. This edition
|
|
applies to @command{lbtt} versions 1.0.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 automatic testing of programs which 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 execution 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 is often specified as an
|
|
LTL formula, and the B@"uchi automaton used for model checking is obtained
|
|
automatically from the formula with a translation algorithm. (Detailed
|
|
descriptions and optimization techniques for such algorithms can be found, for
|
|
example, in
|
|
@ifnottex
|
|
@ref{[GPVW95]},
|
|
@ref{[Cou99]}
|
|
@ref{[DGV99]},
|
|
@ref{[Ete99]},
|
|
@ref{[SB00]},
|
|
@ref{[EH00]},
|
|
@ref{[EWS01]},
|
|
@ref{[GO01]}.)
|
|
@end ifnottex
|
|
@iftex
|
|
[GPVW95, Cou99, DGV99, Ete99, SB00, EH00, EWS01, GO01].)
|
|
@end iftex
|
|
In practice, the implementation correctness of such a translation algorithm
|
|
is crucial to the soundness of the model checking procedure.
|
|
|
|
The goal of @command{lbtt} is to assist in the correct implementation of
|
|
LTL-to-B@"uchi translation algorithms 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 operate 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 tests
|
|
suggest an implementation
|
|
error in a translator, @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 implementation errors
|
|
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.
|
|
* Buchi 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
|
|
(@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 labelled 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
|
|
(representing a set of conditions 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 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 occurrence likelihood 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}' \in \{\neg, \bf{X}, \bf{F}, \bf{G}\}}\it{pri}\it(op')
|
|
$$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{pri(@var{op}) / Sum (pri(@var{op'}))},
|
|
@end ifnottex
|
|
|
|
@noindent
|
|
where
|
|
@iftex
|
|
@tex
|
|
$\it{op}'$
|
|
@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}' \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')
|
|
$$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{pri(@var{op}) / Sum (pri(@var{op'}))},
|
|
@end ifnottex
|
|
|
|
@noindent
|
|
where
|
|
@iftex
|
|
@tex
|
|
$\it{op}'$
|
|
@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.
|
|
|
|
|
|
|
|
@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 labelled graphs, each node of which is labelled
|
|
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, you should always start testing 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 stays 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{Buchi
|
|
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, Buchi 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 Buchi automata intersection emptiness check, , Model checking result consistency check, Test methods
|
|
@section Buchi automata intersection emptiness check
|
|
|
|
@cindex B@"uchi automata intersection emptiness check
|
|
@cindex tests, B@"uchi automata intersection emptiness check
|
|
|
|
The semantics of LTL guarantee 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 must be
|
|
always enclosed in quotes (@samp{"}).
|
|
The backslash (@samp{\}) is treated as an escape character (to be used
|
|
e.g.@: if the string itself contains quotes; use @samp{\\} to get a backslash).
|
|
|
|
@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{Algorithm}
|
|
section specifying an LTL-to-B@"uchi translator. The other sections
|
|
are optional and can be used to override the default testing parameters.
|
|
|
|
@menu
|
|
* Algorithm section:: Each LTL-to-B@"uchi translator to be
|
|
tested requires a separate
|
|
@samp{Algorithm} 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 Algorithm section, GlobalOptions section, Configuration file, Configuration file
|
|
@subsection The @samp{Algorithm} section
|
|
|
|
@cindex configuration file, @samp{Algorithm} section
|
|
@cindex @samp{Algorithm} section (configuration file)
|
|
@cindex configuration file, minimal requirements
|
|
|
|
Each LTL-to-B@"uchi translator to be tested requires a separate
|
|
@samp{Algorithm} section 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 configuration file,
|
|
starting from zero. These numbers must be used when referring to the
|
|
different translators when using @command{lbtt}'s internal commands
|
|
(@pxref{Analyzing test results}).
|
|
|
|
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{[}Algorithm@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{[}Algorithm@r{]}
|
|
This option can be used to specify a textual identifier for the LTL-to-B@"uchi
|
|
translator. This identifier will then be used when displaying various messages
|
|
concerning the implementation. (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.)
|
|
|
|
@item Parameters = @var{STRING}
|
|
@findex Parameters @r{[}Algorithm@r{]}
|
|
This option can be used to specify any additional parameters that should
|
|
be passed to the translator executable whenever running it. (The default
|
|
value of this option is the empty string.)
|
|
|
|
@item Path = @var{STRING}
|
|
@findex Path @r{[}Algorithm@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, Algorithm 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 = Always @r{|} OnError @r{|} Never
|
|
@cindex interactivity modes
|
|
@findex Interactive @r{[}GlobalOptions@r{]}
|
|
The interactivity mode determines whether @command{lbtt} should pause to wait
|
|
for user input between test rounds. A value of @samp{Always} causes
|
|
@command{lbtt} to pause unconditionally after each test round, @samp{OnError}
|
|
will interrupt testing only after failed test rounds, and @samp{Never} will
|
|
simply run all tests without interruption.
|
|
|
|
The default value for this option is @samp{Always}.
|
|
|
|
@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{Buchi 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 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}
|
|
@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 three dots 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
|
|
@ifnottex
|
|
(@pxref{FormulaOptions section}).
|
|
@end ifnottex
|
|
@iftex
|
|
(see the previous section).
|
|
@end iftex
|
|
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}
|
|
@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
|
|
|
|
Algorithm
|
|
@{
|
|
Name = "Translator 1"
|
|
Path = "~/lbtt/bin/t-1" # location of the translator
|
|
# executable
|
|
Enabled = Yes
|
|
@}
|
|
|
|
Algorithm
|
|
@{
|
|
Name = "Translator 2"
|
|
Path = "~/lbtt/bin/t-2"
|
|
Parameters = "-x -y 3 -v 0" # parameters to be passed to the
|
|
# `~/lbtt/bin/t-2' executable
|
|
Enabled = Yes
|
|
@}
|
|
|
|
GlobalOptions
|
|
@{
|
|
Rounds = 100 # 100 test rounds
|
|
|
|
Interactive = OnError # pause only in case of an error
|
|
|
|
Verbosity = 1 # suppress most of the output
|
|
|
|
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
|
|
@}
|
|
|
|
FormulaOptions
|
|
@{
|
|
AbbreviatedOperators = Yes # formula generation mode
|
|
GenerateMode = Normal
|
|
OutputMode = Normal
|
|
|
|
ChangeInterval = 1 # new formula after each test
|
|
# round
|
|
|
|
RandomSeed = 4632912 # random seed
|
|
|
|
Size = 5...15 # 5 to 15 nodes in the parse
|
|
# tree of each formula
|
|
|
|
Propositions = 3 # max. 3 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
|
|
|
|
NextPriority = 5 # priorities for some temporal
|
|
UntilPriority = 5 # operators
|
|
ReleasePriority = 5
|
|
|
|
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 # 3 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
|
|
@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 instead of generating them randomly. The file should contain
|
|
LTL formulas separated from each other with white space. Currently the
|
|
only supported format for the formulas is the same prefix notation that
|
|
@command{lbtt} uses for its output files (@pxref{Format for LTL formulas},
|
|
for details).
|
|
|
|
If this option is used, all LTL formula generation parameters in the command
|
|
line or in the configuration file 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. These options also imply the @samp{--nopause} option, i.e., all
|
|
tests will be run without interruption. 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 --version
|
|
@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
|
|
@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
|
|
@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 integers (the implementation identifiers).
|
|
The implementations are numbered in the order in which they appear in the
|
|
configuration file, starting from zero. (The @samp{--showconfig}
|
|
option, see @ref{Special options}, can be used 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=always | onerror | never
|
|
@vindex --interactive
|
|
@cindex interactivity modes
|
|
This option can be used to override whether @command{lbtt} should pause
|
|
between test rounds to wait for user input.
|
|
|
|
@item --intersectiontest
|
|
@item --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{Buchi 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 --nopause
|
|
@vindex --nopause
|
|
@cindex interactivity modes
|
|
This option forces @command{lbtt} to run all tests without interruption.
|
|
|
|
@item --pause
|
|
@vindex --pause
|
|
@cindex interactivity modes
|
|
This option forces @command{lbtt} to pause between each test round to
|
|
wait for user commands.
|
|
|
|
@item --pauseonerror
|
|
@vindex --pauseonerror
|
|
@cindex interactivity modes
|
|
Using this option will cause testing to be paused each time an error occurs
|
|
during testing,
|
|
giving the user an opportunity to analyze the error situation using
|
|
@command{lbtt}'s internal commands before proceeding to the next test round.
|
|
|
|
@item --rounds=@var{NUMBER-OF-ROUNDS}
|
|
@vindex --rounds
|
|
This option can be used to override the number of test rounds to run.
|
|
|
|
@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
|
|
@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}
|
|
@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 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}
|
|
@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 is using enumerated paths as state
|
|
spaces.)
|
|
|
|
@end table
|
|
|
|
|
|
|
|
@node Interpreting the output, Analyzing test results, Invocation, Top
|
|
@chapter Interpreting the output
|
|
|
|
This chapter briefly intoduces the most typical messages that
|
|
@command{lbtt} outputs during testing when running in its default output
|
|
verbosity mode (3). In lower verbosity modes some (or all) of these
|
|
messages will be suppressed; higher verbosity modes show information about
|
|
@command{lbtt}'s internal behavior.
|
|
|
|
@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} shows a short 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
|
|
a file; @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.
|
|
Using global model checking for tests.
|
|
Writing error log to `error.log'.
|
|
|
|
Implementations:
|
|
0: `Implementation 0'
|
|
1: `Implementation 1'
|
|
|
|
Enabled tests:
|
|
Model checking result cross-comparison test
|
|
Model checking result consistency check
|
|
B@"uchi automata intersection emptiness check
|
|
|
|
Random state spaces:
|
|
Random connected 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 20 20 20 10 20
|
|
@end smallexample
|
|
|
|
@node Test round messages, Test statistics, Configuration information, Interpreting the output
|
|
@section Test round messages
|
|
|
|
The following example shows a fragment of the output that @command{lbtt} might
|
|
produce during a test round:
|
|
|
|
@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
|
|
Information about a random LTL formula and its negation. Note that in the
|
|
printed output, it is assumed (to remove some parentheses) that all unary
|
|
formula operators have strictly 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).
|
|
|
|
@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).
|
|
|
|
(If the implementation used for translating the positive formula
|
|
@samp{((p1 <-> p0) U (p0 \/ ! p3))} into a B@"uchi automaton is known to be
|
|
correct, the result would then also indicate that no infinite path in the state
|
|
space satisfies the formula.)
|
|
|
|
@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 case,
|
|
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{Buchi automata intersection emptiness check}).
|
|
|
|
The model checking result cross-comparison test might result in the following
|
|
output:
|
|
|
|
@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. In the output, the
|
|
internal implementation has the name @samp{lbtt} and no numeric identifier.
|
|
|
|
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. 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{Buchi automata intersection emptiness check}) for each
|
|
pair of implementations.
|
|
@end itemize
|
|
|
|
Note that the pairwise inconsistency results form a symmetric matrix (although
|
|
@command{lbtt} might display the matrix 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 (either after each test round or only in
|
|
case 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 accept or require 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.
|
|
|
|
@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 written to a pipe (to be processed by an external
|
|
program) instead of a file. This is done by ending the command line with
|
|
@samp{| @var{command}}, where @var{command} is the command line for the
|
|
external program intended to process the output produced by @command{lbtt}.
|
|
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 @emph{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 (@samp{<}, @samp{>})
|
|
denote obligatory command parameters, while arguments in square brackets
|
|
(@samp{[}, @samp{]}) are optional. A vertical bar (@samp{|}) 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 the current interactivity mode requires it
|
|
(@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 this is required 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 or 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
|
|
@kindex algorithms
|
|
Show a list of implementations declared in the program configuration file and
|
|
whether they are currently enabled for testing. The list also shows the
|
|
numeric identifiers of the implementations. These identifiers
|
|
should be used with commands that accept or require implementation identifier
|
|
lists as arguments.
|
|
|
|
@item buchi @r{[}+ @r{|} -@r{]} @var{implementation-id} @r{[}@var{state-id-list} | 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 only certain 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{[}@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
|
|
``traditional'' semantics of LTL, 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 as
|
|
true if even @emph{one} of these paths is accepted by the automaton.
|
|
|
|
Note 2: If using random or enumerated paths as state spaces, @command{lbtt}
|
|
accepts also the symbol @samp{p} in the implementation identifier list. This
|
|
symbol can be used for accessing the model checking results computed using
|
|
@command{lbtt}'s internal ``path'' model checking algorithm.
|
|
|
|
@item formula @r{[}+ @r{|} -@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.
|
|
|
|
@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 for each implementation in the list (or all
|
|
implementations if the list is omitted) in a format very similar to test
|
|
messages shown when running @command{lbtt} in its default verbosity mode 3.
|
|
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{|} 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
|
|
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 @var{implementation-id} @var{implementation-id}
|
|
@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{Buchi 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, model
|
|
checks the positive formula in the witness, 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 @var{implementation-id} @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 space state in which to perform the analysis (use the
|
|
@samp{inconsistencies} command, @ref{Data display commands}, to see a list
|
|
of all state space states in which the check failed). If the state identifier
|
|
is not present, @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, model checks the positive formula in the
|
|
witness separately, and tells which one of the automata seems to reject the
|
|
witness incorrectly.
|
|
|
|
@item resultanalysis @r{[}+ @r{|} -@r{]} @var{implementation-id} @var{implementation-id} @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 a state space state identifier
|
|
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 symbol @samp{p} 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 linear sequence of
|
|
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 look as follows:
|
|
|
|
@smallexample
|
|
Execution M:
|
|
prefix: < s0 @{p0, p4@},
|
|
s2 @{p1, p2, p3, p4@} >
|
|
cycle: < s34 @{p0, p1, p2, p3, p4@},
|
|
s42 @{p4@},
|
|
s44 @{p1, p4@} >
|
|
@end smallexample
|
|
|
|
@noindent
|
|
In this case, the witness (or ``execution'' as displayed in the output)
|
|
@math{M} consists of a prefix of two states followed by a cycle of three
|
|
states. Each state is associated with a set of atomic propositions that hold
|
|
in the state.
|
|
|
|
(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_0, s_2, s_{34}, s_{42}, s_{44}\}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{S = @{s0, s2, s34, s42, s44@}},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
$\rho = \{(s_0, s_2), (s_2, s_{34}), (s_{34}, s_{42}), (s_{42}, s_{44}),
|
|
(s_{44}, s_{34})\}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{R = @{(s0, s2), (s2, s34), (s34, s42), (s42, s44), (s44, s34)@}},
|
|
@end ifnottex
|
|
@iftex
|
|
@tex
|
|
${\cal L}(s_0) = \{p_0, p_4\}, {\cal L}(s_2) = \{p_1, p_2, p_3, p_4\},
|
|
{\cal L}(s_{34}) = \{p_0, p_1, p_2, p_3, p_4\}, {\cal L}(s_{42}) = \{p_4\},$
|
|
and ${\cal L}(s_{44}) = \{p_1, p_4\}$.)
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{L(s0) = @{p0, p4@}, L(s2) = @{p1, p2, p3, p4@}, L(s34) = @{p0, p1, p2, p3, p4@}, L(s42) = @{p4@},} and @math{L(s44) = @{p1, p4@}}.)
|
|
@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,<s0, ...> |== ((p1 U p4) <-> (! p1 -> [] p4)) :
|
|
+-> M,<s0, ...> |== (p1 U p4) :
|
|
| +-> M,<s0, ...> |== p4
|
|
+-> M,<s0, ...> |== (! p1 -> [] p4) :
|
|
+-> M,<s0, ...> |== [] p4 :
|
|
+-> M,<s0, ...> |== p4
|
|
+-> s0 --> s2
|
|
+-> M,<s2, ...> |== p4
|
|
+-> s2 --> s34
|
|
+-> M,<s34, ...> |== p4
|
|
+-> s34 --> s42
|
|
+-> M,<s42, ...> |== p4
|
|
+-> s42 --> s44
|
|
+-> M,<s44, ...> |== p4
|
|
+-> s44 --> s34
|
|
@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 @math{M}. 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 linear sequence, that this
|
|
is the @emph{only} transition originating from @samp{sn}).
|
|
|
|
In the above example, @command{lbtt} claims that the formula
|
|
@samp{((p1 U p4) <-> (! p1 -> [] p4))} holds in the witness presented earlier
|
|
in this section, and that this follows (by the semantics of logical
|
|
equivalence) from the claims that the subformulas @samp{(p1 U p4)} and
|
|
@samp{(! p1 -> [] p4)} both hold in the same witness.
|
|
@samp{(p1 U p4)} holds in the witness because of the fact that
|
|
@iftex
|
|
@tex
|
|
$p_4 \in {\cal L}(s_0)$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{p4} is included in @math{L(s0)},
|
|
@end ifnottex
|
|
and the truth of the implication @samp{(! p1 -> [] p4)} is justified by the
|
|
property that
|
|
@iftex
|
|
@tex
|
|
$p_4$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{p4}
|
|
@end ifnottex
|
|
holds in all states of the (only) infinite sequence beginning at the state
|
|
@iftex
|
|
@tex
|
|
$s_0$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
s0,
|
|
@end ifnottex
|
|
which can be seen from the proof.
|
|
|
|
|
|
|
|
@node Interfacing with lbtt, References, Analyzing test results, Top
|
|
@chapter Interfacing LTL-to-B@"uchi translators with @command{lbtt}
|
|
|
|
@cindex LTL-to-B@"uchi translators, interfacing with
|
|
@cindex interfacing LTL-to-B@"uchi translators with @command{lbtt}
|
|
|
|
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
|
|
@ifnottex
|
|
@ref{The lbtt-translate utility}
|
|
@end ifnottex
|
|
@iftex
|
|
the next chapter
|
|
@end iftex
|
|
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.
|
|
* Buchi 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, Interfacing with lbtt
|
|
@section Translator interface requirements
|
|
|
|
@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{Buchi 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 any non-zero 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{Algorithm} section for it into
|
|
@command{lbtt}'s configuration file (@pxref{Configuration file}), for example
|
|
|
|
@smallexample
|
|
Algorithm
|
|
@{
|
|
Name = "LTL-to-B@"uchi translator"
|
|
Path = "~/bin/ltl-to-buchi-translator"
|
|
Parameters = "-x -y -z"
|
|
Enabled = Yes
|
|
@}
|
|
@end smallexample
|
|
|
|
|
|
|
|
@node Format for LTL formulas, Buchi 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 Buchi automata, The lbtt-translate utility, Format for LTL formulas, Interfacing with lbtt
|
|
@section Output file format for B@"uchi 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 on
|
|
transitions. For the full formal definition and some general guidelines on how
|
|
to convert your automata to support the definition, see @ref{Definitions}.
|
|
|
|
The output file generated by the translator should contain an @var{automaton}
|
|
described using the following grammar:
|
|
|
|
@smallexample
|
|
@var{automaton} @r{::=} @var{number-of-states} @var{sp} @var{number-of-acceptance-conditions} @var{states}
|
|
|
|
@var{number-of-states} @r{::=} @r{[}0@r{---}9@r{]+}
|
|
|
|
@var{number-of-acceptance-conditions} @r{::=} @r{[}0@r{---}9@r{]+}
|
|
|
|
@var{states} @r{::=} @var{states} @var{sp} @var{state}
|
|
@r{|} @r{// empty}
|
|
|
|
@var{state} @r{::=} @var{state-id} @var{sp} @var{initial?} @var{acceptance-conditions} @var{sp} `-1' @var{transitions} @var{sp} `-1'
|
|
|
|
@var{state-id} @r{::=} @r{[}0@r{---}9@r{]+}
|
|
|
|
@var{initial?} @r{::=} `0' @r{|} `1'
|
|
|
|
@var{acceptance-conditions} @r{::=} @var{acceptance-conditions} @var{sp} @var{acceptance-set-id}
|
|
@r{|} @r{// empty}
|
|
|
|
@var{acceptance-set-id} @r{::=} @r{[}0@r{---}9@r{]+}
|
|
|
|
@var{transitions} @r{::=} @var{transitions} @var{sp} @var{transition}
|
|
@r{|} @r{// empty}
|
|
|
|
@var{transition} @r{::=} @var{state-id} @var{sp} @var{guard-formula}
|
|
|
|
@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 quoted characters denote the characters themselves; @var{sp} denotes any
|
|
non-empty string of white space. Lines containing a // are comments and are not
|
|
part of the grammar.)
|
|
|
|
The automaton description begins with two nonnegative numbers, the first one
|
|
of which gives the number of states in the automaton, and the second one
|
|
tells the number of acceptance conditions in the automaton. If the number of
|
|
states is 0, the automaton will not accept any input. 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}).
|
|
|
|
If the number of states is greater than zero, the acceptance condition count
|
|
should be followed by a list of states. 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.
|
|
This number is then followed by a list of the identifiers of the acceptance
|
|
conditions to which the state belongs. This list should be terminated with
|
|
@samp{-1}.
|
|
|
|
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{number-of-states} or @var{number-of-acceptance-conditions},
|
|
respectively. (The same identifiers can be shared between states and acceptance
|
|
conditions, however.)
|
|
|
|
Finally, the acceptance condition list of each state should be followed by a
|
|
list of transitions (terminated again by @samp{-1}). Each transition consists
|
|
of a state identifier (the target state of the transition) and a propositional
|
|
formula 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.
|
|
|
|
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 example illustrates the file format.
|
|
|
|
@smallexample
|
|
6 2 @r{// an automaton with six states and two acceptance conditions}
|
|
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
|
|
|
|
|
|
|
|
@node The lbtt-translate utility, , Buchi 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} --- a free 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.
|
|
|
|
@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{Algorithm} section in
|
|
@command{lbtt}'s configuration file:
|
|
|
|
@smallexample
|
|
Algorithm
|
|
@{
|
|
Name = "@var{name for the implementation}"
|
|
Path = "@var{path-to-@command{lbtt-translate}} @var{implementation-selector} @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.
|
|
|
|
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{[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 Conference on Computer Aided Verification
|
|
(CAV'99)}, volume 1633 of @i{Lecture Notes in Computer Science}, pages
|
|
236---248. Springer-Verlag, 1999.
|
|
|
|
@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{[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'01)}, volume 2102 of @i{Lecture Notes in Computer
|
|
Science}, pages 53---65. Springer-Verlag, 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 Workshop Protocol Specification, Testing, and
|
|
Verification (PSTV'95)}, pages 3---18. Chapman & Hall, 1995.
|
|
|
|
@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. 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{[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'00)}, 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{[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 1st IEEE
|
|
Symposium on Logic in Computer Science (LICS'86)}, pages 332---344. IEEE
|
|
Computer Society Press, 1986.
|
|
|
|
@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 Buchi 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 Buchi 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 Buchi automata, State spaces, LTL formulas, Definitions
|
|
@appendixsec Generalized B@"uchi 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 B@"uchi automata
|
|
|
|
Formally, a generalized B@"uchi automaton can be represented as a tuple
|
|
@iftex
|
|
@tex
|
|
$\langle \Sigma, Q, \Delta, q^0, \cal{F}\rangle$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<S, Q, R, q, F>},
|
|
@end ifnottex
|
|
where
|
|
|
|
@itemize @bullet
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\Sigma$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{S}
|
|
@end ifnottex
|
|
is the @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 set of @emph{states},
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$\Delta \subseteq Q \times 2^\Sigma \times Q$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{R} (a subset of @math{Q x 2^S x Q})
|
|
@end ifnottex
|
|
is the
|
|
@emph{transition relation},
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
$q^0$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{q}
|
|
@end ifnottex
|
|
is the @emph{initial state}, and
|
|
|
|
@item
|
|
@iftex
|
|
@tex
|
|
${\cal F} \subseteq 2^Q$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{F}, a collection of subsets of @math{Q},
|
|
@end ifnottex
|
|
is the set of @emph{acceptance conditions}. (A ``nongeneralized''
|
|
B@"uchi automaton has exactly one acceptance condition.)
|
|
|
|
@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 states
|
|
@iftex
|
|
@tex
|
|
$\langle q_0, q_1, q_2, \ldots \rangle \in Q^\omega$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<q(0), q(1), q(2), ...>} (where each @math{q(i)} is a state in @math{Q})
|
|
@end ifnottex
|
|
such that
|
|
@iftex
|
|
@tex
|
|
$q_0 = q^0$
|
|
@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
|
|
there is a triple
|
|
@iftex
|
|
@tex
|
|
$\langle q_i, X, q_{i+1}\rangle \in \Delta$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<q(i), X, q(i+1)>} in @math{R}
|
|
@end ifnottex
|
|
such that
|
|
@iftex
|
|
@tex
|
|
$x_i \in X$.
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{x(i)} belongs to @math{X}.
|
|
@end ifnottex
|
|
Because
|
|
@iftex
|
|
@tex
|
|
$\Delta$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{R}
|
|
@end ifnottex
|
|
is not necessarily a function from
|
|
@iftex
|
|
@tex
|
|
$Q \times 2^\Sigma$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{Q x 2^S}
|
|
@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, q_1, q_2, \ldots\rangle$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{<q(0), q(1), q(2), ...>}
|
|
@end ifnottex
|
|
is @emph{accepting} if and only if additionally
|
|
for each acceptance condition
|
|
@iftex
|
|
@tex
|
|
$F_j \in {@cal F}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{C(j)} in @math{F},
|
|
@end ifnottex
|
|
there is a state
|
|
@iftex
|
|
@tex
|
|
$q_j \in F_j$
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{q(j)} in @math{C(j)}
|
|
@end ifnottex
|
|
that occurs infinitely often in the run. 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
|
|
|
|
In practice, a transition label of a B@"uchi automaton can be expressed as a
|
|
propositional formula, since these formulas readily encode sets of subsets of
|
|
the alphabet
|
|
@iftex
|
|
@tex
|
|
$2^{AP}$,
|
|
@end tex
|
|
@end iftex
|
|
@ifnottex
|
|
@math{2^AP},
|
|
@end ifnottex
|
|
namely, the models of the 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
|
|
use a slightly different definition for generalized B@"uchi automata,
|
|
which permits a B@"uchi automaton to have several initial states and
|
|
places the labels on states instead of transitions. However, these B@"uchi
|
|
automata can be easily converted into an equivalent B@"uchi automaton in the
|
|
above format with the following steps (we assume here that
|
|
each state of the automaton is labelled with a set of LTL formulas that
|
|
should hold in that state):
|
|
|
|
@enumerate
|
|
@item
|
|
Add a new state (with an empty label) 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 (i.e., all formulas with no temporal operators) in the label of
|
|
the state and copy the conjunction onto each transition coming into the
|
|
state. Then remove all labels from the states.
|
|
@end enumerate
|
|
|
|
Conversions from other definitions can be handled in a similar way. In
|
|
some cases (e.g., if the acceptance conditions are subsets of transitions
|
|
instead of subsets of states), the conversion may also require making copies
|
|
of some states and then adjusting the transition labels appropriately.
|
|
|
|
|
|
|
|
@node State spaces, , Generalized Buchi 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 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 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} (a function from @math{S} to @math{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
|