From e0bd0ad4c03381c3d23cf4f2e1c916fb765c64e6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 21 Apr 2015 19:13:55 +0200 Subject: [PATCH] rename tgba_digraph as twa_graph Automatic mass renaming. * src/bin/autfilt.cc, src/bin/common_aoutput.cc, src/bin/common_aoutput.hh, src/bin/common_conv.cc, src/bin/common_conv.hh, src/bin/common_output.hh, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/randaut.cc, src/dstarparse/dra2ba.cc, src/dstarparse/dstar2tgba.cc, src/dstarparse/dstarparse.yy, src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc, src/dstarparse/public.hh, src/graphtest/tgbagraph.cc, src/hoaparse/hoaparse.yy, src/hoaparse/public.hh, src/ltlvisit/contain.hh, src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh, src/priv/accmap.hh, src/taalgos/minimize.cc, src/tgba/fwd.hh, src/tgba/tgba.cc, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh, src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh, src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.hh, src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh, src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbacomp.hh, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh, src/tgbaalgos/hoa.cc, src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh, src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh, src/tgbaalgos/product.cc, src/tgbaalgos/product.hh, src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.cc, src/tgbaalgos/randomize.hh, src/tgbaalgos/relabel.cc, src/tgbaalgos/relabel.hh, src/tgbaalgos/remfin.cc, src/tgbaalgos/remfin.hh, src/tgbaalgos/remprop.cc, src/tgbaalgos/remprop.hh, src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh, src/tgbaalgos/sbacc.cc, src/tgbaalgos/sbacc.hh, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh, src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh, src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh, src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh, src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh, src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc, wrap/python/spot_impl.i, wrap/python/tests/automata-io.ipynb, wrap/python/tests/automata.ipynb, wrap/python/tests/piperead.ipynb, wrap/python/tests/testingaut.ipynb: Rename tgba_digraph as twa_graph. --- src/bin/autfilt.cc | 12 +++---- src/bin/common_aoutput.cc | 2 +- src/bin/common_aoutput.hh | 4 +-- src/bin/common_conv.cc | 2 +- src/bin/common_conv.hh | 2 +- src/bin/common_output.hh | 2 +- src/bin/dstar2tgba.cc | 2 +- src/bin/ltlcross.cc | 20 +++++------ src/bin/ltldo.cc | 4 +-- src/bin/randaut.cc | 4 +-- src/dstarparse/dra2ba.cc | 10 +++--- src/dstarparse/dstar2tgba.cc | 2 +- src/dstarparse/dstarparse.yy | 2 +- src/dstarparse/nra2nba.cc | 10 +++--- src/dstarparse/nsa2tgba.cc | 4 +-- src/dstarparse/public.hh | 14 ++++---- src/graphtest/tgbagraph.cc | 2 +- src/hoaparse/hoaparse.yy | 6 ++-- src/hoaparse/public.hh | 6 ++-- src/ltlvisit/contain.hh | 2 +- src/ltlvisit/exclusive.cc | 4 +-- src/ltlvisit/exclusive.hh | 2 +- src/priv/accmap.hh | 10 +++--- src/taalgos/minimize.cc | 6 ++-- src/tgba/fwd.hh | 6 ++-- src/tgba/tgba.cc | 4 +-- src/tgba/tgbagraph.cc | 6 ++-- src/tgba/tgbagraph.hh | 44 ++++++++++++------------ src/tgba/tgbasafracomplement.cc | 22 ++++++------ src/tgba/tgbasafracomplement.hh | 6 ++-- src/tgbaalgos/are_isomorphic.cc | 18 +++++----- src/tgbaalgos/are_isomorphic.hh | 8 ++--- src/tgbaalgos/canonicalize.cc | 8 ++--- src/tgbaalgos/canonicalize.hh | 2 +- src/tgbaalgos/cleanacc.cc | 6 ++-- src/tgbaalgos/cleanacc.hh | 8 ++--- src/tgbaalgos/complete.cc | 6 ++-- src/tgbaalgos/complete.hh | 6 ++-- src/tgbaalgos/compsusp.cc | 10 +++--- src/tgbaalgos/compsusp.hh | 2 +- src/tgbaalgos/cycles.hh | 2 +- src/tgbaalgos/degen.cc | 22 ++++++------ src/tgbaalgos/degen.hh | 8 ++--- src/tgbaalgos/dotty.cc | 10 +++--- src/tgbaalgos/dtbasat.cc | 28 ++++++++-------- src/tgbaalgos/dtbasat.hh | 12 +++---- src/tgbaalgos/dtgbacomp.cc | 10 +++--- src/tgbaalgos/dtgbacomp.hh | 4 +-- src/tgbaalgos/dtgbasat.cc | 28 ++++++++-------- src/tgbaalgos/dtgbasat.hh | 12 +++---- src/tgbaalgos/dupexp.cc | 10 +++--- src/tgbaalgos/dupexp.hh | 4 +-- src/tgbaalgos/emptiness.cc | 4 +-- src/tgbaalgos/emptiness.hh | 2 +- src/tgbaalgos/hoa.cc | 12 +++---- src/tgbaalgos/isdet.cc | 8 ++--- src/tgbaalgos/isdet.hh | 6 ++-- src/tgbaalgos/lbtt.cc | 6 ++-- src/tgbaalgos/ltl2tgba_fm.cc | 14 ++++---- src/tgbaalgos/ltl2tgba_fm.hh | 6 ++-- src/tgbaalgos/mask.cc | 8 ++--- src/tgbaalgos/mask.hh | 20 +++++------ src/tgbaalgos/minimize.cc | 32 +++++++++--------- src/tgbaalgos/minimize.hh | 10 +++--- src/tgbaalgos/neverclaim.cc | 8 ++--- src/tgbaalgos/postproc.cc | 30 ++++++++--------- src/tgbaalgos/postproc.hh | 8 ++--- src/tgbaalgos/powerset.cc | 32 +++++++++--------- src/tgbaalgos/powerset.hh | 18 +++++----- src/tgbaalgos/product.cc | 10 +++--- src/tgbaalgos/product.hh | 8 ++--- src/tgbaalgos/randomgraph.cc | 6 ++-- src/tgbaalgos/randomgraph.hh | 2 +- src/tgbaalgos/randomize.cc | 4 +-- src/tgbaalgos/randomize.hh | 2 +- src/tgbaalgos/relabel.cc | 2 +- src/tgbaalgos/relabel.hh | 2 +- src/tgbaalgos/remfin.cc | 6 ++-- src/tgbaalgos/remfin.hh | 4 +-- src/tgbaalgos/remprop.cc | 4 +-- src/tgbaalgos/remprop.hh | 2 +- src/tgbaalgos/safety.cc | 4 +-- src/tgbaalgos/safety.hh | 4 +-- src/tgbaalgos/sbacc.cc | 4 +-- src/tgbaalgos/sbacc.hh | 2 +- src/tgbaalgos/sccfilter.cc | 20 +++++------ src/tgbaalgos/sccfilter.hh | 12 +++---- src/tgbaalgos/sccinfo.cc | 6 ++-- src/tgbaalgos/sccinfo.hh | 8 ++--- src/tgbaalgos/simulation.cc | 52 ++++++++++++++--------------- src/tgbaalgos/simulation.hh | 24 ++++++------- src/tgbaalgos/stats.cc | 2 +- src/tgbaalgos/stats.hh | 2 +- src/tgbaalgos/stripacc.cc | 2 +- src/tgbaalgos/stripacc.hh | 4 +-- src/tgbaalgos/stutter.cc | 40 +++++++++++----------- src/tgbaalgos/stutter.hh | 32 +++++++++--------- src/tgbaalgos/totgba.cc | 6 ++-- src/tgbaalgos/totgba.hh | 4 +-- src/tgbaalgos/translate.cc | 6 ++-- src/tgbaalgos/translate.hh | 4 +-- src/tgbatest/checkpsl.cc | 4 +-- src/tgbatest/complementation.cc | 4 +-- src/tgbatest/emptchk.cc | 2 +- src/tgbatest/ltl2tgba.cc | 14 ++++---- src/tgbatest/randtgba.cc | 12 +++---- wrap/python/spot_impl.i | 10 +++--- wrap/python/tests/automata-io.ipynb | 10 +++--- wrap/python/tests/automata.ipynb | 16 ++++----- wrap/python/tests/piperead.ipynb | 12 +++---- wrap/python/tests/testingaut.ipynb | 2 +- 111 files changed, 523 insertions(+), 523 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 6faec223e..3a8919b94 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -208,7 +208,7 @@ static const struct argp_child children[] = { 0, 0, 0, 0 } }; -typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; +typedef spot::twa_graph::graph_t::trans_storage_t tr_t; typedef std::set> unique_aut_t; static long int match_count = 0; static spot::option_map extra_options; @@ -223,9 +223,9 @@ static int opt_seed = 0; static struct opt_t { spot::bdd_dict_ptr dict = spot::make_bdd_dict(); - spot::tgba_digraph_ptr product = nullptr; - spot::tgba_digraph_ptr intersect = nullptr; - spot::tgba_digraph_ptr are_isomorphic = nullptr; + spot::twa_graph_ptr product = nullptr; + spot::twa_graph_ptr intersect = nullptr; + spot::twa_graph_ptr are_isomorphic = nullptr; std::unique_ptr isomorphism_checker = nullptr; std::unique_ptr uniq = nullptr; @@ -488,7 +488,7 @@ namespace // never modify the original automaton (e.g. with // merge_transitions()) and the statistics about it make sense. auto aut = ((automaton_format == Stats) || opt_name) - ? spot::make_tgba_digraph(haut->aut, spot::twa::prop_set::all()) + ? spot::make_twa_graph(haut->aut, spot::twa::prop_set::all()) : haut->aut; // Preprocessing. @@ -576,7 +576,7 @@ namespace if (opt->uniq) { auto tmp = - spot::canonicalize(make_tgba_digraph(aut, + spot::canonicalize(make_twa_graph(aut, spot::twa::prop_set::all())); if (!opt->uniq->emplace(tmp->transition_vector().begin() + 1, tmp->transition_vector().end()).second) diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 0de670db5..3c072f72c 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -231,7 +231,7 @@ automaton_printer::automaton_printer(stat_style input) } void -automaton_printer::print(const spot::tgba_digraph_ptr& aut, +automaton_printer::print(const spot::twa_graph_ptr& aut, const spot::ltl::formula* f, // Input location for errors and statistics. const char* filename, diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index 7f402c65a..648b4283a 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -107,7 +107,7 @@ public: /// to be output. std::ostream& print(const spot::const_hoa_aut_ptr& haut, - const spot::const_tgba_digraph_ptr& aut, + const spot::const_twa_graph_ptr& aut, const spot::ltl::formula* f, const char* filename, int loc, double run_time) { @@ -225,7 +225,7 @@ public: automaton_printer(stat_style input = no_input); void - print(const spot::tgba_digraph_ptr& aut, + print(const spot::twa_graph_ptr& aut, const spot::ltl::formula* f = nullptr, // Input location for errors and statistics. const char* filename = nullptr, diff --git a/src/bin/common_conv.cc b/src/bin/common_conv.cc index 8bead3eea..5429fe01c 100644 --- a/src/bin/common_conv.cc +++ b/src/bin/common_conv.cc @@ -70,7 +70,7 @@ to_probability(const char* s) return res; } -spot::tgba_digraph_ptr +spot::twa_graph_ptr read_automaton(const char* filename, spot::bdd_dict_ptr& dict) { spot::hoa_parse_error_list pel; diff --git a/src/bin/common_conv.hh b/src/bin/common_conv.hh index 8843b681a..1abf61b36 100644 --- a/src/bin/common_conv.hh +++ b/src/bin/common_conv.hh @@ -31,5 +31,5 @@ float to_probability(const char* s); // Parse the comma or space seperate string of numbers. std::vector to_longs(const char* s); -spot::tgba_digraph_ptr +spot::twa_graph_ptr read_automaton(const char* filename, spot::bdd_dict_ptr& dict); diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index e340f2cd3..1a2ee334f 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -77,7 +77,7 @@ public: using spot::formater::set_output; std::ostream& - print(const spot::const_tgba_digraph_ptr& aut, + print(const spot::const_twa_graph_ptr& aut, const spot::ltl::formula* f = 0, double run_time = -1.) { diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index f96084016..230d7e6d3 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -268,7 +268,7 @@ namespace /// to be output. std::ostream& print(const spot::const_dstar_aut_ptr& daut, - const spot::const_tgba_digraph_ptr& aut, + const spot::const_twa_graph_ptr& aut, const char* filename, double run_time) { filename_ = filename; diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 67e0de9f6..f367674c9 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -484,7 +484,7 @@ namespace has_sr = has('D'); } - spot::tgba_digraph_ptr + spot::twa_graph_ptr translate(unsigned int translator_num, char l, statistics_formula* fstats, bool& problem) { @@ -505,7 +505,7 @@ namespace const char* status_str = 0; - spot::tgba_digraph_ptr res = 0; + spot::twa_graph_ptr res = 0; if (timed_out) { // This is not considered to be a global error. @@ -696,8 +696,8 @@ namespace }; static bool - check_empty_prod(const spot::const_tgba_digraph_ptr& aut_i, - const spot::const_tgba_digraph_ptr& aut_j, + check_empty_prod(const spot::const_twa_graph_ptr& aut_i, + const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j, bool icomp, bool jcomp) { auto prod = spot::product(aut_i, aut_j); @@ -1022,12 +1022,12 @@ namespace // These store the result of the translation of the positive and // negative formulas. size_t m = translators.size(); - std::vector pos(m); - std::vector neg(m); + std::vector pos(m); + std::vector neg(m); // These store the complement of the above results, when we can // compute it easily. - std::vector comp_pos(m); - std::vector comp_neg(m); + std::vector comp_pos(m); + std::vector comp_neg(m); unsigned n = vstats.size(); @@ -1213,9 +1213,9 @@ namespace << " edges\n"; // Products of the state space with the positive automata. - std::vector pos_prod(m); + std::vector pos_prod(m); // Products of the state space with the negative automata. - std::vector neg_prod(m); + std::vector neg_prod(m); // Associated SCC maps. std::vector pos_map(m); std::vector neg_map(m); diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index 3f1d114ff..2366bb694 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -126,7 +126,7 @@ namespace { } - spot::tgba_digraph_ptr + spot::twa_graph_ptr translate(unsigned int translator_num, bool& problem, double& duration) { output.reset(translator_num); @@ -144,7 +144,7 @@ namespace int es = exec_with_timeout(cmd.c_str()); duration = sw.stop(); - spot::tgba_digraph_ptr res = nullptr; + spot::twa_graph_ptr res = nullptr; if (timed_out) { problem = false; // A timeout is considered benign diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index c00c7d0d9..ee788da20 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -124,7 +124,7 @@ ARGMATCH_VERIFY(acc_args, acc_types); static acc_type opt_acc = acc_buchi; -typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; +typedef spot::twa_graph::graph_t::trans_storage_t tr_t; typedef std::set> unique_aut_t; static spot::ltl::atomic_prop_set aprops; static bool ap_count_given = false; @@ -307,7 +307,7 @@ main(int argc, char** argv) if (opt_uniq) { auto tmp = spot::canonicalize - (make_tgba_digraph(aut, spot::twa::prop_set::all())); + (make_twa_graph(aut, spot::twa::prop_set::all())); std::vector trans(tmp->transition_vector().begin() + 1, tmp->transition_vector().end()); if (!opt_uniq->emplace(trans).second) diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index effc454c7..4daa8ca9d 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -49,7 +49,7 @@ namespace spot // This function is defined in nra2nba.cc, and used only here. SPOT_LOCAL - tgba_digraph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, + twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, const const_tgba_ptr& aut); namespace @@ -217,7 +217,7 @@ namespace spot const std::vector& realizable): tgba_reachable_iterator_depth_first(a->aut), in_(a), - out_(make_tgba_digraph(a->aut->get_dict())), + out_(make_twa_graph(a->aut->get_dict())), final_(final), num_states_(a->aut->num_states()), sm_(sm), @@ -231,7 +231,7 @@ namespace spot } - tgba_digraph_ptr + twa_graph_ptr result() { return out_; @@ -291,7 +291,7 @@ namespace spot protected: const const_dstar_aut_ptr& in_; - tgba_digraph_ptr out_; + twa_graph_ptr out_; const state_set& final_; size_t num_states_; acc_cond::mark_t acc_; @@ -302,7 +302,7 @@ namespace spot } - tgba_digraph_ptr dra_to_ba(const const_dstar_aut_ptr& dra, bool* dba) + twa_graph_ptr dra_to_ba(const const_dstar_aut_ptr& dra, bool* dba) { assert(dra->type == Rabin); diff --git a/src/dstarparse/dstar2tgba.cc b/src/dstarparse/dstar2tgba.cc index 849c509b0..bdb1ec80a 100644 --- a/src/dstarparse/dstar2tgba.cc +++ b/src/dstarparse/dstar2tgba.cc @@ -21,7 +21,7 @@ namespace spot { - tgba_digraph_ptr + twa_graph_ptr dstar_to_tgba(const const_dstar_aut_ptr& daut) { switch (daut->type) diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy index 07332c546..afb8a5d23 100644 --- a/src/dstarparse/dstarparse.yy +++ b/src/dstarparse/dstarparse.yy @@ -330,7 +330,7 @@ namespace spot } result_ r; r.d = std::make_shared(); - r.d->aut = make_tgba_digraph(dict); + r.d->aut = make_twa_graph(dict); r.d->accsets = 0; r.env = &env; dstaryy::parser parser(error_list, r); diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc index fa1900866..2aab4b54a 100644 --- a/src/dstarparse/nra2nba.cc +++ b/src/dstarparse/nra2nba.cc @@ -40,7 +40,7 @@ namespace spot // makes its possible to mask AUT, as needed in dra_to_ba(). nra_to_nba_worker(const const_dstar_aut_ptr& a, const_tgba_ptr aut): tgba_reachable_iterator_depth_first(aut), - out_(make_tgba_digraph(aut->get_dict())), + out_(make_twa_graph(aut->get_dict())), d_(a), num_states_(a->aut->num_states()) { @@ -55,7 +55,7 @@ namespace spot i->destroy(); } - tgba_digraph_ptr + twa_graph_ptr result() { return out_; @@ -105,7 +105,7 @@ namespace spot } protected: - tgba_digraph_ptr out_; + twa_graph_ptr out_; const_dstar_aut_ptr d_; size_t num_states_; }; @@ -115,7 +115,7 @@ 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_digraph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, + twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, const const_tgba_ptr& aut) { assert(nra->type == Rabin); @@ -124,7 +124,7 @@ namespace spot return scc_filter_states(w.result()); } - tgba_digraph_ptr nra_to_nba(const const_dstar_aut_ptr& nra) + twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra) { return nra_to_nba(nra, nra->aut); } diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index a667f1e49..dca78234f 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -98,11 +98,11 @@ namespace spot } - tgba_digraph_ptr nsa_to_tgba(const const_dstar_aut_ptr& nsa) + twa_graph_ptr nsa_to_tgba(const const_dstar_aut_ptr& nsa) { assert(nsa->type == Streett); auto a = nsa->aut; - auto res = make_tgba_digraph(a->get_dict()); + auto res = make_twa_graph(a->get_dict()); res->copy_ap_of(a); // Create accpair_count acceptance sets for the output. diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh index 5c8dd4c6d..18440120c 100644 --- a/src/dstarparse/public.hh +++ b/src/dstarparse/public.hh @@ -46,7 +46,7 @@ namespace spot { // Transition structure of the automaton. // This is encoded as a TGBA without acceptance condition. - tgba_digraph_ptr aut; + twa_graph_ptr aut; /// Type of the acceptance. dstar_type type; /// Number of acceptance pairs. @@ -68,7 +68,7 @@ namespace spot typedef std::shared_ptr dstar_aut_ptr; typedef std::shared_ptr const_dstar_aut_ptr; - /// \brief Build a spot::tgba_digraph from ltl2dstar's output. + /// \brief Build a spot::twa_graph from ltl2dstar's output. /// \param filename The name of the file to parse. /// \param error_list A list that will be filled with /// parse errors that occured during parsing. @@ -106,14 +106,14 @@ namespace spot /// \brief Convert a non-deterministic Rabin automaton into a /// non-deterministic Büchi automaton. - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& 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_digraph_ptr + SPOT_API twa_graph_ptr nra_to_nba(const const_dstar_aut_ptr& nra, const state_set* ignore); /// \brief Convert a deterministic Rabin automaton into a @@ -132,18 +132,18 @@ namespace spot /// If the optional \a dba_output argument is non-null, the /// pointed Boolean will be updated to indicate whether the /// returned Büchi automaton is deterministic. - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr dra_to_ba(const const_dstar_aut_ptr& dra, bool* dba_output = 0); /// \brief Convert a non-deterministic Streett automaton into a /// non-deterministic tgba. - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr nsa_to_tgba(const const_dstar_aut_ptr& nra); /// \brief Convert a Rabin or Streett automaton into a TGBA. /// /// This function calls dra_to_ba() or nsa_to_tgba(). - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr dstar_to_tgba(const const_dstar_aut_ptr& dstar); /// @} diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/tgbagraph.cc index e5fe33f9a..a65465491 100644 --- a/src/graphtest/tgbagraph.cc +++ b/src/graphtest/tgbagraph.cc @@ -29,7 +29,7 @@ void f1() auto& e = spot::ltl::default_environment::instance(); - auto tg = make_tgba_digraph(d); + auto tg = make_twa_graph(d); auto* f1 = e.require("p1"); auto* f2 = e.require("p2"); diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index e538b8c0c..9ee323967 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -49,7 +49,7 @@ typedef std::map formula_cache; typedef std::pair pair; - typedef typename spot::tgba_digraph::namer::type named_tgba_t; + typedef typename spot::twa_graph::namer::type named_tgba_t; // Note: because this parser is meant to be used on a stream of // automata, it tries hard to recover from errors, so that we get a @@ -1682,7 +1682,7 @@ namespace spot restart: result_ r; r.h = std::make_shared(); - r.h->aut = make_tgba_digraph(dict); + r.h->aut = make_twa_graph(dict); r.env = &env; hoayy::parser parser(error_list, r, last_loc); static bool env_debug = !!getenv("SPOT_DEBUG_PARSER"); @@ -1717,7 +1717,7 @@ namespace spot return r.h; }; - tgba_digraph_ptr + twa_graph_ptr hoa_stream_parser::parse_strict(const bdd_dict_ptr& dict, ltl::environment& env, bool debug) diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index f65beafad..cf5d56ded 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -49,7 +49,7 @@ namespace spot { // Transition structure of the automaton. // This is encoded as a TGBA without acceptance condition. - tgba_digraph_ptr aut; + twa_graph_ptr aut; bool aborted = false; spot::location loc; }; @@ -75,13 +75,13 @@ namespace spot ltl::default_environment::instance(), bool debug = false); // Raises a parse_error on any syntax error - tgba_digraph_ptr parse_strict(const bdd_dict_ptr& dict, + twa_graph_ptr parse_strict(const bdd_dict_ptr& dict, ltl::environment& env = ltl::default_environment::instance(), bool debug = false); }; - /// \brief Build a spot::tgba_digraph from a HOA file or a neverclaim. + /// \brief Build a spot::twa_graph from a HOA file or a neverclaim. /// \param filename The name of the file to parse. /// \param error_list A list that will be filled with /// parse errors that occured during parsing. diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh index 000ed413d..991eb5a49 100644 --- a/src/ltlvisit/contain.hh +++ b/src/ltlvisit/contain.hh @@ -36,7 +36,7 @@ namespace spot { struct record_ { - const_tgba_digraph_ptr translation; + const_twa_graph_ptr translation; typedef std::map incomp_map; incomp_map incompatible; }; diff --git a/src/ltlvisit/exclusive.cc b/src/ltlvisit/exclusive.cc index 9ca574fc4..ba832679a 100644 --- a/src/ltlvisit/exclusive.cc +++ b/src/ltlvisit/exclusive.cc @@ -161,7 +161,7 @@ namespace spot return ltl::multop::instance(ltl::multop::And, f->clone(), c); } - tgba_digraph_ptr exclusive_ap::constrain(const_tgba_digraph_ptr aut, + twa_graph_ptr exclusive_ap::constrain(const_twa_graph_ptr aut, bool simplify_guards) const { // Compute the support of the automaton. @@ -194,7 +194,7 @@ namespace spot restrict &= group[j] | group[k]; } - tgba_digraph_ptr res = make_tgba_digraph(aut->get_dict()); + twa_graph_ptr res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); res->prop_copy(aut, { true, true, true, true }); res->copy_acceptance_of(aut); diff --git a/src/ltlvisit/exclusive.hh b/src/ltlvisit/exclusive.hh index 33e1c72c1..3aa94bfd5 100644 --- a/src/ltlvisit/exclusive.hh +++ b/src/ltlvisit/exclusive.hh @@ -42,7 +42,7 @@ namespace spot } const ltl::formula* constrain(const ltl::formula* f) const; - tgba_digraph_ptr constrain(const_tgba_digraph_ptr aut, + twa_graph_ptr constrain(const_twa_graph_ptr aut, bool simplify_guards = false) const; }; } diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh index 37e6500b6..4962fef53 100644 --- a/src/priv/accmap.hh +++ b/src/priv/accmap.hh @@ -30,9 +30,9 @@ namespace spot { protected: bdd_dict_ptr dict_; - tgba_digraph_ptr aut_; + twa_graph_ptr aut_; - acc_mapper_common(const tgba_digraph_ptr& aut) + acc_mapper_common(const twa_graph_ptr& aut) : dict_(aut->get_dict()), aut_(aut) { } @@ -43,7 +43,7 @@ namespace spot std::unordered_map map_; public: - acc_mapper_string(const tgba_digraph_ptr& aut) + acc_mapper_string(const twa_graph_ptr& aut) : acc_mapper_common(aut) { } @@ -73,7 +73,7 @@ namespace spot class acc_mapper_consecutive_int: public acc_mapper_common { public: - acc_mapper_consecutive_int(const tgba_digraph_ptr& aut, unsigned count) + acc_mapper_consecutive_int(const twa_graph_ptr& aut, unsigned count) : acc_mapper_common(aut) { std::vector vmap(count); @@ -97,7 +97,7 @@ namespace spot std::map map_; public: - acc_mapper_int(const tgba_digraph_ptr& aut, unsigned count) + acc_mapper_int(const twa_graph_ptr& aut, unsigned count) : acc_mapper_consecutive_int(aut, count), used_(0) { } diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index fb1123264..74a81b5f3 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -76,7 +76,7 @@ namespace spot // automaton static void build_result(const const_ta_ptr& a, std::list& sets, - tgba_digraph_ptr result_tgba, const ta_explicit_ptr& result) + twa_graph_ptr result_tgba, const ta_explicit_ptr& result) { // For each set, create a state in the tgbaulting automaton. // For a state s, state_num[s] is the number of the state in the minimal @@ -508,7 +508,7 @@ namespace spot minimize_ta(const const_ta_ptr& ta_) { - auto tgba = make_tgba_digraph(ta_->get_dict()); + auto tgba = make_twa_graph(ta_->get_dict()); auto res = make_ta_explicit(tgba, ta_->acc().num_sets(), 0); partition_t partition = build_partition(ta_); @@ -528,7 +528,7 @@ namespace spot minimize_tgta(const const_tgta_explicit_ptr& tgta_) { - auto tgba = make_tgba_digraph(tgta_->get_dict()); + auto tgba = make_twa_graph(tgta_->get_dict()); auto res = make_tgta_explicit(tgba, tgta_->acc().num_sets(), 0); auto ta = tgta_->get_ta(); diff --git a/src/tgba/fwd.hh b/src/tgba/fwd.hh index b8d32b844..c3b588d0b 100644 --- a/src/tgba/fwd.hh +++ b/src/tgba/fwd.hh @@ -27,9 +27,9 @@ namespace spot typedef std::shared_ptr tgba_ptr; typedef std::shared_ptr const_tgba_ptr; - class tgba_digraph; - typedef std::shared_ptr const_tgba_digraph_ptr; - typedef std::shared_ptr tgba_digraph_ptr; + class twa_graph; + typedef std::shared_ptr const_twa_graph_ptr; + typedef std::shared_ptr twa_graph_ptr; class tgba_product; typedef std::shared_ptr const_tgba_product_ptr; diff --git a/src/tgba/tgba.cc b/src/tgba/tgba.cc index d34066f8a..bcdd2c31b 100644 --- a/src/tgba/tgba.cc +++ b/src/tgba/tgba.cc @@ -82,9 +82,9 @@ namespace spot auto a = shared_from_this(); if (a->acc().uses_fin_acceptance()) { - auto aa = std::dynamic_pointer_cast(a); + auto aa = std::dynamic_pointer_cast(a); if (!aa) - aa = make_tgba_digraph(a, prop_set::all()); + aa = make_twa_graph(a, prop_set::all()); a = remove_fin(aa); } return !couvreur99(a)->check(); diff --git a/src/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc index 8c5900a14..da487a460 100644 --- a/src/tgba/tgbagraph.cc +++ b/src/tgba/tgbagraph.cc @@ -23,7 +23,7 @@ namespace spot { - void tgba_digraph::merge_transitions() + void twa_graph::merge_transitions() { g_.remove_dead_transitions_(); @@ -130,7 +130,7 @@ namespace spot g_.chain_transitions_(); } - void tgba_digraph::purge_unreachable_states() + void twa_graph::purge_unreachable_states() { unsigned num_states = g_.num_states(); if (SPOT_UNLIKELY(num_states == 0)) @@ -173,7 +173,7 @@ namespace spot g_.defrag_states(std::move(todo), current); } - void tgba_digraph::purge_dead_states() + void twa_graph::purge_dead_states() { unsigned num_states = g_.num_states(); if (num_states == 0) diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 695bbd84f..f3bf0808d 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -105,7 +105,7 @@ namespace spot template - class SPOT_API tgba_digraph_succ_iterator final: + class SPOT_API twa_graph_succ_iterator final: public tgba_succ_iterator { private: @@ -116,7 +116,7 @@ namespace spot transition p_; public: - tgba_digraph_succ_iterator(const Graph* g, transition t) + twa_graph_succ_iterator(const Graph* g, transition t) : g_(g), t_(t) { } @@ -169,7 +169,7 @@ namespace spot }; - class SPOT_API tgba_digraph final: public twa + class SPOT_API twa_graph final: public twa { public: typedef digraph graph_t; @@ -180,13 +180,13 @@ namespace spot mutable unsigned init_number_; public: - tgba_digraph(const bdd_dict_ptr& dict) + twa_graph(const bdd_dict_ptr& dict) : twa(dict), init_number_(0) { } - explicit tgba_digraph(const const_tgba_digraph_ptr& other, prop_set p) + explicit twa_graph(const const_twa_graph_ptr& other, prop_set p) : twa(other->get_dict()), g_(other->g_), init_number_(other->init_number_) { @@ -195,7 +195,7 @@ namespace spot prop_copy(other, p); } - virtual ~tgba_digraph() + virtual ~twa_graph() { get_dict()->unregister_all_my_variables(this); // Prevent this state from being destroyed by ~twa(), @@ -278,12 +278,12 @@ namespace spot if (this->iter_cache_) { auto it = - down_cast*>(this->iter_cache_); + down_cast*>(this->iter_cache_); it->recycle(s->succ); this->iter_cache_ = nullptr; return it; } - return new tgba_digraph_succ_iterator(&g_, s->succ); + return new twa_graph_succ_iterator(&g_, s->succ); } graph_t::state @@ -314,7 +314,7 @@ namespace spot tgba_graph_trans_data& trans_data(const tgba_succ_iterator* it) { - auto* i = down_cast*>(it); + auto* i = down_cast*>(it); return g_.trans_data(i->pos()); } @@ -325,7 +325,7 @@ namespace spot const tgba_graph_trans_data& trans_data(const tgba_succ_iterator* it) const { - auto* i = down_cast*>(it); + auto* i = down_cast*>(it); return g_.trans_data(i->pos()); } @@ -336,7 +336,7 @@ namespace spot trans_storage_t& trans_storage(const tgba_succ_iterator* it) { - auto* i = down_cast*>(it); + auto* i = down_cast*>(it); return g_.trans_storage(i->pos()); } @@ -348,7 +348,7 @@ namespace spot const trans_storage_t trans_storage(const tgba_succ_iterator* it) const { - auto* i = down_cast*>(it); + auto* i = down_cast*>(it); return g_.trans_storage(i->pos()); } @@ -440,7 +440,7 @@ namespace spot return state_is_accepting(state_number(s)); } - bool operator==(const tgba_digraph& aut) const + bool operator==(const twa_graph& aut) const { if (num_states() != aut.num_states() || num_transitions() != aut.num_transitions() || @@ -453,29 +453,29 @@ namespace spot } }; - inline tgba_digraph_ptr make_tgba_digraph(const bdd_dict_ptr& dict) + inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict) { - return std::make_shared(dict); + return std::make_shared(dict); } - inline tgba_digraph_ptr make_tgba_digraph(const tgba_digraph_ptr& aut, + inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut, twa::prop_set p) { - return std::make_shared(aut, p); + return std::make_shared(aut, p); } - inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_digraph_ptr& aut, + inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut, twa::prop_set p) { - return std::make_shared(aut, p); + return std::make_shared(aut, p); } - inline tgba_digraph_ptr make_tgba_digraph(const const_tgba_ptr& aut, + inline twa_graph_ptr make_twa_graph(const const_tgba_ptr& aut, twa::prop_set p) { - auto a = std::dynamic_pointer_cast(aut); + auto a = std::dynamic_pointer_cast(aut); if (a) - return std::make_shared(a, p); + return std::make_shared(a, p); else return tgba_dupexp_dfs(aut, p); } diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index e3f85669f..e190a223c 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -53,7 +53,7 @@ namespace spot /// \brief Automaton with Safra's tree as states. struct safra_tree_automaton { - safra_tree_automaton(const const_tgba_digraph_ptr& sba); + safra_tree_automaton(const const_twa_graph_ptr& sba); ~safra_tree_automaton(); typedef std::map transition_list; typedef @@ -66,14 +66,14 @@ namespace spot int get_nb_acceptance_pairs() const; safra_tree* get_initial_state() const; void set_initial_state(safra_tree* s); - const const_tgba_digraph_ptr& get_sba(void) const + const const_twa_graph_ptr& get_sba(void) const { return a_; } private: mutable int max_nb_pairs_; safra_tree* initial_state; - const_tgba_digraph_ptr a_; + const_twa_graph_ptr a_; }; /// \brief A Safra tree, used as state during the determinization @@ -111,7 +111,7 @@ namespace spot int max_name() const; // Operations to get successors of a tree. - safra_tree* branch_accepting(const tgba_digraph& a); + safra_tree* branch_accepting(const twa_graph& a); safra_tree* succ_create(const bdd& condition, cache_t& cache_transition); safra_tree* normalize_siblings(); @@ -313,7 +313,7 @@ namespace spot /// is inserted with the set of all accepting states of \c nodes /// as label and an unused name. safra_tree* - safra_tree::branch_accepting(const tgba_digraph& a) + safra_tree::branch_accepting(const twa_graph& a) { for (auto c: children) c->branch_accepting(a); @@ -568,12 +568,12 @@ namespace spot { public: static safra_tree_automaton* - create_safra_automaton(const const_tgba_digraph_ptr& a); + create_safra_automaton(const const_twa_graph_ptr& a); private: typedef std::set atomic_list_t; typedef std::set conjunction_list_t; static void retrieve_atomics(const safra_tree* node, - tgba_digraph_ptr sba_aut, + twa_graph_ptr sba_aut, safra_tree::cache_t& cache, atomic_list_t& atomic_list); static void set_atomic_list(atomic_list_t& list, bdd condition); @@ -584,7 +584,7 @@ namespace spot /// \brief The body of Safra's construction. safra_tree_automaton* safra_determinisation::create_safra_automaton - (const const_tgba_digraph_ptr& a) + (const const_twa_graph_ptr& a) { // initialization. auto sba_aut = degeneralize(a); @@ -664,7 +664,7 @@ namespace spot /// of the states in the label of the node. void safra_determinisation::retrieve_atomics(const safra_tree* node, - tgba_digraph_ptr sba_aut, + twa_graph_ptr sba_aut, safra_tree::cache_t& cache, atomic_list_t& atomic_list) { @@ -1031,7 +1031,7 @@ namespace spot // safra_tree_automaton //////////////////////// - safra_tree_automaton::safra_tree_automaton(const const_tgba_digraph_ptr& a) + safra_tree_automaton::safra_tree_automaton(const const_twa_graph_ptr& a) : max_nb_pairs_(-1), initial_state(0), a_(a) { a->get_dict()->register_all_variables_of(a, this); @@ -1073,7 +1073,7 @@ namespace spot // tgba_safra_complement ////////////////////////// - tgba_safra_complement::tgba_safra_complement(const const_tgba_digraph_ptr& a) + tgba_safra_complement::tgba_safra_complement(const const_twa_graph_ptr& a) : twa(a->get_dict()), automaton_(a), safra_(safra_determinisation::create_safra_automaton(a)) { diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh index a05311ef8..c47cf04e6 100644 --- a/src/tgba/tgbasafracomplement.hh +++ b/src/tgba/tgbasafracomplement.hh @@ -49,7 +49,7 @@ namespace spot class SPOT_API tgba_safra_complement : public twa { public: - tgba_safra_complement(const const_tgba_digraph_ptr& a); + tgba_safra_complement(const const_twa_graph_ptr& a); virtual ~tgba_safra_complement(); // tgba interface. @@ -66,7 +66,7 @@ namespace spot protected: virtual bdd compute_support_conditions(const state* state) const; private: - const_tgba_digraph_ptr automaton_; + const_twa_graph_ptr automaton_; void* safra_; #if TRANSFORM_TO_TBA acc_cond::mark_t the_acceptance_cond_; @@ -81,7 +81,7 @@ namespace spot typedef std::shared_ptr const_tgba_safra_complement_ptr; inline tgba_safra_complement_ptr - make_safra_complement(const const_tgba_digraph_ptr& a) + make_safra_complement(const const_twa_graph_ptr& a) { return std::make_shared(a); } diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc index 69e72907d..db391ec1f 100644 --- a/src/tgbaalgos/are_isomorphic.cc +++ b/src/tgbaalgos/are_isomorphic.cc @@ -29,7 +29,7 @@ namespace { - typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; + typedef spot::twa_graph::graph_t::trans_storage_t tr_t; bool tr_t_less_than(const tr_t& t1, const tr_t& t2) { @@ -43,8 +43,8 @@ namespace } bool - are_isomorphic_det(const spot::const_tgba_digraph_ptr aut1, - const spot::const_tgba_digraph_ptr aut2) + are_isomorphic_det(const spot::const_twa_graph_ptr aut1, + const spot::const_twa_graph_ptr aut2) { typedef std::pair state_pair_t; std::queue workqueue; @@ -97,8 +97,8 @@ namespace } bool - trivially_different(const spot::const_tgba_digraph_ptr aut1, - const spot::const_tgba_digraph_ptr aut2) + trivially_different(const spot::const_twa_graph_ptr aut1, + const spot::const_twa_graph_ptr aut2) { return aut1->num_states() != aut2->num_states() || aut1->num_transitions() != aut2->num_transitions() || @@ -110,9 +110,9 @@ namespace namespace spot { - isomorphism_checker::isomorphism_checker(const const_tgba_digraph_ptr ref) + isomorphism_checker::isomorphism_checker(const const_twa_graph_ptr ref) { - ref_ = make_tgba_digraph(ref, twa::prop_set::all()); + ref_ = make_twa_graph(ref, twa::prop_set::all()); ref_deterministic_ = ref_->is_deterministic(); if (!ref_deterministic_) { @@ -123,7 +123,7 @@ namespace spot } bool - isomorphism_checker::is_isomorphic(const const_tgba_digraph_ptr aut) + isomorphism_checker::is_isomorphic(const const_twa_graph_ptr aut) { if (trivially_different(ref_, aut)) return false; @@ -144,7 +144,7 @@ namespace spot } } - auto tmp = make_tgba_digraph(aut, twa::prop_set::all()); + auto tmp = make_twa_graph(aut, twa::prop_set::all()); spot::canonicalize(tmp); return *tmp == *ref_; } diff --git a/src/tgbaalgos/are_isomorphic.hh b/src/tgbaalgos/are_isomorphic.hh index f0d6011b8..67dedcb0f 100644 --- a/src/tgbaalgos/are_isomorphic.hh +++ b/src/tgbaalgos/are_isomorphic.hh @@ -28,7 +28,7 @@ namespace spot class SPOT_API isomorphism_checker { public: - isomorphism_checker(const const_tgba_digraph_ptr ref); + isomorphism_checker(const const_twa_graph_ptr ref); /// \ingroup tgba_misc /// \brief Check whether an automaton is isomorphic to the one passed to @@ -43,12 +43,12 @@ namespace spot /// canonicalize(aut1) == canonicalize(aut2), but is_isomorphic can do some /// optimizations in some cases. bool - is_isomorphic(const const_tgba_digraph_ptr aut); + is_isomorphic(const const_twa_graph_ptr aut); private: - tgba_digraph_ptr ref_; + twa_graph_ptr ref_; bool ref_deterministic_ = false; unsigned nondet_states_ = 0; - std::vector reftrans_; + std::vector reftrans_; }; } diff --git a/src/tgbaalgos/canonicalize.cc b/src/tgbaalgos/canonicalize.cc index 868fd1df8..a535c038c 100644 --- a/src/tgbaalgos/canonicalize.cc +++ b/src/tgbaalgos/canonicalize.cc @@ -24,7 +24,7 @@ namespace { - typedef std::pair + typedef std::pair trans_sig_t; struct signature_t @@ -45,7 +45,7 @@ namespace typedef std::map> sig2states_t; static sig2states_t - sig_to_states(spot::tgba_digraph_ptr aut, std::vector& state2class) + sig_to_states(spot::twa_graph_ptr aut, std::vector& state2class) { std::vector signature(aut->num_states(), signature_t()); @@ -70,8 +70,8 @@ namespace namespace spot { - tgba_digraph_ptr - canonicalize(tgba_digraph_ptr aut) + twa_graph_ptr + canonicalize(twa_graph_ptr aut) { std::vector state2class(aut->num_states(), 0); state2class[aut->get_init_state_number()] = 1; diff --git a/src/tgbaalgos/canonicalize.hh b/src/tgbaalgos/canonicalize.hh index 4262321f8..b1ab59176 100644 --- a/src/tgbaalgos/canonicalize.hh +++ b/src/tgbaalgos/canonicalize.hh @@ -26,5 +26,5 @@ namespace spot /// \ingroup tgba_misc /// \brief Reorder the states and transitions of aut in a way that will be the /// same for every isomorphic automata. - SPOT_API tgba_digraph_ptr canonicalize(tgba_digraph_ptr aut); + SPOT_API twa_graph_ptr canonicalize(twa_graph_ptr aut); } diff --git a/src/tgbaalgos/cleanacc.cc b/src/tgbaalgos/cleanacc.cc index 34fd1498e..758afe2c3 100644 --- a/src/tgbaalgos/cleanacc.cc +++ b/src/tgbaalgos/cleanacc.cc @@ -21,7 +21,7 @@ namespace spot { - tgba_digraph_ptr cleanup_acceptance_here(tgba_digraph_ptr aut) + twa_graph_ptr cleanup_acceptance_here(twa_graph_ptr aut) { auto& acc = aut->acc(); if (acc.num_sets() == 0) @@ -53,9 +53,9 @@ namespace spot return cleanup_acceptance_here(aut); } - tgba_digraph_ptr cleanup_acceptance(const_tgba_digraph_ptr aut) + twa_graph_ptr cleanup_acceptance(const_twa_graph_ptr aut) { - return cleanup_acceptance_here(make_tgba_digraph(aut, + return cleanup_acceptance_here(make_twa_graph(aut, twa::prop_set::all())); } diff --git a/src/tgbaalgos/cleanacc.hh b/src/tgbaalgos/cleanacc.hh index 148ab8c34..bf76f7e2c 100644 --- a/src/tgbaalgos/cleanacc.hh +++ b/src/tgbaalgos/cleanacc.hh @@ -25,10 +25,10 @@ namespace spot { /// \brief Remove useless acceptance sets /// @{ - SPOT_API tgba_digraph_ptr - cleanup_acceptance_here(tgba_digraph_ptr aut); + SPOT_API twa_graph_ptr + cleanup_acceptance_here(twa_graph_ptr aut); - SPOT_API tgba_digraph_ptr - cleanup_acceptance(const_tgba_digraph_ptr aut); + SPOT_API twa_graph_ptr + cleanup_acceptance(const_twa_graph_ptr aut); /// @} } diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index 54e0b73e7..b10be5d7c 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -21,7 +21,7 @@ namespace spot { - unsigned tgba_complete_here(tgba_digraph_ptr aut) + unsigned tgba_complete_here(twa_graph_ptr aut) { unsigned n = aut->num_states(); unsigned sink = -1U; @@ -117,9 +117,9 @@ namespace spot return sink; } - tgba_digraph_ptr tgba_complete(const const_tgba_ptr& aut) + twa_graph_ptr tgba_complete(const const_tgba_ptr& aut) { - auto res = make_tgba_digraph(aut, { + auto res = make_twa_graph(aut, { true, // state based true, // inherently_weak true, // deterministic diff --git a/src/tgbaalgos/complete.hh b/src/tgbaalgos/complete.hh index 95cde2732..7d18804e2 100644 --- a/src/tgbaalgos/complete.hh +++ b/src/tgbaalgos/complete.hh @@ -23,17 +23,17 @@ namespace spot { - /// \brief Complete a tgba_digraph in place. + /// \brief Complete a twa_graph in place. /// /// If the tgba has no acceptance set, one will be added. The /// returned value is the number of the sink state (it can be a new /// state added for completion, or an existing non-accepting state /// that has been reused as sink state because it had not outgoing /// transitions apart from self-loops.) - SPOT_API unsigned tgba_complete_here(tgba_digraph_ptr aut); + SPOT_API unsigned tgba_complete_here(twa_graph_ptr aut); /// \brief Clone a tgba and complete it. /// /// If the tgba has no acceptance set, one will be added. - SPOT_API tgba_digraph_ptr tgba_complete(const const_tgba_ptr& aut); + SPOT_API twa_graph_ptr tgba_complete(const const_tgba_ptr& aut); } diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index a60ccac8c..07e4aef39 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -211,7 +211,7 @@ namespace spot typedef std::deque pair_queue; static - tgba_digraph_ptr + twa_graph_ptr susp_prod(const const_tgba_ptr& left, const ltl::formula* f, bdd v) { bdd_dict_ptr dict = left->get_dict(); @@ -219,7 +219,7 @@ namespace spot iterated_simulations(scc_filter(ltl_to_tgba_fm(f, dict, true, true), false)); - tgba_digraph_ptr res = make_tgba_digraph(dict); + twa_graph_ptr res = make_twa_graph(dict); dict->register_all_variables_of(left, res); dict->register_all_variables_of(right, res); dict->unregister_variable(bdd_var(v), res); @@ -321,7 +321,7 @@ namespace spot } - tgba_digraph_ptr + twa_graph_ptr compsusp(const ltl::formula* f, const bdd_dict_ptr& dict, bool no_wdba, bool no_simulation, bool early_susp, bool no_susp_product, bool wdba_smaller, @@ -333,13 +333,13 @@ namespace spot const ltl::formula* g = v.recurse(f); // Translate the patched formula, and remove useless SCCs. - tgba_digraph_ptr res = + twa_graph_ptr res = scc_filter(ltl_to_tgba_fm(g, dict, true, true, false, false, 0, 0), false); if (!no_wdba) { - tgba_digraph_ptr min = minimize_obligation(res, g, 0, wdba_smaller); + twa_graph_ptr min = minimize_obligation(res, g, 0, wdba_smaller); if (min != res) { res = min; diff --git a/src/tgbaalgos/compsusp.hh b/src/tgbaalgos/compsusp.hh index c4aea6a4b..eb3fcd42e 100644 --- a/src/tgbaalgos/compsusp.hh +++ b/src/tgbaalgos/compsusp.hh @@ -48,7 +48,7 @@ namespace spot /// This interface is subject to change, and clients aiming for /// long-term stability should better use the services of the /// spot::translator class instead. - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr compsusp(const ltl::formula* f, const bdd_dict_ptr& dict, bool no_wdba = false, bool no_simulation = false, bool early_susp = false, bool no_susp_product = false, diff --git a/src/tgbaalgos/cycles.hh b/src/tgbaalgos/cycles.hh index 74391fb2b..fc18482cb 100644 --- a/src/tgbaalgos/cycles.hh +++ b/src/tgbaalgos/cycles.hh @@ -100,7 +100,7 @@ namespace spot }; // The automaton we are working on. - const_tgba_digraph_ptr aut_; + const_twa_graph_ptr aut_; // Store the state_info for all visited states. std::vector info_; // The SCC map built for aut_. diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index d6091b900..ad75f091e 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -59,7 +59,7 @@ namespace spot // SCC -- we do not care about the other) of some state. class outgoing_acc { - const_tgba_digraph_ptr a_; + const_twa_graph_ptr a_; typedef std::tuple cache_entry; @@ -94,7 +94,7 @@ namespace spot } public: - outgoing_acc(const const_tgba_digraph_ptr& a, const scc_info* sm): + outgoing_acc(const const_twa_graph_ptr& a, const scc_info* sm): a_(a), cache_(a->num_states()), sm_(sm) { unsigned n = a->num_states(); @@ -189,8 +189,8 @@ namespace spot }; template - tgba_digraph_ptr - degeneralize_aux(const const_tgba_digraph_ptr& a, bool use_z_lvl, + twa_graph_ptr + degeneralize_aux(const const_twa_graph_ptr& a, bool use_z_lvl, bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels, bool ignaccsl) { @@ -203,7 +203,7 @@ namespace spot bdd_dict_ptr dict = a->get_dict(); // The result automaton is an SBA. - auto res = make_tgba_digraph(dict); + auto res = make_twa_graph(dict); res->copy_ap_of(a); res->set_buchi(); if (want_sba) @@ -551,29 +551,29 @@ namespace spot } } - tgba_digraph_ptr - degeneralize(const const_tgba_digraph_ptr& a, + twa_graph_ptr + degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl, bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels, bool ignaccsl) { // If this already a degeneralized digraph, there is nothing we // can improve. if (a->is_sba()) - return std::const_pointer_cast(a); + return std::const_pointer_cast(a); return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, use_lvl_cache, skip_levels, ignaccsl); } - tgba_digraph_ptr - degeneralize_tba(const const_tgba_digraph_ptr& a, + twa_graph_ptr + degeneralize_tba(const const_twa_graph_ptr& a, bool use_z_lvl, bool use_cust_acc_orders, int use_lvl_cache, bool skip_levels, bool ignaccsl) { // If this already a degeneralized digraph, there is nothing we // can improve. if (a->acc().is_buchi()) - return std::const_pointer_cast(a); + return std::const_pointer_cast(a); return degeneralize_aux(a, use_z_lvl, use_cust_acc_orders, use_lvl_cache, skip_levels, ignaccsl); diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index 7f01a6bb5..c0c1541d3 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -49,15 +49,15 @@ namespace spot /// The degeneralize_tba() variant produce a degeneralized automaton /// with transition-based acceptance. /// \@{ - SPOT_API tgba_digraph_ptr - degeneralize(const const_tgba_digraph_ptr& a, bool use_z_lvl = true, + SPOT_API twa_graph_ptr + degeneralize(const const_twa_graph_ptr& a, bool use_z_lvl = true, bool use_cust_acc_orders = false, int use_lvl_cache = 1, bool skip_levels = true, bool ignaccsl = false); - SPOT_API tgba_digraph_ptr - degeneralize_tba(const const_tgba_digraph_ptr& a, bool use_z_lvl = true, + SPOT_API twa_graph_ptr + degeneralize_tba(const const_twa_graph_ptr& a, bool use_z_lvl = true, bool use_cust_acc_orders = false, int use_lvl_cache = 1, bool skip_levels = true, diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 7d0f48620..2f0d85451 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -52,7 +52,7 @@ namespace spot bool mark_states_ = false; bool opt_scc_ = false; bool opt_html_labels_ = false; - const_tgba_digraph_ptr aut_; + const_twa_graph_ptr aut_; std::vector* sn_; std::string* name_ = nullptr; acc_cond::mark_t inf_sets_ = 0U; @@ -400,7 +400,7 @@ namespace spot } void - process_link(const tgba_digraph::trans_storage_t& t, int number) + process_link(const twa_graph::trans_storage_t& t, int number) { std::string label = bdd_format_formula(aut_->get_dict(), t.cond); os_ << " " << t.src << " -> " << t.dst; @@ -433,7 +433,7 @@ namespace spot os_ << "]\n"; } - void print(const const_tgba_digraph_ptr& aut) + void print(const const_twa_graph_ptr& aut) { aut_ = aut; sn_ = aut->get_named_prop>("state-names"); @@ -492,9 +492,9 @@ namespace spot const char* options) { dotty_output d(os, options); - auto aut = std::dynamic_pointer_cast(g); + auto aut = std::dynamic_pointer_cast(g); if (!aut) - aut = make_tgba_digraph(g, twa::prop_set::all()); + aut = make_twa_graph(g, twa::prop_set::all()); d.print(aut); return os; } diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 8d53da684..1fec0dc8a 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -214,7 +214,7 @@ namespace spot unsigned cand_size; }; - unsigned declare_vars(const const_tgba_digraph_ptr& aut, + unsigned declare_vars(const const_twa_graph_ptr& aut, dict& d, bdd ap, bool state_based, @@ -295,7 +295,7 @@ namespace spot static sat_stats dtba_to_sat(std::ostream& out, - const const_tgba_digraph_ptr& ref, + const const_twa_graph_ptr& ref, dict& d, bool state_based) { clause_counter nclauses; @@ -631,12 +631,12 @@ namespace spot return std::make_pair(d.nvars, nclauses.nb_clauses()); } - static tgba_digraph_ptr + static twa_graph_ptr sat_build(const satsolver::solution& solution, dict& satdict, - const_tgba_digraph_ptr aut, bool state_based) + const_twa_graph_ptr aut, bool state_based) { auto autdict = aut->get_dict(); - auto a = make_tgba_digraph(autdict); + auto a = make_twa_graph(autdict); a->copy_ap_of(aut); acc_cond::mark_t acc = a->set_buchi(); if (state_based) @@ -737,8 +737,8 @@ namespace spot } } - tgba_digraph_ptr - dtba_sat_synthetize(const const_tgba_digraph_ptr& a, + twa_graph_ptr + dtba_sat_synthetize(const const_twa_graph_ptr& a, int target_state_number, bool state_based) { if (!a->acc().is_buchi()) @@ -762,7 +762,7 @@ namespace spot solution = solver.get_solution(); t.stop("solve"); - tgba_digraph_ptr res = nullptr; + twa_graph_ptr res = nullptr; if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); @@ -805,12 +805,12 @@ namespace spot return res; } - tgba_digraph_ptr - dtba_sat_minimize(const const_tgba_digraph_ptr& a, bool state_based) + twa_graph_ptr + dtba_sat_minimize(const const_twa_graph_ptr& a, bool state_based) { int n_states = stats_reachable(a).states; - tgba_digraph_ptr prev = nullptr; + twa_graph_ptr prev = nullptr; for (;;) { auto next = @@ -824,14 +824,14 @@ namespace spot SPOT_UNREACHABLE(); } - tgba_digraph_ptr - dtba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, + twa_graph_ptr + dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, bool state_based) { int max_states = stats_reachable(a).states - 1; int min_states = 1; - tgba_digraph_ptr prev = nullptr; + twa_graph_ptr prev = nullptr; while (min_states <= max_states) { int target = (max_states + min_states) / 2; diff --git a/src/tgbaalgos/dtbasat.hh b/src/tgbaalgos/dtbasat.hh index 543f695f2..b6a09d159 100644 --- a/src/tgbaalgos/dtbasat.hh +++ b/src/tgbaalgos/dtbasat.hh @@ -39,8 +39,8 @@ namespace spot /// /// If no equivalent deterministic TBA with \a target_state_number /// states is found, a null pointer - SPOT_API tgba_digraph_ptr - dtba_sat_synthetize(const const_tgba_digraph_ptr& a, + SPOT_API twa_graph_ptr + dtba_sat_synthetize(const const_twa_graph_ptr& a, int target_state_number, bool state_based = false); @@ -50,8 +50,8 @@ namespace spot /// number of states, and returns the last successfully built TBA. /// /// If no smaller TBA exist, this returns a null pointer. - SPOT_API tgba_digraph_ptr - dtba_sat_minimize(const const_tgba_digraph_ptr& a, + SPOT_API twa_graph_ptr + dtba_sat_minimize(const const_twa_graph_ptr& a, bool state_based = false); /// \brief Attempt to minimize a deterministic TBA with a SAT solver. @@ -60,7 +60,7 @@ namespace spot /// find the minimum number of states using a binary search. // /// If no smaller TBA exist, this returns a null pointer. - SPOT_API tgba_digraph_ptr - dtba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, + SPOT_API twa_graph_ptr + dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, bool state_based = false); } diff --git a/src/tgbaalgos/dtgbacomp.cc b/src/tgbaalgos/dtgbacomp.cc index b4091c705..6555804f4 100644 --- a/src/tgbaalgos/dtgbacomp.cc +++ b/src/tgbaalgos/dtgbacomp.cc @@ -24,10 +24,10 @@ namespace spot { - tgba_digraph_ptr dtgba_complement_nonweak(const const_tgba_digraph_ptr& aut) + twa_graph_ptr dtgba_complement_nonweak(const const_twa_graph_ptr& aut) { // Clone the original automaton. - auto res = make_tgba_digraph(aut, + auto res = make_twa_graph(aut, { false, // state based false, // inherently_weak false, // deterministic @@ -112,10 +112,10 @@ namespace spot return res; } - tgba_digraph_ptr dtgba_complement_weak(const const_tgba_digraph_ptr& aut) + twa_graph_ptr dtgba_complement_weak(const const_twa_graph_ptr& aut) { // Clone the original automaton. - auto res = make_tgba_digraph(aut, + auto res = make_twa_graph(aut, { true, // state based true, // inherently weak true, // determinisitic @@ -160,7 +160,7 @@ namespace spot return res; } - tgba_digraph_ptr dtgba_complement(const const_tgba_digraph_ptr& aut) + twa_graph_ptr dtgba_complement(const const_twa_graph_ptr& aut) { if (aut->acc().is_generalized_buchi()) { diff --git a/src/tgbaalgos/dtgbacomp.hh b/src/tgbaalgos/dtgbacomp.hh index 072ed47a3..412075524 100644 --- a/src/tgbaalgos/dtgbacomp.hh +++ b/src/tgbaalgos/dtgbacomp.hh @@ -30,6 +30,6 @@ namespace spot /// state-based. Unless the input automaton is marked as weak (in /// which case the output will also be weak and deterministic) the /// resulting automaton is very unlikely to be deterministic. - SPOT_API tgba_digraph_ptr - dtgba_complement(const const_tgba_digraph_ptr& aut); + SPOT_API twa_graph_ptr + dtgba_complement(const const_twa_graph_ptr& aut); } diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 6c1c9d61e..47c5b4b0b 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -285,7 +285,7 @@ namespace spot }; - unsigned declare_vars(const const_tgba_digraph_ptr& aut, + unsigned declare_vars(const const_twa_graph_ptr& aut, dict& d, bdd ap, bool state_based, scc_info& sm) { bdd_dict_ptr bd = aut->get_dict(); @@ -424,7 +424,7 @@ namespace spot typedef std::pair sat_stats; static - sat_stats dtgba_to_sat(std::ostream& out, const_tgba_digraph_ptr ref, + sat_stats dtgba_to_sat(std::ostream& out, const_twa_graph_ptr ref, dict& d, bool state_based) { clause_counter nclauses; @@ -772,12 +772,12 @@ namespace spot return std::make_pair(d.nvars, nclauses.nb_clauses()); } - static tgba_digraph_ptr + static twa_graph_ptr sat_build(const satsolver::solution& solution, dict& satdict, - const_tgba_digraph_ptr aut, bool state_based) + const_twa_graph_ptr aut, bool state_based) { auto autdict = aut->get_dict(); - auto a = make_tgba_digraph(autdict); + auto a = make_twa_graph(autdict); a->copy_ap_of(aut); a->set_generalized_buchi(satdict.cand_nacc); if (state_based) @@ -873,8 +873,8 @@ namespace spot } } - tgba_digraph_ptr - dtgba_sat_synthetize(const const_tgba_digraph_ptr& a, + twa_graph_ptr + dtgba_sat_synthetize(const const_twa_graph_ptr& a, unsigned target_acc_number, int target_state_number, bool state_based) { @@ -902,7 +902,7 @@ namespace spot solution = solver.get_solution(); t.stop("solve"); - tgba_digraph_ptr res = nullptr; + twa_graph_ptr res = nullptr; if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); @@ -945,14 +945,14 @@ namespace spot return res; } - tgba_digraph_ptr - dtgba_sat_minimize(const const_tgba_digraph_ptr& a, + twa_graph_ptr + dtgba_sat_minimize(const const_twa_graph_ptr& a, unsigned target_acc_number, bool state_based) { int n_states = stats_reachable(a).states; - tgba_digraph_ptr prev = nullptr; + twa_graph_ptr prev = nullptr; for (;;) { auto next = @@ -967,15 +967,15 @@ namespace spot SPOT_UNREACHABLE(); } - tgba_digraph_ptr - dtgba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, + twa_graph_ptr + dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, unsigned target_acc_number, bool state_based) { int max_states = stats_reachable(a).states - 1; int min_states = 1; - tgba_digraph_ptr prev = nullptr; + twa_graph_ptr prev = nullptr; while (min_states <= max_states) { int target = (max_states + min_states) / 2; diff --git a/src/tgbaalgos/dtgbasat.hh b/src/tgbaalgos/dtgbasat.hh index daddbd24f..ad4a64283 100644 --- a/src/tgbaalgos/dtgbasat.hh +++ b/src/tgbaalgos/dtgbasat.hh @@ -43,8 +43,8 @@ namespace spot /// acceptance sets and target_state_number states that is /// equivalent to \a a. If no such TGBA is found, a null pointer is /// returned. - SPOT_API tgba_digraph_ptr - dtgba_sat_synthetize(const const_tgba_digraph_ptr& a, + SPOT_API twa_graph_ptr + dtgba_sat_synthetize(const const_twa_graph_ptr& a, unsigned target_acc_number, int target_state_number, bool state_based = false); @@ -55,8 +55,8 @@ namespace spot /// number of states, and returns the last successfully built TGBA. /// /// If no smaller TGBA exist, this returns a null pointer. - SPOT_API tgba_digraph_ptr - dtgba_sat_minimize(const const_tgba_digraph_ptr& a, + SPOT_API twa_graph_ptr + dtgba_sat_minimize(const const_twa_graph_ptr& a, unsigned target_acc_number, bool state_based = false); @@ -66,8 +66,8 @@ namespace spot /// find the minimum number of states using a binary search. // /// If no smaller TBA exist, this returns a null pointer. - SPOT_API tgba_digraph_ptr - dtgba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, + SPOT_API twa_graph_ptr + dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, unsigned target_acc_number, bool state_based = false); } diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc index e49591dba..de20804de 100644 --- a/src/tgbaalgos/dupexp.cc +++ b/src/tgbaalgos/dupexp.cc @@ -37,14 +37,14 @@ namespace spot { public: dupexp_iter(const const_tgba_ptr& a, twa::prop_set p) - : T(a), out_(make_tgba_digraph(a->get_dict())) + : T(a), out_(make_twa_graph(a->get_dict())) { out_->copy_acceptance_of(a); out_->copy_ap_of(a); out_->prop_copy(a, p); } - tgba_digraph_ptr + twa_graph_ptr result() { return out_; @@ -70,12 +70,12 @@ namespace spot } protected: - tgba_digraph_ptr out_; + twa_graph_ptr out_; }; } // anonymous - tgba_digraph_ptr + twa_graph_ptr tgba_dupexp_bfs(const const_tgba_ptr& aut, twa::prop_set p) { dupexp_iter di(aut, p); @@ -83,7 +83,7 @@ namespace spot return di.result(); } - tgba_digraph_ptr + twa_graph_ptr tgba_dupexp_dfs(const const_tgba_ptr& aut, twa::prop_set p) { dupexp_iter di(aut, p); diff --git a/src/tgbaalgos/dupexp.hh b/src/tgbaalgos/dupexp.hh index 5cf83dcd3..3a7fa1c0c 100644 --- a/src/tgbaalgos/dupexp.hh +++ b/src/tgbaalgos/dupexp.hh @@ -32,11 +32,11 @@ namespace spot /// \ingroup tgba_misc /// \brief Build an explicit automaton from all states of \a aut, /// numbering states in bread first order as they are processed. - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr tgba_dupexp_bfs(const const_tgba_ptr& aut, twa::prop_set p); /// \ingroup tgba_misc /// \brief Build an explicit automaton from all states of \a aut, /// numbering states in depth first order as they are processed. - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr tgba_dupexp_dfs(const const_tgba_ptr& aut, twa::prop_set p); } diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 458d4ec01..8a863bf32 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -290,11 +290,11 @@ namespace spot // tgba_run_to_tgba ////////////////////////////////////////////////////////////////////// - tgba_digraph_ptr + twa_graph_ptr tgba_run_to_tgba(const const_tgba_ptr& a, const const_tgba_run_ptr& run) { auto d = a->get_dict(); - auto res = make_tgba_digraph(d); + auto res = make_twa_graph(d); res->copy_ap_of(a); res->copy_acceptance_of(a); diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 77685e434..912245343 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -315,7 +315,7 @@ namespace spot /// states are merged). /// /// \pre \a run must correspond to an actual run of the automaton \a a. - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr tgba_run_to_tgba(const const_tgba_ptr& a, const const_tgba_run_ptr& run); /// @} diff --git a/src/tgbaalgos/hoa.cc b/src/tgbaalgos/hoa.cc index 3a631d31a..1854522c6 100644 --- a/src/tgbaalgos/hoa.cc +++ b/src/tgbaalgos/hoa.cc @@ -58,7 +58,7 @@ namespace spot typedef std::map sup_map; sup_map sup; - metadata(const const_tgba_digraph_ptr& aut, bool implicit) + metadata(const const_twa_graph_ptr& aut, bool implicit) { check_det_and_comp(aut); use_implicit_labels = implicit && is_deterministic && is_complete; @@ -67,7 +67,7 @@ namespace spot std::ostream& emit_acc(std::ostream& os, - const const_tgba_digraph_ptr& aut, + const const_twa_graph_ptr& aut, acc_cond::mark_t b) { // FIXME: We could use a cache for this. @@ -87,7 +87,7 @@ namespace spot return os; } - void check_det_and_comp(const const_tgba_digraph_ptr& aut) + void check_det_and_comp(const const_twa_graph_ptr& aut) { std::string empty; @@ -223,7 +223,7 @@ namespace spot static std::ostream& hoa_reachable(std::ostream& os, - const const_tgba_digraph_ptr& aut, + const const_twa_graph_ptr& aut, const char* opt) { bool newline = true; @@ -436,9 +436,9 @@ namespace spot const char* opt) { - auto a = std::dynamic_pointer_cast(aut); + auto a = std::dynamic_pointer_cast(aut); if (!a) - a = make_tgba_digraph(aut, twa::prop_set::all()); + a = make_twa_graph(aut, twa::prop_set::all()); return hoa_reachable(os, a, opt); } diff --git a/src/tgbaalgos/isdet.cc b/src/tgbaalgos/isdet.cc index 9d9ae40ea..038de920c 100644 --- a/src/tgbaalgos/isdet.cc +++ b/src/tgbaalgos/isdet.cc @@ -28,7 +28,7 @@ namespace spot template static unsigned - count_nondet_states_aux(const const_tgba_digraph_ptr& aut) + count_nondet_states_aux(const const_twa_graph_ptr& aut) { unsigned nondet_states = 0; unsigned ns = aut->num_states(); @@ -55,13 +55,13 @@ namespace spot } unsigned - count_nondet_states(const const_tgba_digraph_ptr& aut) + count_nondet_states(const const_twa_graph_ptr& aut) { return count_nondet_states_aux(aut); } bool - is_deterministic(const const_tgba_digraph_ptr& aut) + is_deterministic(const const_twa_graph_ptr& aut) { if (aut->is_deterministic()) return true; @@ -69,7 +69,7 @@ namespace spot } bool - is_complete(const const_tgba_digraph_ptr& aut) + is_complete(const const_twa_graph_ptr& aut) { unsigned ns = aut->num_states(); for (unsigned src = 0; src < ns; ++src) diff --git a/src/tgbaalgos/isdet.hh b/src/tgbaalgos/isdet.hh index 55972bf5d..04b428395 100644 --- a/src/tgbaalgos/isdet.hh +++ b/src/tgbaalgos/isdet.hh @@ -32,7 +32,7 @@ namespace spot /// but it is more efficient to call is_deterministic() if you do not /// care about the number of nondeterministic states. SPOT_API unsigned - count_nondet_states(const const_tgba_digraph_ptr& aut); + count_nondet_states(const const_twa_graph_ptr& aut); /// \brief Return true iff \a aut is deterministic. /// @@ -40,14 +40,14 @@ namespace spot /// the automaton is nondeterministic, because it can return before /// the entire automaton has been explored. SPOT_API bool - is_deterministic(const const_tgba_digraph_ptr& aut); + is_deterministic(const const_twa_graph_ptr& aut); /// \brief Return true iff \a aut is complete. /// /// An automaton is complete if its translation relation is total, /// i.e., each state as a successor for any possible configuration. SPOT_API bool - is_complete(const const_tgba_digraph_ptr& aut); + is_complete(const const_twa_graph_ptr& aut); /// @} } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index f3db37255..acae023c6 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -45,10 +45,10 @@ namespace spot sba_(nullptr) { // Check if the automaton can be converted into a - // tgba_digraph. This makes the state_is_accepting() function + // twa_graph. This makes the state_is_accepting() function // more efficient. if (a->is_sba()) - sba_ = std::dynamic_pointer_cast(a); + sba_ = std::dynamic_pointer_cast(a); } bool @@ -128,7 +128,7 @@ namespace spot std::ostringstream body_; bdd all_acc_conds_; bool sba_format_; - const_tgba_digraph_ptr sba_; + const_twa_graph_ptr sba_; }; } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index de52301bb..7f001ca6d 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -110,15 +110,15 @@ namespace spot class ratexp_to_dfa { - typedef typename tgba_digraph::namer::type namer; + typedef typename twa_graph::namer::type namer; public: ratexp_to_dfa(translate_dict& dict); - std::tuple + std::tuple succ(const formula* f); ~ratexp_to_dfa(); protected: - typedef std::pair labelled_aut; + typedef std::pair labelled_aut; labelled_aut translate(const formula* f); private: @@ -1125,7 +1125,7 @@ namespace spot { assert(f->is_in_nenoform()); - auto a = make_tgba_digraph(dict_.dict); + auto a = make_twa_graph(dict_.dict); auto namer = a->create_namer(); typedef std::set set_type; @@ -1252,7 +1252,7 @@ namespace spot } // FIXME: use the new tgba::succ() interface - std::tuple ratexp_to_dfa::succ(const formula* f) @@ -2200,7 +2200,7 @@ namespace spot typedef std::vector dest_map; } - tgba_digraph_ptr + twa_graph_ptr ltl_to_tgba_fm(const formula* f, const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, @@ -2231,7 +2231,7 @@ namespace spot assert(dict == s->get_dict()); - tgba_digraph_ptr a = make_tgba_digraph(dict); + twa_graph_ptr a = make_twa_graph(dict); auto namer = a->create_namer(); translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence()); diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 01254845c..c9449dcf7 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -30,7 +30,7 @@ namespace spot { /// \ingroup tgba_ltl - /// \brief Build a spot::tgba_digraph_ptr from an LTL formula. + /// \brief Build a spot::twa_graph_ptr from an LTL formula. /// /// This is based on the following paper. /** \verbatim @@ -120,8 +120,8 @@ namespace spot } \endverbatim */ /// - /// \return A spot::tgba_digraph that recognizes the language of \a f. - SPOT_API tgba_digraph_ptr + /// \return A spot::twa_graph that recognizes the language of \a f. + SPOT_API twa_graph_ptr ltl_to_tgba_fm(const ltl::formula* f, const bdd_dict_ptr& dict, bool exprop = false, bool symb_merge = true, bool branching_postponement = false, diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc index d7c024a9d..eb3675728 100644 --- a/src/tgbaalgos/mask.cc +++ b/src/tgbaalgos/mask.cc @@ -21,10 +21,10 @@ namespace spot { - tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in, + twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in, acc_cond::mark_t to_remove) { - auto res = make_tgba_digraph(in->get_dict()); + auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); res->prop_copy(in, { true, true, true, false }); unsigned na = in->acc().num_sets(); @@ -45,14 +45,14 @@ namespace spot return res; } - tgba_digraph_ptr mask_keep_states(const const_tgba_digraph_ptr& in, + twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in, std::vector& to_keep, unsigned int init) { if (to_keep.size() < in->num_states()) to_keep.resize(in->num_states(), false); - auto res = make_tgba_digraph(in->get_dict()); + auto res = make_twa_graph(in->get_dict()); res->copy_ap_of(in); res->prop_copy(in, { true, true, true, false }); res->copy_acceptance_of(in); diff --git a/src/tgbaalgos/mask.hh b/src/tgbaalgos/mask.hh index 7773c848a..aff67953f 100644 --- a/src/tgbaalgos/mask.hh +++ b/src/tgbaalgos/mask.hh @@ -39,8 +39,8 @@ namespace spot /// \param init The optional new initial state. template - void transform_accessible(const const_tgba_digraph_ptr& old, - tgba_digraph_ptr& cpy, + void transform_accessible(const const_twa_graph_ptr& old, + twa_graph_ptr& cpy, Trans trans, unsigned int init) { std::vector todo; @@ -97,8 +97,8 @@ namespace spot /// all transtions will be processed. /// \param init The optional new initial state. template - void transform_copy(const const_tgba_digraph_ptr& old, - tgba_digraph_ptr& cpy, + void transform_copy(const const_twa_graph_ptr& old, + twa_graph_ptr& cpy, Trans trans, unsigned int init) { // Each state in cpy corresponds to a unique state in old. @@ -119,15 +119,15 @@ namespace spot } template - void transform_accessible(const const_tgba_digraph_ptr& old, - tgba_digraph_ptr& cpy, + void transform_accessible(const const_twa_graph_ptr& old, + twa_graph_ptr& cpy, Trans trans) { transform_accessible(old, cpy, trans, old->get_init_state_number()); } template - void transform_copy(const const_tgba_digraph_ptr& old, - tgba_digraph_ptr& cpy, + void transform_copy(const const_twa_graph_ptr& old, + twa_graph_ptr& cpy, Trans trans) { transform_copy(old, cpy, trans, old->get_init_state_number()); @@ -135,7 +135,7 @@ namespace spot /// \brief Remove all transitions that are in some given acceptance sets. SPOT_API - tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in, + twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in, acc_cond::mark_t to_remove); /// \brief Keep only the states as specified by \a to_keep. @@ -143,7 +143,7 @@ namespace spot /// Each index in the vector \a to_keep specifies wether or not to keep that /// state. The initial state will be set to \a init. SPOT_API - tgba_digraph_ptr mask_keep_states(const const_tgba_digraph_ptr& in, + twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in, std::vector& to_keep, unsigned int init); } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 87903faf1..4e17b76f8 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -114,12 +114,12 @@ namespace spot // From the base automaton and the list of sets, build the minimal // resulting automaton - tgba_digraph_ptr build_result(const const_tgba_ptr& a, + twa_graph_ptr build_result(const const_tgba_ptr& a, std::list& sets, hash_set* final) { auto dict = a->get_dict(); - auto res = make_tgba_digraph(dict); + auto res = make_twa_graph(dict); res->copy_ap_of(a); res->prop_state_based_acc(); @@ -194,7 +194,7 @@ namespace spot filter(const state* s) { s = seen(s); - if (sm.scc_of(std::static_pointer_cast(a_) + if (sm.scc_of(std::static_pointer_cast(a_) ->state_number(s)) != scc_n) return 0; return s; @@ -215,8 +215,8 @@ namespace spot bool - wdba_scc_is_accepting(const const_tgba_digraph_ptr& det_a, unsigned scc_n, - const const_tgba_digraph_ptr& orig_a, scc_info& sm, + wdba_scc_is_accepting(const const_twa_graph_ptr& det_a, unsigned scc_n, + const const_twa_graph_ptr& orig_a, scc_info& sm, power_map& pm) { // Get some state from the SCC #n. @@ -230,7 +230,7 @@ namespace spot (void)reached; // Build an automaton representing this loop. - auto loop_a = make_tgba_digraph(det_a->get_dict()); + auto loop_a = make_twa_graph(det_a->get_dict()); tgba_run::steps::const_iterator i; int loop_size = loop.size(); loop_a->new_states(loop_size); @@ -269,7 +269,7 @@ namespace spot } - tgba_digraph_ptr minimize_dfa(const const_tgba_digraph_ptr& det_a, + twa_graph_ptr minimize_dfa(const const_twa_graph_ptr& det_a, hash_set* final, hash_set* non_final) { typedef std::list partition_t; @@ -475,11 +475,11 @@ namespace spot } - tgba_digraph_ptr minimize_monitor(const const_tgba_digraph_ptr& a) + twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a) { hash_set* final = new hash_set; hash_set* non_final = new hash_set; - tgba_digraph_ptr det_a = tgba_powerset(a); + twa_graph_ptr det_a = tgba_powerset(a); // non_final contain all states. // final is empty: there is no acceptance condition @@ -492,7 +492,7 @@ namespace spot return res; } - tgba_digraph_ptr minimize_wdba(const const_tgba_digraph_ptr& a) + twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a) { if (a->acc().uses_fin_acceptance()) throw std::runtime_error @@ -501,7 +501,7 @@ namespace spot hash_set* final = new hash_set; hash_set* non_final = new hash_set; - tgba_digraph_ptr det_a; + twa_graph_ptr det_a; { power_map pm; @@ -595,10 +595,10 @@ namespace spot return res; } - tgba_digraph_ptr - minimize_obligation(const const_tgba_digraph_ptr& aut_f, + twa_graph_ptr + minimize_obligation(const const_twa_graph_ptr& aut_f, const ltl::formula* f, - const_tgba_digraph_ptr aut_neg_f, + const_twa_graph_ptr aut_neg_f, bool reject_bigger) { auto min_aut_f = minimize_wdba(aut_f); @@ -608,7 +608,7 @@ namespace spot // Abort if min_aut_f has more states than aut_f. unsigned orig_states = aut_f->num_states(); if (orig_states < min_aut_f->num_states()) - return std::const_pointer_cast(aut_f); + return std::const_pointer_cast(aut_f); } // If the input automaton was already weak and deterministic, the @@ -675,6 +675,6 @@ namespace spot if (ok) return min_aut_f; - return std::const_pointer_cast(aut_f); + return std::const_pointer_cast(aut_f); } } diff --git a/src/tgbaalgos/minimize.hh b/src/tgbaalgos/minimize.hh index 2101a51bc..3ffc3334b 100644 --- a/src/tgbaalgos/minimize.hh +++ b/src/tgbaalgos/minimize.hh @@ -56,7 +56,7 @@ namespace spot /// \param a the automaton to convert into a minimal deterministic monitor /// \pre Dead SCCs should have been removed from \a a before /// calling this function. - SPOT_API tgba_digraph_ptr minimize_monitor(const const_tgba_digraph_ptr& a); + SPOT_API twa_graph_ptr minimize_monitor(const const_twa_graph_ptr& a); /// \brief Minimize a Büchi automaton in the WDBA class. /// @@ -92,7 +92,7 @@ namespace spot month = oct } \endverbatim */ - SPOT_API tgba_digraph_ptr minimize_wdba(const const_tgba_digraph_ptr& a); + SPOT_API twa_graph_ptr minimize_wdba(const const_twa_graph_ptr& a); /// \brief Minimize an automaton if it represents an obligation property. /// @@ -149,10 +149,10 @@ namespace spot /// determinization step during minimize_wdba().) Note that /// checking the size of the minimized WDBA occurs before ensuring /// that the minimized WDBA is correct. - SPOT_API tgba_digraph_ptr - minimize_obligation(const const_tgba_digraph_ptr& aut_f, + SPOT_API twa_graph_ptr + minimize_obligation(const const_twa_graph_ptr& aut_f, const ltl::formula* f = 0, - const_tgba_digraph_ptr aut_neg_f = nullptr, + const_twa_graph_ptr aut_neg_f = nullptr, bool reject_bigger = false); /// @} } diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 5d2ee4303..017c7e80d 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -40,7 +40,7 @@ namespace spot bool opt_comments_ = false; std::vector* sn_ = nullptr; bool opt_624_ = false; - const_tgba_digraph_ptr aut_; + const_twa_graph_ptr aut_; bool fi_needed_ = false; bool need_accept_all_ = false; unsigned accept_all_ = 0; @@ -183,7 +183,7 @@ namespace spot os_ << (opt_624_ ? " od;\n" : " fi;\n"); } - void print(const const_tgba_digraph_ptr& aut) + void print(const const_twa_graph_ptr& aut) { aut_ = aut; if (opt_comments_) @@ -208,9 +208,9 @@ namespace spot throw std::runtime_error ("Never claim output only supports Büchi acceptance"); never_claim_output d(os, options); - auto aut = std::dynamic_pointer_cast(g); + auto aut = std::dynamic_pointer_cast(g); if (!aut) - aut = make_tgba_digraph(g, twa::prop_set::all()); + aut = make_twa_graph(g, twa::prop_set::all()); d.print(aut); return os; } diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 00357ce03..9ed0d2263 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -36,8 +36,8 @@ namespace spot { namespace { - static tgba_digraph_ptr - ensure_ba(tgba_digraph_ptr& a) + static twa_graph_ptr + ensure_ba(twa_graph_ptr& a) { if (a->acc().num_sets() == 0) { @@ -89,8 +89,8 @@ namespace spot } } - tgba_digraph_ptr - postprocessor::do_simul(const tgba_digraph_ptr& a, int opt) + twa_graph_ptr + postprocessor::do_simul(const twa_graph_ptr& a, int opt) { switch (opt) { @@ -106,8 +106,8 @@ namespace spot } } - tgba_digraph_ptr - postprocessor::do_ba_simul(const tgba_digraph_ptr& a, int opt) + twa_graph_ptr + postprocessor::do_ba_simul(const twa_graph_ptr& a, int opt) { switch (opt) { @@ -123,8 +123,8 @@ namespace spot } } - tgba_digraph_ptr - postprocessor::do_degen(const tgba_digraph_ptr& a) + twa_graph_ptr + postprocessor::do_degen(const twa_graph_ptr& a) { auto d = degeneralize(a, degen_reset_, degen_order_, @@ -138,8 +138,8 @@ namespace spot #define PREF_ (pref_ & (Small | Deterministic)) #define COMP_ (pref_ & Complete) - tgba_digraph_ptr - postprocessor::run(tgba_digraph_ptr a, const ltl::formula* f) + twa_graph_ptr + postprocessor::run(twa_graph_ptr a, const ltl::formula* f) { if (type_ != Generic && !a->acc().is_generalized_buchi()) a = to_generalized_buchi(a); @@ -215,8 +215,8 @@ namespace spot bool dba_is_wdba = false; bool dba_is_minimal = false; - tgba_digraph_ptr dba = 0; - tgba_digraph_ptr sim = 0; + twa_graph_ptr dba = 0; + twa_graph_ptr sim = 0; // (Small,Low) is the only configuration where we do not run // WDBA-minimization. @@ -269,7 +269,7 @@ namespace spot // If we don't have a DBA, attempt tba-determinization if requested. if (tba_determinisation_ && !dba) { - tgba_digraph_ptr tmpd = nullptr; + twa_graph_ptr tmpd = nullptr; if (PREF_ == Deterministic && f && f->is_syntactic_recurrence() @@ -334,7 +334,7 @@ namespace spot // sure it is at least 1. target_acc = original_acc > 0 ? original_acc : 1; - const_tgba_digraph_ptr in = 0; + const_twa_graph_ptr in = 0; if (target_acc == 1) { // If we are seeking a minimal DBA with unknown number of @@ -352,7 +352,7 @@ namespace spot in = dba; } - const_tgba_digraph_ptr res = tgba_complete(in); + const_twa_graph_ptr res = tgba_complete(in); if (target_acc == 1) { if (sat_states_ != -1) diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 71a7e5e8f..7efb0461c 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -99,13 +99,13 @@ namespace spot /// /// The returned automaton might be a new automaton, /// or an in-place modification of the \a input automaton. - tgba_digraph_ptr run(tgba_digraph_ptr input, + twa_graph_ptr run(twa_graph_ptr input, const ltl::formula* f); protected: - tgba_digraph_ptr do_simul(const tgba_digraph_ptr& input, int opt); - tgba_digraph_ptr do_ba_simul(const tgba_digraph_ptr& input, int opt); - tgba_digraph_ptr do_degen(const tgba_digraph_ptr& input); + twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt); + twa_graph_ptr do_ba_simul(const twa_graph_ptr& input, int opt); + twa_graph_ptr do_degen(const twa_graph_ptr& input); output_type type_; int pref_; diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 34de9065f..3c8549702 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -85,8 +85,8 @@ namespace spot }; } - tgba_digraph_ptr - tgba_powerset(const const_tgba_digraph_ptr& aut, power_map& pm, bool merge) + twa_graph_ptr + tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge) { bdd allap = bddtrue; { @@ -155,7 +155,7 @@ namespace spot std::vectortoclean; - auto res = make_tgba_digraph(aut->get_dict()); + auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); { @@ -217,8 +217,8 @@ namespace spot return res; } - tgba_digraph_ptr - tgba_powerset(const const_tgba_digraph_ptr& aut) + twa_graph_ptr + tgba_powerset(const const_twa_graph_ptr& aut) { power_map pm; return tgba_powerset(aut, pm); @@ -236,7 +236,7 @@ namespace spot typedef std::set trans_set; typedef std::vector set_set; protected: - const_tgba_digraph_ptr ref_; + const_twa_graph_ptr ref_; power_map& refmap_; trans_set reject_; // set of rejecting transitions set_set accept_; // set of cycles that are accepting @@ -245,7 +245,7 @@ namespace spot unsigned cycles_left_; // count of cycles left to explore public: - fix_scc_acceptance(const scc_info& sm, const_tgba_digraph_ptr ref, + fix_scc_acceptance(const scc_info& sm, const_twa_graph_ptr ref, power_map& refmap, unsigned threshold) : enumerate_cycles(sm), ref_(ref), refmap_(refmap), threshold_(threshold) @@ -279,10 +279,10 @@ namespace spot bool is_cycle_accepting(cycle_iter begin, trans_set& ts) const { - auto a = std::const_pointer_cast(aut_); + auto a = std::const_pointer_cast(aut_); // Build an automaton representing this loop. - auto loop_a = make_tgba_digraph(aut_->get_dict()); + auto loop_a = make_twa_graph(aut_->get_dict()); int loop_size = std::distance(begin, dfs_.end()); loop_a->new_states(loop_size); int n; @@ -362,8 +362,8 @@ namespace spot }; static bool - fix_dba_acceptance(tgba_digraph_ptr det, - const_tgba_digraph_ptr ref, power_map& refmap, + fix_dba_acceptance(twa_graph_ptr det, + const_twa_graph_ptr ref, power_map& refmap, unsigned threshold) { det->copy_acceptance_of(ref); @@ -382,8 +382,8 @@ namespace spot } } - tgba_digraph_ptr - tba_determinize(const const_tgba_digraph_ptr& aut, + twa_graph_ptr + tba_determinize(const const_twa_graph_ptr& aut, unsigned threshold_states, unsigned threshold_cycles) { power_map pm; @@ -401,12 +401,12 @@ namespace spot return det; } - tgba_digraph_ptr - tba_determinize_check(const tgba_digraph_ptr& aut, + twa_graph_ptr + tba_determinize_check(const twa_graph_ptr& aut, unsigned threshold_states, unsigned threshold_cycles, const ltl::formula* f, - const_tgba_digraph_ptr neg_aut) + const_twa_graph_ptr neg_aut) { if (f == 0 && neg_aut == 0) return 0; diff --git a/src/tgbaalgos/powerset.hh b/src/tgbaalgos/powerset.hh index 784ca1e84..a27c4926e 100644 --- a/src/tgbaalgos/powerset.hh +++ b/src/tgbaalgos/powerset.hh @@ -54,11 +54,11 @@ namespace spot /// The \a merge argument can be set to false to prevent merging of /// transitions. //@{ - SPOT_API tgba_digraph_ptr - tgba_powerset(const const_tgba_digraph_ptr& aut, + SPOT_API twa_graph_ptr + tgba_powerset(const const_twa_graph_ptr& aut, power_map& pm, bool merge = true); - SPOT_API tgba_digraph_ptr - tgba_powerset(const const_tgba_digraph_ptr& aut); + SPOT_API twa_graph_ptr + tgba_powerset(const const_twa_graph_ptr& aut); //@} @@ -97,8 +97,8 @@ namespace spot /// If \a threshold_cycles is non null, abort the construction /// whenever an SCC of the constructed automaton has more than \a /// threshold_cycles cycles. - SPOT_API tgba_digraph_ptr - tba_determinize(const const_tgba_digraph_ptr& aut, + SPOT_API twa_graph_ptr + tba_determinize(const const_twa_graph_ptr& aut, unsigned threshold_states = 0, unsigned threshold_cycles = 0); @@ -129,11 +129,11 @@ namespace spot /// the automaton cannot be determinized, 0 if we do not know if the /// determinization is correct because neither \a f nor \a neg_aut /// were supplied. - SPOT_API tgba_digraph_ptr - tba_determinize_check(const tgba_digraph_ptr& aut, + SPOT_API twa_graph_ptr + tba_determinize_check(const twa_graph_ptr& aut, unsigned threshold_states = 0, unsigned threshold_cycles = 0, const ltl::formula* f = 0, - const_tgba_digraph_ptr neg_aut = 0); + const_twa_graph_ptr neg_aut = 0); } diff --git a/src/tgbaalgos/product.cc b/src/tgbaalgos/product.cc index 46c01990c..51568a42d 100644 --- a/src/tgbaalgos/product.cc +++ b/src/tgbaalgos/product.cc @@ -40,8 +40,8 @@ namespace spot } - tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, - const const_tgba_digraph_ptr& right, + twa_graph_ptr product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, unsigned left_state, unsigned right_state) { @@ -49,7 +49,7 @@ namespace spot std::deque> todo; assert(left->get_dict() == right->get_dict()); - auto res = make_tgba_digraph(left->get_dict()); + auto res = make_twa_graph(left->get_dict()); res->copy_ap_of(left); res->copy_ap_of(right); auto left_num = left->acc().num_sets(); @@ -102,8 +102,8 @@ namespace spot return res; } - tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, - const const_tgba_digraph_ptr& right) + twa_graph_ptr product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right) { return product(left, right, left->get_init_state_number(), diff --git a/src/tgbaalgos/product.hh b/src/tgbaalgos/product.hh index 0cb176c21..fad190baf 100644 --- a/src/tgbaalgos/product.hh +++ b/src/tgbaalgos/product.hh @@ -31,12 +31,12 @@ namespace spot typedef std::vector> product_states; SPOT_API - tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, - const const_tgba_digraph_ptr& right); + twa_graph_ptr product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right); SPOT_API - tgba_digraph_ptr product(const const_tgba_digraph_ptr& left, - const const_tgba_digraph_ptr& right, + twa_graph_ptr product(const const_twa_graph_ptr& left, + const const_twa_graph_ptr& right, unsigned left_state, unsigned right_state); } diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 0d921ccb2..7d0eaa03f 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -78,7 +78,7 @@ namespace spot } acc_cond::mark_t - random_acc_cond(tgba_digraph_ptr aut, unsigned n_accs, float a) + random_acc_cond(twa_graph_ptr aut, unsigned n_accs, float a) { acc_cond::mark_t m = 0U; for (unsigned i = 0U; i < n_accs; ++i) @@ -114,14 +114,14 @@ namespace spot } } - tgba_digraph_ptr + twa_graph_ptr random_graph(int n, float d, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, unsigned n_accs, float a, float t, bool deterministic, bool state_acc) { assert(n > 0); - auto res = make_tgba_digraph(dict); + auto res = make_twa_graph(dict); if (deterministic) res->prop_deterministic(); if (state_acc) diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index dd58b977c..386a241b8 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -77,7 +77,7 @@ namespace spot /// \f$1+(n-1)d\f$ and variance \f$(n-1)d(1-d)\f$. (This is less /// accurate, but faster than considering all possible \a n /// successors one by one.) - SPOT_API tgba_digraph_ptr + SPOT_API twa_graph_ptr random_graph(int n, float d, const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, unsigned n_accs = 0, float a = 0.1, float t = 0.5, diff --git a/src/tgbaalgos/randomize.cc b/src/tgbaalgos/randomize.cc index dad931904..9e02862ea 100644 --- a/src/tgbaalgos/randomize.cc +++ b/src/tgbaalgos/randomize.cc @@ -26,7 +26,7 @@ namespace spot { void - randomize(tgba_digraph_ptr& aut, bool randomize_states, + randomize(twa_graph_ptr& aut, bool randomize_states, bool randomize_transitions) { if (!randomize_states && !randomize_transitions) @@ -58,7 +58,7 @@ namespace spot mrandom_shuffle(v.begin() + 1, v.end()); } - typedef tgba_digraph::graph_t::trans_storage_t tr_t; + typedef twa_graph::graph_t::trans_storage_t tr_t; g.sort_transitions_([](const tr_t& lhs, const tr_t& rhs) { return lhs.src < rhs.src; }); g.chain_transitions_(); diff --git a/src/tgbaalgos/randomize.hh b/src/tgbaalgos/randomize.hh index a3234e19d..373ff7dd9 100644 --- a/src/tgbaalgos/randomize.hh +++ b/src/tgbaalgos/randomize.hh @@ -28,7 +28,7 @@ namespace spot /// Make a random permutation of the state, and of the transitions /// leaving this state. SPOT_API void - randomize(tgba_digraph_ptr& aut, + randomize(twa_graph_ptr& aut, bool randomize_states = true, bool randomize_transitions = true); } diff --git a/src/tgbaalgos/relabel.cc b/src/tgbaalgos/relabel.cc index e909efc6c..f69ee624b 100644 --- a/src/tgbaalgos/relabel.cc +++ b/src/tgbaalgos/relabel.cc @@ -22,7 +22,7 @@ namespace spot { void - relabel_here(tgba_digraph_ptr& aut, ltl::relabeling_map* relmap) + relabel_here(twa_graph_ptr& aut, ltl::relabeling_map* relmap) { bddPair* pairs = bdd_newpair(); auto d = aut->get_dict(); diff --git a/src/tgbaalgos/relabel.hh b/src/tgbaalgos/relabel.hh index 70ff39609..591afa5e2 100644 --- a/src/tgbaalgos/relabel.hh +++ b/src/tgbaalgos/relabel.hh @@ -26,6 +26,6 @@ namespace spot { /// replace atomic propositions in an automaton SPOT_API void - relabel_here(tgba_digraph_ptr& aut, + relabel_here(twa_graph_ptr& aut, ltl::relabeling_map* relmap); } diff --git a/src/tgbaalgos/remfin.cc b/src/tgbaalgos/remfin.cc index 088dc53c6..347125ab8 100644 --- a/src/tgbaalgos/remfin.cc +++ b/src/tgbaalgos/remfin.cc @@ -108,10 +108,10 @@ namespace spot } } - tgba_digraph_ptr remove_fin(const const_tgba_digraph_ptr& aut) + twa_graph_ptr remove_fin(const const_twa_graph_ptr& aut) { if (!aut->acc().uses_fin_acceptance()) - return std::const_pointer_cast(aut); + return std::const_pointer_cast(aut); std::vector code; std::vector rem; @@ -260,7 +260,7 @@ namespace spot scc_info si(aut); unsigned nst = aut->num_states(); - auto res = make_tgba_digraph(aut->get_dict()); + auto res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); res->prop_copy(aut, { false, false, false, true }); res->new_states(nst); diff --git a/src/tgbaalgos/remfin.hh b/src/tgbaalgos/remfin.hh index 46df0c454..e478a6706 100644 --- a/src/tgbaalgos/remfin.hh +++ b/src/tgbaalgos/remfin.hh @@ -24,6 +24,6 @@ namespace spot { /// \brief Rewrite an automaton without Fin acceptance. - SPOT_API tgba_digraph_ptr - remove_fin(const const_tgba_digraph_ptr& aut); + SPOT_API twa_graph_ptr + remove_fin(const const_twa_graph_ptr& aut); } diff --git a/src/tgbaalgos/remprop.cc b/src/tgbaalgos/remprop.cc index 9be2b3c95..09bd19f06 100644 --- a/src/tgbaalgos/remprop.cc +++ b/src/tgbaalgos/remprop.cc @@ -138,13 +138,13 @@ namespace spot } } - tgba_digraph_ptr remove_ap::strip(const_tgba_digraph_ptr aut) const + twa_graph_ptr remove_ap::strip(const_twa_graph_ptr aut) const { bdd restrict = bddtrue; bdd exist = bddtrue; auto d = aut->get_dict(); - tgba_digraph_ptr res = make_tgba_digraph(d); + twa_graph_ptr res = make_twa_graph(d); res->copy_ap_of(aut); res->prop_copy(aut, { true, true, false, false }); res->copy_acceptance_of(aut); diff --git a/src/tgbaalgos/remprop.hh b/src/tgbaalgos/remprop.hh index dbd72bed8..8fe078b84 100644 --- a/src/tgbaalgos/remprop.hh +++ b/src/tgbaalgos/remprop.hh @@ -39,6 +39,6 @@ namespace spot return props_exist.empty() && props_pos.empty() && props_neg.empty(); } - tgba_digraph_ptr strip(const_tgba_digraph_ptr aut) const; + twa_graph_ptr strip(const_twa_graph_ptr aut) const; }; } diff --git a/src/tgbaalgos/safety.cc b/src/tgbaalgos/safety.cc index 5d8db0524..5bac45045 100644 --- a/src/tgbaalgos/safety.cc +++ b/src/tgbaalgos/safety.cc @@ -24,7 +24,7 @@ namespace spot { bool - is_guarantee_automaton(const const_tgba_digraph_ptr& aut, + is_guarantee_automaton(const const_twa_graph_ptr& aut, const scc_info* si) { if (aut->acc().uses_fin_acceptance()) @@ -70,7 +70,7 @@ namespace spot return result; } - bool is_safety_mwdba(const const_tgba_digraph_ptr& aut) + bool is_safety_mwdba(const const_twa_graph_ptr& aut) { if (!(aut->acc().is_buchi() || aut->acc().is_true())) throw std::runtime_error diff --git a/src/tgbaalgos/safety.hh b/src/tgbaalgos/safety.hh index 114b5fc36..328006fe5 100644 --- a/src/tgbaalgos/safety.hh +++ b/src/tgbaalgos/safety.hh @@ -45,7 +45,7 @@ namespace spot /// \param sm an scc_info object for the automaton if available (it /// will be built otherwise). SPOT_API bool - is_guarantee_automaton(const const_tgba_digraph_ptr& aut, + is_guarantee_automaton(const const_twa_graph_ptr& aut, const scc_info* sm = 0); /// \brief Whether a minimized WDBA represents a safety property. @@ -56,6 +56,6 @@ namespace spot /// /// \param aut the automaton to check SPOT_API bool - is_safety_mwdba(const const_tgba_digraph_ptr& aut); + is_safety_mwdba(const const_twa_graph_ptr& aut); } diff --git a/src/tgbaalgos/sbacc.cc b/src/tgbaalgos/sbacc.cc index a6038ba7b..e3eb05165 100644 --- a/src/tgbaalgos/sbacc.cc +++ b/src/tgbaalgos/sbacc.cc @@ -24,12 +24,12 @@ namespace spot { - tgba_digraph_ptr sbacc(tgba_digraph_ptr& old) + twa_graph_ptr sbacc(twa_graph_ptr& old) { if (old->has_state_based_acc()) return old; - auto res = make_tgba_digraph(old->get_dict()); + auto res = make_twa_graph(old->get_dict()); res->copy_ap_of(old); res->copy_acceptance_of(old); res->prop_copy(old, {false, true, true, true}); diff --git a/src/tgbaalgos/sbacc.hh b/src/tgbaalgos/sbacc.hh index 76dd0108d..2290d1222 100644 --- a/src/tgbaalgos/sbacc.hh +++ b/src/tgbaalgos/sbacc.hh @@ -26,5 +26,5 @@ namespace spot /// \brief Transform an automaton to use state-based acceptance /// /// This is independent on the acceptance condition used. - SPOT_API tgba_digraph_ptr sbacc(tgba_digraph_ptr& aut); + SPOT_API twa_graph_ptr sbacc(twa_graph_ptr& aut); } diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 790dc81d9..17ed35329 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -248,14 +248,14 @@ namespace spot template - tgba_digraph_ptr scc_filter_apply(const_tgba_digraph_ptr aut, + twa_graph_ptr scc_filter_apply(const_twa_graph_ptr aut, scc_info* given_si, Args&&... args) { if (!aut->acc().is_generalized_buchi()) throw std::runtime_error ("scc_filter() works only with generalized Büchi acceptance"); - tgba_digraph_ptr filtered = make_tgba_digraph(aut->get_dict()); + twa_graph_ptr filtered = make_twa_graph(aut->get_dict()); unsigned in_n = aut->num_states(); // Number of input states. if (in_n == 0) // Nothing to filter. return filtered; @@ -313,19 +313,19 @@ namespace spot } - tgba_digraph_ptr - scc_filter_states(const const_tgba_digraph_ptr& aut, scc_info* given_si) + twa_graph_ptr + scc_filter_states(const const_twa_graph_ptr& aut, scc_info* given_si) { auto res = scc_filter_apply>(aut, given_si); res->prop_copy(aut, { true, true, true, true }); return res; } - tgba_digraph_ptr - scc_filter(const const_tgba_digraph_ptr& aut, bool remove_all_useless, + twa_graph_ptr + scc_filter(const const_twa_graph_ptr& aut, bool remove_all_useless, scc_info* given_si) { - tgba_digraph_ptr res; + twa_graph_ptr res; if (remove_all_useless) res = scc_filter_applynum_states(); @@ -61,7 +61,7 @@ namespace spot int num_; // Number of visited nodes, negated. - typedef tgba_digraph::graph_t::const_iterator iterator; + typedef twa_graph::graph_t::const_iterator iterator; typedef std::pair pair_state_iter; std::stack todo_; // DFS stack. Holds (STATE, // ITERATOR) pairs where @@ -299,7 +299,7 @@ namespace spot std::ostream& dump_scc_info_dot(std::ostream& out, - const_tgba_digraph_ptr aut, scc_info* sccinfo) + const_twa_graph_ptr aut, scc_info* sccinfo) { scc_info* m = sccinfo ? sccinfo : new scc_info(aut); diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh index 9c38f0a9f..0222c6ce4 100644 --- a/src/tgbaalgos/sccinfo.hh +++ b/src/tgbaalgos/sccinfo.hh @@ -110,7 +110,7 @@ namespace spot std::vector sccof_; std::vector node_; - const_tgba_digraph_ptr aut_; + const_twa_graph_ptr aut_; const scc_node& node(unsigned scc) const @@ -120,9 +120,9 @@ namespace spot } public: - scc_info(const_tgba_digraph_ptr aut); + scc_info(const_twa_graph_ptr aut); - const_tgba_digraph_ptr get_aut() const + const_twa_graph_ptr get_aut() const { return aut_; } @@ -226,6 +226,6 @@ namespace spot /// If \a sccinfo is not given, it will be computed. SPOT_API std::ostream& dump_scc_info_dot(std::ostream& out, - const_tgba_digraph_ptr aut, scc_info* sccinfo = nullptr); + const_twa_graph_ptr aut, scc_info* sccinfo = nullptr); } diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index b6a62f83a..7569fc2c5 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -100,13 +100,13 @@ namespace spot { } - automaton_size(const tgba_digraph_ptr& a) + automaton_size(const twa_graph_ptr& a) : transitions(a->num_transitions()), states(a->num_states()) { } - void set_size(const tgba_digraph_ptr& a) + void set_size(const twa_graph_ptr& a) { states = a->num_states(); transitions = a->num_transitions(); @@ -171,7 +171,7 @@ namespace spot return res; } - acc_cond::mark_t bdd_to_mark(const tgba_digraph_ptr& aut, bdd b) + acc_cond::mark_t bdd_to_mark(const twa_graph_ptr& aut, bdd b) { // FIXME: Use a cache. std::vector res; @@ -183,7 +183,7 @@ namespace spot return aut->acc().marks(res.begin(), res.end()); } - direct_simulation(const const_tgba_digraph_ptr& in) + direct_simulation(const const_twa_graph_ptr& in) : po_size_(0), all_class_var_(bddtrue), original_(in) @@ -205,7 +205,7 @@ namespace spot // (In the case of Cosimulation, we also flip the transitions.) if (Cosimulation) { - a_ = make_tgba_digraph(in->get_dict()); + a_ = make_twa_graph(in->get_dict()); a_->copy_ap_of(in); a_->copy_acceptance_of(in); a_->new_states(ns); @@ -242,7 +242,7 @@ namespace spot } else { - a_ = make_tgba_digraph(in, twa::prop_set::all()); + a_ = make_twa_graph(in, twa::prop_set::all()); auto& acccond = a_->acc(); for (auto& t: a_->transitions()) t.acc = acccond.comp(t.acc); @@ -341,7 +341,7 @@ namespace spot } // The core loop of the algorithm. - tgba_digraph_ptr run() + twa_graph_ptr run() { main_loop(); return build_result(); @@ -481,9 +481,9 @@ namespace spot } // Build the minimal resulting automaton. - tgba_digraph_ptr build_result() + twa_graph_ptr build_result() { - tgba_digraph_ptr res = make_tgba_digraph(a_->get_dict()); + twa_graph_ptr res = make_twa_graph(a_->get_dict()); res->copy_ap_of(a_); res->copy_acceptance_of(a_); if (Sba) @@ -676,7 +676,7 @@ namespace spot protected: // The automaton which is simulated. - tgba_digraph_ptr a_; + twa_graph_ptr a_; // Relation is aimed to represent the same thing than // rel_. The difference is in the way it does. @@ -719,35 +719,35 @@ namespace spot std::unique_ptr scc_info_; - const const_tgba_digraph_ptr original_; + const const_twa_graph_ptr original_; }; } // End namespace anonymous. - tgba_digraph_ptr - simulation(const const_tgba_digraph_ptr& t) + twa_graph_ptr + simulation(const const_twa_graph_ptr& t) { direct_simulation simul(t); return simul.run(); } - tgba_digraph_ptr - simulation_sba(const const_tgba_digraph_ptr& t) + twa_graph_ptr + simulation_sba(const const_twa_graph_ptr& t) { direct_simulation simul(t); return simul.run(); } - tgba_digraph_ptr - cosimulation(const const_tgba_digraph_ptr& t) + twa_graph_ptr + cosimulation(const const_twa_graph_ptr& t) { direct_simulation simul(t); return simul.run(); } - tgba_digraph_ptr - cosimulation_sba(const const_tgba_digraph_ptr& t) + twa_graph_ptr + cosimulation_sba(const const_twa_graph_ptr& t) { direct_simulation simul(t); return simul.run(); @@ -755,10 +755,10 @@ namespace spot template - tgba_digraph_ptr - iterated_simulations_(const const_tgba_digraph_ptr& t) + twa_graph_ptr + iterated_simulations_(const const_twa_graph_ptr& t) { - tgba_digraph_ptr res = 0; + twa_graph_ptr res = 0; automaton_size prev; automaton_size next; @@ -784,14 +784,14 @@ namespace spot return res; } - tgba_digraph_ptr - iterated_simulations(const const_tgba_digraph_ptr& t) + twa_graph_ptr + iterated_simulations(const const_twa_graph_ptr& t) { return iterated_simulations_(t); } - tgba_digraph_ptr - iterated_simulations_sba(const const_tgba_digraph_ptr& t) + twa_graph_ptr + iterated_simulations_sba(const const_twa_graph_ptr& t) { return iterated_simulations_(t); } diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh index ae4013769..8e41c2c62 100644 --- a/src/tgbaalgos/simulation.hh +++ b/src/tgbaalgos/simulation.hh @@ -67,10 +67,10 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - SPOT_API tgba_digraph_ptr - simulation(const const_tgba_digraph_ptr& automaton); - SPOT_API tgba_digraph_ptr - simulation_sba(const const_tgba_digraph_ptr& automaton); + SPOT_API twa_graph_ptr + simulation(const const_twa_graph_ptr& automaton); + SPOT_API twa_graph_ptr + simulation_sba(const const_twa_graph_ptr& automaton); /// @} /// @{ @@ -120,10 +120,10 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - SPOT_API tgba_digraph_ptr - cosimulation(const const_tgba_digraph_ptr& automaton); - SPOT_API tgba_digraph_ptr - cosimulation_sba(const const_tgba_digraph_ptr& automaton); + SPOT_API twa_graph_ptr + cosimulation(const const_twa_graph_ptr& automaton); + SPOT_API twa_graph_ptr + cosimulation_sba(const const_twa_graph_ptr& automaton); /// @} /// @{ @@ -141,10 +141,10 @@ namespace spot /// \param automaton the automaton to simulate. /// \return a new automaton which is at worst a copy of the received /// one - SPOT_API tgba_digraph_ptr - iterated_simulations(const const_tgba_digraph_ptr& automaton); - SPOT_API tgba_digraph_ptr - iterated_simulations_sba(const const_tgba_digraph_ptr& automaton); + SPOT_API twa_graph_ptr + iterated_simulations(const const_twa_graph_ptr& automaton); + SPOT_API twa_graph_ptr + iterated_simulations_sba(const const_twa_graph_ptr& automaton); /// @} } // End namespace spot. diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index 43b766b7b..cf39a728c 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -161,7 +161,7 @@ namespace spot } std::ostream& - stat_printer::print(const const_tgba_digraph_ptr& aut, + stat_printer::print(const const_twa_graph_ptr& aut, const ltl::formula* f, double run_time) { diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index 2a684af77..1eece70d5 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -84,7 +84,7 @@ namespace spot /// The \a f argument is not needed if the Formula does not need /// to be output, and so is \a run_time). std::ostream& - print(const const_tgba_digraph_ptr& aut, const ltl::formula* f = 0, + print(const const_twa_graph_ptr& aut, const ltl::formula* f = 0, double run_time = -1.); private: diff --git a/src/tgbaalgos/stripacc.cc b/src/tgbaalgos/stripacc.cc index 81a1c9a4b..3bc5c2c02 100644 --- a/src/tgbaalgos/stripacc.cc +++ b/src/tgbaalgos/stripacc.cc @@ -22,7 +22,7 @@ namespace spot { - void strip_acceptance_here(tgba_digraph_ptr a) + void strip_acceptance_here(twa_graph_ptr a) { unsigned n = a->num_states(); for (unsigned s = 0; s < n; ++s) diff --git a/src/tgbaalgos/stripacc.hh b/src/tgbaalgos/stripacc.hh index 4f170075a..67286a8a1 100644 --- a/src/tgbaalgos/stripacc.hh +++ b/src/tgbaalgos/stripacc.hh @@ -24,9 +24,9 @@ namespace spot { /// \ingroup tgba_misc - /// \brief Remove all acceptance sets from a tgba_digraph. + /// \brief Remove all acceptance sets from a twa_graph. /// /// This is equivalent to marking all states/transitions as accepting. SPOT_API void - strip_acceptance_here(tgba_digraph_ptr a); + strip_acceptance_here(twa_graph_ptr a); } diff --git a/src/tgbaalgos/stutter.cc b/src/tgbaalgos/stutter.cc index 70f620777..ca33bca72 100644 --- a/src/tgbaalgos/stutter.cc +++ b/src/tgbaalgos/stutter.cc @@ -281,7 +281,7 @@ namespace spot typedef std::deque queue_t; static bdd - get_all_ap(const const_tgba_digraph_ptr& a) + get_all_ap(const const_twa_graph_ptr& a) { bdd res = bddtrue; for (auto& i: a->transitions()) @@ -291,8 +291,8 @@ namespace spot } - tgba_digraph_ptr - sl(const const_tgba_digraph_ptr& a, const ltl::formula* f) + twa_graph_ptr + sl(const const_twa_graph_ptr& a, const ltl::formula* f) { bdd aps = f ? atomic_prop_collect_as_bdd(f, a) @@ -300,8 +300,8 @@ namespace spot return sl(a, aps); } - tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f) + twa_graph_ptr + sl2(const const_twa_graph_ptr& a, const ltl::formula* f) { bdd aps = f ? atomic_prop_collect_as_bdd(f, a) @@ -309,11 +309,11 @@ namespace spot return sl2(a, aps); } - tgba_digraph_ptr - sl(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + twa_graph_ptr + sl(const const_twa_graph_ptr& a, bdd atomic_propositions) { // The result automaton uses numbered states. - tgba_digraph_ptr res = make_tgba_digraph(a->get_dict()); + twa_graph_ptr res = make_twa_graph(a->get_dict()); // We use the same BDD variables as the input. res->copy_ap_of(a); res->copy_acceptance_of(a); @@ -373,8 +373,8 @@ namespace spot return res; } - tgba_digraph_ptr - sl2(tgba_digraph_ptr&& a, bdd atomic_propositions) + twa_graph_ptr + sl2(twa_graph_ptr&& a, bdd atomic_propositions) { if (atomic_propositions == bddfalse) atomic_propositions = get_all_ap(a); @@ -439,16 +439,16 @@ namespace spot return a; } - tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + twa_graph_ptr + sl2(const const_twa_graph_ptr& a, bdd atomic_propositions) { - return sl2(make_tgba_digraph(a, twa::prop_set::all()), + return sl2(make_twa_graph(a, twa::prop_set::all()), atomic_propositions); } - tgba_digraph_ptr - closure(tgba_digraph_ptr&& a) + twa_graph_ptr + closure(twa_graph_ptr&& a) { a->prop_keep({false, // state_based false, // inherently_weak @@ -529,10 +529,10 @@ namespace spot return a; } - tgba_digraph_ptr - closure(const const_tgba_digraph_ptr& a) + twa_graph_ptr + closure(const const_twa_graph_ptr& a) { - return closure(make_tgba_digraph(a, {true, true, true, false})); + return closure(make_twa_graph(a, {true, true, true, false})); } // The stutter check algorithm to use can be overridden via an @@ -599,8 +599,8 @@ namespace spot } bool - is_stutter_invariant(tgba_digraph_ptr&& aut_f, - tgba_digraph_ptr&& aut_nf, bdd aps, int algo) + is_stutter_invariant(twa_graph_ptr&& aut_f, + twa_graph_ptr&& aut_nf, bdd aps, int algo) { if (algo == 0) algo = default_stutter_check_algorithm(); diff --git a/src/tgbaalgos/stutter.hh b/src/tgbaalgos/stutter.hh index 680539772..7bc5fe27d 100644 --- a/src/tgbaalgos/stutter.hh +++ b/src/tgbaalgos/stutter.hh @@ -23,29 +23,29 @@ namespace spot { - SPOT_API tgba_digraph_ptr - sl(const const_tgba_digraph_ptr&, const ltl::formula* = nullptr); + SPOT_API twa_graph_ptr + sl(const const_twa_graph_ptr&, const ltl::formula* = nullptr); - SPOT_API tgba_digraph_ptr - sl(const const_tgba_digraph_ptr&, bdd); + SPOT_API twa_graph_ptr + sl(const const_twa_graph_ptr&, bdd); - SPOT_API tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr&, const ltl::formula* = nullptr); + SPOT_API twa_graph_ptr + sl2(const const_twa_graph_ptr&, const ltl::formula* = nullptr); - SPOT_API tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr&, bdd); + SPOT_API twa_graph_ptr + sl2(const const_twa_graph_ptr&, bdd); #ifndef SWIG - SPOT_API tgba_digraph_ptr - sl2(tgba_digraph_ptr&&, bdd = bddfalse); + SPOT_API twa_graph_ptr + sl2(twa_graph_ptr&&, bdd = bddfalse); #endif - SPOT_API tgba_digraph_ptr - closure(const const_tgba_digraph_ptr&); + SPOT_API twa_graph_ptr + closure(const const_twa_graph_ptr&); #ifndef SWIG - SPOT_API tgba_digraph_ptr - closure(tgba_digraph_ptr&&); + SPOT_API twa_graph_ptr + closure(twa_graph_ptr&&); #endif /// \ingroup ltl_misc @@ -54,7 +54,7 @@ namespace spot is_stutter_invariant(const ltl::formula* f); SPOT_API bool - is_stutter_invariant(tgba_digraph_ptr&& aut_f, - tgba_digraph_ptr&& aut_nf, bdd aps, + is_stutter_invariant(twa_graph_ptr&& aut_f, + twa_graph_ptr&& aut_nf, bdd aps, int algo = 0); } diff --git a/src/tgbaalgos/totgba.cc b/src/tgbaalgos/totgba.cc index 210c08b45..71062928b 100644 --- a/src/tgbaalgos/totgba.cc +++ b/src/tgbaalgos/totgba.cc @@ -58,8 +58,8 @@ namespace spot /// \brief Take an automaton with any acceptance condition and return /// an equivalent Generalized Büchi automaton. - tgba_digraph_ptr - to_generalized_buchi(const const_tgba_digraph_ptr& aut) + twa_graph_ptr + to_generalized_buchi(const const_twa_graph_ptr& aut) { auto res = remove_fin(cleanup_acceptance(aut)); if (res->acc().is_generalized_buchi()) @@ -81,7 +81,7 @@ namespace spot if (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Fin) { assert(cnf.front().mark == 0U); - res = make_tgba_digraph(aut->get_dict()); + res = make_twa_graph(aut->get_dict()); res->set_init_state(res->new_state()); res->prop_state_based_acc(); res->prop_inherently_weak(); diff --git a/src/tgbaalgos/totgba.hh b/src/tgbaalgos/totgba.hh index b05e35cca..4d230398e 100644 --- a/src/tgbaalgos/totgba.hh +++ b/src/tgbaalgos/totgba.hh @@ -25,6 +25,6 @@ namespace spot { /// \brief Take an automaton with any acceptance condition and return /// an equivalent Generalized Büchi automaton. - SPOT_API tgba_digraph_ptr - to_generalized_buchi(const const_tgba_digraph_ptr& aut); + SPOT_API twa_graph_ptr + to_generalized_buchi(const const_twa_graph_ptr& aut); } diff --git a/src/tgbaalgos/translate.cc b/src/tgbaalgos/translate.cc index 24e39aa0d..1388ebdab 100644 --- a/src/tgbaalgos/translate.cc +++ b/src/tgbaalgos/translate.cc @@ -61,7 +61,7 @@ namespace spot simpl_owned_ = simpl_ = new ltl::ltl_simplifier(options, dict); } - tgba_digraph_ptr translator::run(const ltl::formula** f) + twa_graph_ptr translator::run(const ltl::formula** f) { const ltl::formula* r = simpl_->simplify(*f); (*f)->destroy(); @@ -71,7 +71,7 @@ namespace spot // natural way (improving the degeneralization). simpl_->clear_as_bdd_cache(); - tgba_digraph_ptr aut; + twa_graph_ptr aut; if (comp_susp_ > 0) { int skel_wdba = skel_wdba_; @@ -91,7 +91,7 @@ namespace spot return aut; } - tgba_digraph_ptr translator::run(const ltl::formula* f) + twa_graph_ptr translator::run(const ltl::formula* f) { f->clone(); auto aut = run(&f); diff --git a/src/tgbaalgos/translate.hh b/src/tgbaalgos/translate.hh index 08f191239..061c99e24 100644 --- a/src/tgbaalgos/translate.hh +++ b/src/tgbaalgos/translate.hh @@ -102,14 +102,14 @@ namespace spot /// /// The formula \a f is simplified internally, but it is not /// not destroyed (this is the responsibility of the caller). - tgba_digraph_ptr run(const ltl::formula* f); + twa_graph_ptr run(const ltl::formula* f); /// \brief Convert \a f into an automaton, and update f. /// /// The formula *f is destroyed, and replaced /// by the simplified version, which should be destroyed by /// the caller. - tgba_digraph_ptr run(const ltl::formula** f); + twa_graph_ptr run(const ltl::formula** f); protected: void setup_opt(const option_map* opt); diff --git a/src/tgbatest/checkpsl.cc b/src/tgbatest/checkpsl.cc index 7e7ef0ee6..417195370 100644 --- a/src/tgbatest/checkpsl.cc +++ b/src/tgbatest/checkpsl.cc @@ -93,10 +93,10 @@ main(int argc, char** argv) if (fpos->is_ltl_formula()) { auto apos = - scc_filter(make_tgba_digraph(ltl_to_taa(fpos, d), + scc_filter(make_twa_graph(ltl_to_taa(fpos, d), spot::twa::prop_set::all())); auto aneg = - scc_filter(make_tgba_digraph(ltl_to_taa(fneg, d), + scc_filter(make_twa_graph(ltl_to_taa(fneg, d), spot::twa::prop_set::all())); if (!spot::product(apos, aneg)->is_empty()) { diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index b00a2e9dc..4c43ca3fd 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -125,7 +125,7 @@ int main(int argc, char* argv[]) auto h = spot::hoa_parse(file, pel, dict, env); if (spot::format_hoa_parse_errors(std::cerr, file, pel)) return 2; - spot::tgba_digraph_ptr a = h->aut; + spot::twa_graph_ptr a = h->aut; spot::tgba_ptr complement = 0; @@ -163,7 +163,7 @@ int main(int argc, char* argv[]) } else if (stats) { - spot::tgba_digraph_ptr a; + spot::twa_graph_ptr a; const spot::ltl::formula* f1 = 0; if (formula) diff --git a/src/tgbatest/emptchk.cc b/src/tgbatest/emptchk.cc index 33e4a9a76..8b53f261d 100644 --- a/src/tgbatest/emptchk.cc +++ b/src/tgbatest/emptchk.cc @@ -103,7 +103,7 @@ main(int argc, char** argv) auto a = spot::ltl_to_taa(f, d); aut[0] = a; auto all = spot::twa::prop_set::all(); - aut[1] = spot::degeneralize_tba(spot::make_tgba_digraph(a, all)); + aut[1] = spot::degeneralize_tba(spot::make_twa_graph(a, all)); } { auto a = spot::ltl_to_tgba_fm(f, d); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 78c23e647..5b4c5b9f4 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -309,12 +309,12 @@ to_int(const char* s) return res; } -spot::tgba_digraph_ptr ensure_digraph(const spot::tgba_ptr& a) +spot::twa_graph_ptr ensure_digraph(const spot::tgba_ptr& a) { - auto aa = std::dynamic_pointer_cast(a); + auto aa = std::dynamic_pointer_cast(a); if (aa) return aa; - return spot::make_tgba_digraph(a, spot::twa::prop_set::all()); + return spot::make_twa_graph(a, spot::twa::prop_set::all()); } int @@ -1289,7 +1289,7 @@ checked_main(int argc, char** argv) if (scc_filter && (reduction_dir_sim || reduction_rev_sim)) { tm.start("SCC-filter post-sim"); - auto aa = std::dynamic_pointer_cast(a); + auto aa = std::dynamic_pointer_cast(a); assert(aa); // Do not filter_all for SBA a = spot::scc_filter(aa, assume_sba ? @@ -1495,7 +1495,7 @@ checked_main(int argc, char** argv) case 10: { auto aa = - std::dynamic_pointer_cast(a); + std::dynamic_pointer_cast(a); if (!aa) dump_scc_dot(a, std::cout, false); else @@ -1504,8 +1504,8 @@ checked_main(int argc, char** argv) break; case 11: { - //const spot::tgba_digraph_ptr g = - // dynamic_cast(a); + //const spot::twa_graph_ptr g = + // dynamic_cast(a); //if (!g) dump_scc_dot(a, std::cout, true); //else diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 328710a93..e94d4f8db 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -83,8 +83,8 @@ const char* default_algos[] = { std::vector ec_algos; spot::emptiness_check_ptr -cons_emptiness_check(int num, spot::const_tgba_digraph_ptr a, - const spot::const_tgba_digraph_ptr& degen, +cons_emptiness_check(int num, spot::const_twa_graph_ptr a, + const spot::const_twa_graph_ptr& degen, unsigned int n_acc) { auto inst = ec_algos[num].inst; @@ -579,8 +579,8 @@ main(int argc, char** argv) bool stop_on_first_difference = false; - spot::tgba_digraph_ptr formula = nullptr; - spot::tgba_digraph_ptr product = nullptr; + spot::twa_graph_ptr formula = nullptr; + spot::twa_graph_ptr product = nullptr; spot::option_map options; @@ -909,7 +909,7 @@ main(int argc, char** argv) spot::srand(opt_ec_seed); - spot::tgba_digraph_ptr a = + spot::twa_graph_ptr a = spot::random_graph(opt_n, opt_d, apf, dict, opt_n_acc, opt_a, opt_t, opt_det); if (formula) @@ -928,7 +928,7 @@ main(int argc, char** argv) } else { - spot::tgba_digraph_ptr degen = nullptr; + spot::twa_graph_ptr degen = nullptr; if (opt_degen && real_n_acc > 1) degen = degeneralize_tba(a); diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 4c7e8e996..3e195ea63 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -49,7 +49,7 @@ %shared_ptr(spot::tgta_explicit) %shared_ptr(spot::bdd_dict) %shared_ptr(spot::twa) -%shared_ptr(spot::tgba_digraph) +%shared_ptr(spot::twa_graph) %shared_ptr(spot::tgba_product) %shared_ptr(spot::tgba_product_init) %shared_ptr(spot::taa_tgba) @@ -256,7 +256,7 @@ using namespace spot; %include "tgba/tgbaproduct.hh" %include "tgba/tgbagraph.hh" -// Should come after the definition of tgba_digraph +// Should come after the definition of twa_graph %include "tgbaalgos/cleanacc.hh" %include "tgbaalgos/degen.hh" @@ -375,13 +375,13 @@ empty_hoa_parse_error_list() return l; } -spot::tgba_digraph_ptr +spot::twa_graph_ptr ensure_digraph(const spot::tgba_ptr& a) { - auto aa = std::dynamic_pointer_cast(a); + auto aa = std::dynamic_pointer_cast(a); if (aa) return aa; - return spot::make_tgba_digraph(a, spot::twa::prop_set::all()); + return spot::make_twa_graph(a, spot::twa::prop_set::all()); } std::ostream& diff --git a/wrap/python/tests/automata-io.ipynb b/wrap/python/tests/automata-io.ipynb index c0c3179f2..c4e8c8a1c 100644 --- a/wrap/python/tests/automata-io.ipynb +++ b/wrap/python/tests/automata-io.ipynb @@ -161,7 +161,7 @@ "\n" ], "text": [ - " *' at 0x7f48240566f0> >" + " *' at 0x7f48240566f0> >" ] } ], @@ -272,7 +272,7 @@ "\n" ], "text": [ - " *' at 0x7f4824056960> >" + " *' at 0x7f4824056960> >" ] }, { @@ -329,7 +329,7 @@ "\n" ], "text": [ - " *' at 0x7f4824056990> >" + " *' at 0x7f4824056990> >" ] } ], @@ -448,7 +448,7 @@ "\n" ], "text": [ - " *' at 0x7f4824056ba0> >" + " *' at 0x7f4824056ba0> >" ] } ], @@ -563,7 +563,7 @@ "\n" ], "text": [ - " *' at 0x7f4824056d20> >" + " *' at 0x7f4824056d20> >" ] }, { diff --git a/wrap/python/tests/automata.ipynb b/wrap/python/tests/automata.ipynb index 2b0f14ae5..a30adae99 100644 --- a/wrap/python/tests/automata.ipynb +++ b/wrap/python/tests/automata.ipynb @@ -171,7 +171,7 @@ "\n" ], "text": [ - " *' at 0x105ac14b0> >" + " *' at 0x105ac14b0> >" ] } ], @@ -542,7 +542,7 @@ "\n" ], "text": [ - " *' at 0x10747f180> >" + " *' at 0x10747f180> >" ] } ], @@ -612,7 +612,7 @@ "\n" ], "text": [ - " *' at 0x10747f210> >" + " *' at 0x10747f210> >" ] } ], @@ -681,7 +681,7 @@ "\n" ], "text": [ - " *' at 0x10747f0f0> >" + " *' at 0x10747f0f0> >" ] } ], @@ -1080,7 +1080,7 @@ "\n" ], "text": [ - " *' at 0x10747f2d0> >" + " *' at 0x10747f2d0> >" ] } ], @@ -1554,7 +1554,7 @@ "\n" ], "text": [ - " *' at 0x105b2ed80> >" + " *' at 0x105b2ed80> >" ] } ], @@ -1750,7 +1750,7 @@ "\n" ], "text": [ - " *' at 0x105b2ec90> >" + " *' at 0x105b2ec90> >" ] } ], @@ -1771,4 +1771,4 @@ "metadata": {} } ] -} \ No newline at end of file +} diff --git a/wrap/python/tests/piperead.ipynb b/wrap/python/tests/piperead.ipynb index e744e9c83..c85f9fd27 100644 --- a/wrap/python/tests/piperead.ipynb +++ b/wrap/python/tests/piperead.ipynb @@ -117,7 +117,7 @@ "\n" ], "text": [ - " *' at 0x7f3b24ce6630> >" + " *' at 0x7f3b24ce6630> >" ] }, { @@ -169,7 +169,7 @@ "\n" ], "text": [ - " *' at 0x7f3b24ce6720> >" + " *' at 0x7f3b24ce6720> >" ] }, { @@ -215,7 +215,7 @@ "\n" ], "text": [ - " *' at 0x7f3b24ce67e0> >" + " *' at 0x7f3b24ce67e0> >" ] }, { @@ -272,7 +272,7 @@ "\n" ], "text": [ - " *' at 0x7f3b24ce68a0> >" + " *' at 0x7f3b24ce68a0> >" ] } ], @@ -349,7 +349,7 @@ "\n" ], "text": [ - " *' at 0x7f3b24ce6960> >" + " *' at 0x7f3b24ce6960> >" ] } ], @@ -452,7 +452,7 @@ "\n" ], "text": [ - " *' at 0x7f3b24ce6720> >" + " *' at 0x7f3b24ce6720> >" ] }, { diff --git a/wrap/python/tests/testingaut.ipynb b/wrap/python/tests/testingaut.ipynb index 804cbf41f..b0ac6a053 100644 --- a/wrap/python/tests/testingaut.ipynb +++ b/wrap/python/tests/testingaut.ipynb @@ -102,7 +102,7 @@ "\n" ], "text": [ - " *' at 0x7f1eb80416f0> >" + " *' at 0x7f1eb80416f0> >" ] } ],