\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
@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
@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 = }
@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, |== ((p1 U p4) <-> (! p1 -> [] p4)) :
+-> M, |== (p1 U p4) :
| +-> M, |== p4
+-> M, |== (! p1 -> [] p4) :
+-> M, |== [] p4 :
+-> M, |== p4
+-> s0 --> s2
+-> M, |== p4
+-> s2 --> s34
+-> M, |== p4
+-> s34 --> s42
+-> M, |== p4
+-> s42 --> s44
+-> M, |== p4
+-> s44 --> s34
@end smallexample
@noindent
The proof (or refutation) can be considered a tree of statements of the form
@samp{M, |== @var{subformula}} or
@samp{M, |/= @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 = }
@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{} 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{} 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{} 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{},
@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{}
@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{} (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{} 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{}
@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{} 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{},
@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