diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index d16efeb50..7d4a05c3f 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -39,12 +39,24 @@ enum { - OPT_INPUT = 256, + OPT_ALGO = 256, + OPT_INPUT, + OPT_OUTPUT, OPT_PRINT }; +enum solver +{ + QP, + REC +}; + static const argp_option options[] = { + { "algo", OPT_ALGO, "ALGO", 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 }, { "input", OPT_INPUT, "PROPS", 0, "comma-separated list of atomic propositions", 0}, { "print-pg", OPT_PRINT, nullptr, 0, @@ -65,7 +77,9 @@ const char argp_program_doc[] = std::vector input_aps; -bool opt_print_pg{false}; +bool opt_print_pg(false); +bool opt_real(false); +solver opt_solver(REC); namespace { @@ -195,11 +209,26 @@ namespace pg.print(std::cout); return 0; } - if (pg.solve_qp()) - std::cout << "realizable\n"; - else - std::cout << "unrealizable\n"; - return 0; + switch (opt_solver) + { + case REC: + { + if (pg.winner()) + std::cout << "REALIZABLE\n"; + else + std::cout << "UNREALIZABLE\n"; + return 0; + } + case QP: + if (pg.solve_qp()) + std::cout << "REALIZABLE\n"; + else + std::cout << "UNREALIZABLE\n"; + return 0; + default: + SPOT_UNREACHABLE(); + return 0; + } } }; } @@ -223,6 +252,17 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_PRINT: opt_print_pg = true; break; + case OPT_ALGO: + if (arg && strcmp(arg, "rec") == 0) + opt_solver = REC; + else if (arg && strcmp(arg, "qp") == 0) + opt_solver = QP; + else + { + std::cout << "Unknown solver: " << (arg ? arg : "") << '\n'; + return 1; + } + break; } return 0; } @@ -234,6 +274,8 @@ int main(int argc, char **argv) argp_program_doc, children, nullptr, nullptr }; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); + check_no_formula(); + spot::translator trans; ltl_processor processor(trans, input_aps); processor.run(); diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 318086985..a7e6e31ee 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -50,6 +50,10 @@ 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 +You can control the parity game solving step in two ways: +- By choosing a different algorithm using the =--algo= option. The default is +=rec= for Zielonka's recursive algorithm, and as of now the only other +available option is =qp= for Calude et al.'s quasi-polynomial time algorithm. +- By asking =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. diff --git a/spot/misc/game.cc b/spot/misc/game.cc index 34aa9ce5e..5e5249d49 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -54,11 +54,111 @@ void parity_game::print(std::ostream& os) } } +bool parity_game::winner() const +{ + std::unordered_set states_; + for (unsigned i = 0; i < num_states(); ++i) + states_.insert(i); + unsigned m = max_parity(); + auto w1 = winning_region(states_, m); + return w1.find(get_init_state_number()) != w1.end(); +} + bool parity_game::solve_qp() const { return reachability_game(*this).is_reachable(); } +void parity_game::attractor(const std::unordered_set& subgame, + std::unordered_set& set, + unsigned max_parity, bool odd, + bool attr_max) const +{ + unsigned size; + do + { + size = set.size(); + for (unsigned s: subgame) + { + bool any = false; + bool all = true; + for (auto& e: out(s)) + { + if (e.acc.max_set() - 1 <= max_parity + && subgame.find(e.dst) != subgame.end()) + { + if (set.find(e.dst) != set.end() + || (attr_max && e.acc.max_set() - 1 == max_parity)) + any = true; + else + all = false; + } + } + if ((owner_[s] == odd && any) || (owner_[s] != odd && all)) + set.insert(s); + } + } while (set.size() != size); +} + +std::unordered_set +parity_game::winning_region(std::unordered_set& subgame, + unsigned max_parity) const +{ + // The algorithm works recursively on subgames. To avoid useless copies of + // the game at each call, subgame and max_parity are used to filter states + // and transitions. + if (max_parity == 0 || subgame.empty()) + return std::unordered_set(); + bool odd = max_parity % 2 == 1; + std::unordered_set w1; + std::unordered_set removed; + + while (!subgame.empty()) + { + // Recursion on max_parity. + std::unordered_set u; + attractor(subgame, u, max_parity, odd, true); + + for (unsigned s: u) + subgame.erase(s); + auto w1_ = winning_region(subgame, max_parity - 1); + std::unordered_set w0_; + if (odd && w1_.size() != subgame.size()) + std::set_difference(subgame.begin(), subgame.end(), + w1_.begin(), w1_.end(), + std::inserter(w0_, w0_.begin())); + // if !odd, w0_ is not used. + for (unsigned s: u) + subgame.insert(s); + + if (odd && w1_.size() + u.size() == subgame.size()) + { + for (unsigned s: subgame) + w1.insert(s); + break; + } + else if (!odd && w1_.empty()) + break; + + // Unrolled tail-recursion on game size. + auto& wni = odd ? w0_ : w1_; + attractor(subgame, wni, max_parity, !odd); + + for (unsigned s: wni) + { + subgame.erase(s); + removed.insert(s); + } + + if (!odd) + for (unsigned s: wni) + w1.insert(s); + } + for (unsigned s: removed) + subgame.insert(s); + return w1; +} + int reachability_state::compare(const state* other) const { auto o = down_cast(other); diff --git a/spot/misc/game.hh b/spot/misc/game.hh index 34a1048e3..a0e35f155 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -82,33 +82,74 @@ public: return owner_[src]; } + unsigned max_parity() const + { + unsigned max_parity = 0; + for (auto& e: dpa_->edges()) + max_parity = std::max(max_parity, e.acc.max_set()); + SPOT_ASSERT(max_parity); + return max_parity - 1; + } + /// Print the parity game in PGSolver's format. void print(std::ostream& os); + // Compute the winner of this game using Zielonka's recursive algorithm. + // False is Even and True is Odd. + /** \verbatim + @article{ zielonka.98.tcs + title = "Infinite games on finitely coloured graphs with applications to + automata on infinite trees", + journal = "Theoretical Computer Science", + volume = "200", + number = "1", + pages = "135 - 183", + year = "1998", + author = "Wieslaw Zielonka", + } + \endverbatim */ + bool winner() 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}, + 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; + + // Compute (in place) a set of states from which player can force a visit + // through set. + // if attr_max is true, states that can force a visit through an edge with + // max parity are also counted in. + void attractor(const std::unordered_set& subgame, + std::unordered_set& set, unsigned max_parity, + bool player, bool attr_max = false) const; + + // Compute the winning region for player Odd. + std::unordered_set + winning_region(std::unordered_set& subgame, + unsigned max_parity) const; }; @@ -246,8 +287,7 @@ private: public: reachability_game(const parity_game& pg) - : twa(std::make_shared()), - pg_(pg) + : twa(std::make_shared()), pg_(pg) { init_state_ = std::shared_ptr(get_init_state()); }