From 8068cfad93df340389835727cfa9acea74049ba0 Mon Sep 17 00:00:00 2001 From: Alexandre Lewkowicz Date: Thu, 14 Jan 2016 16:54:08 +0100 Subject: [PATCH] safra: Add complete option and rename files * src/tests/safra.cc, src/twaalgos/safra.cc, src/twaalgos/safra.hh, src/tests/safra.test: Rename as... * spot/twaalgos/safra.cc, spot/twaalgos/safra.hh, tests/core/safra.cc tests/core/safra.test: ... these. * tests/Makefile.am: Update. --- {src => spot}/twaalgos/safra.cc | 39 ++++++++++++---------------- {src => spot}/twaalgos/safra.hh | 9 ++++--- tests/Makefile.am | 3 +++ {src/tests => tests/core}/safra.cc | 26 +++++++++++-------- {src/tests => tests/core}/safra.test | 4 +-- 5 files changed, 41 insertions(+), 40 deletions(-) rename {src => spot}/twaalgos/safra.cc (96%) rename {src => spot}/twaalgos/safra.hh (95%) rename {src/tests => tests/core}/safra.cc (85%) rename {src/tests => tests/core}/safra.test (97%) diff --git a/src/twaalgos/safra.cc b/spot/twaalgos/safra.cc similarity index 96% rename from src/twaalgos/safra.cc rename to spot/twaalgos/safra.cc index 9ca4fbb28..fa5e82a45 100644 --- a/src/twaalgos/safra.cc +++ b/spot/twaalgos/safra.cc @@ -24,9 +24,10 @@ #include #include "safra.hh" -#include "twaalgos/degen.hh" -#include "twaalgos/sccfilter.hh" -#include "twaalgos/simulation.hh" +#include "spot/twaalgos/degen.hh" +#include "spot/twaalgos/sccfilter.hh" +#include "spot/twaalgos/simulation.hh" +#include "spot/twaalgos/complete.hh" namespace spot { @@ -168,6 +169,8 @@ namespace spot } +std::vector find_scc_paths(const scc_info& scc); + unsigned safra_state::find_scc_brace_id(unsigned scc_id, const scc_info& scc) { @@ -459,23 +462,6 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, return nodes_ < other.nodes_; } - // All edge going into an accepting SCC are marked as accepting - // This helps safra make fewer trees as we immediately see the accepting - // edge and don't create useless states - void - emit_accepting_scc(twa_graph_ptr& aut, scc_info& scc) - { - for (auto& e: aut->edges()) - { - unsigned src_scc = scc.scc_of(e.src); - unsigned dst_scc = scc.scc_of(e.dst); - if (src_scc == dst_scc) - continue; - if (scc.is_accepting_scc(dst_scc)) - e.acc |= 1; - } - } - std::vector find_scc_paths(const scc_info& scc) { @@ -504,12 +490,17 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, twa_graph_ptr tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation, - bool pretty_print, bool scc_opt, bool use_bisimulation) + bool pretty_print, bool scc_opt, bool use_bisimulation, + bool complete) { // Degeneralize - twa_graph_ptr aut = spot::scc_filter(spot::degeneralize_tba(a)); + twa_graph_ptr aut = spot::degeneralize_tba(a); std::map implications; - aut = simulation(aut, &implications); + if (use_bisimulation) + { + aut = spot::scc_filter(aut); + aut = simulation(aut, &implications); + } scc_info scc = scc_info(aut); std::vector is_connected = find_scc_paths(scc); @@ -620,6 +611,8 @@ safra_state::compute_succs(const const_twa_graph_ptr& aut, res = simulation(res); if (pretty_print) res->set_named_prop("state-names", print_debug(seen)); + if (complete) + spot::complete_here(res); return res; } } diff --git a/src/twaalgos/safra.hh b/spot/twaalgos/safra.hh similarity index 95% rename from src/twaalgos/safra.hh rename to spot/twaalgos/safra.hh index 7fb323eb4..7d6d7a0bb 100644 --- a/src/twaalgos/safra.hh +++ b/spot/twaalgos/safra.hh @@ -22,9 +22,9 @@ #include #include -#include "misc/bddlt.hh" -#include "twa/twagraph.hh" -#include "twaalgos/sccinfo.hh" +#include +#include +#include namespace spot { @@ -98,5 +98,6 @@ namespace spot bool bisimulation = false, bool pretty_print = false, bool scc_opt = false, - bool use_bisimulation = false); + bool use_bisimulation = false, + bool complete = false); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 3b67497f2..f52b208b1 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -87,6 +87,7 @@ check_PROGRAMS = \ core/reduccmp \ core/reduceu \ core/reductaustr \ + core/safra \ core/syntimpl \ core/taatgba \ core/trival \ @@ -134,6 +135,7 @@ core_reduceu_SOURCES = core/equalsf.cc core_reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV core_reductaustr_SOURCES = core/equalsf.cc core_reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR +core_safra_SOURCES = core/safra.cc core_syntimpl_SOURCES = core/syntimpl.cc core_tostring_SOURCES = core/tostring.cc core_trival_SOURCES = core/trival.cc @@ -256,6 +258,7 @@ TESTS_twa = \ core/randtgba.test \ core/isomorph.test \ core/uniq.test \ + core/safra.test \ core/sbacc.test \ core/stutter-tgba.test \ core/strength.test \ diff --git a/src/tests/safra.cc b/tests/core/safra.cc similarity index 85% rename from src/tests/safra.cc rename to tests/core/safra.cc index 3a9466d30..15de7a24f 100644 --- a/src/tests/safra.cc +++ b/tests/core/safra.cc @@ -20,17 +20,18 @@ #include #include -#include "tl/parse.hh" // spot::parse_infix_psl -#include "tl/formula.hh" // spot::formula -#include "parseaut/public.hh" -#include "twa/twagraph.hh" -#include "twaalgos/degen.hh" -#include "twaalgos/dot.hh" // print_dot -#include "twaalgos/hoa.hh" // print_hoa -#include "twaalgos/safra.hh" -#include "twaalgos/translate.hh" +#include "spot/tl/parse.hh" // spot::parse_infix_psl +#include "spot/tl/formula.hh" // spot::formula +#include "spot/parseaut/public.hh" +#include "spot/twa/twagraph.hh" +#include "spot/twaalgos/degen.hh" +#include "spot/twaalgos/dot.hh" // print_dot +#include "spot/twaalgos/hoa.hh" // print_hoa +#include "spot/twaalgos/safra.hh" +#include "spot/twaalgos/translate.hh" +int help(); int help() { std::cerr << "safra [OPTIONS]\n"; @@ -53,6 +54,7 @@ int main(int argc, char* argv[]) bool out_dot = true; bool out_hoa = false; bool pretty_print = false; + bool complete = false; char* input = nullptr; if (argc <= 2) @@ -82,6 +84,8 @@ int main(int argc, char* argv[]) pretty_print = true; else if (!strncmp(argv[i], "-b", 2)) sim = true; + else if (!strncmp(argv[i], "-c", 2)) + complete = true; else if (!strncmp(argv[i], "--scc_opt", 9)) scc_opt = true; else if (!strncmp(argv[i], "--bisim_opt", 10)) @@ -108,7 +112,7 @@ int main(int argc, char* argv[]) trans.set_pref(spot::postprocessor::Deterministic); auto tmp = trans.run(f); res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt, - use_bisim); + use_bisim, complete); } else if (in_hoa) { @@ -116,7 +120,7 @@ int main(int argc, char* argv[]) if (aut->format_errors(std::cerr)) return 2; res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt, - use_bisim); + use_bisim, complete); } res->merge_edges(); diff --git a/src/tests/safra.test b/tests/core/safra.test similarity index 97% rename from src/tests/safra.test rename to tests/core/safra.test index af907b0af..2257450b7 100755 --- a/src/tests/safra.test +++ b/tests/core/safra.test @@ -173,7 +173,7 @@ a M G(F!b | X!a) G!a R XFb EOF run 0 ../safra --hoa double_b.hoa -H > out.hoa -ltl2tgba=../../bin/ltl2tgba -../../bin/ltlcross -F formulae \ +ltl2tgba=ltl2tgba +ltlcross -F formulae \ "../safra -f %f -H > %O" \ "$ltl2tgba -f %f -H > %O"