diff --git a/NEWS b/NEWS index a8d7f1a9f..137e11256 100644 --- a/NEWS +++ b/NEWS @@ -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 diff --git a/bin/.gitignore b/bin/.gitignore index e993c0a55..935ab53b1 100644 --- a/bin/.gitignore +++ b/bin/.gitignore @@ -9,6 +9,7 @@ ltlcross ltldo ltlfilt ltlgrind +ltlsynt randaut randltl spot diff --git a/bin/Makefile.am b/bin/Makefile.am index 9469b535f..14be7285a 100644 --- a/bin/Makefile.am +++ b/bin/Makefile.am @@ -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 diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc new file mode 100644 index 000000000..d16efeb50 --- /dev/null +++ b/bin/ltlsynt.cc @@ -0,0 +1,240 @@ +// -*- 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 . + +#include +#include + +#include "common_aoutput.hh" +#include "common_finput.hh" +#include "common_setup.hh" +#include "common_sys.hh" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +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 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 make_alternating_owner(const spot::twa_graph_ptr& dpa, + bool init_owner = false) + { + std::vector seen(dpa->num_states(), false); + std::vector todo({dpa->get_init_state_number()}); + std::vector 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 input_aps; + + ltl_processor(spot::translator& trans, std::vector 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(); +} diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am index e2a704eed..64f1809df 100644 --- a/bin/man/Makefile.am +++ b/bin/man/Makefile.am @@ -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 $@ diff --git a/bin/man/ltlsynt.x b/bin/man/ltlsynt.x new file mode 100644 index 000000000..3481feecc --- /dev/null +++ b/bin/man/ltlsynt.x @@ -0,0 +1,3 @@ +.\" -*- coding: utf-8 -*- +[NAME] +ltlsynt \- synthesize AIGER circuits from LTL specifications diff --git a/doc/Makefile.am b/doc/Makefile.am index a63221a08..4502787b1 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -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 \ diff --git a/doc/org/arch.tex b/doc/org/arch.tex index 66c77713c..90306b998 100644 --- a/doc/org/arch.tex +++ b/doc/org/arch.tex @@ -28,6 +28,7 @@ \texttt{dstar2tgba}\\ \texttt{ltlcross}\\ \texttt{ltlgrind}\\ + \texttt{ltlsynt}\\ \texttt{ltldo}\\ \texttt{autcross} }; diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org new file mode 100644 index 000000000..318086985 --- /dev/null +++ b/doc/org/ltlsynt.org @@ -0,0 +1,55 @@ +# -*- 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. diff --git a/doc/org/tools.org b/doc/org/tools.org index 9925367dc..2d0e64eba 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -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), diff --git a/spot/misc/Makefile.am b/spot/misc/Makefile.am index 103e9db45..7bfdb0df2 100644 --- a/spot/misc/Makefile.am +++ b/spot/misc/Makefile.am @@ -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 \ diff --git a/spot/misc/game.cc b/spot/misc/game.cc new file mode 100644 index 000000000..34aa9ce5e --- /dev/null +++ b/spot/misc/game.cc @@ -0,0 +1,224 @@ +// -*- 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 . + +#include + +#include +#include "spot/misc/game.hh" + +namespace spot +{ + +void parity_game::print(std::ostream& os) +{ + os << "parity " << num_states() - 1 << ";\n"; + std::vector seen(num_states(), false); + std::vector 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(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 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(i + 1), + false); +} + +reachability_game_succ_iterator* +reachability_game::succ_iter(const state* s) const +{ + auto state = down_cast(s); + return new reachability_game_succ_iterator(pg_, *state); +} + +std::string reachability_game::format_state(const state* s) const +{ + auto state = down_cast(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 todo{*init_state_}; + while (!todo.empty()) + { + spot::reachability_state v = *todo.begin(); + todo.erase(todo.begin()); + + std::vector 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(); +} + +} diff --git a/spot/misc/game.hh b/spot/misc/game.hh new file mode 100644 index 000000000..34a1048e3 --- /dev/null +++ b/spot/misc/game.hh @@ -0,0 +1,270 @@ +// -*- 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 . + +#pragma once + +#include +#include +#include +#include + +#include +#include +#include + +namespace spot +{ + +class SPOT_API parity_game +{ +private: + const const_twa_graph_ptr dpa_; + const std::vector owner_; + +public: + /// \a parity_game provides an interface to manipulate a deterministic parity + /// automaton as a parity game, including methods to solve the game. + /// + /// \param dpa the underlying deterministic parity automaton + /// \param owner a vector of Booleans indicating the owner of each state, + /// with the convention that true represents player 1 and false represents + /// player 0. + parity_game(const twa_graph_ptr dpa, std::vector owner) + : dpa_(dpa), owner_(owner) + { + bool max; + bool odd; + dpa_->acc().is_parity(max, odd, true); + SPOT_ASSERT(max && odd); + SPOT_ASSERT(owner_.size() == dpa_->num_states()); + } + + unsigned num_states() const + { + return dpa_->num_states(); + } + + unsigned get_init_state_number() const + { + return dpa_->get_init_state_number(); + } + + internal::state_out + out(unsigned src) const + { + return dpa_->out(src); + } + + internal::state_out + out(unsigned src) + { + return dpa_->out(src); + } + + bool owner(unsigned src) const + { + return owner_[src]; + } + + /// Print the parity game in PGSolver's format. + void print(std::ostream& os); + + /// 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; +}; + + +class reachability_state: public state +{ +private: + unsigned num_; + std::vector b_; + bool anke_; + +public: + reachability_state(unsigned state, const std::vector& 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 b() const + { + return b_; + } + + unsigned num() const + { + return num_; + } + + bool anke() const + { + return anke_; + } +}; + +typedef std::shared_ptr + 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 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 0; + } +}; + +// 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 wincount_t; + typedef std::unordered_map, + 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()), + pg_(pg) + { + init_state_ = std::shared_ptr(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); + +}; + +}