From 1b69ed96f94dea816432310bf96d0c62cbb2f8e6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 2 Oct 2021 18:16:39 +0200 Subject: [PATCH] ltlsynt: deduce --outs from --ins or vice-versa * bin/ltlsynt.cc: Implement it. * NEWS, doc/org/ltlsynt.org: Document it. * tests/core/ltlsynt.test: Test it. --- NEWS | 5 ++++- bin/ltlsynt.cc | 40 +++++++++++++++++++++++++++++++++------- doc/org/ltlsynt.org | 37 +++++++++++++++++++------------------ tests/core/ltlsynt.test | 21 +++++++++++++++++++++ 4 files changed, 77 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index c0d4ef704..6807bac61 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,9 @@ New in spot 2.9.8.dev (not yet released) Command-line tools: + - ltlsynt now accepts only one of the --ins or --outs options + to be given and will deduce the value of this other one. + - ltlsynt learned --print-game-hoa to output its internal parity game in the HOA format (with an extension described below). @@ -42,7 +45,7 @@ New in spot 2.9.8.dev (not yet released) 5, 2 then 3. - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi - option, or -b for short. This output Büchi automata without + option, or -b for short. This outputs Büchi automata without forcing state-based acceptance. The following aliases have also been added for consistency: diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 33fb15fe3..208c6d41a 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -30,6 +30,7 @@ #include #include #include +#include #include #include #include @@ -511,7 +512,35 @@ namespace int process_formula(spot::formula f, const char*, int) override { - int res = solve_formula(f, input_aps_, output_aps_); + auto unknown_aps = [](spot::formula f, + const std::vector& known) + { + std::vector unknown; + std::set seen; + f.traverse([&](const spot::formula& s) + { + if (s.is(spot::op::ap)) + { + if (!seen.insert(s).second) + return false; + const std::string& a = s.ap_name(); + if (std::find(known.begin(), known.end(), a) == known.end()) + unknown.push_back(a); + } + return false; + }); + return unknown; + }; + + // Decide which atomic propositions are input or output. + int res; + if (input_aps_.empty() && !output_aps_.empty()) + res = solve_formula(f, unknown_aps(f, output_aps_), output_aps_); + else if (output_aps_.empty() && !input_aps_.empty()) + res = solve_formula(f, input_aps_, unknown_aps(f, input_aps_)); + else + res = solve_formula(f, input_aps_, output_aps_); + if (opt_csv) print_csv(f); return res; @@ -611,14 +640,11 @@ main(int argc, char **argv) check_no_formula(); // Check if inputs and outputs are distinct - // Inputs can be empty, outputs not - if (not all_input_aps.empty()) - { - for (const auto& ai : all_input_aps) - if (std::count(all_output_aps.begin(), all_output_aps.end(), ai)) + for (const auto& ai : all_input_aps) + if (std::find(all_output_aps.begin(), all_output_aps.end(), ai) + != all_output_aps.end()) throw std::runtime_error("ltlsynt(): " + ai + " appears in the input AND output APs."); - } ltl_processor processor(all_input_aps, all_output_aps); if (int res = processor.run(); res == 0 || res == 1) diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 8ca35d9b8..af1bcba9f 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -19,13 +19,16 @@ N}$ satisfies \phi. =ltlsynt= has three mandatory options: - =--ins=: a comma-separated list of input atomic propositions; - =--outs=: a comma-separated list of output atomic propositions; -- =--formula= or =--file=: a LTL/PSL specification. +- =--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. 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: -#+BEGIN_SRC sh -ltlsynt --ins=a,b --outs=c -f 'G (a & b <=> c)' +#+BEGIN_SRC sh :exports both +ltlsynt --ins=a,b -f 'G (a & b <=> c)' #+END_SRC #+RESULTS: @@ -40,15 +43,15 @@ Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 -[0&1&2] 0 [!0&!1 | !1&!2] 0 +[0&1&2] 0 --END-- #+end_example The output is composed of two parts: -- the first one is a single line REALIZABLE or UNREALIZABLE; -- the second one is an automaton describing the controller (if the input - specification is realizable). In this example, the controller has a single +- 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=. If a controller exists, then one with finite memory exists. Such controllers @@ -61,29 +64,27 @@ The following example illustrates the case of an unrealizable specification. As eventually hold. #+BEGIN_SRC sh :epilogue true -ltlsynt --ins=a --outs=b -f 'F a' +ltlsynt --ins=a -f 'F a' #+END_SRC #+RESULTS: : 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. +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. The generation of a controller can be disabled with the flag =--realizability=. -In this case, =ltlsynt= output is limited to REALIZABLE or UNREALIZABLE. +In this case, =ltlsynt= output is limited to =REALIZABLE= or =UNREALIZABLE=. * TLSF -=ltlsynt= was made with the [[http://syntcomp.org/][SYNTCOMP]] competition in -mind, and more specifically the TLSF track of this competition. TLSF is a -high-level specification language created for the purpose of this competition. +=ltlsynt= was made with the [[http://syntcomp.org/][SYNTCOMP]] competition in mind, and more +specifically the TLSF track of this competition. TLSF is a high-level +specification language created for the purpose of this competition. Fortunately, the SYNTCOMP organizers also provide a tool called -[[https://github.com/reactive-systems/syfco][=syfco=]] which can translate a -TLSF specification to an LTL formula. +[[https://github.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula. The following four steps show you how a TLSF specification called =FILE= can be synthesized using =syfco= and =ltlsynt=: diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index ed2d65151..1cd3455a6 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -515,3 +515,24 @@ diff out exp ltlsynt -f 'a U (b' 2>err && exit 1 test $? -eq 2 test `wc -l expected < c)' >stdout +diff stdout expected +ltlsynt --outs=c -f 'G (a & b <=> c)' >stdout +diff stdout expected