diff --git a/src/dstarparse/Makefile.am b/src/dstarparse/Makefile.am index 4c8c18cf0..a09e59e24 100644 --- a/src/dstarparse/Makefile.am +++ b/src/dstarparse/Makefile.am @@ -52,6 +52,8 @@ EXTRA_DIST = $(DSTARPARSE_YY) libdstarparse_la_SOURCES = \ fmterror.cc \ + dra2dba.cc \ + dstar2tgba.cc \ nra2nba.cc \ nsa2tgba.cc \ $(FROM_DSTARPARSE_YY) \ diff --git a/src/dstarparse/dra2dba.cc b/src/dstarparse/dra2dba.cc new file mode 100644 index 000000000..c10039f94 --- /dev/null +++ b/src/dstarparse/dra2dba.cc @@ -0,0 +1,293 @@ +// Copyright (C) 2013 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 "public.hh" +#include "tgba/tgbamask.hh" +#include "tgbaalgos/scc.hh" +#include "tgbaalgos/reachiter.hh" +#include "tgbaalgos/gtec/gtec.hh" +#include "tgbaalgos/sccfilter.hh" +#include "ltlast/constant.hh" + +namespace spot +{ + + // IMPORTANT NOTE: If you attempt to follow Krishnan et + // al. (ISAAC'94) paper while reading this code, make sure you + // understand the difference between their Rabin acceptance + // definition and the one we are using. + // + // Here, a cycle is accepting in a Rabin automaton if there exists + // an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ are + // visited while no states from Uᵢ are visited. This is the + // same definition used by ltl2dstar. + // + // In the Krishnan et al. paper, a cycle is accepting in a Rabin + // automaton if there exists an acceptance pair (Lᵢ, Uᵢ) such that + // some states from Lᵢ are visited and all visited states belongs to + // Uᵢ. In other words, you can switch from one definition to + // the other by complementing the Uᵢ set. + // + // This is a source of confusion; you have been warned. + + + // This function is defined in nra2nba.cc, and used only here. + SPOT_LOCAL + tgba* nra_to_nba(const dstar_aut* nra, const tgba* aut); + + namespace + { + typedef std::list state_list; + + static bool + filter_states(const tgba* aut, + const dstar_aut* dra, + const state_list& sl, + state_list& final, + state_list& nonfinal); + + static bool + filter_scc(const tgba* aut, + const dstar_aut* dra, + state_list& final, + state_list& nonfinal) + { + // Iterate over all non-trivial SCCs. + scc_map sm(aut); + sm.build_map(); + for (unsigned scc_max = sm.scc_count(), scc = 0; + scc < scc_max; ++scc) + { + if (sm.trivial(scc)) + { + nonfinal.push_back(sm.one_state_of(scc)); + continue; + } + + // Get the list of states of that SCC + const std::list& sl = sm.states_of(scc); + assert(!sl.empty()); + if (!filter_states(aut, dra, sl, final, nonfinal)) + return false; + } + return true; + } + + static bool + filter_states(const tgba* aut, + const dstar_aut* dra, + const state_list& sl, + state_list& final, + state_list& nonfinal) + { + // Check whether the SCC composed of all states in sl contains + // non-accepting cycles. + // + // A cycle is accepting (in a Rabin automaton) if there exists + // an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ + // are visited while no states from Uᵢ are visited. + // + // Consequently, a cycle is non-accepting if for all acceptance + // pairs (Lᵢ, Uᵢ), either no states from Lᵢ are visited or some + // states from Uᵢ are visited. (This corresponds to an + // accepting cycle with Streett acceptance.) + // + // Now we consider the SCC as one large cycle and check its + // intersection with all Lᵢs and Uᵢs. Let l=[l₁,l₂,...] and + // u=[u₁,u₂,...] be bitvectors where bit lᵢ (resp. uᵢ) + // indicates that Lᵢ (resp. Uᵢ) has been visited in the SCC. + state_list::const_iterator it = sl.begin(); + int num = dra->aut->get_label(*it++); + bitvect* l = dra->accsets->at(num * 2).clone(); + bitvect* u = dra->accsets->at(num * 2 + 1).clone(); + for (; it != sl.end(); ++it) + { + num = dra->aut->get_label(*it); + *l |= dra->accsets->at(num * 2); + *u |= dra->accsets->at(num * 2 + 1); + } + // If we have l&!u = [0,0,...] that means that the cycle formed + // by the entire SCC is not accepting. However that does not + // necessarily imply that all cycles in the SCC are also + // non-accepting. We may have a smaller cycle that is + // accepting, but which becomes non-accepting when extended with + // more states. + *l -= *u; + delete u; + if (l->is_fully_clear()) + { + delete l; + // Check whether the SCC is accepting. We do that by simply + // converting that SCC into a TGBA and running our emptiness + // check. This is not a really smart implementation and + // could be improved. + { + state_set keep(sl.begin(), sl.end()); + const tgba* masked = + build_tgba_mask_keep(dra->aut, keep, sl.front()); + const tgba* nba = nra_to_nba(dra, masked); + emptiness_check* ec = couvreur99(nba); + emptiness_check_result* ecr = ec->check(); + delete ecr; + delete ec; + delete nba; + delete masked; + if (ecr) + { + // This SCC is not DBA-realizable. + //std::cerr << "not DBA-realizable\n"; + return false; + } + } + //std::cerr << "non-accepting\n"; + for (state_list::const_iterator i = sl.begin(); + i != sl.end(); ++i) + nonfinal.push_back(*i); + return true; + } + // The bits sets in *l corresponds to Lᵢs that have been seen + // without seeing the matching Uᵢ. In this SCC, any state in Lᵢ + // is therefore final. Otherwise we do not know: it is possible + // that there is a non-accepting cycle in the SCC that do not + // visit Lᵢ. + state_set unknown; + for (it = sl.begin(); it != sl.end(); ++it) + { + num = dra->aut->get_label(*it); + bitvect* l2 = dra->accsets->at(num * 2).clone(); + *l2 &= *l; + if (!l2->is_fully_clear()) + { + final.push_back(*it); + } + else + { + unknown.insert(*it); + } + delete l2; + } + delete l; + // Check whether it is possible to build non-accepting cycles + // using only the "unknown" states. + while (!unknown.empty()) + { + //std::cerr << "unknown\n"; + // Build a sub-automaton for just the unknown states, + // starting from any state in the SCC. + const tgba* scc_mask = + build_tgba_mask_keep(aut, unknown, *unknown.begin()); + state_list local_final; + state_list local_nonfinal; + bool dbarealizable = + filter_scc(scc_mask, dra, local_final, local_nonfinal); + delete scc_mask; + if (!dbarealizable) + return false; + for (state_list::const_iterator i = local_final.begin(); + i != local_final.end(); ++i) + unknown.erase(*i); + final.splice(final.end(), local_final); + for (state_list::const_iterator i = local_nonfinal.begin(); + i != local_nonfinal.end(); ++i) + unknown.erase(*i); + nonfinal.splice(nonfinal.end(), local_nonfinal); + } + return true; + } + + + + class dra_to_dba_worker: public tgba_reachable_iterator_depth_first + { + public: + dra_to_dba_worker(const tgba_explicit_number* a, const state_set& final): + tgba_reachable_iterator_depth_first(a), + in_(a), + out_(new tgba_explicit_number(a->get_dict())), + final_(final) + { + bdd_dict* bd = a->get_dict(); + bd->register_all_variables_of(a, out_); + + // Invent a new acceptance set for the degeneralized automaton. + int accvar = + bd->register_acceptance_variable(ltl::constant::true_instance(), + out_); + acc_ = bdd_ithvar(accvar); + out_->set_acceptance_conditions(acc_); + } + + tgba_explicit_number* + result() + { + return out_; + } + + void + process_link(const state* sin, int, + const state* sout, int, + const tgba_succ_iterator* si) + { + int in = in_->get_label(sin); + int out = in_->get_label(sout); + + typedef state_explicit_number::transition trans; + trans* t = out_->create_transition(in, out); + bdd cond = t->condition = si->current_condition(); + + if (final_.find(sin) != final_.end()) + t->acceptance_conditions = acc_; + } + + protected: + const tgba_explicit_number* in_; + tgba_explicit_number* out_; + const tgba* d_; + const state_set& final_; + bdd acc_; + }; + + } + + + tgba* dra_to_dba(const dstar_aut* dra) + { + assert(dra->type == Rabin); + + state_list final; + state_list nonfinal; + if (!filter_scc(dra->aut, dra, final, nonfinal)) + return 0; + + // for (state_list::const_iterator i = final.begin(); + // i != final.end(); ++i) + // std::cerr << dra->aut->get_label(*i) << " is final\n"; + // for (state_list::const_iterator i = nonfinal.begin(); + // i != nonfinal.end(); ++i) + // std::cerr << dra->aut->get_label(*i) << " is non-final\n"; + + state_set fs(final.begin(), final.end()); + dra_to_dba_worker w(dra->aut, fs); + w.run(); + tgba_explicit_number* res1 = w.result(); + tgba* res2 = scc_filter_states(res1); + delete res1; + return res2; + } + +} diff --git a/src/dstarparse/dstar2tgba.cc b/src/dstarparse/dstar2tgba.cc new file mode 100644 index 000000000..3af64598f --- /dev/null +++ b/src/dstarparse/dstar2tgba.cc @@ -0,0 +1,41 @@ +// Copyright (C) 2013 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 "public.hh" + +namespace spot +{ + tgba* + dstar_to_tgba(const dstar_aut* daut) + { + switch (daut->type) + { + case spot::Rabin: + { + tgba* res = dra_to_dba(daut); + if (res) + return res; + return nra_to_nba(daut); + } + case spot::Streett: + return spot::nsa_to_tgba(daut); + } + assert(!"unreachable code"); + return 0; + } +} diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index cfcec40a7..accaf1790 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -35,14 +35,17 @@ namespace spot class nra_to_nba_worker: public tgba_reachable_iterator_depth_first { public: - nra_to_nba_worker(const dstar_aut* a): - tgba_reachable_iterator_depth_first(a->aut), - out_(new tgba_explicit_number(a->aut->get_dict())), + // AUT is the automate we iterate on, while A is the automaton + // we read the acceptance conditions from. Separating the two + // makes its possible to mask AUT, as needed in dra_to_dba(). + nra_to_nba_worker(const dstar_aut* a, const tgba* aut): + tgba_reachable_iterator_depth_first(aut), + out_(new tgba_explicit_number(aut->get_dict())), d_(a), num_states_(a->aut->num_states()) { bdd_dict* bd = out_->get_dict(); - bd->register_all_variables_of(a->aut, out_); + bd->register_all_variables_of(aut, out_); // Invent a new acceptance set for the degeneralized automaton. int accvar = @@ -113,16 +116,24 @@ namespace spot } + // In dra_to_dba() we call this function with a second argument + // that is a masked version of nra->aut. + SPOT_LOCAL + tgba* nra_to_nba(const dstar_aut* nra, const tgba* aut) + { + assert(nra->type == Rabin); + nra_to_nba_worker w(nra, aut); + w.run(); + tgba_explicit_number* res1 = w.result(); + tgba* res2 = scc_filter_states(res1); + delete res1; + return res2; + } + SPOT_API tgba* nra_to_nba(const dstar_aut* nra) { - assert(nra->type == Rabin); - nra_to_nba_worker w(nra); - w.run(); - tgba_explicit_number* aut = w.result(); - tgba* res = scc_filter_states(aut); - delete aut; - return res; + return nra_to_nba(nra, nra->aut); } } diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh index 634d15e65..d635d05ca 100644 --- a/src/dstarparse/public.hh +++ b/src/dstarparse/public.hh @@ -106,13 +106,40 @@ namespace spot /// \brief Convert a non-deterministic Rabin automaton into a /// non-deterministic Büchi automaton. - SPOT_API - tgba* nra_to_nba(const dstar_aut* nra); + SPOT_API tgba* + nra_to_nba(const dstar_aut* nra); + + /// \brief Convert a non-deterministic Rabin automaton into a + /// non-deterministic Büchi automaton. + /// + /// This version simply ignores all states in \a ignore. + SPOT_API tgba* + nra_to_nba(const dstar_aut* nra, const state_set* ignore); + + /// \brief Convert a deterministic Rabin automaton into a + /// deterministic Büchi automaton when possible. + /// + /// See "Deterministic ω-automata vis-a-vis Deterministic Büchi + /// Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94) for + /// more details. + /// + /// If the DRA is DBA-realizable, return that DBA. Otherwise, + /// return NULL. + SPOT_API tgba* + dra_to_dba(const dstar_aut* dra); /// \brief Convert a non-deterministic Streett automaton into a /// non-deterministic tgba. - SPOT_API - tgba* nsa_to_tgba(const dstar_aut* nra); + SPOT_API tgba* + nsa_to_tgba(const dstar_aut* nra); + + /// \brief Convert a Rabin or Streett automaton into a TGBA. + /// + /// For DRA, this function uses dra_to_dba() when possible, or fall + /// back to nra_to_nba(). + SPOT_API tgba* + dstar_to_tgba(const dstar_aut* dstar); + /// @} } diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test index 0d6c1863b..ffec48eb7 100755 --- a/src/tgbatest/dstar.test +++ b/src/tgbatest/dstar.test @@ -25,6 +25,9 @@ . ./defs set -e + +# DRA generated with +# ltlfilt -f 'a U b' -l | ltl2dstar --ltl2nba=spin:path/ltl2tgba@-s - - cat >dra.dstar <expected < 1 + 1 [label="1"] + 1 -> 1 [label="a & !b\n"] + 1 -> 2 [label="b\n"] + 2 [label="3", peripheries=2] + 2 -> 2 [label="1\n{Acc[1]}"] +} +EOF + +diff expected stdout + + + +# DSA generated with +# ltlfilt -f 'FGa' -l | +# ltl2dstar --automata=streett --ltl2nba=spin:path/ltl2tgba@-s - - cat >dsa.dstar <dra.dstar <expected < 1 + 1 [label="1"] + 1 -> 2 [label="!a & !b\n"] + 1 -> 3 [label="a & !b\n"] + 1 -> 4 [label="b & !a\n"] + 1 -> 5 [label="a & b\n"] + 2 [label="2"] + 2 -> 2 [label="!b\n"] + 2 -> 4 [label="b\n"] + 3 [label="3", peripheries=2] + 3 -> 2 [label="!a & !b\n{Acc[1]}"] + 3 -> 3 [label="a & !b\n{Acc[1]}"] + 3 -> 4 [label="b & !a\n{Acc[1]}"] + 3 -> 5 [label="a & b\n{Acc[1]}"] + 4 [label="4", peripheries=2] + 4 -> 4 [label="1\n{Acc[1]}"] + 5 [label="5", peripheries=2] + 5 -> 4 [label="!a\n{Acc[1]}"] + 5 -> 5 [label="a\n{Acc[1]}"] +} +EOF + +diff expected stdout diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7667034ef..bb10ffa1a 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -124,6 +124,8 @@ syntax(char* prog) << " ltl2dstar file" << std::endl << " -XDB read the from an ltl2dstar file and convert it to " << "TGBA" << std::endl + << " -XDD read the from an ltl2dstar file and convert it to " + << "TGBA,\n keeping it deterministic when possible\n" << " -XL do not compute an automaton, read it from an" << " LBTT file" << std::endl << " -XN do not compute an automaton, read it from a" @@ -368,6 +370,7 @@ main(int argc, char** argv) bool from_file = false; enum { ReadSpot, ReadLbtt, ReadNeverclaim, ReadDstar } readformat = ReadSpot; bool nra2nba = false; + bool dra2dba = false; bool scc_filter = false; bool simpltl = false; spot::ltl::ltl_simplifier_options redopt(false, false, false, false, @@ -917,6 +920,13 @@ main(int argc, char** argv) readformat = ReadDstar; nra2nba = true; } + else if (!strcmp(argv[formula_index], "-XDD")) + { + from_file = true; + readformat = ReadDstar; + nra2nba = true; + dra2dba = true; + } else if (!strcmp(argv[formula_index], "-XL")) { from_file = true; @@ -1104,11 +1114,22 @@ main(int argc, char** argv) spot::dstar_aut* daut; daut = spot::dstar_parse(input, pel, dict, env, debug_opt); + tm.stop("parsing dstar"); + if (spot::format_dstar_parse_errors(std::cerr, input, pel)) + { + delete to_free; + delete dict; + return 2; + } + tm.start("dstar2tgba"); if (nra2nba) { if (daut->type == spot::Rabin) { - to_free = a = spot::nra_to_nba(daut); + if (dra2dba) + to_free = a = spot::dstar_to_tgba(daut); + else + to_free = a = spot::nra_to_nba(daut); assume_sba = true; } else @@ -1123,14 +1144,8 @@ main(int argc, char** argv) daut->aut = 0; assume_sba = false; } + tm.stop("dstar2tgba"); delete daut; - tm.stop("parsing dstar"); - if (spot::format_dstar_parse_errors(std::cerr, input, pel)) - { - delete to_free; - delete dict; - return 2; - } } break; }