Commit bd75ab5b authored by Maximilien Colange's avatar Maximilien Colange
Browse files

ltlsynt: rework synthesis algorithms

ltlsynt now offers two algorithms: one where splitting occurs before
determinization (the historical one) and one where determinization
occurs before splitting.

* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: test it and refactor test file
* NEWS: document it
* spot/misc/game.hh, spot/misc/game.cc: remove Calude's algorithm
parent 516e9536
......@@ -34,6 +34,16 @@ New in spot 2.6.0.dev (not yet released)
- "ltlfilt --suspendable" is now a synonym for
"ltlfilt --universal --eventual".
- ltlsynt now has two algorithms for synthesis:
--algo=sd is the historical one. The automaton of the formula
is split to separate inputs and outputs, then
determinized.
--algo=ds the automaton of the formula is determinized, then
split to separate inputs and outputs.
In both cases, the obtained parity game is solved using
Zielonka algorithm. Calude's quasi-polynomial time algorithm has
been dropped as it was not used.
Bugs fixed:
- scc_info::split_on_sets() did not correctly register the
......
......@@ -70,10 +70,10 @@ static const argp_option options[] =
" propositions", 0},
/**************************************************/
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
{ "algo", OPT_ALGO, "qp|rec", 0,
"choose the parity game algorithm, valid ones are rec (Zielonka's"
" recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial"
" time algorithm)", 0 },
{ "algo", OPT_ALGO, "ds|sd", 0,
"choose the algorithm for synthesis:\n"
" - sd: split then determinize (default)\n"
" - ds: determinize then split", 0 },
/**************************************************/
{ nullptr, 0, nullptr, 0, "Output options:", 20 },
{ "print-pg", OPT_PRINT, nullptr, 0,
......@@ -112,27 +112,26 @@ bool opt_print_pg(false);
bool opt_real(false);
bool opt_print_aiger(false);
// FIXME rename options to choose the algorithm
enum solver
{
QP,
REC
DET_SPLIT,
SPLIT_DET
};
static char const *const solver_args[] =
{
"qp", "quasi-polynomial",
"recursive",
"detsplit", "ds",
"splitdet", "sd",
nullptr
};
static solver const solver_types[] =
{
QP, QP,
REC,
DET_SPLIT, DET_SPLIT,
SPLIT_DET, SPLIT_DET
};
ARGMATCH_VERIFY(solver_args, solver_types);
static solver opt_solver = REC;
static solver opt_solver = SPLIT_DET;
static bool verbose = false;
namespace
......@@ -187,7 +186,8 @@ namespace
{
// if the input automaton is deterministic, degeneralize it to be sure to
// end up with a parity automaton
auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split));
auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split),
false, true, true, false);
dpa->merge_edges();
if (opt_print_pg)
dpa = spot::sbacc(dpa);
......@@ -293,12 +293,40 @@ namespace
all_outputs &= bdd_ithvar(v);
}
auto split = split_2step(aut, all_inputs);
if (verbose)
std::cerr << "split inputs and outputs done" << std::endl;
auto dpa = to_dpa(split);
if (verbose)
std::cerr << "determinization done" << std::endl;
spot::twa_graph_ptr dpa = nullptr;
if (opt_solver == DET_SPLIT)
{
auto tmp = to_dpa(aut);
if (verbose)
std::cerr << "determinization done\n"
<< "dpa has " << tmp->num_states() << " states" << std::endl;
tmp->merge_states();
if (verbose)
std::cerr << "simulation done\n"
<< "dpa has " << tmp->num_states() << " states" << std::endl;
dpa = split_2step(tmp, all_inputs);
if (verbose)
std::cerr << "split inputs and outputs done\n"
<< "automaton has " << dpa->num_states() << " states"
<< std::endl;
spot::colorize_parity_here(dpa, true);
}
else
{
auto split = split_2step(aut, all_inputs);
if (verbose)
std::cerr << "split inputs and outputs done\n"
<< "automaton has " << split->num_states() << " states"
<< std::endl;
dpa = to_dpa(split);
if (verbose)
std::cerr << "determinization done\n"
<< "dpa has " << dpa->num_states() << " states" << std::endl;
dpa->merge_states();
if (verbose)
std::cerr << "simulation done\n"
<< "dpa has " << dpa->num_states() << " states" << std::endl;
}
auto owner = complete_env(dpa);
auto pg = spot::parity_game(dpa, owner);
if (verbose)
......@@ -310,58 +338,33 @@ namespace
pg.print(std::cout);
return 0;
}
switch (opt_solver)
spot::parity_game::strategy_t strategy[2];
spot::parity_game::region_t winning_region[2];
pg.solve(winning_region, strategy);
if (winning_region[1].count(pg.get_init_state_number()))
{
case REC:
std::cout << "REALIZABLE\n";
if (!opt_real)
{
spot::parity_game::strategy_t strategy[2];
spot::parity_game::region_t winning_region[2];
pg.solve(winning_region, strategy);
if (winning_region[1].count(pg.get_init_state_number()))
{
std::cout << "REALIZABLE\n";
if (!opt_real)
{
auto strat_aut =
strat_to_aut(pg, strategy[1], dpa, all_outputs);
// 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;
}
auto strat_aut =
strat_to_aut(pg, strategy[1], dpa, all_outputs);
// output the winning strategy
if (opt_print_aiger)
spot::print_aiger(std::cout, strat_aut);
else
{
std::cout << "UNREALIZABLE\n";
return 1;
automaton_printer printer;
printer.print(strat_aut, timer);
}
}
case QP:
if (!opt_real)
{
std::cout << "The quasi-polynomial time algorithm does not"
" implement synthesis yet, use --realizability\n";
return 2;
}
else if (pg.solve_qp())
{
std::cout << "REALIZABLE\n";
return 0;
}
else
{
std::cout << "UNREALIZABLE\n";
return 1;
}
default:
SPOT_UNREACHABLE();
return 2;
return 0;
}
else
{
std::cout << "UNREALIZABLE\n";
return 1;
}
}
};
......
......@@ -82,11 +82,6 @@ void parity_game::solve(region_t (&w)[2], strategy_t (&s)[2]) const
solve_rec(states_, m, w, s);
}
bool parity_game::solve_qp() const
{
return reachability_game(*this).is_reachable();
}
parity_game::strategy_t
parity_game::attractor(const region_t& subgame, region_t& set,
unsigned max_parity, int p, bool attr_max) const
......@@ -223,166 +218,4 @@ void parity_game::solve_rec(region_t& subgame, unsigned max_parity,
subgame.insert(w0[!p].begin(), w0[!p].end());
}
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;
}
}
return false;
}
bool reachability_game::is_target(const reachability_state& v)
{
return v.b().back();
}
}
......@@ -108,31 +108,6 @@ public:
\endverbatim */
void solve(region_t (&w)[2], strategy_t (&s)[2]) const;
/// Whether player 1 has a winning strategy from the initial state.
/// Implements Calude et al.'s quasipolynomial time algorithm.
/** \verbatim
@inproceedings{calude.17.stoc,
author = {Calude, Cristian S. and Jain, Sanjay and Khoussainov,
Bakhadyr and Li, Wei and Stephan, Frank},
title = {Deciding Parity Games in Quasipolynomial Time},
booktitle = {Proceedings of the 49th Annual ACM SIGACT Symposium on
Theory of Computing},
series = {STOC 2017},
year = {2017},
isbn = {978-1-4503-4528-6},
location = {Montreal, Canada},
pages = {252--263},
numpages = {12},
url = {http://doi.acm.org/10.1145/3055399.3055409},
doi = {10.1145/3055399.3055409},
acmid = {3055409},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Muller Games, Parity Games, Quasipolynomial Time Algorithm},
}
\endverbatim */
bool solve_qp() const;
private:
typedef twa_graph::graph_t::edge_storage_t edge_t;
......@@ -149,159 +124,4 @@ private:
region_t (&w)[2], strategy_t (&s)[2]) const;
};
class reachability_state: public state
{
private:
unsigned num_;
std::vector<unsigned> b_;
bool anke_;
public:
reachability_state(unsigned state, const std::vector<unsigned>& b,
bool anke)
: num_(state), b_(b), anke_(anke)
{
}
int compare(const state* other) const override;
bool operator==(const reachability_state& o) const
{
return compare(&o) == 0;
}
bool operator!=(const reachability_state& o) const
{
return compare(&o) != 0;
}
bool operator<(const reachability_state& o) const;
size_t hash() const override
{
size_t hash = wang32_hash(num_);
for (unsigned i = 0; i < b_.size(); ++i)
hash ^= wang32_hash(b_[i]) ^ wang32_hash(i);
return hash;
}
reachability_state* clone() const override
{
return new reachability_state(*this);
}
std::vector<unsigned> b() const
{
return b_;
}
unsigned num() const
{
return num_;
}
bool anke() const
{
return anke_;
}
};
typedef std::shared_ptr<const reachability_state>
const_reachability_state_ptr;
struct reachability_state_hash
{
size_t operator()(const reachability_state& state) const
{
return state.hash();
}
};
class reachability_game_succ_iterator final: public twa_succ_iterator
{
private:
const parity_game& pg_;
const reachability_state& state_;
internal::edge_iterator<const twa_graph::graph_t> it_;
public:
reachability_game_succ_iterator(const parity_game& pg,
const reachability_state& s)
: pg_(pg), state_(s)
{
}
bool first() override
{
it_ = pg_.out(state_.num()).begin();
return it_ != pg_.out(state_.num()).end();
}
bool next() override
{
++it_;
return it_ != pg_.out(state_.num()).end();
}
bool done() const override
{
return it_ == pg_.out(state_.num()).end();
}
const reachability_state* dst() const override;
bdd cond() const override
{
return bddtrue;
}
acc_cond::mark_t acc() const override
{
return {};
}
};
// On-the-fly reachability game interface for a max even parity game such
// that a target is reachable iff there is a memoryless winning strategy
// in the parity game for player 1.
class reachability_game final: public twa
{
private:
typedef std::unordered_map<spot::reachability_state, unsigned,
spot::reachability_state_hash> wincount_t;
typedef std::unordered_map<spot::reachability_state,
std::vector<spot::reachability_state>,
spot::reachability_state_hash> parents_t;
const parity_game& pg_;
// number of successors that need to have a winning strategy in order for
// a given node to have a winning strategy.
wincount_t c_;
parents_t parents_;
const_reachability_state_ptr init_state_; // cache
public:
reachability_game(const parity_game& pg)
: twa(std::make_shared<bdd_dict>()), pg_(pg)
{
init_state_ = std::shared_ptr<const reachability_state>(get_init_state());
}
const reachability_state* get_init_state() const override;
reachability_game_succ_iterator* succ_iter(const state* s) const override;
std::string format_state(const state* s) const override;
bool is_reachable();
private:
bool mark(const spot::reachability_state& s);
bool is_target(const reachability_state& s);
};
}
......@@ -104,7 +104,11 @@ diff out exp
cat >exp <<EOF
translating formula done
split inputs and outputs done
automaton has 9 states
determinization done
dpa has 14 states
simulation done
dpa has 14 states
parity game built
EOF
ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
......@@ -179,10 +183,11 @@ for i in 0 1 7 8 9; do
IN=$(eval echo \$IN$i)
OUT=$(eval echo \$OUT$i)
EXP=$(eval echo \$EXP$i)
test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \
--algo=rec)
test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \
--algo=qp)
for algo in sd ds; do
test $EXP = $(ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --realizability \
--algo=$algo)
done
done
for i in 2 3 4 5 6 10; do
......@@ -190,11 +195,18 @@ for i in 2 3 4 5 6 10; do
IN=$(eval echo \$IN$i)
OUT=$(eval echo \$OUT$i)
EXP=$(eval echo \$EXP$i)
ltlsynt -f "$F" --ins="$IN" --outs="$OUT" > out$i
REAL=`head -1 out$i`
test $REAL = $EXP
tail -n +2 out$i > res$i
ltl2tgba -f "!($F)" > negf_aut$i
# check that the L(strategy) is included in L(F)
autfilt -q -v --intersect=negf_aut$i res$i
# test ltlsynt
for algo in sd ds; do
ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true
REAL=`head -1 out$i`
test $REAL = $EXP
tail -n +2 out$i > res$i
# check that the L(strategy) is included in L(F)