Commit 1da0afba authored by Maximilien Colange's avatar Maximilien Colange

Improve ltlsynt interface

To ease debugging and testing, ltlsynt can output the synthesized
strategy as an automaton, not just an aiger circuit.
Also, its exit code has been changed to something meaningful.

* bin/ltlsynt.cc: Various improvements: options, exit code, code style
* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc,
  spot/twaalgos/Makefile.am: Move the aiger printer to separate files
* tests/core/ltlsynt.test: Clean up and update test file
* tests/Makefile.am: Add the test file to the test suite
* NEWS: document the new aiger printer
* doc/org/concepts.org: document the named property "synthesis-outputs",
  used by print_aiger
parent 502ddc6d
......@@ -44,8 +44,8 @@ New in spot 2.4.2.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.
- ltlsynt is a new tool for synthesizing a controller from LTL/PSL
specifications.
- ltldo learned to limit the number of automata it outputs using -n.
......@@ -190,6 +190,15 @@ New in spot 2.4.2.dev (not yet released)
- The new spot::formula::is_leaf() method can be used to detect
formulas without children (atomic propositions, or constants).
- The new function spot::print_aiger() encodes an automaton as an
AIGER circuit and prints it. This is only possible for automata
whose acceptance condition is trivial. It relies on a new named
property "synthesis outputs" that describes which atomic
propositions are to be encoded as outputs of the circuits.
This function is used by ltlsynt to output the synthesized
controllers in the format required by the synthesis tools
competition SYNTCOMP.
Deprecation notices:
(These functions still work but compilers emit warnings.)
......
......@@ -19,8 +19,6 @@
#include <config.h>
#include <cmath>
#include <map>
#include <memory>
#include <string>
#include <sstream>
......@@ -39,6 +37,7 @@
#include <spot/misc/minato.hh>
#include <spot/tl/formula.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/aiger.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/parity.hh>
......@@ -53,6 +52,7 @@ enum
OPT_INPUT,
OPT_OUTPUT,
OPT_PRINT,
OPT_PRINT_AIGER,
OPT_REAL
};
......@@ -60,10 +60,10 @@ static const argp_option options[] =
{
/**************************************************/
{ nullptr, 0, nullptr, 0, "Input options:", 1 },
{ "input", OPT_INPUT, "PROPS", 0,
{ "ins", OPT_INPUT, "PROPS", 0,
"comma-separated list of uncontrollable (a.k.a. input) atomic"
" propositions", 0},
{ "output", OPT_OUTPUT, "PROPS", 0,
{ "outs", OPT_OUTPUT, "PROPS", 0,
"comma-separated list of controllable (a.k.a. output) atomic"
" propositions", 0},
/**************************************************/
......@@ -77,30 +77,38 @@ static const argp_option options[] =
{ "print-pg", OPT_PRINT, nullptr, 0,
"print the parity game in the pgsolver format, do not solve it", 0},
{ "realizability", OPT_REAL, nullptr, 0,
"realizability only, do not synthesize the circuit", 0},
"realizability only, do not compute a winning strategy", 0},
{ "aiger", OPT_PRINT_AIGER, nullptr, 0,
"prints the winning strategy as an AIGER circuit", 0},
/**************************************************/
{ nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
{ nullptr, 0, nullptr, 0, nullptr, 0 },
};
const struct argp_child children[] =
static const struct argp_child children[] =
{
{ &finput_argp_headless, 0, nullptr, 0 },
{ &aoutput_argp, 0, nullptr, 0 },
//{ &aoutput_o_format_argp, 0, nullptr, 0 },
{ &misc_argp, 0, nullptr, 0 },
{ nullptr, 0, nullptr, 0 }
};
const char argp_program_doc[] =
"Synthesize an AIGER circuit from its LTL specifications.";
const char argp_program_doc[] = "\
Synthesize a controller from its LTL specification.\v\
Exit status:\n\
0 if the input problem is realizable\n\
1 if the input problem is not realizable\n\
2 if any error has been reported";
std::vector<std::string> input_aps;
std::vector<std::string> output_aps;
std::unordered_map<unsigned, unsigned> bddvar_to_inputnum;
std::unordered_map<unsigned, unsigned> bddvar_to_outputnum;
static std::vector<std::string> input_aps;
static std::vector<std::string> output_aps;
bool opt_print_pg(false);
bool opt_real(false);
bool opt_print_aiger(false);
// FIXME rename options to choose the algorithm
enum solver
{
QP,
......@@ -120,7 +128,7 @@ static solver const solver_types[] =
};
ARGMATCH_VERIFY(solver_args, solver_types);
solver opt_solver = REC;
static solver opt_solver = REC;
namespace
{
......@@ -144,7 +152,7 @@ namespace
// strategy iff aut has an accepting run for any valuation of atomic
// propositions in I.
spot::twa_graph_ptr
static spot::twa_graph_ptr
split_automaton(const spot::twa_graph_ptr& aut,
bdd input_bdd)
{
......@@ -177,8 +185,9 @@ namespace
// 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)
static 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()});
......@@ -201,7 +210,8 @@ namespace
return owner;
}
spot::twa_graph_ptr to_dpa(const spot::twa_graph_ptr& split)
static spot::twa_graph_ptr
to_dpa(const spot::twa_graph_ptr& split)
{
auto dpa = spot::tgba_determinize(split);
dpa->merge_edges();
......@@ -218,225 +228,10 @@ namespace
return dpa;
}
// Parity game strategy to AIGER
class aig
{
private:
unsigned num_inputs_;
unsigned max_var_;
std::map<unsigned, std::pair<unsigned, unsigned>> and_gates_;
std::vector<unsigned> latches_;
std::vector<unsigned> outputs_;
// Cache the function computed by each variable as a bdd.
std::unordered_map<unsigned, bdd> var2bdd_;
std::unordered_map<bdd, unsigned, spot::bdd_hash> bdd2var_;
public:
aig(unsigned num_inputs, unsigned num_latches, unsigned num_outputs)
: num_inputs_(num_inputs),
max_var_((num_inputs + num_latches) * 2),
latches_(std::vector<unsigned>(num_latches)),
outputs_(std::vector<unsigned>(num_outputs))
{
bdd2var_[bddtrue] = 1;
var2bdd_[1] = bddtrue;
bdd2var_[bddfalse] = 0;
var2bdd_[0] = bddfalse;
}
unsigned input_var(unsigned i, bdd b)
{
assert(i < num_inputs_);
unsigned v = (1 + i) * 2;
bdd2var_[b] = v;
var2bdd_[v] = b;
return v;
}
unsigned latch_var(unsigned i, bdd b)
{
assert(i < latches_.size());
unsigned v = (1 + num_inputs_ + i) * 2;
bdd2var_[b] = v;
var2bdd_[v] = b;
return v;
}
void set_output(unsigned i, unsigned v)
{
outputs_[i] = v;
}
void set_latch(unsigned i, unsigned v)
{
latches_[i] = v;
}
unsigned aig_true() const
{
return 1;
}
unsigned aig_false() const
{
return 0;
}
unsigned aig_not(unsigned v)
{
unsigned not_v = v + 1 - 2 * (v % 2);
assert(var2bdd_.count(v));
var2bdd_[not_v] = !(var2bdd_[v]);
bdd2var_[var2bdd_[not_v]] = not_v;
return not_v;
}
unsigned aig_and(unsigned v1, unsigned v2)
{
assert(var2bdd_.count(v1));
assert(var2bdd_.count(v2));
bdd b = var2bdd_[v1] & var2bdd_[v2];
auto it = bdd2var_.find(b);
if (it != bdd2var_.end())
return it->second;
max_var_ += 2;
and_gates_[max_var_] = {v1, v2};
bdd v1v2 = var2bdd_[v1] & var2bdd_[v2];
bdd2var_[v1v2] = max_var_;
var2bdd_[max_var_] = v1v2;
return max_var_;
}
unsigned aig_and(std::vector<unsigned> vs)
{
if (vs.empty())
return aig_true();
if (vs.size() == 1)
return vs[0];
if (vs.size() == 2)
return aig_and(vs[0], vs[1]);
unsigned m = vs.size() / 2;
std::vector<unsigned> left(vs.begin(), vs.begin() + m);
std::vector<unsigned> right(vs.begin() + m, vs.end());
return aig_and(aig_and(left), aig_and(right));
}
unsigned aig_or(unsigned v1, unsigned v2)
{
return aig_not(aig_and(aig_not(v1), aig_not(v2)));
}
unsigned aig_or(std::vector<unsigned> vs)
{
for (unsigned i = 0; i < vs.size(); ++i)
vs[i] = aig_not(vs[i]);
return aig_not(aig_and(vs));
}
unsigned aig_pos(unsigned v)
{
return v - v % 2;
}
void remove_unused()
{
std::unordered_set<unsigned> todo;
for (unsigned v : outputs_)
todo.insert(aig_pos(v));
std::unordered_set<unsigned> used;
while (!todo.empty())
{
used.insert(todo.begin(), todo.end());
std::unordered_set<unsigned> todo_next;
for (unsigned v : todo)
{
auto it_and = and_gates_.find(v);
if (it_and != and_gates_.end())
{
if (!used.count(aig_pos(it_and->second.first)))
todo_next.insert(aig_pos(it_and->second.first));
if (!used.count(aig_pos(it_and->second.second)))
todo_next.insert(aig_pos(it_and->second.second));
}
else if (v <= (num_inputs_ + latches_.size()) * 2
&& v > num_inputs_ * 2)
{
unsigned l = v / 2 - num_inputs_ - 1;
if (!used.count(aig_pos(latches_[l])))
todo_next.insert(aig_pos(latches_[l]));
}
}
todo = todo_next;
}
std::unordered_set<unsigned> unused;
for (auto& p : and_gates_)
if (!used.count(p.first))
unused.insert(p.first);
for (unsigned v : unused)
and_gates_.erase(v);
}
void print()
{
std::cout << "aag " << max_var_ / 2
<< ' ' << num_inputs_
<< ' ' << latches_.size()
<< ' ' << outputs_.size()
<< ' ' << and_gates_.size() << '\n';
for (unsigned i = 0; i < num_inputs_; ++i)
std::cout << (1 + i) * 2 << '\n';
for (unsigned i = 0; i < latches_.size(); ++i)
std::cout << (1 + num_inputs_ + i) * 2
<< ' ' << latches_[i] << '\n';
for (unsigned i = 0; i < outputs_.size(); ++i)
std::cout << outputs_[i] << '\n';
for (auto& p : and_gates_)
std::cout << p.first
<< ' ' << p.second.first
<< ' ' << p.second.second << '\n';
for (unsigned i = 0; i < num_inputs_; ++i)
std::cout << 'i' << i << ' ' << input_aps[i] << '\n';
for (unsigned i = 0; i < outputs_.size(); ++i)
std::cout << 'o' << i << ' ' << output_aps[i] << '\n';
}
};
std::vector<bool> output_to_vec(bdd b)
{
std::vector<bool> v(bddvar_to_outputnum.size());
while (b != bddtrue && b != bddfalse)
{
unsigned i = bddvar_to_outputnum[bdd_var(b)];
v[i] = (bdd_low(b) == bddfalse);
if (v[i])
b = bdd_high(b);
else
b = bdd_low(b);
}
return v;
}
bdd state_to_bdd(unsigned s, bdd all)
{
bdd b = bddtrue;
unsigned size = bdd_nodecount(all);
if (size)
{
unsigned st0 = bdd_var(all);
for (unsigned i = 0; i < size; ++i)
{
b &= s % 2 ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i);
s >>= 1;
}
}
return b;
}
// Construct a smaller automaton, filtering out states that are not
// accessible. Also merge back pairs of p --(i)--> q --(o)--> r
// transitions to p --(i&o)--> r.
spot::twa_graph_ptr
static spot::twa_graph_ptr
strat_to_aut(const spot::parity_game& pg,
const spot::parity_game::strategy_t& strat,
const spot::twa_graph_ptr& dpa,
......@@ -477,110 +272,10 @@ namespace
}
}
aut->purge_dead_states();
aut->set_named_prop("synthesis-outputs", new bdd(all_outputs));
return aut;
}
std::vector<bool> state_to_vec(unsigned s, unsigned size)
{
std::vector<bool> v(size);
for (unsigned i = 0; i < size; ++i)
{
v[i] = s % 2;
s >>= 1;
}
return v;
}
// Switch initial state and 0 in the AIGER encoding, so that the
// 0-initialized latches correspond to the initial state.
unsigned encode_init_0(unsigned src, unsigned init)
{
return src == init ? 0 : src == 0 ? init : src;
}
aig aut_to_aiger(const spot::twa_graph_ptr& aut,
bdd all_inputs, bdd all_outputs)
{
// Encode state in log2(num_states) latches.
unsigned log2n = std::ceil(std::log2(aut->num_states()));
unsigned st0 = aut->get_dict()->register_anonymous_variables(log2n, aut);
bdd all_states = bddtrue;
for (unsigned i = 0; i < log2n; ++i)
all_states &= bdd_ithvar(st0 + i);
unsigned num_inputs = bdd_nodecount(all_inputs);
unsigned num_outputs = bdd_nodecount(all_outputs);
unsigned num_latches = bdd_nodecount(all_states);
unsigned init = aut->get_init_state_number();
aig circuit(num_inputs, num_latches, num_outputs);
bdd b;
// Latches and outputs are expressed as a DNF in which each term represents
// a transition.
// latch[i] (resp. out[i]) represents the i-th latch's (resp. output's)
// DNF.
std::vector<std::vector<unsigned>> latch(num_latches);
std::vector<std::vector<unsigned>> out(num_outputs);
for (unsigned s = 0; s < aut->num_states(); ++s)
for (auto& e: aut->out(s))
{
spot::minato_isop cond(e.cond);
while ((b = cond.next()) != bddfalse)
{
bdd input = bdd_existcomp(b, all_inputs);
bdd letter_out = bdd_existcomp(b, all_outputs);
auto out_vec = output_to_vec(letter_out);
unsigned dst = encode_init_0(e.dst, init);
auto next_state_vec = state_to_vec(dst, log2n);
unsigned src = encode_init_0(s, init);
bdd state_bdd = state_to_bdd(src, all_states);
std::vector<unsigned> prod;
while (input != bddfalse && input != bddtrue)
{
unsigned v =
circuit.input_var(bddvar_to_inputnum[bdd_var(input)],
bdd_ithvar(bdd_var(input)));
if (bdd_high(input) == bddfalse)
{
v = circuit.aig_not(v);
input = bdd_low(input);
}
else
input = bdd_high(input);
prod.push_back(v);
}
while (state_bdd != bddfalse && state_bdd != bddtrue)
{
unsigned v =
circuit.latch_var(bdd_var(state_bdd) - st0,
bdd_ithvar(bdd_var(state_bdd)));
if (bdd_high(state_bdd) == bddfalse)
{
v = circuit.aig_not(v);
state_bdd = bdd_low(state_bdd);
}
else
state_bdd = bdd_high(state_bdd);
prod.push_back(v);
}
unsigned t = circuit.aig_and(prod);
for (unsigned i = 0; i < next_state_vec.size(); ++i)
if (next_state_vec[i])
latch[i].push_back(t);
for (unsigned i = 0; i < num_outputs; ++i)
if (out_vec[i])
out[i].push_back(t);
}
}
for (unsigned i = 0; i < num_latches; ++i)
circuit.set_latch(i, circuit.aig_or(latch[i]));
for (unsigned i = 0; i < num_outputs; ++i)
circuit.set_output(i, circuit.aig_or(out[i]));
circuit.remove_unused();
return circuit;
}
class ltl_processor final : public job_processor
{
......@@ -601,6 +296,9 @@ namespace
int process_formula(spot::formula f,
const char*, int) override
{
spot::process_timer timer;
timer.start();
auto aut = trans_.run(&f);
bdd all_inputs = bddtrue;
bdd all_outputs = bddtrue;
......@@ -611,7 +309,6 @@ namespace
lowercase << (char)std::tolower(c);
unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
all_inputs &= bdd_ithvar(v);
bddvar_to_inputnum[v] = i;
}
for (unsigned i = 0; i < output_aps_.size(); ++i)
{
......@@ -620,12 +317,13 @@ namespace
lowercase << (char)std::tolower(c);
unsigned v = aut->register_ap(spot::formula::ap(lowercase.str()));
all_outputs &= bdd_ithvar(v);
bddvar_to_outputnum[v] = i;
}
auto split = split_automaton(aut, all_inputs);
auto dpa = to_dpa(split);
auto owner = make_alternating_owner(dpa);
auto pg = spot::parity_game(dpa, owner);
timer.stop();
if (opt_print_pg)
{
pg.print(std::cout);
......@@ -645,30 +343,44 @@ namespace
{
auto strat_aut =
strat_to_aut(pg, strategy, dpa, all_outputs);
auto circuit =
aut_to_aiger(strat_aut, all_inputs, all_outputs);
circuit.print();
// output the winning strategy
if (opt_print_aiger)
spot::print_aiger(std::cout, strat_aut);
else
{
automaton_printer printer;
printer.print(strat_aut, timer);
}
}
return 0;
}
else
std::cout << "UNREALIZABLE\n";
return 0;
{
std::cout << "UNREALIZABLE\n";
return 1;
}
}
case QP:
if (!opt_real)
{
std::cout << "The quasi-polynomial time algorithm does not"
" implement synthesis yet, use --realizability\n";
return 1;
return 2;
}
else if (pg.solve_qp())
std::cout << "REALIZABLE\n";
{
std::cout << "REALIZABLE\n";
return 0;
}
else
std::cout << "UNREALIZABLE\n";
return 0;
{
std::cout << "UNREALIZABLE\n";
return 1;
}
default:
SPOT_UNREACHABLE();
return 0;
return 2;
}
}
};
......@@ -710,11 +422,15 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_REAL:
opt_real = true;
break;
case OPT_PRINT_AIGER:
opt_print_aiger = true;
break;
}
return 0;
}
int main(int argc, char **argv)
int
main(int argc, char **argv)
{
setup(argv);
const argp ap = { options, parse_opt, nullptr,
......@@ -725,5 +441,5 @@ int main(int argc, char **argv)
spot::translator trans;
ltl_processor processor(trans, input_aps, output_aps);
processor.run();
return processor.run();
}
......@@ -1130,7 +1130,7 @@ Here is a list of named properties currently used inside Spot:
| ~incomplete-states~ | ~std::set<unsigned>~ | set of states numbers that should be displayed as incomplete (used internally by ~print_dot()~ when truncating large automata) |
| ~degen-levels~ | ~std::vector<unsigned>~ | level associated to each state by the degeneralization algorithm |
| ~simulated-states~ | ~std::vector<unsigned>~ | map states of the original automaton to states if the current automaton in the result of simulation-based reductions |
| ~synthesis-outputs~ | ~bdd~ | conjunction of controllable atomic propositions (used by ~print_aiger()~ to determine which propositions should be encoded as outputs of the circuit)
Objects referenced via named properties are automatically destroyed
when the automaton is destroyed, but this can be altered by passing a
custom destructor as a third parameter to =twa::set_named_prop()=.
......
......@@ -28,6 +28,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
twaalgosdir = $(pkgincludedir)/twaalgos
twaalgos_HEADERS = \
aiger.hh \
alternation.hh \
are_isomorphic.hh \
bfssteps.hh \
......@@ -93,6 +94,7 @@ twaalgos_HEADERS = \
noinst_LTLIBRARIES = libtwaalgos.la
libtwaalgos_la_SOURCES = \
aiger.cc \
alternation.cc \
are_isomorphic.cc \
bfssteps.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 <spot/twaalgos/aiger.hh>
#include <cmath>
#include <deque>
#include <map>
#include <unordered_map>
#include <vector>
#include <spot/twa/twagraph.hh>