diff --git a/NEWS b/NEWS index aff07a2a3..93cda64d0 100644 --- a/NEWS +++ b/NEWS @@ -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 diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 8ed98fa33..0d6e6ec6e 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -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 diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index c3f026556..7866a39a9 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -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 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"; diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 27dca38ad..232d875b6 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -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 diff --git a/src/tgbatest/ltl2dstar.test b/src/tgbatest/ltl2dstar.test index 3e8bb93e7..190bc149b 100755 --- a/src/tgbatest/ltl2dstar.test +++ b/src/tgbatest/ltl2dstar.test @@ -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 diff --git a/src/tgbatest/ltlcross3.test b/src/tgbatest/ltlcross3.test index 1c6714d1e..386afbe25 100755 --- a/src/tgbatest/ltlcross3.test +++ b/src/tgbatest/ltlcross3.test @@ -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`