From 1fdc32f9bb10ee3f76751e753ba1540407d61496 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Mon, 23 Apr 2018 10:51:17 +0200 Subject: [PATCH] ltlsynt: improve construction of turn-based games Improve the way transitions are duplicated when preparing the turn-based game for synthesis. The resulting arena should now be deterministic on nodes owned by the environment. Also move the code to another file, so that it is easier to test (e.g. in Python). * bin/ltlsynt.cc: move the code * spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and implement the improvements * tests/Makefile.am, tests/python/split.py: test it * tests/core/ltlsynt.test: update existing tests to reflect the changes --- bin/ltlsynt.cc | 59 ++-------------- spot/twaalgos/split.cc | 145 ++++++++++++++++++++++++++++++++++++++++ spot/twaalgos/split.hh | 20 ++++++ tests/Makefile.am | 1 + tests/core/ltlsynt.test | 23 ++++--- tests/python/split.py | 103 ++++++++++++++++++++++++++++ 6 files changed, 289 insertions(+), 62 deletions(-) create mode 100644 tests/python/split.py diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index be9af818f..910bca39c 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -34,17 +34,18 @@ #include #include -#include #include #include #include -#include +#include #include #include #include #include #include #include +#include +#include enum { @@ -136,54 +137,6 @@ static bool verbose = 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 any valuation of atomic - // propositions in I. - - static 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, {}); - split->new_edge(q, e.dst, out, e.acc); - } - } - split->prop_universal(spot::trival::maybe()); - return split; - } // Ensures that the game is complete for player 0. // Also computes the owner of each state (false for player 0, i.e. env). @@ -232,7 +185,9 @@ namespace static spot::twa_graph_ptr to_dpa(const spot::twa_graph_ptr& split) { - auto dpa = spot::tgba_determinize(split); + // 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)); dpa->merge_edges(); if (opt_print_pg) dpa = spot::sbacc(dpa); @@ -338,7 +293,7 @@ namespace all_outputs &= bdd_ithvar(v); } - auto split = split_automaton(aut, all_inputs); + auto split = split_2step(aut, all_inputs); if (verbose) std::cerr << "split inputs and outputs done" << std::endl; auto dpa = to_dpa(split); diff --git a/spot/twaalgos/split.cc b/spot/twaalgos/split.cc index f2d1bae92..df4aa5863 100644 --- a/spot/twaalgos/split.cc +++ b/spot/twaalgos/split.cc @@ -19,9 +19,154 @@ #include "config.h" #include +#include +#include +#include namespace spot { + twa_graph_ptr + split_2step(const const_twa_graph_ptr& aut, bdd input_bdd) + { + if (!aut->acc().is_generalized_buchi()) + throw std::runtime_error("2step_split only works on TGBA"); + auto split = make_twa_graph(aut->get_dict()); + split->copy_ap_of(aut); + split->copy_acceptance_of(aut); + split->new_states(aut->num_states()); + split->set_init_state(aut->get_init_state_number()); + + std::unordered_map sig2state; + + unsigned set_num = split->get_dict() + ->register_anonymous_variables(aut->num_states()+1, &sig2state); + bdd all_states = bddtrue; + for (unsigned i = 0; i <= aut->num_states(); ++i) + all_states &= bdd_ithvar(set_num + i); + + unsigned acc_vars = split->get_dict() + ->register_anonymous_variables(aut->num_sets(), &sig2state); + bdd all_acc = bddtrue; + for (unsigned i = 0; i < aut->num_sets(); ++i) + all_acc &= bdd_ithvar(acc_vars + i); + + for (unsigned src = 0; src < aut->num_states(); ++src) + { + std::unordered_map input2sig; + bdd support = bddtrue; + for (const auto& e : aut->out(src)) + support &= bdd_support(e.cond); + support = bdd_existcomp(support, input_bdd); + + bdd all_letters = bddtrue; + while (all_letters != bddfalse) + { + bdd one_letter = bdd_satoneset(all_letters, support, bddtrue); + all_letters -= one_letter; + auto it = input2sig.emplace(one_letter, bddfalse).first; + + for (const auto& e : aut->out(src)) + { + bdd sig = bddtrue; + sig &= bdd_exist(e.cond & one_letter, input_bdd); + + for (auto n : e.acc.sets()) + sig &= bdd_ithvar(acc_vars + n); + sig &= bdd_ithvar(set_num + e.dst); + + it->second |= sig; + } + } + + for (const auto& in : input2sig) + { + bdd sig = in.second; + auto it = sig2state.find(sig); + if (it == sig2state.end()) + { + unsigned ns = split->new_state(); + it = sig2state.emplace(sig, ns).first; + } + split->new_edge(src, it->second, in.first); + } + } + + // Now add all states based on their signatures + // This is very similar to the code of the simulation + bdd nonapvars = all_acc & all_states; + for (const auto& sig : sig2state) + { + // for each valuation, extract cond, acc and dst + bdd sup_sig = bdd_support(sig.first); + bdd sup_all_atomic_prop = bdd_exist(sup_sig, nonapvars); + bdd all_atomic_prop = bdd_exist(sig.first, nonapvars); + + // FIXME this is overkill, is not it? + while (all_atomic_prop != bddfalse) + { + bdd one = bdd_satoneset(all_atomic_prop, sup_all_atomic_prop, + bddtrue); + all_atomic_prop -= one; + + minato_isop isop(sig.first & one); + bdd cond_acc_dest; + while ((cond_acc_dest = isop.next()) != bddfalse) + { + + bdd cond = bdd_existcomp(cond_acc_dest, sup_all_atomic_prop); + unsigned dst = + bdd_var(bdd_existcomp(cond_acc_dest, all_states)) - set_num; + + bdd acc = bdd_existcomp(cond_acc_dest, all_acc); + spot::acc_cond::mark_t m({}); + while (acc != bddtrue) + { + m.set(bdd_var(acc) - acc_vars); + acc = bdd_high(acc); + } + + split->new_edge(sig.second, dst, cond, m); + } + } + } + + split->get_dict()->unregister_all_my_variables(&sig2state); + + split->merge_edges(); + + split->prop_universal(spot::trival::maybe()); + return split; + } + + twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut) + { + twa_graph_ptr out = make_twa_graph(aut->get_dict()); + out->copy_acceptance_of(aut); + out->copy_ap_of(aut); + out->new_states(aut->num_states()); + out->set_init_state(aut->get_init_state_number()); + + std::vector seen(aut->num_states(), false); + std::deque todo; + todo.push_back(aut->get_init_state_number()); + seen[aut->get_init_state_number()] = true; + while (!todo.empty()) + { + unsigned cur = todo.front(); + todo.pop_front(); + seen[cur] = true; + + for (const auto& i : aut->out(cur)) + for (const auto& o : aut->out(i.dst)) + { + out->new_edge(cur, o.dst, i.cond & o.cond, i.acc | o.acc); + if (!seen[o.dst]) + todo.push_back(o.dst); + } + } + return out; + } + twa_graph_ptr split_edges(const const_twa_graph_ptr& aut) { twa_graph_ptr out = make_twa_graph(aut->get_dict()); diff --git a/spot/twaalgos/split.hh b/spot/twaalgos/split.hh index 9247c4aab..80947ebfb 100644 --- a/spot/twaalgos/split.hh +++ b/spot/twaalgos/split.hh @@ -31,4 +31,24 @@ namespace spot /// propositions. After this we can consider that each edge of the /// automate is a transition labeled by one letter. SPOT_API twa_graph_ptr split_edges(const const_twa_graph_ptr& aut); + + /// \brief make each transition a 2-step transition + /// + /// Given a set of atomic propositions I, split each transition + /// p -- cond --> q cond in 2^2^AP + /// into a set of transitions of the form + /// p -- {a} --> (p,a) -- o --> q + /// for each a in cond \cap 2^2^I + /// and where o = (cond & a) \cap 2^2^(AP - I) + /// + /// By definition, the states p are deterministic, only the states of the form + /// (p,a) may be non-deterministic. + /// This function is used to transform an automaton into a turn-based game in + /// the context of LTL reactive synthesis. + SPOT_API twa_graph_ptr + split_2step(const const_twa_graph_ptr& aut, bdd input_bdd); + + /// \brief the reverse of 2step_split + SPOT_API twa_graph_ptr + unsplit_2step(const const_twa_graph_ptr& aut); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 8bb47e250..7e4fa0b98 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -393,6 +393,7 @@ TESTS_python = \ python/setacc.py \ python/setxor.py \ python/simstate.py \ + python/split.py \ python/streett_totgba.py \ python/streett_totgba2.py \ python/rs_like.py \ diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index aa8567850..d69446e77 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -23,22 +23,25 @@ set -e cat >exp < GFb' --print-pg > out diff out exp diff --git a/tests/python/split.py b/tests/python/split.py new file mode 100644 index 000000000..b4b2b7460 --- /dev/null +++ b/tests/python/split.py @@ -0,0 +1,103 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2018 Laboratoire de Recherche et +# Développement de l'Epita +# +# 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 . + +import spot + +def incl(a,b): + return not b.intersects(spot.dualize(spot.tgba_determinize(a))) +def equiv(a,b): + return incl(a,b) and incl(b,a) + +def do_split(f, in_list): + aut = spot.translate(f) + inputs = spot.buddy.bddtrue + for a in in_list: + inputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a))) + s = spot.split_2step(aut, inputs) + return aut,s + +aut, s = do_split('(FG !a) <-> (GF b)', ['a']) +assert equiv(aut, spot.unsplit_2step(s)) + +aut, s = do_split('GFa && GFb', ['a']) +assert equiv(aut, spot.unsplit_2step(s)) +assert s.to_str() == """HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0] 1 +[0] 2 +State: 1 +[!1] 0 +[1] 0 {1} +State: 2 +[!1] 0 {0} +[1] 0 {0 1} +--END--""" + +aut, s = do_split('! ((G (req -> (F ack))) && (G (go -> (F grant))))', ['go', + 'req']) +assert equiv(aut, spot.unsplit_2step(s)) +# FIXME s.to_str() is NOT the same on Debian stable and on Debian unstable +# we should investigate this +#assert s.to_str() == """HOA: v1 +#States: 9 +#Start: 0 +#AP: 4 "ack" "req" "go" "grant" +#acc-name: Buchi +#Acceptance: 1 Inf(0) +#properties: trans-labels explicit-labels state-acc +#--BODY-- +#State: 0 +#[1&!2] 3 +#[!1&!2] 4 +#[1&2] 5 +#[!1&2] 6 +#State: 1 +#[t] 7 +#State: 2 +#[t] 8 +#State: 3 +#[t] 0 +#[!0] 1 +#State: 4 +#[t] 0 +#State: 5 +#[t] 0 +#[!0] 1 +#[!3] 2 +#State: 6 +#[t] 0 +#[!3] 2 +#State: 7 {0} +#[!0] 1 +#State: 8 {0} +#[!3] 2 +#--END--""" + +aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \ + && g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))', ['r_0', 'r_1']) +assert equiv(aut, spot.unsplit_2step(s)) +