alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: Complement deterministic automata.

Browse source 
* src/bin/ltlcross.cc: Complement deterministic automata,
and use them for additional intersection checks.
* NEWS, doc/org/ltlcross.org, src/bin/man/ltlcross.x: Document it.
This commit is contained in:
Alexandre Duret-Lutz 2013-08-18 22:37:25 +02:00
parent 2dda2c9122
commit 1029d08a77
4 changed files with 182 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -20,6 +20,12 @@ New in spot 1.1.4a (not relased)
search for bugs in translators to Rabin or Streett automata, but
the statistics might not be very relevant.
- When ltlcross obtains a deterministic automaton from a
translator it will now complement this automaton to perform
additional intersection checks. This is complementation is done
only for deterministic automata (because that is cheap) and can
be disabled with --no-complement.
- To help with debugging problems detected by ltlcross, the
environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where
temporary files are created and if they should be erased. Read

88
doc/org/ltlcross.org
View file

@ -8,32 +8,38 @@ translators. It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Softw
/LTL-to-Büchi Translator Testbench/, that essentially performs the
same sanity checks.
The main motivations for rewriting this tool were:
The main differences are:
- support for PSL formulas in addition to LTL
- more statistics, especially:
- the number of logical transitions represented by each physical edge,
- the number of deterministic states and automata
- the number of SCCs with their various strengths (nonaccepting, terminal, weak, strong)
- the number of terminal, weak, and strong automata
- output in a format that can be more easily be post-processed,
- statistics output in a format that can be more easily be post-processed,
- more precise time measurement (LBTT was only precise to
1/100 of a second, reporting most times as "0.00s").
1/100 of a second, reporting most times as "0.00s"),
- support for deterministic Rabin or Streett automata written in
[[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dsar='s format]],
- additional intersection checks with the complement of any
deterministic automaton produced by a translator.
Although =ltlcross= performs the same sanity checks as LBTT, it does
not implement any of the interactive features of LBTT. In our almost
10-year usage of LBTT, we never had to use its interactive features to
understand bugs in our translation. Therefore =ltlcross= will report
problems, but you will be on your own to investigate and fix them.
problems, maybe with a conterexample, but you will be on your own to
investigate and fix them.
The core of =ltlcross= is a loop that does the following steps:
- Input a formula
- Translate the formula and its negation using each configured translator.
If there are 3 translators, the positive and negative translations
will be denoted =P0=, =N0=, =P1=, =N1=, =P2=, =N2=.
will be denoted =P0=, =N0=, =P1=, =N1=, =P2=, =N2=. Optionally
build complemented automata denoted =Comp(P0)=, =Comp(N0)=, etc.
- Perform sanity checks between all these automata to detect any problem.
- Build the products of these automata with a random state-space (the same
state-space for all translations). (If the =--products=N= option is given,
=N= products are performed instead.)
- Perform sanity checks between all these automata to detect any problem.
- Gather statistics if requested.
* Formula selection
@ -54,8 +60,8 @@ ltlcross --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d'
: LBT, or Wring's syntax
: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or
: Wring's syntax
: %N,%T the output automaton as a Never claim, or in
: LBTT's format
: %N,%T,%D the output automaton as a Never claim, in LBTT's
: or in LTL2DSTAR's format
For instance here is how we could cross-compare the never claims
output by =spin= and =ltl2tgba= for the formulas =GFa= and =X(a U b)=.
@ -92,17 +98,55 @@ Performing sanity checks and gathering statistics...
no problem detected
#+end_example
=ltlcross= can only read two kinds of output:
=ltlcross= can only read three kinds of output:
- Never claims (only if they are restricted to representing an
automaton using =if=, =goto=, and =skip= statements) such as those
output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. These
should be indicated using =%N=.
should be indicated using =%N=. The newer syntax introduced by
Spin 6.24, using =do= instead of =if=, is also supported.
- [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with
either state-based acceptance or transition-based acceptance.
This output is used for instance by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][=lbt=]], [[http://web.archive.org/web/20080607170403/http://www.science.unitn.it/~stonetta/modella.html][=modella=]], or =ltl2tgba
--lbtt=. These should be indicated using =%T=.
- [[http://www.ltl2dstar.de/docs/ltl2dstar.html][=ltl2dsar='s format]], which support deterministic Rabin or Streett
automata. After =ltlcross= reads such input, it immediately
convert it into a Büchi automaton. Rabin automata are converted
to (degeneralized) Büchi automata and the conversion will preserve
the determinism anytime a deterministic Büchi automaton exists for
that property (this determinism is good for the complemented
intersection check discussed below). Streett automata are
converted to non-deterministic TGBA, where generalized acceptance
conditions are used to reduce the size of the automaton you would
get by the classical conversion from Streett to Büchi.
This kind of output (Rabin or Streett) should be indicated with =%T=.
Of course all configured tools need not the same =%= sequences.
Of course all configured tools need not use the same =%= sequences.
The following list shows some typical configurations for some existing
tools:
- '=spin -f %s >%N='
- '=ltl2ba -f %s >%N='
- '=ltl3ba -f -S %s >%N='
- '=ltl3ba -f -S -M %s >%N=' (more deterministic output)
- '=modella -r12 -g -e %L %T='
- '=/path/to/script4lbtt.py %L %T=' (script supplied by [[http://www.ti.informatik.uni-kiel.de/~fritz/][ltl2nba]] for
its interface with LBTT)
- '=ltl2tgba -s %s >%N=' (smaller output, Büchi automaton)
- '=ltl2tgba -s -D %s >%N=' (more deterministic output, Büchi automaton)
- '=ltl2tgba --lbtt %s >%T=' (smaller output, TGBA)
- '=ltl2tgba --lbtt -D %s >%T=' (more deterministic output, TGBA)
- '=lbt <%L >%T='
- '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L %T='
(deterministic Rabin output)
- '=ltl2dstar --automata=streett --ltl2nba=spin:path/tp/ltl2tgba@-sD
%L %T=' (deterministic Streett output)
- '=ltl2dstar --ltl2nba=spin:path/tp/ltl2tgba@-sD %L - | dstar2tgba
-s >%N=' (external conversion from Rabin to Büchi done by
=dstar2tgba= for additional reduction of the Büchi automaton than
what =ltlcross= would provide)
- '=java -jar Rabinizer.jar -ltl2dstar %F %D; mv %D.dst %D=' (Rabinizer
uses the last =%D= argument as a prefix to which it always append =.dst=,
so we have to rename =%D.dst= as =%D= so that =ltlcross= can find the file)
* Getting statistics
@ -423,6 +467,24 @@ positive and negative formulas by the ith translator).
followed by a cycle that should be repeated infinitely often.
The cycle part is denoted by =cycle{...}=.
- Complemented intersection check. If $P_i$ and $P_j$ are
deterministic, we =ltlcross= builds their complements, $Comp(P_i)$
and $Comp(P_j)$, and then ensures that $Comp(P_i)\otimes
Comp(P_j)$ is empty. If only one of them is deterministic,
for instance $P_i$, we check that $P_j\otimes Comp(P_i)$ for all
$j \ne i$; likewise if it's $N_i$ that is deterministic.
This check is only done for deterministic automata, because
complementation is cheap is that case. When validating a
translator with =ltlcross=, we highly recommend to include a
translator with good deterministic output to augment test
coverage. Using '=ltl2tgba -lD %f >%T=' will produce
deterministic automata for all obligation properties and many
recurrence properties. Using '=ltl2dstar
--ltl2nba=spin:pathto/ltl2tgba@-sD %L %D=' is more expansive, but
it will produce a deterministic Büchi automaton whenever one
exists.
- Cross-comparison checks: for some state-space $S$,
all $P_i\otimes S$ are either all empty, or all non-empty.
Similarly all $N_i\otimes S$ are either all empty, or all non-empty.
@ -451,7 +513,9 @@ positive and negative formulas by the ith translator).
the state-space in which the inconsistency was detected is also
printed.
The above checks are similar to those that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]].
The above checks are similar to those that are performed by [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]],
except for the complemented intersection check, which is only done in
=ltlcross=.
If any problem was reported during the translation of one of the
formulas, =ltlcheck= will exit with an exit status of =1=. Statistics

89
src/bin/ltlcross.cc
View file

@ -53,6 +53,7 @@
#include "tgbaalgos/isweakscc.hh"
#include "tgbaalgos/reducerun.hh"
#include "tgbaalgos/word.hh"
#include "tgbaalgos/dbacomp.hh"
#include "misc/formater.hh"
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/isdet.hh"
@ -91,6 +92,7 @@ Exit status:\n\
#define OPT_SEED 8
#define OPT_PRODUCTS 9
#define OPT_COLOR 10
#define OPT_NOCOMP 11
static const argp_option options[] =
{
@ -122,6 +124,8 @@ static const argp_option options[] =
{ "no-checks", OPT_NOCHECKS, 0, 0,
"do not perform any sanity checks (negated formulas "
"will not be translated)", 0 },
{ "no-complement", OPT_NOCOMP, 0, 0,
"do not complement deterministic automata to perform extra checks", 0 },
{ "stop-on-error", OPT_STOP_ERR, 0, 0,
"stop on first execution error or failure to pass"
" sanity checks (timeouts are OK)", 0 },
@ -190,6 +194,7 @@ const char* csv_output = 0;
bool want_stats = false;
bool allow_dups = false;
bool no_checks = false;
bool no_complement = false;
bool stop_on_error = false;
int seed = 0;
unsigned products = 1;
@ -403,6 +408,10 @@ parse_opt(int key, char* arg, struct argp_state*)
break;
case OPT_NOCHECKS:
no_checks = true;
no_complement = true;
break;
case OPT_NOCOMP:
no_complement = true;
break;
case OPT_SEED:
seed = to_pos_int(arg);
@ -850,7 +859,7 @@ namespace
static void
check_empty_prod(const spot::tgba* aut_i, const spot::tgba* aut_j,
size_t i, size_t j)
size_t i, size_t j, bool icomp, bool jcomp)
{
spot::tgba_product* prod = new spot::tgba_product(aut_i, aut_j);
spot::emptiness_check* ec = spot::couvreur99(prod);
@ -858,8 +867,17 @@ namespace
if (res)
{
global_error() << "error: P" << i << "*N" << j
<< " is nonempty";
std::ostream& err = global_error();
err << "error: ";
if (icomp)
err << "Comp(N" << i << ")";
else
err << "P" << i;
if (jcomp)
err << "*Comp(P" << j << ")";
else
err << "*N" << j;
err << " is nonempty";
spot::tgba_run* run = res->accepting_run();
if (run)
@ -1059,9 +1077,16 @@ namespace
}
}
// These store the result of the translation of the positive and
// negative formulas.
size_t m = translators.size();
std::vector<const spot::tgba*> pos(m);
std::vector<const spot::tgba*> neg(m);
// These store the complement of the above results, when we can
// compute it easily.
std::vector<const spot::tgba*> comp_pos(m);
std::vector<const spot::tgba*> comp_neg(m);
unsigned n = vstats.size();
vstats.resize(n + (no_checks ? 1 : 2));
@ -1071,7 +1096,17 @@ namespace
formulas.push_back(fstr);
for (size_t n = 0; n < m; ++n)
pos[n] = runner.translate(n, 'P', pstats);
{
pos[n] = runner.translate(n, 'P', pstats);
// If the automaton is deterministic, compute its complement
// as well. Note that if we have computed statistics
// already, there is no need to call is_deterministic()
// again.
if (!no_complement && pos[n]
&& ((want_stats && !(*pstats)[n].nondeterministic)
|| (!want_stats && is_deterministic(pos[n]))))
comp_pos[n] = dba_complement(pos[n]);
}
// ---------- Negative Formula ----------
@ -1099,7 +1134,17 @@ namespace
formulas.push_back(runner.formula());
for (size_t n = 0; n < m; ++n)
neg[n] = runner.translate(n, 'N', nstats);
{
neg[n] = runner.translate(n, 'N', nstats);
// If the automaton is deterministic, compute its
// complement as well. Note that if we have computed
// statistics already, there is no need to call
// is_deterministic() again.
if (!no_complement && neg[n]
&& ((want_stats && !(*nstats)[n].nondeterministic)
|| (!want_stats && is_deterministic(neg[n]))))
comp_neg[n] = dba_complement(neg[n]);
}
nf->destroy();
}
@ -1116,7 +1161,33 @@ namespace
if (pos[i])
for (size_t j = 0; j < m; ++j)
if (neg[j])
check_empty_prod(pos[i], neg[j], i, j);
{
check_empty_prod(pos[i], neg[j], i, j, false, false);
// Deal with the extra complemented automata if we
// have some.
// If comp_pos[j] and comp_neg[j] exist for the
// same j, it means pos[j] and neg[j] were both
// deterministic. In that case, we will want to
// make sure that comp_pos[j]*comp_neg[j] is empty
// to assert the complementary of pos[j] and
// neg[j]. However using comp_pos[j] and
// comp_neg[j] against other translator will not
// give us any more insight than pos[j] and
// neg[j]. So we only do intersection checks with
// a complement automata when one of the two
// translation was not deterministic.
if (i != j && comp_pos[j] && !comp_neg[j])
check_empty_prod(pos[i], comp_pos[j], i, j, false, true);
if (i != j && comp_neg[i] && !comp_neg[i])
check_empty_prod(comp_neg[i], neg[j], i, j, true, false);
if (comp_pos[i] && comp_neg[j] &&
(i == j || (!comp_neg[i] && !comp_pos[j])))
check_empty_prod(comp_pos[i], comp_neg[j],
i, j, true, true);
}
}
else
{
@ -1236,7 +1307,11 @@ namespace
if (!no_checks)
for (size_t i = 0; i < m; ++i)
delete neg[i];
{
delete neg[i];
delete comp_neg[i];
delete comp_pos[i];
}
for (size_t i = 0; i < m; ++i)
delete pos[i];

22
src/bin/man/ltlcross.x
View file

@ -81,10 +81,7 @@ Technology. The main motivation for the reimplementation was to
support PSL, and output more statistics about the translations.
The sanity checks performed on the result of each translator (by
either LBTT or ltlcross) are described in the following paper. Our
implementation will detect and reports problems (like inconsistencies
between two translations) but unlike LBTT it does not offer an
interactive mode to investigate such problems.
either LBTT or ltlcross) are described in the following paper.
.TP
th02
@ -92,3 +89,20 @@ H. Tauriainen and K. Heljanko: Testing LTL formula translation into
Büchi automata. Int. J. on Software Tools for Technology Transfer.
Volume 4, number 1, October 2002.
LBTT did not implement Test 2 described in this paper. ltlcross
implements a slight variation: when an automaton produced by some
translator is deterministic, its complement is built and used for
additional cross-comparisons with other tools. If the translation P1
of the positive formula and the translation N1 of the negative formula
both yield deterministic automata (this may only happen for obligation
properties) then the emptiness check of Comp(P1)*Comp(N1) is
equivalent to Test 2 of Tauriainen and Heljanko. If only one
automaton is deterministic, say P1, it can still be used to check we
can be used to check the result of another translators, for instance
checking the emptiness of Comp(P1)*P2.
Our implementation will detect and reports problems (like
inconsistencies between two translations) but unlike LBTT it does not
offer an interactive mode to investigate such problems.