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

ltlcross: add support for --reference translators

Browse source 
Suggested by Tobias Meggendorfer.  Fixes #295.

* bin/ltlcross.cc, bin/common_trans.hh, bin/common_trans.cc: Implement
this --reference option.
* NEWS, doc/org/ltlcross.org: Document it.
* tests/core/ltlcross3.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2017-10-15 19:16:12 +02:00
parent 77c0e76258
commit fcccd5f425
6 changed files with 278 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -38,6 +38,13 @@ New in spot 2.4.1.dev (not yet released)
- autcross, ltlcross, and ltldo learned --fail-on-timeout.
- ltlcross learned --reference=COMMANDFMT to specify a translator
that should be trusted. Doing so makes it possible to reduce the
number of tests to be performed, as all other translators will be
compared to the reference's output when available. Multiple
reference can be given; in that case other tools are compared
against the smallest reference automaton.
- The new -x tls-impl=N option allows to fine-tune the
implication-based simplification rules of ltl2tgba. See the
spot-x man-page for details.

18
bin/common_trans.cc
View file

@ -81,8 +81,9 @@ static void show_shorthands(shorthands_t* begin, shorthands_t* end)
}
tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end)
: spec(spec), cmd(spec), name(spec)
tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end,
bool is_ref)
: spec(spec), cmd(spec), name(spec), reference(is_ref)
{
if (*cmd == '{')
{
@ -144,7 +145,8 @@ tool_spec::tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end)
}
tool_spec::tool_spec(const tool_spec& other)
: spec(other.spec), cmd(other.cmd), name(other.name)
: spec(other.spec), cmd(other.cmd), name(other.name),
reference(other.reference)
{
if (cmd != spec)
cmd = strdup(cmd);
@ -174,18 +176,20 @@ tool_spec::~tool_spec()
std::vector<tool_spec> tools;
void tools_push_trans(const char* trans)
void tools_push_trans(const char* trans, bool is_ref)
{
tools.emplace_back(trans,
std::begin(shorthands_ltl),
std::end(shorthands_ltl));
std::end(shorthands_ltl),
is_ref);
}
void tools_push_autproc(const char* proc)
void tools_push_autproc(const char* proc, bool is_ref)
{
tools.emplace_back(proc,
std::begin(shorthands_autproc),
std::end(shorthands_autproc));
std::end(shorthands_autproc),
is_ref);
}
void

9
bin/common_trans.hh
View file

@ -47,8 +47,11 @@ struct tool_spec
const char* cmd;
// name of the translator (or spec)
const char* name;
// Whether the tool is a reference.
bool reference;
tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end);
tool_spec(const char* spec, shorthands_t* begin, shorthands_t* end,
bool is_ref);
tool_spec(const tool_spec& other);
tool_spec& operator=(const tool_spec& other);
~tool_spec();
@ -56,8 +59,8 @@ struct tool_spec
extern std::vector<tool_spec> tools;
void tools_push_trans(const char* trans);
void tools_push_autproc(const char* proc);
void tools_push_trans(const char* trans, bool is_ref = false);
void tools_push_autproc(const char* proc, bool is_ref = false);
struct quoted_string final: public spot::printable_value<std::string>
{

102
bin/ltlcross.cc
View file

@ -95,6 +95,7 @@ enum {
OPT_NOCOMP,
OPT_OMIT,
OPT_PRODUCTS,
OPT_REFERENCE,
OPT_SEED,
OPT_STATES,
OPT_STOP_ERR,
@ -104,6 +105,9 @@ enum {
static const argp_option options[] =
{
{ "reference", OPT_REFERENCE, "COMMANDFMT", 0,
"register one translator and assume it is correct (do not"
"check it for error, but use it to check other translators)", 2 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "ltlcross behavior:", 5 },
{ "allow-dups", OPT_DUPS, nullptr, 0,
@ -482,6 +486,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_OMIT:
opt_omit = true;
break;
case OPT_REFERENCE:
tools_push_trans(arg, true);
break;
case OPT_SEED:
seed = to_pos_int(arg);
break;
@ -1092,6 +1099,39 @@ namespace
std::cerr << "Performing sanity checks and gathering statistics..."
<< std::endl;
// If we have reference tools, pick the smallest of their
// automata for positive and negative references.
auto smallest_ref = [&](std::vector<spot::twa_graph_ptr>& from)
{
typedef std::tuple<bool, unsigned, unsigned, unsigned> aut_size;
int smallest_ref = -1;
aut_size smallest_size(true, -1U, -1U, -1U);
for (unsigned i = 0; i < m; ++i)
if (tools[i].reference && from[i])
{
aut_size pisize(!is_deterministic(from[i]),
from[i]->num_states(),
from[i]->num_edges(),
from[i]->num_sets());
if (pisize < smallest_size)
{
smallest_ref = i;
smallest_size = pisize;
}
}
return smallest_ref;
};
// This are not our definitive choice for reference
// automata, because the sizes might change after we remove
// alternation and Fin acceptance. But we need to know now
// if we will have a pair of reference automata in order to
// skip some of the constructions.
int smallest_pos_ref = smallest_ref(pos);
int smallest_neg_ref = smallest_ref(neg);
if (smallest_pos_ref < 0 || smallest_neg_ref < 0)
smallest_pos_ref = smallest_neg_ref = -1;
bool print_first = verbose;
auto unalt = [&](std::vector<spot::twa_graph_ptr>& x,
unsigned i, char prefix)
@ -1126,11 +1166,15 @@ namespace
comp[i] = dualize(x[i]);
};
for (unsigned i = 0; i < m; ++i)
for (size_t i = 0; i < m; ++i)
{
unalt(pos, i, 'P');
complement(pos, comp_pos, i);
unalt(neg, i, 'N');
// Do not complement reference automata if we have a
// reference pair.
if (smallest_pos_ref >= 0 && tools[i].reference)
continue;
complement(pos, comp_pos, i);
complement(neg, comp_neg, i);
}
@ -1138,11 +1182,15 @@ namespace
{
print_first = verbose;
auto tmp = [&](std::vector<spot::twa_graph_ptr>& from,
std::vector<spot::twa_graph_ptr>& to, unsigned i,
std::vector<spot::twa_graph_ptr>& to, int i,
char prefix)
{
if (from[i] && !to[i])
{
// Do not complement reference automata if we have a
// reference pair.
if (smallest_pos_ref >= 0 && tools[i].reference)
return;
if (print_first)
{
std::cerr << "info: complementing non-deterministic "
@ -1207,7 +1255,7 @@ namespace
cleanup_acceptance_here(x[i]);
}
};
for (unsigned i = 0; i < m; ++i)
for (size_t i = 0; i < m; ++i)
{
tmp(pos, i, " P", " ");
tmp(neg, i, " N", " ");
@ -1215,14 +1263,40 @@ namespace
tmp(comp_neg, i, "Comp(N", ")");
}
if (smallest_pos_ref >= 0)
{
// Recompute the smallest references now, because removing
// alternation and Fin acceptance might have changed the
// sizes.
smallest_pos_ref = smallest_ref(pos);
smallest_neg_ref = smallest_ref(neg);
if (verbose)
std::cerr << "info: P" << smallest_pos_ref
<< " and N" << smallest_neg_ref << " assumed "
<< "correct and used as references\n";
}
// intersection test
for (size_t i = 0; i < m; ++i)
if (pos[i])
for (size_t j = 0; j < m; ++j)
if (neg[j])
{
problems +=
check_empty_prod(pos[i], neg[j], i, j, false, false);
// Do not compare reference translators.
if (tools[i].reference && tools[j].reference)
continue;
// If we have a reference pair, only compare
// against that pair when i != j.
if (i == j ||
!((!tools[i].reference &&
smallest_neg_ref >= 0 &&
(size_t)smallest_neg_ref != j)
|| (!tools[j].reference &&
smallest_pos_ref >= 0 &&
(size_t)smallest_pos_ref != i)))
problems +=
check_empty_prod(pos[i], neg[j], i, j, false, false);
// Deal with the extra complemented automata if we
// have some.
@ -1240,13 +1314,15 @@ namespace
// translation was not deterministic.
if (i != j && comp_pos[j] && !comp_neg[j])
problems +=
check_empty_prod(pos[i], comp_pos[j],
i, j, false, true);
if (smallest_pos_ref < 0 || i == (size_t)smallest_pos_ref)
problems +=
check_empty_prod(pos[i], comp_pos[j],
i, j, false, true);
if (i != j && comp_neg[i] && !comp_pos[i])
problems +=
check_empty_prod(comp_neg[i], neg[j],
i, j, true, false);
if (smallest_neg_ref < 0 || j == (size_t)smallest_neg_ref)
problems +=
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])))
problems +=
@ -1370,7 +1446,7 @@ namespace
// consistency check
for (size_t i = 0; i < m; ++i)
if (pos_map[i] && neg_map[i])
if (pos_map[i] && neg_map[i] && !tools[i].reference)
{
if (verbose)
std::cerr << "info: consistency_check (P" << i

88
doc/org/ltlcross.org
View file

@ -53,6 +53,8 @@ and no =-f= or =-F= options are given.
* Configuring translators
** Translator specifications
Each translator should be specified as a string that use some of the
following character sequences:
@ -65,8 +67,8 @@ following character sequences:
: LBT, or Wring's syntax
: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or
: Wring's syntax
: %O the automaton is output in HOA, never claim, LBTT,
: or ltl2dstar's format
: %O the automaton output in HOA, never claim, LBTT, or
: 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)=.
@ -207,6 +209,26 @@ Because only the prefix of the actual command is checked, you can
still specify some options. For instance =ltlcross 'ltl2tgba -D' ...=
is short for =ltlcross 'ltl2tgba -D -H %F>%O' ...=
** Trusted and untrusted translators
By default, all translators specified are not trusted. This means
that =ltlcross= will cross-compare the output of all translators,
possibly yielding a quadratic number of tests.
It is possible to declare that certain translators should be trusted
by specifying them with the =--reference=COMMANDFMT= option. This has
a few implications:
- the automata output by reference translators are not tested
- a pair of positive and negative reference automata are selected
from the reference translators (the smallest automata, in case
multiple references are available), and all other translators will
only be compared to these reference automata.
Consequently, the number of test performed is now linear in the number
of untrusted references. The easiest way to observe the effect of
=--reference= is to run the =ltlcross= with the [[#verbose][=--verbose= option]],
with and without some =--reference= translators.
* Getting statistics
Detailed statistics about the result of each translation, and the
@ -969,6 +991,9 @@ be used to gather statistics about a specific set of formulas.
# LocalWords: cvs LaTeX datacols len ith otimes ltlcheck eval setq
# LocalWords: setenv concat getenv
** =--verbose=
:PROPERTIES:
:CUSTOM_ID: verbose
:END:
The verbose option can be useful to troubleshoot problems or simply
follow the list of transformations and tests performed by =ltlcross=.
@ -1055,8 +1080,6 @@ that the automaton =N0= is really the complement of =P0=. Similarly
=P1=. Finally =P0*N1= and =P1*N0= ensure that =P1= is equivalent to
=P0= and =N1= is equivalent to =N0=.
Note that if we had not used the =--determinize= option, the procedure
would look slightly more complex:
@ -1128,3 +1151,60 @@ it with the four automata, and then performs additional checks
and =P1= are equivalent, they can catch some problems, and would
easily catch the case of an automaton with an empty language by
mistake.
Here is the same example, if we declare that =ltl3ba= is a reference
implementation that should not be checked, and we just want to check
the output of =ltl2tgba= against this reference. See how the number
of tests performed has been reduced.
#+BEGIN_SRC sh :results verbatim :exports code
ltlcross -f 'FGa' ltl2tgba --reference 'ltl3ba -H1' --verbose
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports results
SPOT_HOA_TOLERANT=1 ltlcross -f 'FGa' ltl2tgba --reference 'ltl3ba -H1' --verbose 2>&1
#+END_SRC
#+RESULTS:
#+begin_example
F(G(a))
Running [P0]: ltl3ba -H1 -f '<>([](a))'>'lcr-o0-UanRv9'
Running [P1]: ltl2tgba -H 'F(G(a))'>'lcr-o1-43jbVn'
Running [N0]: ltl3ba -H1 -f '!(<>([](a)))'>'lcr-o0-TUeymC'
Running [N1]: ltl2tgba -H '!(F(G(a)))'>'lcr-o1-5PYsOQ'
info: collected automata:
info: P0 (2 st.,3 ed.,1 sets)
info: N0 (3 st.,5 ed.,1 sets) univ-edges complete
info: P1 (2 st.,3 ed.,1 sets)
info: N1 (1 st.,2 ed.,1 sets) deterministic complete
Performing sanity checks and gathering statistics...
info: getting rid of universal edges...
info: N0 (3 st.,5 ed.,1 sets) -> (2 st.,4 ed.,1 sets)
info: getting rid of any Fin acceptance...
info: P0 (2 st.,3 ed.,1 sets) -> (2 st.,3 ed.,1 sets)
info: Comp(N1) (1 st.,2 ed.,1 sets) -> (2 st.,3 ed.,1 sets)
info: P0 and N0 assumed correct and used as references
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty Comp(N1)*N0
info: check_empty P1*N1
info: building state-space #0/1 of 200 states with seed 0
info: state-space has 4136 edges
info: building product between state-space and P0 (2 st., 3 ed.)
info: product has 400 st., 8298 ed.
info: 2 SCCs
info: building product between state-space and P1 (2 st., 3 ed.)
info: product has 400 st., 8298 ed.
info: 2 SCCs
info: building product between state-space and N0 (2 st., 4 ed.)
info: product has 400 st., 8272 ed.
info: 1 SCCs
info: building product between state-space and N1 (1 st., 2 ed.)
info: product has 200 st., 4136 ed.
info: 1 SCCs
info: cross_check {P0,P1}, state-space #0/1
info: cross_check {N0,N1}, state-space #0/1
info: consistency_check (P1,N1), state-space #0/1
No problem detected.
#+end_example

82
tests/core/ltlcross3.test
View file

@ -36,10 +36,90 @@ ltl2tgba=ltl2tgba
# Make sure ltlcross quotes formulas correctly
cat >formula <<\EOF
G"a'-'>'b"
FGa
EOF
run 0 ltlcross -F formula --csv=out.csv \
"$ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N"
"$ltl2tgba --lenient -s %s >%N" \
--verbose 2> error
cat >ceplan <<EOF
info: check_empty P0*N0
info: check_empty Comp(N0)*Comp(P0)
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty P1*N1
info: check_empty Comp(N1)*Comp(P1)
info: check_empty P0*N0
info: check_empty P0*N1
info: check_empty Comp(N0)*N1
info: check_empty P1*N0
info: check_empty Comp(N1)*N0
info: check_empty P1*N1
EOF
grep 'info: check_empty' error > ce
diff -u ce ceplan
ltlcross -F formula --csv=out.csv \
--ref "$ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N" \
--verbose 2> error
cat >ceplan <<EOF
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty P1*N1
info: check_empty Comp(N1)*Comp(P1)
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty Comp(N1)*N0
info: check_empty P1*N1
EOF
grep 'info: check_empty' error > ce
diff -u ce ceplan
ltlcross -F formula --csv=out.csv \
-D "$ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N" \
--verbose 2> error
cat >ceplan <<EOF
info: check_empty P0*N0
info: check_empty Comp(N0)*Comp(P0)
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty P1*N1
info: check_empty Comp(N1)*Comp(P1)
info: check_empty P0*N0
info: check_empty Comp(N0)*Comp(P0)
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty P1*N1
info: check_empty Comp(N1)*Comp(P1)
EOF
grep 'info: check_empty' error > ce
diff -u ce ceplan
ltlcross -F formula --csv=out.csv \
-D --ref "$ltl2tgba -s %f >%N" \
"$ltl2tgba --lenient -s %s >%N" \
--verbose 2> error
cat >ceplan <<EOF
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty P1*N1
info: check_empty Comp(N1)*Comp(P1)
info: check_empty P0*N1
info: check_empty P1*N0
info: check_empty P1*N1
info: check_empty Comp(N1)*Comp(P1)
EOF
grep 'info: check_empty' error > ce
diff -u ce ceplan
ltlcross -F formula --csv=out.csv \
--ref "$ltl2tgba -s %f >%N" \
--ref "$ltl2tgba --lenient -s %s >%N" \
--verbose 2> error
grep 'info: check_empty' error && exit 1
run 2 ltlcross "$ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a
grep 'ltlcross.*no input.*in.*foo bar' stderr