From 8ea5f73c1a20964faa46c993faef4b12cbfb8697 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 4 Nov 2015 18:25:49 +0100 Subject: [PATCH] twa: no default argument for property setters This is a preliminary for the renaming suggested in #116. * src/twa/twa.hh (prop_state_based_acc, prop_inherently_weak, prop_deterministic, prop_unambiguous, prop_stutter_invariant, prop_stutter_sensitive): Do not default the argument to true. * src/parseaut/parseaut.yy, src/twaalgos/degen.cc, src/twaalgos/dtbasat.cc, src/twaalgos/dtgbasat.cc, src/twaalgos/minimize.cc, src/twaalgos/randomgraph.cc, src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc, src/twaalgos/simulation.cc, src/twaalgos/totgba.cc, wrap/python/tests/remfin.py: Adjust. --- src/parseaut/parseaut.yy | 10 +++++----- src/twa/twa.hh | 18 +++++++++--------- src/twaalgos/degen.cc | 2 +- src/twaalgos/dtbasat.cc | 4 ++-- src/twaalgos/dtgbasat.cc | 4 ++-- src/twaalgos/minimize.cc | 12 ++++++------ src/twaalgos/randomgraph.cc | 4 ++-- src/twaalgos/remfin.cc | 6 +++--- src/twaalgos/sbacc.cc | 2 +- src/twaalgos/simulation.cc | 4 ++-- src/twaalgos/totgba.cc | 8 ++++---- wrap/python/tests/remfin.py | 2 +- 12 files changed, 38 insertions(+), 38 deletions(-) diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index fd5c3b0f5..722c8bac3 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -1158,8 +1158,8 @@ dstar_header: dstar_sizes res.h->aut->new_states(res.states);; res.info_states.resize(res.states); } - res.h->aut->prop_state_based_acc(); - res.h->aut->prop_deterministic(); + res.h->aut->prop_state_based_acc(true); + res.h->aut->prop_deterministic(true); // res.h->aut->prop_complete(); fill_guards(res); res.cur_guard = res.guards.end(); @@ -1303,7 +1303,7 @@ dstar_states: never: "never" { res.namer = res.h->aut->create_namer(); res.h->aut->set_buchi(); - res.h->aut->prop_state_based_acc(); + res.h->aut->prop_state_based_acc(true); res.acc_state = State_Acc; res.pos_acc_sets = res.h->aut->acc().all_sets(); } @@ -1560,7 +1560,7 @@ lbtt-header-states: LBTT lbtt-header: lbtt-header-states INT_S { res.acc_mapper = new spot::acc_mapper_int(res.h->aut, $2); - res.h->aut->prop_state_based_acc(); + res.h->aut->prop_state_based_acc(true); res.acc_state = State_Acc; } | lbtt-header-states INT @@ -1869,7 +1869,7 @@ static void fix_properties(result_& r) //r.h->aut->prop_complete(r.complete); if (r.acc_style == State_Acc || (r.acc_style == Mixed_Acc && !r.trans_acc_seen)) - r.h->aut->prop_state_based_acc(); + r.h->aut->prop_state_based_acc(true); } static void check_version(const result_& r) diff --git a/src/twa/twa.hh b/src/twa/twa.hh index cf1adc5ca..885e602e9 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -706,7 +706,7 @@ namespace spot set_num_sets_(num); acc_.set_acceptance(c); if (num == 0) - prop_state_based_acc(); + prop_state_based_acc(true); } /// \brief Copy the acceptance condition of another tgba. @@ -715,7 +715,7 @@ namespace spot acc_ = a->acc(); unsigned num = acc_.num_sets(); if (num == 0) - prop_state_based_acc(); + prop_state_based_acc(true); } void copy_ap_of(const const_twa_ptr& a) @@ -730,7 +730,7 @@ namespace spot set_num_sets_(num); acc_.set_generalized_buchi(); if (num == 0) - prop_state_based_acc(); + prop_state_based_acc(true); } acc_cond::mark_t set_buchi() @@ -810,7 +810,7 @@ namespace spot return is.state_based_acc; } - void prop_state_based_acc(bool val = true) + void prop_state_based_acc(bool val) { is.state_based_acc = val; } @@ -825,7 +825,7 @@ namespace spot return is.inherently_weak; } - void prop_inherently_weak(bool val = true) + void prop_inherently_weak(bool val) { is.inherently_weak = val; } @@ -835,7 +835,7 @@ namespace spot return is.deterministic; } - void prop_deterministic(bool val = true) + void prop_deterministic(bool val) { is.deterministic = val; } @@ -845,7 +845,7 @@ namespace spot return is.unambiguous; } - void prop_unambiguous(bool val = true) + void prop_unambiguous(bool val) { is.unambiguous = val; } @@ -860,12 +860,12 @@ namespace spot return is.stutter_sensitive; } - void prop_stutter_invariant(bool val = true) + void prop_stutter_invariant(bool val) { is.stutter_invariant = val; } - void prop_stutter_sensitive(bool val = true) + void prop_stutter_sensitive(bool val) { is.stutter_sensitive = val; } diff --git a/src/twaalgos/degen.cc b/src/twaalgos/degen.cc index 2a3f65a57..712179639 100644 --- a/src/twaalgos/degen.cc +++ b/src/twaalgos/degen.cc @@ -207,7 +207,7 @@ namespace spot res->copy_ap_of(a); res->set_buchi(); if (want_sba) - res->prop_state_based_acc(); + res->prop_state_based_acc(true); // Preserve determinism, weakness, and stutter-invariance res->prop_copy(a, { false, true, true, true }); diff --git a/src/twaalgos/dtbasat.cc b/src/twaalgos/dtbasat.cc index ba41867ab..bc1ef9caa 100644 --- a/src/twaalgos/dtbasat.cc +++ b/src/twaalgos/dtbasat.cc @@ -640,8 +640,8 @@ namespace spot a->copy_ap_of(aut); acc_cond::mark_t acc = a->set_buchi(); if (state_based) - a->prop_state_based_acc(); - a->prop_deterministic(); + a->prop_state_based_acc(true); + a->prop_deterministic(true); a->new_states(satdict.cand_size); unsigned last_aut_trans = -1U; diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index 09ac57911..d193e40ed 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -1026,8 +1026,8 @@ namespace spot auto a = make_twa_graph(autdict); a->copy_ap_of(aut); if (state_based) - a->prop_state_based_acc(); - a->prop_deterministic(); + a->prop_state_based_acc(true); + a->prop_deterministic(true); a->set_acceptance(satdict.cand_nacc, satdict.cand_acc); a->new_states(satdict.cand_size); diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index dc466697f..eb6127733 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -122,7 +122,7 @@ namespace spot auto dict = a->get_dict(); auto res = make_twa_graph(dict); res->copy_ap_of(a); - res->prop_state_based_acc(); + res->prop_state_based_acc(true); // For each set, create a state in the resulting automaton. // For a state s, state_num[s] is the number of the state in the minimal @@ -481,9 +481,9 @@ namespace spot build_state_set(det_a, non_final); auto res = minimize_dfa(det_a, final, non_final); res->prop_copy(a, { false, false, false, true }); - res->prop_deterministic(); - res->prop_inherently_weak(); - res->prop_state_based_acc(); + res->prop_deterministic(true); + res->prop_inherently_weak(true); + res->prop_state_based_acc(true); return res; } @@ -582,8 +582,8 @@ namespace spot auto res = minimize_dfa(det_a, final, non_final); res->prop_copy(a, { false, false, false, true }); - res->prop_deterministic(); - res->prop_inherently_weak(); + res->prop_deterministic(true); + res->prop_inherently_weak(true); return res; } diff --git a/src/twaalgos/randomgraph.cc b/src/twaalgos/randomgraph.cc index 41e3d95fb..644401746 100644 --- a/src/twaalgos/randomgraph.cc +++ b/src/twaalgos/randomgraph.cc @@ -130,9 +130,9 @@ namespace spot throw std::invalid_argument("random_graph() requires n>0 states"); auto res = make_twa_graph(dict); if (deterministic) - res->prop_deterministic(); + res->prop_deterministic(true); if (state_acc) - res->prop_state_based_acc(); + res->prop_state_based_acc(true); int props_n = ap->size(); int* props = new int[props_n]; diff --git a/src/twaalgos/remfin.cc b/src/twaalgos/remfin.cc index e65ad92b2..28a38b0f9 100644 --- a/src/twaalgos/remfin.cc +++ b/src/twaalgos/remfin.cc @@ -468,8 +468,8 @@ namespace spot // We will modify res in place, and the resulting // automaton will only have one acceptance set. acc_cond::mark_t all_acc = res->set_buchi(); - res->prop_state_based_acc(); - res->prop_deterministic(); + res->prop_state_based_acc(true); + res->prop_deterministic(true); unsigned sink = res->num_states(); for (unsigned src = 0; src < sink; ++src) @@ -746,7 +746,7 @@ namespace spot // If the input had no Inf, the output is a state-based automaton. if (allinf == 0U) - res->prop_state_based_acc(); + res->prop_state_based_acc(true); res->purge_dead_states(); trace << "before cleanup: " << res->get_acceptance() << '\n'; diff --git a/src/twaalgos/sbacc.cc b/src/twaalgos/sbacc.cc index b1f9e6684..bee851530 100644 --- a/src/twaalgos/sbacc.cc +++ b/src/twaalgos/sbacc.cc @@ -33,7 +33,7 @@ namespace spot res->copy_ap_of(old); res->copy_acceptance_of(old); res->prop_copy(old, {false, true, true, true}); - res->prop_state_based_acc(); + res->prop_state_based_acc(true); typedef std::pair pair_t; std::map s2n; diff --git a/src/twaalgos/simulation.cc b/src/twaalgos/simulation.cc index 966e8343b..23d97d877 100644 --- a/src/twaalgos/simulation.cc +++ b/src/twaalgos/simulation.cc @@ -640,9 +640,9 @@ namespace spot true, // stutter inv. }); if (nb_minato == nb_satoneset && !Cosimulation) - res->prop_deterministic(); + res->prop_deterministic(true); if (Sba) - res->prop_state_based_acc(); + res->prop_state_based_acc(true); return res; } diff --git a/src/twaalgos/totgba.cc b/src/twaalgos/totgba.cc index 9657a23b1..6a4a4ee56 100644 --- a/src/twaalgos/totgba.cc +++ b/src/twaalgos/totgba.cc @@ -334,10 +334,10 @@ namespace spot assert(cnf.front().mark == 0U); res = make_twa_graph(aut->get_dict()); res->set_init_state(res->new_state()); - res->prop_state_based_acc(); - res->prop_inherently_weak(); - res->prop_deterministic(); - res->prop_stutter_invariant(); + res->prop_state_based_acc(true); + res->prop_inherently_weak(true); + res->prop_deterministic(true); + res->prop_stutter_invariant(true); return res; } diff --git a/wrap/python/tests/remfin.py b/wrap/python/tests/remfin.py index 71b2a933d..8b1c7d96e 100644 --- a/wrap/python/tests/remfin.py +++ b/wrap/python/tests/remfin.py @@ -18,7 +18,7 @@ State: 2 [t] 2 --END-- """) -aut.prop_inherently_weak() +aut.prop_inherently_weak(True) aut = spot.dtwa_complement(aut) aut1 = spot.scc_filter_states(aut) assert(aut1.to_str('hoa') == """HOA: v1