diff --git a/NEWS b/NEWS index 93708c0d0..535dee5fa 100644 --- a/NEWS +++ b/NEWS @@ -36,6 +36,16 @@ New in spot 2.10.6.dev (not yet released) - ltlsynt has a new option --from-pgame that takes a parity game in extended HOA format, as used in the Synthesis Competition. + - ltlsynt has a new option --hide-status to hide the REALIZABLE or + UNREALIZABLE output expected by SYNTCOMP. (This line is + superfluous, because the exit status of ltlsynt already indicate + whether the formula is realizable or not.) + + - ltlsynt has a new option --dot to request GraphViz output instead + of most output. This works for displaying Mealy machines, games, + or AIG circuits. See https://spot.lrde.epita.fr/ltlsynt.html for + examples. + - genaut learned the --cyclist-trace-nba and --cyclist-proof-dba options. Those are used to generate pairs of automata that should include each other, and are used to show a regression (in speed) diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 665fafc67..f2c8691ec 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -41,7 +41,7 @@ #include automaton_format_t automaton_format = Hoa; -static const char* automaton_format_opt = nullptr; +const char* automaton_format_opt = nullptr; const char* opt_name = nullptr; static const char* opt_output = nullptr; static const char* stats = ""; diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 1b2e7ae41..0fb2e8d7c 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et +// Copyright (C) 2014-2018, 2020, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -47,6 +47,7 @@ enum automaton_format_t { // The format to use in output_automaton() extern automaton_format_t automaton_format; +extern const char* automaton_format_opt; // Set to the argument of --name, else nullptr. extern const char* opt_name; // Output options diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 1779211ef..e0cf78c47 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -37,6 +37,7 @@ #include #include #include +#include #include #include #include @@ -49,7 +50,9 @@ enum OPT_BYPASS, OPT_CSV, OPT_DECOMPOSE, + OPT_DOT, OPT_FROM_PGAME, + OPT_HIDE, OPT_INPUT, OPT_OUTPUT, OPT_PRINT, @@ -107,32 +110,41 @@ static const argp_option options[] = /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, - "print the parity game in the pgsolver format, do not solve it", 0}, + "print the parity game in the pgsolver format, do not solve it", 0 }, { "print-game-hoa", OPT_PRINT_HOA, "options", OPTION_ARG_OPTIONAL, - "print the parity game in the HOA format, do not solve it", 0}, + "print the parity game in the HOA format, do not solve it", 0 }, { "realizability", OPT_REAL, nullptr, 0, - "realizability only, do not compute a winning strategy", 0}, + "realizability only, do not compute a winning strategy", 0 }, { "aiger", OPT_PRINT_AIGER, "ite|isop|both[+ud][+dc]" "[+sub0|sub1|sub2]", OPTION_ARG_OPTIONAL, - "prints a winning strategy as an AIGER circuit. The first word " - "indicates the encoding to used: \"ite\" for " + "encode the winning strategy as an AIG circuit and print it in AIGER" + " format. The first word indicates the encoding to used: \"ite\" for " "If-Then-Else normal form; " - "\"isop\" for irreducible sum of producs; " + "\"isop\" for irreducible sum of products; " "\"both\" tries both and keeps the smaller one. " - "The other options further " - "refine the encoding, see aiger::encode_bdd. Defaults to \"ite\".", 0}, - { "verbose", OPT_VERBOSE, nullptr, 0, - "verbose mode", -1 }, - { "verify", OPT_VERIFY, nullptr, 0, - "verifies the strategy or (if demanded) aiger against the spec.", -1 }, + "Other options further " + "refine the encoding, see aiger::encode_bdd. Defaults to \"ite\".", 0 }, + { "dot", OPT_DOT, "options", OPTION_ARG_OPTIONAL, + "Use dot format when printing the result (game, strategy, or " + "AIG circuit, depending on other options). The options that " + "may be passed to --dot depend on the nature of what is printed. " + "For games and strategies, standard automata rendering " + "options are supported (e.g., see ltl2tgba --dot). For AIG circuit, " + "use (h) for horizontal and (v) for vertical layouts.", 0 }, { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL, "output statistics as CSV in FILENAME or on standard output " "(if '>>' is used to request append mode, the header line is " "not output)", 0 }, + { "hide-status", OPT_HIDE, nullptr, 0, + "Hide the REALIZABLE or UNREALIZABLE line. (Hint: exit status " + "is enough of an indication.)", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, "fine-tuning options (see spot-x (7))", 0 }, + { "verbose", OPT_VERBOSE, nullptr, 0, "verbose mode", 0 }, + { "verify", OPT_VERIFY, nullptr, 0, + "verify the strategy or (if demanded) AIG against the formula", 0 }, { nullptr, 0, nullptr, 0, nullptr, 0 }, }; @@ -162,8 +174,10 @@ static const char* opt_print_hoa_args = nullptr; static bool opt_real = false; static bool opt_do_verify = false; static const char* opt_print_aiger = nullptr; - +static const char* opt_dot_arg = nullptr; +static bool opt_dot = false; static spot::synthesis_info* gi; +static bool show_status = true; static char const *const algo_names[] = { @@ -254,6 +268,17 @@ namespace return s; }; + static void + dispatch_print_hoa(const spot::const_twa_graph_ptr& game) + { + if (opt_dot) + spot::print_dot(std::cout, game, opt_print_hoa_args); + else if (opt_print_pg) + spot::print_pg(std::cout, game); + else + spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n'; + } + static void print_csv(const spot::formula& f, const char* filename = nullptr) { @@ -326,7 +351,7 @@ namespace outf.close(opt_csv); } - int + static int solve_formula(const spot::formula& f, const std::vector& input_aps, const std::vector& output_aps) @@ -397,15 +422,8 @@ namespace std::vector mealy_machines; auto print_game = want_game ? - [](const spot::twa_graph_ptr& game)->void - { - if (opt_print_pg) - spot::print_pg(std::cout, game); - else - spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n'; - } - : - [](const spot::twa_graph_ptr&)->void{}; + [](const spot::twa_graph_ptr& game)->void { dispatch_print_hoa(game); } + : [](const spot::twa_graph_ptr&)->void{}; for (; sub_f != sub_form.end(); ++sub_f, ++sub_o) { @@ -425,7 +443,8 @@ namespace { case spot::mealy_like::realizability_code::UNREALIZABLE: { - std::cout << "UNREALIZABLE" << std::endl; + if (show_status) + std::cout << "UNREALIZABLE" << std::endl; safe_tot_time(); return 1; } @@ -448,7 +467,8 @@ namespace continue; if (!spot::solve_game(arena, *gi)) { - std::cout << "UNREALIZABLE" << std::endl; + if (show_status) + std::cout << "UNREALIZABLE" << std::endl; safe_tot_time(); return 1; } @@ -506,7 +526,8 @@ namespace return 0; } - std::cout << "REALIZABLE" << std::endl; + if (show_status) + std::cout << "REALIZABLE" << std::endl; if (opt_real) { safe_tot_time(); @@ -545,7 +566,10 @@ namespace << " latches and " << saig->num_gates() << " gates\n"; } - spot::print_aiger(std::cout, saig) << '\n'; + if (opt_dot) + spot::print_dot(std::cout, saig, opt_dot_arg); + else + spot::print_aiger(std::cout, saig) << '\n'; } else { @@ -784,10 +808,7 @@ namespace } if (opt_print_pg || opt_print_hoa) { - if (opt_print_pg) - spot::print_pg(std::cout, arena); - else - spot::print_hoa(std::cout, arena, opt_print_hoa_args) << '\n'; + dispatch_print_hoa(arena); return 0; } auto safe_tot_time = [&]() { @@ -796,13 +817,15 @@ namespace }; if (!spot::solve_game(arena, *gi)) { - std::cout << "UNREALIZABLE" << std::endl; + if (show_status) + std::cout << "UNREALIZABLE" << std::endl; safe_tot_time(); return 1; } if (gi->bv) gi->bv->realizable = true; - std::cout << "REALIZABLE" << std::endl; + if (show_status) + std::cout << "REALIZABLE" << std::endl; if (opt_real) { safe_tot_time(); @@ -905,9 +928,17 @@ parse_opt(int key, char *arg, struct argp_state *) opt_decompose_ltl = XARGMATCH("--decompose", arg, decompose_args, decompose_values); break; + case OPT_DOT: + opt_dot = true; + automaton_format_opt = opt_dot_arg = arg; + automaton_format = Dot; + break; case OPT_FROM_PGAME: jobs.emplace_back(arg, job_type::AUT_FILENAME); break; + case OPT_HIDE: + show_status = false; + break; case OPT_INPUT: { all_input_aps.emplace(std::vector{}); diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index f05d58309..e4fbc66e4 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -7,19 +7,19 @@ * Basic usage -This tool synthesizes controllers from LTL/PSL formulas. +This tool synthesizes reactive controllers from LTL/PSL formulas. Consider a set $I$ of /input/ atomic propositions, a set $O$ of output atomic propositions, and a PSL formula \phi over the propositions in $I \cup O$. A -=controller= realizing \phi is a function $c: (2^{I})^\star \times 2^I \mapsto +*reactive controller* realizing \phi is a function $c: (2^{I})^\star \times 2^I \mapsto 2^O$ such that, for every \omega-word $(u_i)_{i \in N} \in (2^I)^\omega$ over the input propositions, the word $(u_i \cup c(u_0 \dots u_{i-1}, u_i))_{i \in N}$ satisfies \phi. -If a controller exists, then one with finite memory exists. Such controllers -are easily represented as automata (or more specifically as I/O automata or -transducers). In the automaton representing the controller, the acceptance -condition is irrelevant and trivially true. +If a reactive controller exists, then one with finite memory +exists. Such controllers are easily represented as automata (or more +specifically as Mealy machines). In the automaton representing the +controller, the acceptance condition is irrelevant and trivially true. =ltlsynt= has three mandatory options: - =--ins=: a comma-separated list of input atomic propositions; @@ -27,45 +27,52 @@ condition is irrelevant and trivially true. - =--formula= or =--file=: a specification in LTL or PSL. One of =--ins= or =--outs= may be omitted, as any atomic proposition not listed -as input can be assumed to be an output and vice-versa. +as input can be assumed to be output and vice-versa. -The following example illustrates the synthesis of a controller acting as an -=AND= gate. We have two inputs =a= and =b= and one output =c=, and we want =c= -to always be the =AND= of the two inputs: +The following example illustrates the synthesis of a controller +ensuring that input =i1= and =i2= are both true initially if and only +if eventually output =o1= will go from true to false at some point. +Note that this is an equivalence, not an implication. #+NAME: example #+BEGIN_SRC sh :exports both -ltlsynt --ins=a,b -f 'G (a & b <=> c)' +ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' #+END_SRC #+RESULTS: example #+begin_example REALIZABLE HOA: v1 -States: 1 +States: 3 Start: 0 -AP: 3 "a" "b" "c" +AP: 3 "i1" "i2" "o1" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic +controllable-AP: 2 --BODY-- State: 0 -[!0&!2 | !1&!2] 0 -[0&1&2] 0 +[0&1&2] 1 +[!0&2 | !1&2] 2 +State: 1 +[!2] 0 +State: 2 +[2] 2 --END-- #+end_example The output is composed of two parts: -- the first one is a single line =REALIZABLE= or =UNREALIZABLE;= -- the second one, only present in the =REALIZABLE= case is an automaton describing the controller. - In this example, the controller has a single - state, with two loops labeled by =a & b & c= and =(!a | !b) & !c=. +- The first one is a single line =REALIZABLE= or =UNREALIZABLE=; the presence of this + line, required by the [[http://http://www.syntcomp.org/][SyntComp competition]], can be disabled with option =--hide-status=. +- The second one, only present in the =REALIZABLE= case, is an automaton describing the controller. + +The controller contains the line =controllable-AP: 2=, which means that this automaton +should be interpreted as a Mealy machine where =o0= is part of the output. +Using the =--dot= option, makes it easier to visualize this machine. #+NAME: exampledot -#+BEGIN_SRC sh :exports none :noweb yes -sed 1d <> -EOF +#+BEGIN_SRC sh :exports code +ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --hide-status --dot #+END_SRC #+BEGIN_SRC dot :file ltlsyntex.svg :var txt=exampledot :exports results @@ -75,9 +82,6 @@ EOF #+RESULTS: [[file:ltlsyntex.svg]] -The label =a & b & c= should be understood as: "if the input is =a&b=, -the output should be =c=". - The following example illustrates the case of an unrealizable specification. As =a= is an input proposition, there is no way to guarantee that it will eventually hold. @@ -90,11 +94,68 @@ ltlsynt --ins=a -f 'F a' : UNREALIZABLE By default, the controller is output in HOA format, but it can be -output as an [[http://fmv.jku.at/aiger/][AIGER]] circuit thanks to the =--aiger= flag. This is the -output format required for the [[http://syntcomp.org/][SYNTCOMP]] competition. +output as an And-Inverter-Graph in [[http://fmv.jku.at/aiger/][AIGER format]] using the =--aiger= +flag. This is the output format required for the [[http://syntcomp.org/][SYNTCOMP]] competition. -The generation of a controller can be disabled with the flag =--realizability=. -In this case, =ltlsynt= output is limited to =REALIZABLE= or =UNREALIZABLE=. +#+NAME: exampleaig +#+BEGIN_SRC sh :exports both +ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --aiger +#+END_SRC + +#+RESULTS: exampleaig +#+begin_example +REALIZABLE +aag 14 2 2 1 10 +2 +4 +6 14 +8 29 +7 +10 7 9 +12 4 10 +14 2 12 +16 7 8 +18 4 16 +20 5 7 +22 21 19 +24 2 23 +26 3 7 +28 27 25 +i0 i1 +i1 i2 +o0 o1 +#+end_example + +The above format is not very human friendly. Again, by passing both +=--aiger= and =--dot=, one can display the And-Inverter-Graph representing +the controller: + +#+NAME: exampleaigdot +#+BEGIN_SRC sh :exports code +ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --hide-status --aiger --dot +#+END_SRC + +#+BEGIN_SRC dot :file ltlsyntexaig.svg :var txt=exampleaigdot :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltlsyntexaig.svg]] + +In the above diagram, round nodes represent AND gates. Small black +circles represent inversions (or negations), colored triangles are +used to represent input signals (at the bottom) and output signals (at +the top), and finally rectangles represent latches. A latch is a one +bit register that delays the signal by one step. Initially, all +latches are assumed to contain =false=, and them emit their value from +the =L0_out= and =L1_out= rectangles at the bottom. Their input value, +to be emitted at the next step, is received via the =L0_in= and =L1_in= +boxes at the top. In =ltlsynt='s encoding, the set of latches is used +to keep track of the current state of the Mealy machine. + +The generation of a controller can be disabled with the flag +=--realizability=. In this case, =ltlsynt='s output is limited to +=REALIZABLE= or =UNREALIZABLE=. * TLSF @@ -177,7 +238,18 @@ be tried by separating them using commas. For instance You can also ask =ltlsynt= to print to obtained parity game into [[https://github.com/tcsprojects/pgsolver][PGSolver]] format, with the flag =--print-pg=, or in the HOA format, using =--print-game-hoa=. These flag deactivate the resolution of the -parity game. +parity game. Note that if any of those flag is used with =--dot=, the game +will be printed in the Dot format instead: + +#+NAME: examplegamedot +#+BEGIN_SRC sh :exports code +ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --print-game-hoa --dot +#+END_SRC +#+BEGIN_SRC dot :file ltlsyntexgame.svg :var txt=examplegamedot :exports results + $txt +#+END_SRC +#+RESULTS: +[[file:ltlsyntexgame.svg]] For benchmarking purpose, the =--csv= option can be used to record intermediate statistics about the resolution. @@ -200,6 +272,11 @@ Further improvements are described in the following paper: /Alexandre Duret-Lutz/, and /Adrien Pommellet/. Presented at the SYNT'21 workshop. ([[https://www.lrde.epita.fr/~adl/dl/adl/renkin.21.synt.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#renkin.21.synt][bib]]) +Simplification of Mealy machines is discussed in: + +- *Effective reductions of Mealy machines*, /Florian Renkin/, + /Philipp Schlehuber-Caissier/, /Alexandre Duret-Lutz/, and /Adrien Pommellet/. + Presented at FORTE'22. ([[https://www.lrde.epita.fr/~adl/dl/adl/renkin.22.forte.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#renkin.22.forte][bib]]) # LocalWords: utf ltlsynt AIGER html args mapsto SRC acc aiger TLSF # LocalWords: UNREALIZABLE unrealizable SYNTCOMP realizability Proc diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 33369dcde..b9dfac204 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -985,3 +985,22 @@ ltlsynt -f "G(o1|o2) & (GFi <-> GFo1)" --outs="o1,o2" --verbose\ --bypass=yes 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp + +# Test --dot and --hide-status +ltlsynt -f 'i <-> Fo' --ins=i --aiger --dot | grep arrowhead=dot +ltlsynt -f 'i <-> Fo' --ins=i --print-game-hoa --dot | grep 'shape="diamond"' +ltlsynt -f 'i <-> Fo' --ins=i --dot --hide-status > res +cat >exp < 0 + 0 [label="0"] + 0 -> 0 [label="i / o"] + 0 -> 1 [label="!i / !o"] + 1 [label="1"] + 1 -> 1 [label="1 / !o"] +} +EOF +diff res exp