diff --git a/NEWS b/NEWS index 3dc7f3c2f..fbf894e08 100644 --- a/NEWS +++ b/NEWS @@ -99,6 +99,10 @@ New in spot 1.99b (not yet released) ignore translator returning non-zero exist status instead of returning an error. + - ltlcross has a new option --automata to save the produced + automata into the CSV or JSON file. Those automata are saved + into the HOA format. + - "ltlfilt --stutter-invariant" will now work with PSL formulas. The implementation is actually much more efficient than our previous implementation that was only for LTL. diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index fb3ee6047..69cb3abb0 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -46,6 +46,7 @@ #include "ltlvisit/relabel.hh" #include "ltlvisit/lbt.hh" #include "twaalgos/lbtt.hh" +#include "twaalgos/hoa.hh" #include "twaalgos/product.hh" #include "twaalgos/remfin.hh" #include "twaalgos/gtec/gtec.hh" @@ -78,7 +79,8 @@ Exit status:\n\ "; enum { - OPT_BOGUS = 256, + OPT_AUTOMATA = 256, + OPT_BOGUS, OPT_COLOR, OPT_CSV, OPT_DENSITY, @@ -135,6 +137,8 @@ static const argp_option options[] = "not output)", 0 }, { "omit-missing", OPT_OMIT, 0, 0, "do not output statistics for timeouts or failed translations", 0 }, + { "automata", OPT_AUTOMATA, 0, 0, + "store automata (in the HOA format) into the CSV or JSON output", 0 }, /**************************************************/ { 0, 0, 0, 0, "Miscellaneous options:", -2 }, { "color", OPT_COLOR, "WHEN", OPTION_ARG_OPTIONAL, @@ -203,6 +207,7 @@ static output_file* grind_output = 0; static bool verbose = false; static bool ignore_exec_fail = false; static unsigned ignored_exec_fail = 0; +static bool opt_automata = false; static bool global_error_flag = false; @@ -295,6 +300,7 @@ struct statistics std::vector product_transitions; std::vector product_scc; bool ambiguous; + std::string hoa_str; static void fields(std::ostream& os, bool show_exit, bool show_sr) @@ -323,10 +329,13 @@ struct statistics size_t m = products_avg ? 1U : products; for (size_t i = 0; i < m; ++i) os << ",\"product_states\",\"product_transitions\",\"product_scc\""; + if (opt_automata) + os << ",\"automaton\""; } void - to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "") + to_csv(std::ostream& os, bool show_exit, bool show_sr, const char* na = "", + bool csv_escape = true) { if (show_exit) os << '"' << status_str << "\"," << status_code << ','; @@ -390,6 +399,16 @@ struct statistics for (size_t i = 0; i < m; ++i) os << ',' << na; } + if (opt_automata) + { + os << ','; + if (hoa_str.empty()) + os << na; + else if (csv_escape) + spot::escape_rfc4180(os << '"', hoa_str) << '"'; + else + spot::escape_str(os << '"', hoa_str) << '"'; + } } }; @@ -407,6 +426,9 @@ parse_opt(int key, char* arg, struct argp_state*) case ARGP_KEY_ARG: translators.push_back(arg); break; + case OPT_AUTOMATA: + opt_automata = true; + break; case OPT_BOGUS: { bogus_output = new output_file(arg); @@ -693,6 +715,13 @@ namespace else st->terminal_aut = true; st->ambiguous = !spot::is_unambiguous(res); + + if (opt_automata) + { + std::ostringstream os; + spot::hoa_reachable(os, res, "l"); + st->hoa_str = os.str(); + } } } output.cleanup(); @@ -1397,7 +1426,7 @@ print_stats_json(const char* filename) out << ','; notfirst = true; out << "\n [ " << r << ',' << t << ','; - vstats[r][t].to_csv(out, !opt_omit, has_sr, "null"); + vstats[r][t].to_csv(out, !opt_omit, has_sr, "null", false); out << " ]"; } out << "\n ]\n}\n"; diff --git a/src/tests/ltlcross3.test b/src/tests/ltlcross3.test index 4a92fa61b..3dc9e9090 100755 --- a/src/tests/ltlcross3.test +++ b/src/tests/ltlcross3.test @@ -80,14 +80,15 @@ test `grep 'warning:.*timeout' stderr | wc -l` -eq 2 test `wc -l < out.csv` -eq 1 check_csv out.csv -# Check with --products=5 +# Check with --products=5 --automata run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ - -f a --csv=out.csv --products=5 2>stderr + -f a --csv=out.csv --products=5 --automata 2>stderr p=`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 +test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2 check_csv out.csv # ... unless --omit-missing is supplied. @@ -102,12 +103,13 @@ check_csv out.csv # Check with --products=+5 run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ - -f a --csv=out.csv --products=+5 2>stderr + -f a --csv=out.csv --products=+5 --automata 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 +test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2 check_csv out.csv # ... unless --omit-missing is supplied. @@ -128,7 +130,7 @@ echo "$first" > bug.txt run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \ -f 'X a' --csv=out.csv --save-bogus='>>bug.txt' 2>stderr q=`sed 's/[^,]//g;q' out.csv | wc -c` -test $q -eq `expr $p + 6` +test $q -eq `expr $p + 5` grep '"exit_status"' out.csv grep '"exit_code"' out.csv test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2