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)) +