Commit 0821c97e authored by Thibaud Michaud's avatar Thibaud Michaud
Browse files

add ltlsynt executable

For now, ltlsynt only handles LTL realizability. It uses a reduction to
parity game followed by Calude et al.'s reduction from parity game to
reachability game.

* bin/ltlsynt.cc, bin/Makefile.am, bin/man/ltlsynt.x,
bin/man/Makefile.am, bin/.gitignore: New binary.
* doc/org/arch.tex, doc/Makefile.am, doc/org/tools.org,
doc/org/ltlsynt.org: Document it.
* spot/misc/game.cc, spot/misc/game.hh, spot/misc/Makefile.am: Parity
game wrapper for parity automata + reachability game interface from
Calude et al.'s paper.
parent 7a118426
......@@ -31,6 +31,9 @@ New in spot 2.4.0.dev (not yet released)
also be used to detect unreliable measurements. See
https://spot.lrde.epita.fr/oaut.html#timing
- ltlsynt is a new tool for synthesizing AIGER circuits from LTL/PSL
formulas.
Library:
- Rename three methods of spot::scc_info. New names are clearer. The
......
......@@ -9,6 +9,7 @@ ltlcross
ltldo
ltlfilt
ltlgrind
ltlsynt
randaut
randltl
spot
......
......@@ -70,6 +70,7 @@ bin_PROGRAMS = \
ltldo \
ltlfilt \
ltlgrind \
ltlsynt \
randaut \
randltl
......@@ -92,6 +93,7 @@ ltl2tgta_SOURCES = ltl2tgta.cc
ltlcross_SOURCES = ltlcross.cc
ltlgrind_SOURCES = ltlgrind.cc
ltldo_SOURCES = ltldo.cc
ltlsynt_SOURCES = ltlsynt.cc
dstar2tgba_SOURCES = dstar2tgba.cc
spot_x_SOURCES = spot-x.cc
spot_SOURCES = spot.cc
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <memory>
#include <vector>
#include "common_aoutput.hh"
#include "common_finput.hh"
#include "common_setup.hh"
#include "common_sys.hh"
#include <spot/misc/game.hh>
#include <spot/misc/minato.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/parity.hh>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twa/twagraph.hh>
enum
{
OPT_INPUT = 256,
OPT_PRINT
};
static const argp_option options[] =
{
{ "input", OPT_INPUT, "PROPS", 0,
"comma-separated list of atomic propositions", 0},
{ "print-pg", OPT_PRINT, nullptr, 0,
"print the parity game in the pgsolver format, do not solve it", 0},
{ nullptr, 0, nullptr, 0, nullptr, 0 },
};
const struct argp_child children[] =
{
{ &finput_argp, 0, nullptr, 1 },
{ &misc_argp, 0, nullptr, -1 },
{ nullptr, 0, nullptr, 0 }
};
const char argp_program_doc[] =
"Answer the LTL realizability problem given an LTL formula and a list of"
" uncontrollable (a.k.a. input) proposition names.";
std::vector<std::string> input_aps;
bool opt_print_pg{false};
namespace
{
// Take an automaton and a set of atomic propositions I, and split each
// transition
//
// p -- cond --> q cond in 2^2^AP
//
// into a set of transitions of the form
//
// p -- i1 --> r1 -- o1 --> q i1 in 2^I
// o1 in 2^O
//
// p -- i2 --> r2 -- o2 --> q i2 in 2^I
// o2 in 2^O
// ...
//
// where O = AP\I, and such that cond = (i1 & o1) | (i2 & o2) | ...
//
// When determinized, this encodes a game automaton that has a winning
// strategy iff aut has an accepting run for all valuation of atomic
// propositions in I.
spot::twa_graph_ptr
split_automaton(const spot::twa_graph_ptr& aut,
bdd input_bdd)
{
auto tgba = spot::to_generalized_buchi(aut);
auto split = spot::make_twa_graph(tgba->get_dict());
split->copy_ap_of(tgba);
split->copy_acceptance_of(tgba);
split->new_states(tgba->num_states());
split->set_init_state(tgba->get_init_state_number());
for (unsigned src = 0; src < tgba->num_states(); ++src)
for (const auto& e: tgba->out(src))
{
spot::minato_isop isop(e.cond);
bdd cube;
while ((cube = isop.next()) != bddfalse)
{
unsigned q = split->new_state();
bdd in = bdd_existcomp(cube, input_bdd);
bdd out = bdd_exist(cube, input_bdd);
split->new_edge(src, q, in, 0);
split->new_edge(q, e.dst, out, e.acc);
}
}
split->prop_universal(spot::trival::maybe());
return split;
}
// Generates a vector indicating the owner of each state, with the
// convention that false is player 0 (the environment) and true is player 1
// (the controller). Starting with player 0 on the initial state, the owner
// is switched after each transition.
std::vector<bool> make_alternating_owner(const spot::twa_graph_ptr& dpa,
bool init_owner = false)
{
std::vector<bool> seen(dpa->num_states(), false);
std::vector<unsigned> todo({dpa->get_init_state_number()});
std::vector<bool> owner(dpa->num_states());
owner[dpa->get_init_state_number()] = init_owner;
while (!todo.empty())
{
unsigned src = todo.back();
todo.pop_back();
seen[src] = true;
for (auto& e: dpa->out(src))
{
if (!seen[e.dst])
{
owner[e.dst] = !owner[src];
todo.push_back(e.dst);
}
}
}
return owner;
}
spot::parity_game to_parity_game(const spot::twa_graph_ptr& split)
{
auto dpa = spot::tgba_determinize(split);
dpa->merge_edges();
spot::complete_here(dpa);
spot::colorize_parity_here(dpa, true);
spot::change_parity_here(dpa, spot::parity_kind_max,
spot::parity_style_odd);
if (opt_print_pg)
dpa = spot::sbacc(dpa);
bool max, odd;
dpa->acc().is_parity(max, odd);
assert(max && odd);
assert(spot::is_deterministic(dpa));
auto owner = make_alternating_owner(dpa);
return spot::parity_game(dpa, owner);
}
class ltl_processor final : public job_processor
{
public:
spot::translator& trans;
std::vector<std::string> input_aps;
ltl_processor(spot::translator& trans, std::vector<std::string> input_aps)
: trans(trans), input_aps(input_aps)
{
}
int process_formula(spot::formula f,
const char*, int) override
{
auto aut = trans.run(&f);
bdd input_bdd = bddtrue;
for (unsigned i = 0; i < input_aps.size(); ++i)
{
std::ostringstream lowercase;
for (char c: input_aps[i])
lowercase << (char)std::tolower(c);
auto ap = spot::formula::ap(lowercase.str());
input_bdd &= bdd_ithvar(aut->register_ap(ap));
}
auto split = split_automaton(aut, input_bdd);
auto pg = to_parity_game(split);
if (opt_print_pg)
{
pg.print(std::cout);
return 0;
}
if (pg.solve_qp())
std::cout << "realizable\n";
else
std::cout << "unrealizable\n";
return 0;
}
};
}
static int
parse_opt(int key, char* arg, struct argp_state*)
{
switch (key)
{
case OPT_INPUT:
{
std::istringstream aps(arg);
std::string ap;
while (std::getline(aps, ap, ','))
{
ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
input_aps.push_back(ap);
}
break;
}
case OPT_PRINT:
opt_print_pg = true;
break;
}
return 0;
}
int main(int argc, char **argv)
{
setup(argv);
const argp ap = { options, parse_opt, nullptr,
argp_program_doc, children, nullptr, nullptr };
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
exit(err);
spot::translator trans;
ltl_processor processor(trans, input_aps);
processor.run();
}
......@@ -36,6 +36,7 @@ dist_man1_MANS = \
ltldo.1 \
ltlfilt.1 \
ltlgrind.1 \
ltlsynt.1 \
randaut.1 \
randltl.1
dist_man7_MANS = \
......@@ -69,6 +70,12 @@ ltldo.1: $(common_dep) $(srcdir)/ltlcross.x $(srcdir)/../ltldo.cc
ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc
$(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@
ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc
$(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@
ltlsynt.1: $(common_dep) $(srcdir)/ltlsynt.x $(srcdir)/../ltlsynt.cc
$(convman) ../ltlsynt$(EXEEXT) $(srcdir)/ltlsynt.x $@
genaut.1: $(common_dep) $(srcdir)/genaut.x $(srcdir)/../genaut.cc
$(convman) ../genaut$(EXEEXT) $(srcdir)/genaut.x $@
......@@ -86,6 +93,3 @@ spot-x.7: $(common_dep) $(srcdir)/spot-x.x $(srcdir)/../spot-x.cc
spot.7: $(common_dep) $(srcdir)/spot.x $(srcdir)/../spot.cc
$(convman7) ../spot$(EXEEXT) $(srcdir)/spot.x $@
ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc
$(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@
.\" -*- coding: utf-8 -*-
[NAME]
ltlsynt \- synthesize AIGER circuits from LTL specifications
......@@ -100,6 +100,7 @@ ORG_FILES = \
org/ltldo.org \
org/ltlfilt.org \
org/ltlgrind.org \
org/ltlsynt.org \
org/oaut.org \
org/randaut.org \
org/randltl.org \
......
......@@ -28,6 +28,7 @@
\texttt{dstar2tgba}\\
\texttt{ltlcross}\\
\texttt{ltlgrind}\\
\texttt{ltlsynt}\\
\texttt{ltldo}\\
\texttt{autcross}
};
......
# -*- coding: utf-8 -*-
#+TITLE: =ltlsynt=
#+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas.
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
* Basic usage
This tool answers whether a controller can be built given an LTL/PSL formula
specifying its behavior. =ltlsynt= is typically called with
the following three options:
- =--input=: a comma-separated list of input signal names
- =--output=: a comma-separated list of output signal names
- =--formula= or =--file=: the LTL/PSL specification.
The following example is unrealizable, because =a= is an input, so no circuit
can guarantee that it will be true eventually.
#+BEGIN_SRC sh :results verbatim :exports both
ltlsynt --input=a --output=b -f 'F a'
#+END_SRC
#+RESULTS:
#+begin_example
UNREALIZABLE
#+end_example
* 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.
Fortunately, the SYNTCOMP organizers also provide a tool called =syfco= which
can translate a TLSF specification to an LTL formula.
The following four steps show you how a TLSF specification called spec.tlsf can
be tested for realizability using =syfco= and =ltlsynt=:
#+BEGIN_SRC sh
LTL=$(syfco FILE -f ltlxba -m fully)
IN=$(syfco FILE -f ltlxba -m fully)
OUT=$(syfco FILE -f ltlxba -m fully)
ltlsynt --formula="$LTL" --input="$IN" --output="$OUT"
#+END_SRC
* Algorithm
The tool reduces the synthesis problem to a parity game, and solves the parity
game using Zielonka's recursive algorithm. The full reduction from LTL to
parity game is described in a paper yet to be written and published.
You can ask =ltlsynt= not to solve the game and print it instead (in the
PGSolver format) using the =--print-pg= option, and leaving you the choice of
an external solver such as PGSolver.
......@@ -49,6 +49,7 @@ corresponding commands are hidden.
formula.
- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]]
and [[file:oaut.org][output]] interfaces.
- [[file:ltlsynt.org][=ltlsynt=]] Synthesize AIGER circuits from LTL/PSL specifications.
- [[file:dstar2tgba.org][=dstar2tgba=]] Convert \omega-automata with any acceptance into
variants of Büchi automata.
- [[file:randaut.org][=randaut=]] Generate random \omega-automata.
......@@ -73,8 +74,9 @@ convenience, you can browse their HTML versions:
[[./man/ltl2tgta.1.html][=ltl2tgta=]](1),
[[./man/ltlcross.1.html][=ltlcross=]](1),
[[./man/ltldo.1.html][=ltldo=]](1),
[[./man/ltlgrind.1.html][=ltlgrind=]](1),
[[./man/ltlfilt.1.html][=ltlfilt=]](1),
[[./man/ltlgrind.1.html][=ltlgrind=]](1),
[[./man/ltlsynt.1.html][=ltlsynt=]](1),
[[./man/randaut.1.html][=randaut=]](1),
[[./man/randltl.1.html][=randltl=]](1),
[[./man/spot-x.7.html][=spot-x=]](7),
......
......@@ -38,6 +38,7 @@ misc_HEADERS = \
escape.hh \
fixpool.hh \
formater.hh \
game.hh \
hash.hh \
hashfunc.hh \
intvcomp.hh \
......@@ -62,6 +63,7 @@ libmisc_la_SOURCES = \
bitvect.cc \
escape.cc \
formater.cc \
game.cc \
intvcomp.cc \
intvcmp2.cc \
memusage.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <config.h>
#include <cmath>
#include "spot/misc/game.hh"
namespace spot
{
void parity_game::print(std::ostream& os)
{
os << "parity " << num_states() - 1 << ";\n";
std::vector<bool> seen(num_states(), false);
std::vector<unsigned> todo({get_init_state_number()});
while (!todo.empty())
{
unsigned src = todo.back();
todo.pop_back();
seen[src] = true;
os << src << ' ';
os << out(src).begin()->acc.max_set() - 1 << ' ';
os << owner(src) << ' ';
bool first = true;
for (auto& e: out(src))
{
if (!first)
os << ',';
first = false;
os << e.dst;
if (!seen[e.dst])
todo.push_back(e.dst);
}
if (src == get_init_state_number())
os << " \"INIT\"";
os << ";\n";
}
}
bool parity_game::solve_qp() const
{
return reachability_game(*this).is_reachable();
}
int reachability_state::compare(const state* other) const
{
auto o = down_cast<const reachability_state*>(other);
assert(o);
if (num_ != o->num())
return num_ - o->num();
if (b_ < o->b())
return -1;
if (b_ > o->b())
return 1;
return 0;
}
bool reachability_state::operator<(const reachability_state& o) const
{
// Heuristic to process nodes with a higher chance of leading to a target
// node first.
assert(b_.size() == o.b().size());
for (unsigned i = b_.size(); i > 0; --i)
if (b_[i - 1] != o.b()[i - 1])
return b_[i - 1] > o.b()[i - 1];
return num_ < o.num();
}
const reachability_state* reachability_game_succ_iterator::dst() const
{
// NB: colors are indexed at 1 in Calude et al.'s paper and at 0 in spot
// All acceptance sets are therefore incremented (which is already done by
// max_set), so that 0 can be kept as a special value indicating that no
// i-sequence is tracked at this index. Hence the parity switch in the
// following implementation, compared to the paper.
std::vector<unsigned> b = state_.b();
unsigned a = it_->acc.max_set();
assert(a);
unsigned i = -1U;
bool all_even = a % 2 == 0;
for (unsigned j = 0; j < b.size(); ++j)
{
if ((b[j] % 2 == 1 || b[j] == 0) && all_even)
i = j;
else if (b[j] > 0 && a > b[j])
i = j;
all_even = all_even && b[j] > 0 && b[j] % 2 == 0;
}
if (i != -1U)
{
b[i] = a;
for (unsigned j = 0; j < i; ++j)
b[j] = 0;
}
return new reachability_state(it_->dst, b, !state_.anke());
}
const reachability_state* reachability_game::get_init_state() const
{
// b[ceil(log(n + 1))] != 0 implies there is an i-sequence of length
// 2^(ceil(log(n + 1))) >= 2^log(n + 1) = n + 1, so it has to contain a
// cycle.
unsigned i = std::ceil(std::log2(pg_.num_states() + 1));
return new reachability_state(pg_.get_init_state_number(),
std::vector<unsigned>(i + 1),
false);
}
reachability_game_succ_iterator*
reachability_game::succ_iter(const state* s) const
{
auto state = down_cast<const reachability_state*>(s);
return new reachability_game_succ_iterator(pg_, *state);
}
std::string reachability_game::format_state(const state* s) const
{
auto state = down_cast<const reachability_state*>(s);
std::ostringstream fmt;
bool first = true;
fmt << state->num() << ", ";
fmt << '[';
for (unsigned b : state->b())
{
if (!first)
fmt << ',';
else
first = false;
fmt << b;
}
fmt << ']';
return fmt.str();
}
bool reachability_game::is_reachable()
{
std::set<spot::reachability_state> todo{*init_state_};
while (!todo.empty())
{
spot::reachability_state v = *todo.begin();
todo.erase(todo.begin());
std::vector<spot::const_reachability_state_ptr> succs;
spot::reachability_game_succ_iterator* it = succ_iter(&v);
for (it->first(); !it->done(); it->next())
succs.push_back(spot::const_reachability_state_ptr(it->dst()));
if (is_target(v))
{
c_[v] = 1;
if (mark(v))
return true;
continue;
}
else if (v.anke())
c_[v] = 1;
else
c_[v] = succs.size();
for (auto succ: succs)
{
if (parents_[*succ].empty())
{
if (*succ != *init_state_)
{
todo.insert(*succ);
parents_[*succ] = { v };
c_[*succ] = -1U;
}
}
else
{
parents_[*succ].push_back(v);
if (c_[*succ] == 0 && mark(v))
return true;
}
}
}
return false;
}
bool reachability_game::mark(const spot::reachability_state& s)
{
if (c_[s] > 0)
{
--c_[s];
if (c_[s] == 0)
{
if (s == *init_state_)
return true;
for (auto& u: parents_[s])
if (mark(u))
return true;