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.
This commit is contained in:
Alexandre Duret-Lutz
parent
60225fd139
commit
1b69ed96f9
4 changed files with 77 additions and 26 deletions
5
NEWS
5
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:
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@
|
|||
#include <spot/misc/escape.hh>
|
||||
#include <spot/misc/timer.hh>
|
||||
#include <spot/tl/formula.hh>
|
||||
#include <spot/tl/apcollect.hh>
|
||||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/twaalgos/aiger.hh>
|
||||
#include <spot/twaalgos/game.hh>
|
||||
|
|
@ -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<std::string>& known)
|
||||
{
|
||||
std::vector<std::string> unknown;
|
||||
std::set<spot::formula> 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))
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -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=:
|
||||
|
|
|
|||
|
|
@ -515,3 +515,24 @@ diff out exp
|
|||
ltlsynt -f 'a U (b' 2>err && exit 1
|
||||
test $? -eq 2
|
||||
test `wc -l <err` -eq 4
|
||||
|
||||
|
||||
cat >expected <<EOF
|
||||
REALIZABLE
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 3 "b" "c" "a"
|
||||
acc-name: all
|
||||
Acceptance: 0 t
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1 | !1&!2] 0
|
||||
[0&1&2] 0
|
||||
--END--
|
||||
EOF
|
||||
ltlsynt --ins=a,b -f 'G (a & b <=> c)' >stdout
|
||||
diff stdout expected
|
||||
ltlsynt --outs=c -f 'G (a & b <=> c)' >stdout
|
||||
diff stdout expected
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue