Commit d719c706 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltlcross: report statistics about Rabin and Streett automata

* src/bin/ltlcross.cc: Implement it.
* src/bin/man/ltlcross.x, doc/org/ltlcross.org, NEWS: Document it.
* src/tgbatest/ltl2dstar.test, src/tgbatest/ltlcross3.test: Test it.
parent 2b10745d
......@@ -17,6 +17,11 @@ New in spot 1.2a (not released)
- if ltlcross is used with --products=+5 instead of --products=5
then the stastics for each of the five products will be output
separately instead of being averaged.
- if ltlcross is used with tools that produce deterministic Streett
or Rabin automata (as specified with %D), then the statistics
output in CSV or JSON will have some extra columns to report
the size of these input automata before ltlcross converts them
into TGBA to perform its regular checks.
* Bug fixes:
- ltlcross' CSV output now stricly follows RFC 4180.
- ltlcross failed to report missing input or output escape sequences
......
......@@ -348,10 +348,22 @@ executed through a shell, it also includes the time to start a shell.
All the values that follow will be missing if =exit_status= is not
equal to "=ok=". (You instruct =ltlcross= to not output lines with
equal to "=ok=". (You may instruct =ltlcross= not to output lines with
such missing data with the option =--omit-missing=.)
=states=, =edged=, =transitions=, =acc= are size measures for the
The columns =in_type=, =in_states=, =in_edges=, =in_transitions=,
=in_acc=, and =in_scc= are only output if one of the translator
produces Rabin or Streett automata (i.e., if =%D= is used to specify
one output filename for any translator). In that case these columns
give the type (DRA or DSA) of the produced automaton, as well as its
size (states, edges, transitions, number of acceptance pairs, and
number of SCCs). This input automaton is then converted by =ltlcross=
into a TGBA before being checked the result of other translators, and
all the following columns are measures of that converted automaton.
(Aside from parsing them and converting them to TGBA, Spot has no support
for Rabin automata and Streett automata.)
=states=, =edges=, =transitions=, =acc= are size measures for the
automaton that was translated. =acc= counts the number of acceptance
sets. When building (degeneralized) Büchi automata, it will always be
=1=, so its value is meaningful only when evaluating translations to
......
......@@ -205,6 +205,7 @@ int seed = 0;
unsigned products = 1;
bool products_avg = true;
bool opt_omit = false;
bool has_sr = false; // Has Streett or Rabin automata to process.
struct translator_spec
{
......@@ -292,10 +293,18 @@ struct statistics
{
statistics()
: ok(false),
has_in(false),
status_str(0),
status_code(0),
time(0),
in_type(0),
in_states(0),
in_edges(0),
in_transitions(0),
in_acc(0),
in_scc(0),
states(0),
edges(0),
transitions(0),
acc(0),
scc(0),
......@@ -314,9 +323,17 @@ struct statistics
// If OK is false, only the status_str, status_code, and time fields
// should be valid.
bool ok;
// has in_* data to display.
bool has_in;
const char* status_str;
int status_code;
double time;
const char* in_type;
unsigned in_states;
unsigned in_edges;
unsigned in_transitions;
unsigned in_acc;
unsigned in_scc;
unsigned states;
unsigned edges;
unsigned transitions;
......@@ -336,12 +353,15 @@ struct statistics
std::vector<double> product_scc;
static void
fields(std::ostream& os, bool all)
fields(std::ostream& os, bool show_exit, bool show_sr)
{
if (all)
if (show_exit)
os << "\"exit_status\",\"exit_code\",";
os << ("\"time\","
"\"states\","
os << "\"time\",";
if (show_sr)
os << ("\"in_type\",\"in_states\",\"in_edges\",\"in_transitions\","
"\"in_acc\",\"in_scc\",");
os << ("\"states\","
"\"edges\","
"\"transitions\","
"\"acc\","
......@@ -361,13 +381,23 @@ struct statistics
}
void
to_csv(std::ostream& os, bool all, const char* na = "")
to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "")
{
if (all)
if (show_exit)
os << '"' << status_str << "\"," << status_code << ',';
os << time << ',';
if (ok)
{
if (has_in)
os << '"' << in_type << "\","
<< in_states << ','
<< in_edges << ','
<< in_transitions << ','
<< in_acc << ','
<< in_scc << ',';
else if (show_sr)
os << na << ',' << na << ',' << na << ','
<< na << ',' << na << ',' << na << ',';
os << states << ','
<< edges << ','
<< transitions << ','
......@@ -407,23 +437,12 @@ struct statistics
}
else
{
os << na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na << ','
<< na;
size_t m = products_avg ? 1U : products;
m *= 3;
m += 13 + show_sr * 6;
os << na;
for (size_t i = 0; i < m; ++i)
os << ',' << na << ',' << na << ',' << na;
os << ',' << na;
}
}
};
......@@ -764,10 +783,12 @@ namespace
error(2, 0, "no input %%-sequence in '%s'.\n Use "
"one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how "
"to pass the formula.", t.spec);
if (!(has['D'] || has['N'] || has['T']))
bool has_d = has['D'];
if (!(has_d || has['N'] || has['T']))
error(2, 0, "no output %%-sequence in '%s'.\n Use one of "
"%%D,%%N,%%T to indicate where the automaton is saved.",
t.spec);
has_sr |= has_d;
// Remember the %-sequences used by all translators.
prime(t.cmd);
......@@ -942,6 +963,34 @@ namespace
}
else
{
// Gather statistics about the input automaton
if (want_stats)
{
statistics* st = &(*fstats)[translator_num];
st->has_in = true;
switch (aut->type)
{
case spot::Rabin:
st->in_type = "DRA";
break;
case spot::Streett:
st->in_type = "DSA";
break;
}
spot::tgba_sub_statistics s =
sub_stats_reachable(aut->aut);
st->in_states= s.states;
st->in_edges = s.transitions;
st->in_transitions = s.sub_transitions;
st->in_acc = aut->accpair_count;
spot::scc_map m(aut->aut);
m.build_map();
st->in_scc = m.scc_count();
}
// convert it into TGBA for further processing
res = dstar_to_tgba(aut);
delete aut;
}
......@@ -972,7 +1021,7 @@ namespace
spot::scc_map m(res);
m.build_map();
unsigned c = m.scc_count();
st->scc = m.scc_count();
st->scc = c;
st->nondetstates = spot::count_nondet_states(res);
st->nondeterministic = st->nondetstates != 0;
for (unsigned n = 0; n < c; ++n)
......@@ -1485,7 +1534,7 @@ print_stats_csv(const char* filename)
assert(rounds == formulas.size());
*out << "\"formula\",\"tool\",";
statistics::fields(*out, !opt_omit);
statistics::fields(*out, !opt_omit, has_sr);
*out << "\r\n";
for (unsigned r = 0; r < rounds; ++r)
for (unsigned t = 0; t < ntrans; ++t)
......@@ -1496,7 +1545,7 @@ print_stats_csv(const char* filename)
*out << "\",\"";
spot::escape_rfc4180(*out, translators[t].name);
*out << "\",";
vstats[r][t].to_csv(*out, !opt_omit);
vstats[r][t].to_csv(*out, !opt_omit, has_sr);
*out << "\r\n";
}
delete outfile;
......@@ -1537,7 +1586,7 @@ print_stats_json(const char* filename)
spot::escape_str(*out, formulas[r]);
}
*out << ("\"\n ],\n \"fields\": [\n \"formula\",\"tool\",");
statistics::fields(*out, !opt_omit);
statistics::fields(*out, !opt_omit, has_sr);
*out << "\n ],\n \"inputs\": [ 0, 1 ],";
*out << "\n \"results\": [";
bool notfirst = false;
......@@ -1549,7 +1598,7 @@ print_stats_json(const char* filename)
*out << ',';
notfirst = true;
*out << "\n [ " << r << ',' << t << ',';
vstats[r][t].to_csv(*out, !opt_omit, "null");
vstats[r][t].to_csv(*out, !opt_omit, has_sr, "null");
*out << " ]";
}
*out << "\n ]\n}\n";
......
......@@ -135,7 +135,17 @@ Unless the \fB\-\-omit\-missing\fR option is used, data for all the
following columns might be missing.
.TP
\fBstate\fR, \fBedges\fR, \fBtransitions\fR, \fBacc\fR
\fBin_type\fR, \fBin_states\fR, \fBin_edges\fR, \fBin_transitions\fR, \fBin_acc\fR , \fBin_scc\fR
These columns are only output if \f(CW%D\fR appears in any command
specification, i.e., if any of the tools output some Streett or Rabin
automata. In this case \fBin_type\fR contains a string that is either
\f(CWDRA\fR (Deterministic Rabin Automaton) or \f(CWDSA\fR
(Deterministic Streett Automaton). The other columns respectively
give the number of states, edges, transitions, acceptance pairs, and
strongly connected components in that automaton.
.TP
\fBstates\fR, \fBedges\fR, \fBtransitions\fR, \fBacc\fR
The number of states, edges, transitions, and acceptance sets in the
translated automaton. Column \fBedges\fR counts the number of edges
(labeled by Boolean formulas) in the automaton seen as a graph, while
......@@ -144,6 +154,12 @@ that might have been merged into a formula-labeled edge. For instance
an edge labeled by \f(CWtrue\fR will be counted as 2^3=8 transitions if
the automaton mention 3 atomic propositions.
If the translator produced a Streett or Rabin automaton, these columns
contains the size of a TGBA (or BA) produced by ltlcross from that
Streett or Rabin automaton. Check \fBin_states\fR, \fBin_edges\fR,
\fBin_transitions\fR, and \fBin_acc\fR for statistics about the actual
input automaton.
.TP
\fBscc\fR, \fBnonacc_scc\fR, \fBterminal_scc\fR, \fBweak_scc\fR, \fBstrong_scc\fR
The number of strongly connected components in the automaton. The
......
......@@ -54,4 +54,10 @@ $ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \
"ltl2dstar $STR --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N"
"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \
--csv=out.csv
grep '"in_type"' out.csv
grep '"DSA"' out.csv
grep '"DRA"' out.csv
grep ',,,,' out.csv
......@@ -111,3 +111,16 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 0
check_csv out.csv
test $q -eq `expr $p + 12`
# Check with Rabin/Streett output
run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \
-f a --csv=out.csv 2>stderr
q=`sed 's/[^,]//g;q' out.csv | wc -c`
grep '"exit_status"' out.csv
grep '"exit_code"' out.csv
test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
check_csv out.csv
test $q -eq `expr $p + 6`
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment