From a4b575db1cd25b3670c2361670b3be901b72a7eb Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 27 Jan 2017 16:58:13 +0100 Subject: [PATCH] ltldo: add portfolio options Fixes #206. * bin/ltldo.cc: Implement --smallest and --greatest. * tests/core/ltldo2.test: Test them. * NEWS, doc/org/ltldo.org: Document them. --- NEWS | 6 ++ bin/ltldo.cc | 80 +++++++++++++++++++--- doc/org/ltldo.org | 149 ++++++++++++++++++++++++++++++++++++++++- tests/core/ltldo2.test | 20 ++++-- 4 files changed, 237 insertions(+), 18 deletions(-) diff --git a/NEWS b/NEWS index bc00ef2d4..5e3f3a134 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,11 @@ New in spot 2.3.0.dev (not yet released) + Tools: + + - ltldo learnt to act like a portfolio: --smallest and --greatest + will select the best output automaton for each formula translated. + See https://spot.lrde.epita.fr/ltldo.html#portfolio for examples. + Bugs fixed: - spot::otf_product() was incorrectly registering atomic diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 14f10df47..6336a74f1 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -51,6 +51,8 @@ of input and output as required."; enum { OPT_ERRORS = 256, + OPT_SMALLEST, + OPT_GREATEST, }; static const argp_option options[] = @@ -59,6 +61,13 @@ static const argp_option options[] = { "errors", OPT_ERRORS, "abort|warn|ignore", 0, "how to deal with tools returning with non-zero exit codes or " "automata that ltldo cannot parse (default: abort)", 0 }, + { nullptr, 0, nullptr, 0, "Output selection:", 5 }, + { "smallest", OPT_SMALLEST, "FORMAT", OPTION_ARG_OPTIONAL, + "for each formula select the smallest automaton given by all " + "translators, using FORMAT for ordering (default is %s,%e)", 0 }, + { "greatest", OPT_GREATEST, "FORMAT", OPTION_ARG_OPTIONAL, + "for each formula select the greatest automaton given by all " + "translators, using FORMAT for ordering (default is %s,%e)", 0 }, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { nullptr, 0, nullptr, 0, nullptr, 0 } }; @@ -110,6 +119,9 @@ build_percent_list() enum errors_type { errors_abort, errors_warn, errors_ignore }; static errors_type errors_opt; +static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection +static const char* best_format = "%s,%e"; + static char const *const errors_args[] = { "stop", "abort", @@ -131,8 +143,8 @@ const struct argp_child children[] = { &hoaread_argp, 0, "Parsing of automata:", 3 }, { &finput_argp, 0, nullptr, 1 }, { &trans_argp, 0, nullptr, 3 }, - { &aoutput_argp, 0, nullptr, 5 }, - { build_percent_list(), 0, nullptr, 6 }, + { &aoutput_argp, 0, nullptr, 6 }, + { build_percent_list(), 0, nullptr, 7 }, { &misc_argp, 0, nullptr, -1 }, { nullptr, 0, nullptr, 0 } }; @@ -145,6 +157,16 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_ERRORS: errors_opt = XARGMATCH("--errors", arg, errors_args, errors_types); break; + case OPT_GREATEST: + best_type = 1; + if (arg) + best_format = arg; + break; + case OPT_SMALLEST: + best_type = -1; + if (arg) + best_format = arg; + break; case ARGP_KEY_ARG: if (arg[0] == '-' && !arg[1]) jobs.emplace_back(arg, true); @@ -252,6 +274,8 @@ namespace spot::bdd_dict_ptr dict = spot::make_bdd_dict(); xtranslator_runner runner; automaton_printer printer; + hoa_stat_printer best_printer; + std::ostringstream best_stream; spot::postprocessor& post; spot::printable_value cmdname; spot::printable_value roundval; @@ -259,11 +283,14 @@ namespace public: processor(spot::postprocessor& post) - : runner(dict), post(post) + : runner(dict), best_printer(best_stream, best_format), post(post) { printer.add_stat('T', &cmdname); printer.add_stat('#', &roundval); printer.add_stat('f', &inputf); + best_printer.declare('T', &cmdname); + best_printer.declare('#', &roundval); + best_printer.declare('f', &inputf); } ~processor() @@ -313,6 +340,12 @@ namespace runner.round_formula(f, round); unsigned ts = translators.size(); + spot::twa_graph_ptr best_aut = nullptr; + std::string best_stats; + std::string best_cmdname; + process_timer best_timer; + + roundval = round; for (unsigned t = 0; t < ts; ++t) { bool problem; @@ -330,13 +363,40 @@ namespace { if (relmap) relabel_here(aut, relmap.get()); - aut = post.run(aut, f); + cmdname = translators[t].name; - roundval = round; - printer.print(aut, timer, f, filename, linenum, - nullptr, prefix, suffix); - }; + aut = post.run(aut, f); + if (best_type) + { + best_printer.print(nullptr, aut, f, filename, linenum, timer, + prefix, suffix); + std::string aut_stats = best_stream.str(); + if (!best_aut || + (strverscmp(best_stats.c_str(), aut_stats.c_str()) + * best_type) < 0) + { + best_aut = aut; + best_stats = aut_stats; + best_cmdname = translators[t].name; + best_timer = timer; + } + best_stream.str(""); + } + else + { + printer.print(aut, timer, f, filename, linenum, + nullptr, prefix, suffix); + } + } } + if (best_aut) + { + cmdname = best_cmdname; + printer.print(best_aut, best_timer, + f, filename, linenum, + nullptr, prefix, suffix); + } + spot::cleanup_tmpfiles(); ++round; return 0; diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 99b8a31b2..3e840f31f 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -182,12 +182,13 @@ ltldo --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: +: %% a single % : %f,%s,%l,%w the formula as a (quoted) string in Spot, Spin, : LBT, or Wring's syntax : %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or : Wring's syntax -: %O,%D the automaton is output as either (%O) HOA/never -: claim/LBTT, or (%D) in LTL2DSTAR's format +: %O the automaton output in HOA, never claim, LBTT, or +: ltl2dstar's format Contrarily to =ltlcross=, it this not mandatory to specify an output filename using one of the sequence for that last line. For instance @@ -464,6 +465,150 @@ State: 0 "accept_init" {0} --END-- #+END_SRC +* Acting as a portfolio of translators + :PROPERTIES: + :CUSTOM_ID: portfolio + :END: + +Here is a formula on which different translators produce Büchi automata of +different sizes (states and edges): + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' \ + --stats='%T: %s st. (%n non-det.), %e ed.' +#+END_SRC + +#+RESULTS: +: ltl2ba: 5 st. (2 non-det.), 9 ed. +: ltl3ba: 3 st. (1 non-det.), 4 ed. +: ltl2tgba -s: 3 st. (0 non-det.), 5 ed. + +Instead of outputting the result of the translation of each formula by each +translator, =ltldo= can also be configured to output the smallest +automaton obtained for each formula: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 3 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[t] 0 +[0] 1 +State: 1 +[0] 2 +State: 2 {0} +[t] 2 +--END-- +#+end_example + +Therefore, in practice, =ltldo --smallest trans1 trans2 trans3...= +acts like a portfolio of translators, always returning the smallest +produced automaton. + +The sorting criterion can be specified using =--smallest= or +=--greatest=, optionally followed by a format string with +=%=-sequences. The default criterion is =%s,%e=, so the number of +states will be compared first, and in case of equality the number of +edges. If we desire the automaton that has the fewest states, and in +case of equality the smallest number of non-deterministic states, we +can use the following command instead. + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest=%s,%n +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +name: "F(a & Xa)" +States: 3 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic terminal +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[!0] 0 +[0] 2 +State: 2 {0} +[t] 2 +--END-- +#+end_example + +We can of course apply this on a large number of formulas. For +instance here is a more complex pipeline, where we take 11 patterns +from Dwyer et al. (FMSP'98), and print which translator among +=ltl2ba=, =ltl3ba=, and =ltl2tgba -s= would produce the smallest +automaton. + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --dac=10..20 --format=%F:%L,%f | + ltldo -F-/2 ltl2ba ltl3ba 'ltl2tgba -s' --smallest --stats='%<,%T' +#+END_SRC +#+RESULTS: +#+begin_example +dac-patterns:10,ltl2ba +dac-patterns:11,ltl3ba +dac-patterns:12,ltl2tgba -s +dac-patterns:13,ltl2tgba -s +dac-patterns:14,ltl2tgba -s +dac-patterns:15,ltl2tgba -s +dac-patterns:16,ltl2ba +dac-patterns:17,ltl2tgba -s +dac-patterns:18,ltl2ba +dac-patterns:19,ltl3ba +dac-patterns:20,ltl2ba +#+end_example + +Note that in case of equality, only the first translator is returned. +So when =ltl2ba= is output above, it could be the case that =ltl3ba= +or =ltl2tgba -s= are also producing automata of equal size. + +To understand the above pipeline, remove the =ltldo= invocation. The +[[file:genltl.org][=genltl=]] command outputs this: + +#+BEGIN_SRC sh :results verbatim :exports both +genltl --dac=10..20 --format=%F:%L,%f +#+END_SRC +#+RESULTS: +#+begin_example +dac-patterns:10,G((p0 & !p1) -> (!p1 U (!p1 & p2))) +dac-patterns:11,!p0 W (p0 W (!p0 W (p0 W G!p0))) +dac-patterns:12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0))))))))) +dac-patterns:13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1)))))) +dac-patterns:14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1)))))))))) +dac-patterns:15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1))))))))) +dac-patterns:16,Gp0 +dac-patterns:17,Fp0 -> (p1 U p0) +dac-patterns:18,G(p0 -> Gp1) +dac-patterns:19,G((p0 & !p1 & Fp1) -> (p2 U p1)) +dac-patterns:20,G((p0 & !p1) -> (p2 W p1)) +#+end_example + +This is a two-column CSV file where each line is a description of the +origin of the formula (=%F:%L=), followed by the formula itself +(=%f=). The =ltldo= from the previous pipeline simply takes its input +from the second column of its standard input (=-F-/2=), run that +formula through the three translator, pick the smallest automaton +(=--smallest=), and for this automaton, it display the translator that +was used (=%T=) along with the portion of the CSV file that was before +the input column (=%<=). + * Controlling and measuring time The run time of each command can be restricted with the =-T NUM= diff --git a/tests/core/ltldo2.test b/tests/core/ltldo2.test index faf4f1e01..4d739f39e 100755 --- a/tests/core/ltldo2.test +++ b/tests/core/ltldo2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et +# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -21,11 +21,19 @@ . ./defs set -e -ltldo=ltldo -genltl=genltl - test -n "$LTL2BA" || exit 77 -$genltl --or-g=1..2 | - run 0 $ltldo -d "$LTL2BA -f %s>%H" '{foo}ltl2ba' >output +genltl --or-g=1..2 | + run 0 ltldo -d "$LTL2BA -f %s>%H" '{foo}ltl2ba' >output test 4 = `grep -c digraph output` + + +test "ltl2tgba,4" = "`ltldo 'ltl2tgba -D' ltl2tgba \ + -f 'Ga | Gb | Gc' --stats='%T,%s' --smallest`" + +ltldo 'ltl2tgba -D' ltl2tgba -f 'Ga | Gb | Gc' --smallest=%n > aut1.hoa +ltl2tgba -D 'Ga | Gb | Gc' > aut2.hoa +diff aut1.hoa aut2.hoa + +test "ltl2tgba -D" = \ + "`ltldo 'ltl2tgba -D' ltl2tgba -f 'Ga | Gb | Gc' --greatest=%e --stats=%T`"