From b09c293f1a9a5c9c402d508392a065d9efec8728 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Fri, 2 Mar 2018 16:15:19 +0100 Subject: [PATCH] Clean the usage of spot::acc_cond::mark_t spot::acc_cond::mark_t is implemented as a bit vector using a single unsigned, and implicit conversions between mark_t and unsigned may be confusing. We try to use the proper interface. * bin/autfilt.cc, bin/ltlsynt.cc, spot/kripke/kripke.cc, spot/misc/game.hh, spot/parseaut/parseaut.yy, spot/priv/accmap.hh, spot/ta/ta.cc, spot/ta/taexplicit.cc, spot/ta/taproduct.cc, spot/taalgos/emptinessta.cc, spot/taalgos/tgba2ta.cc, spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/taatgba.cc, spot/twa/taatgba.hh, spot/twa/twagraph.hh, spot/twaalgos/alternation.cc, spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc, spot/twaalgos/complete.cc, spot/twaalgos/couvreurnew.cc, spot/twaalgos/degen.cc, spot/twaalgos/dot.cc, spot/twaalgos/dtwasat.cc, spot/twaalgos/dualize.cc, spot/twaalgos/emptiness.cc, spot/twaalgos/gtec/ce.cc, spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gtec/sccstack.cc, spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/lbtt.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc, spot/twaalgos/ndfs_result.hxx, spot/twaalgos/rabin2parity.cc, spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc, spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc, spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh, spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc, spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc, spot/twaalgos/stripacc.cc, spot/twaalgos/stutter.cc, spot/twaalgos/sum.cc, spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc, spot/twaalgos/toweak.cc, python/spot/impl.i, tests/core/acc.cc, tests/core/twagraph.cc: do not confuse mark_t and unsigned * tests/python/acc_cond.ipynb: warn about possible change of the API --- bin/autfilt.cc | 2 +- bin/ltlsynt.cc | 6 +- python/spot/impl.i | 2 +- spot/kripke/kripke.cc | 4 +- spot/misc/game.hh | 4 +- spot/parseaut/parseaut.yy | 24 ++++---- spot/priv/accmap.hh | 8 +-- spot/ta/ta.cc | 2 +- spot/ta/taexplicit.cc | 2 +- spot/ta/taproduct.cc | 2 +- spot/taalgos/emptinessta.cc | 2 +- spot/taalgos/tgba2ta.cc | 8 +-- spot/twa/acc.cc | 86 +++++++++++++------------- spot/twa/acc.hh | 108 ++++++++++++++++++--------------- spot/twa/taatgba.cc | 4 +- spot/twa/taatgba.hh | 6 +- spot/twa/twagraph.hh | 17 ++++-- spot/twaalgos/alternation.cc | 8 ++- spot/twaalgos/cleanacc.cc | 14 ++--- spot/twaalgos/cobuchi.cc | 6 +- spot/twaalgos/complete.cc | 2 +- spot/twaalgos/couvreurnew.cc | 8 +-- spot/twaalgos/degen.cc | 4 +- spot/twaalgos/dot.cc | 6 +- spot/twaalgos/dtwasat.cc | 26 ++++---- spot/twaalgos/dualize.cc | 6 +- spot/twaalgos/emptiness.cc | 8 +-- spot/twaalgos/gtec/ce.cc | 4 +- spot/twaalgos/gtec/gtec.cc | 2 +- spot/twaalgos/gtec/sccstack.cc | 2 +- spot/twaalgos/gv04.cc | 2 +- spot/twaalgos/hoa.cc | 6 +- spot/twaalgos/lbtt.cc | 2 +- spot/twaalgos/ltl2tgba_fm.cc | 2 +- spot/twaalgos/magic.cc | 2 +- spot/twaalgos/ndfs_result.hxx | 10 +-- spot/twaalgos/rabin2parity.cc | 6 +- spot/twaalgos/randomgraph.cc | 4 +- spot/twaalgos/remfin.cc | 49 +++++++-------- spot/twaalgos/sbacc.cc | 10 +-- spot/twaalgos/sccfilter.cc | 6 +- spot/twaalgos/sccinfo.cc | 13 ++-- spot/twaalgos/sccinfo.hh | 2 +- spot/twaalgos/se05.cc | 2 +- spot/twaalgos/sepsets.cc | 8 +-- spot/twaalgos/simulation.cc | 8 +-- spot/twaalgos/strength.cc | 4 +- spot/twaalgos/stripacc.cc | 2 +- spot/twaalgos/stutter.cc | 8 +-- spot/twaalgos/sum.cc | 6 +- spot/twaalgos/tau03.cc | 4 +- spot/twaalgos/tau03opt.cc | 8 +-- spot/twaalgos/totgba.cc | 65 ++++++++++---------- spot/twaalgos/toweak.cc | 9 +-- tests/core/acc.cc | 4 +- tests/core/twagraph.cc | 8 +-- tests/python/acc_cond.ipynb | 8 ++- 57 files changed, 333 insertions(+), 308 deletions(-) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 75a3227e3..37ca9fa65 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -599,7 +599,7 @@ static bool opt_complement = false; static bool opt_complement_acc = false; static char* opt_decompose_scc = nullptr; static bool opt_dualize = false; -static spot::acc_cond::mark_t opt_mask_acc = 0U; +static spot::acc_cond::mark_t opt_mask_acc = {}; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; static bool opt_simpl_acc = false; diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 7d10a74c7..a7bd73ae0 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -173,7 +173,7 @@ namespace unsigned q = split->new_state(); bdd in = bdd_existcomp(cube, input_bdd); bdd out = bdd_exist(cube, input_bdd); - split->new_edge(src, q, in, 0); + split->new_edge(src, q, in, {}); split->new_edge(q, e.dst, out, e.acc); } } @@ -264,7 +264,7 @@ namespace todo.push_back(e2.dst); } aut->new_edge(pg2aut[s], pg2aut[e2.dst], - (e1.cond & out), 0); + (e1.cond & out), {}); break; } ++i; diff --git a/python/spot/impl.i b/python/spot/impl.i index 54cbb631e..9043c6676 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -881,7 +881,7 @@ def state_is_accepting(self, src) -> "bool": %extend spot::twa_graph { unsigned new_univ_edge(unsigned src, const std::vector& v, - bdd cond, acc_cond::mark_t acc = 0U) + bdd cond, acc_cond::mark_t acc = {}) { return self->new_univ_edge(src, v.begin(), v.end(), cond, acc); } diff --git a/spot/kripke/kripke.cc b/spot/kripke/kripke.cc index 07beb6b10..56b2addbd 100644 --- a/spot/kripke/kripke.cc +++ b/spot/kripke/kripke.cc @@ -40,7 +40,7 @@ namespace spot { // Do not assert(!done()) here. It is OK to call // this function on a state without successor. - return 0U; + return {}; } kripke::~kripke() @@ -50,6 +50,6 @@ namespace spot acc_cond::mark_t kripke::state_acceptance_mark(const state*) const { - return 0U; + return {}; } } diff --git a/spot/misc/game.hh b/spot/misc/game.hh index f86c86c7b..280030712 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -265,7 +265,7 @@ public: acc_cond::mark_t acc() const override { - return 0; + return {}; } }; diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index b138443a7..f926d28b6 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -115,8 +115,8 @@ extern "C" int strverscmp(const char *s1, const char *s2); spot::location state_label_loc; spot::location accset_loc; spot::acc_cond::mark_t acc_state; - spot::acc_cond::mark_t neg_acc_sets = 0U; - spot::acc_cond::mark_t pos_acc_sets = 0U; + spot::acc_cond::mark_t neg_acc_sets = {}; + spot::acc_cond::mark_t pos_acc_sets = {}; int plus; int minus; std::vector* state_names = nullptr; @@ -1366,19 +1366,19 @@ acc-sig: '{' acc-sets '}' } acc-sets: { - $$ = spot::acc_cond::mark_t(0U); + $$ = spot::acc_cond::mark_t({}); } | acc-sets acc-set { if (res.ignore_acc || $2 == -1U) - $$ = spot::acc_cond::mark_t(0U); + $$ = spot::acc_cond::mark_t({}); else $$ = $1 | res.aut_or_ks->acc().mark($2); } state-acc_opt: { - $$ = spot::acc_cond::mark_t(0U); + $$ = spot::acc_cond::mark_t({}); } | acc-sig { @@ -1393,7 +1393,7 @@ state-acc_opt: } trans-acc_opt: { - $$ = spot::acc_cond::mark_t(0U); + $$ = spot::acc_cond::mark_t({}); } | acc-sig { @@ -1686,7 +1686,7 @@ sign: '+' { $$ = res.plus; } // Membership to a pair is represented as (+NUM,-NUM) dstar_accsigs: { - $$ = 0U; + $$ = spot::acc_cond::mark_t({}); } | dstar_accsigs sign INT { @@ -1830,7 +1830,7 @@ nc-state: res.accept_all_seen = true; auto acc = !strncmp("accept", $1->c_str(), 6) ? - res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U); + res.h->aut->acc().all_sets() : spot::acc_cond::mark_t({}); res.namer->new_edge(*$1, *$1, bddtrue, acc); delete $1; } @@ -1839,7 +1839,7 @@ nc-state: | nc-ident-list nc-transition-block { auto acc = !strncmp("accept", $1->c_str(), 6) ? - res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U); + res.h->aut->acc().all_sets() : spot::acc_cond::mark_t({}); for (auto& p: *$2) { bdd c = bdd_from_int(p.first); @@ -2041,7 +2041,7 @@ lbtt-state: STATE_NUM INT lbtt-acc std::vector{res.cur_state}); res.acc_state = $3; } -lbtt-acc: { $$ = 0U; } +lbtt-acc: { $$ = spot::acc_cond::mark_t({}); } | lbtt-acc ACC { $$ = $1; @@ -2183,7 +2183,7 @@ fix_acceptance_aux(spot::acc_cond& acc, { auto m = in[pos - 1].mark; auto c = acc.fin(onlyneg & m); - spot::acc_cond::mark_t tmp = 0U; + spot::acc_cond::mark_t tmp = {}; for (auto i: both.sets()) { if (m.has(i)) @@ -2198,7 +2198,7 @@ fix_acceptance_aux(spot::acc_cond& acc, { auto m = in[pos - 1].mark; auto c = acc.inf(onlyneg & m); - spot::acc_cond::mark_t tmp = 0U; + spot::acc_cond::mark_t tmp = {}; for (auto i: both.sets()) { if (m.has(i)) diff --git a/spot/priv/accmap.hh b/spot/priv/accmap.hh index 2030fb962..f83a58f15 100644 --- a/spot/priv/accmap.hh +++ b/spot/priv/accmap.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Developpement de +// Copyright (C) 2014, 2018 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -63,7 +63,7 @@ namespace spot { auto p = map_.find(name); if (p == map_.end()) - return std::make_pair(false, 0U); + return std::make_pair(false, acc_cond::mark_t({})); return std::make_pair(true, acc_cond::mark_t({p->second})); } }; @@ -85,7 +85,7 @@ namespace spot if (n < aut_->acc().num_sets()) return std::make_pair(true, acc_cond::mark_t({n})); else - return std::make_pair(false, 0U); + return std::make_pair(false, acc_cond::mark_t({})); } }; @@ -113,7 +113,7 @@ namespace spot map_[n] = res; return std::make_pair(true, res); } - return std::make_pair(false, 0U); + return std::make_pair(false, acc_cond::mark_t({})); } }; } diff --git a/spot/ta/ta.cc b/spot/ta/ta.cc index 84d3db390..13a766801 100644 --- a/spot/ta/ta.cc +++ b/spot/ta/ta.cc @@ -29,7 +29,7 @@ namespace spot { index = i; is_accepting = false; - condition = 0U; + condition = {}; } scc_stack_ta::connected_component& diff --git a/spot/ta/taexplicit.cc b/spot/ta/taexplicit.cc index 457bf0ff8..b552c1f42 100644 --- a/spot/ta/taexplicit.cc +++ b/spot/ta/taexplicit.cc @@ -391,7 +391,7 @@ namespace spot { auto i = down_cast(get_artificial_initial_state()); - create_transition(i, condition, 0U, s); + create_transition(i, condition, {}, s); } } diff --git a/spot/ta/taproduct.cc b/spot/ta/taproduct.cc index f5728560d..244ce9467 100644 --- a/spot/ta/taproduct.cc +++ b/spot/ta/taproduct.cc @@ -184,7 +184,7 @@ namespace spot //if stuttering transition, the TA automata stays in the same state current_state_ = new state_ta_product(source_->get_ta_state(), kripke_current_dest_state->clone()); - current_acceptance_conditions_ = 0U; + current_acceptance_conditions_ = {}; return true; } diff --git a/spot/taalgos/emptinessta.cc b/spot/taalgos/emptinessta.cc index 152afc110..b5a9ec93d 100644 --- a/spot/taalgos/emptinessta.cc +++ b/spot/taalgos/emptinessta.cc @@ -109,7 +109,7 @@ namespace spot } scc.push(++num); - arc.push(0U); + arc.push({}); ta_succ_iterator_product* iter = a_->succ_iter(init); iter->first(); diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index e088ffa18..4df1a8ce8 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -175,7 +175,7 @@ namespace spot } sscc.push(++num); - arc.push(0U); + arc.push({}); sscc.top().is_accepting = testing_aut->is_accepting_state(init); twa_succ_iterator* iter = testing_aut->succ_iter(init); @@ -407,7 +407,7 @@ namespace spot twa_succ_iterator* it = tgba_->succ_iter(tgba_init_state); it->first(); if (!it->done()) - is_acc = it->acc() != 0U; + is_acc = !!it->acc(); delete it; } @@ -459,7 +459,7 @@ namespace spot twa_succ_iterator* it = tgba_->succ_iter(tgba_state); it->first(); if (!it->done()) - is_acc = it->acc() != 0U; + is_acc = !!it->acc(); delete it; } @@ -631,7 +631,7 @@ namespace spot if (state->compare(ta->get_artificial_initial_state())) ta->create_transition(state, bdd_stutering_transition, - 0U, state); + {}, state); state->set_livelock_accepting_state(false); state->set_accepting_state(false); diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 1b94f802e..92e339cf8 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -34,13 +34,13 @@ namespace spot { std::ostream& operator<<(std::ostream& os, spot::acc_cond::mark_t m) { - auto a = m.id; + auto a = m; os << '{'; unsigned level = 0; const char* comma = ""; while (a) { - if (a & 1) + if (a.has(0)) { os << comma << level; comma = ","; @@ -129,8 +129,8 @@ namespace spot SPOT_FALLTHROUGH; case acc_cond::acc_op::Inf: { - auto a = code[pos - 1].mark.id; - if (a == 0U) + auto a = code[pos - 1].mark; + if (!a) { if (style == LATEX) os << "\\mathsf{t}"; @@ -164,7 +164,7 @@ namespace spot const char* inf_ = (style == LATEX) ? "\\mathsf{Inf}(" : "Inf("; while (a) { - if (a & 1) + if (a.has(0)) { os << and_ << inf_ << negated_pre; set_printer(os, level); @@ -184,8 +184,8 @@ namespace spot SPOT_FALLTHROUGH; case acc_cond::acc_op::Fin: { - auto a = code[pos - 1].mark.id; - if (a == 0U) + auto a = code[pos - 1].mark; + if (!a) { if (style == LATEX) os << "\\mathsf{f}"; @@ -204,7 +204,7 @@ namespace spot const char* fin_ = (style == LATEX) ? "\\mathsf{Fin}(" : "Fin("; while (a) { - if (a & 1) + if (a.has(0)) { os << or_ << fin_ << negated_pre; set_printer(os, level); @@ -330,14 +330,14 @@ namespace spot case acc_cond::acc_op::And: { auto sub = pos - pos->sub.size; - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; while (sub < pos) { --pos; if (auto s = eval_sets(inf, pos)) m |= s; else - return 0U; + return {}; pos -= pos->sub.size; } return m; @@ -352,20 +352,20 @@ namespace spot return s; pos -= pos->sub.size; } - return 0U; + return {}; } case acc_cond::acc_op::Inf: if ((pos[-1].mark & inf) == pos[-1].mark) return pos[-1].mark; else - return 0U; + return {}; case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: case acc_cond::acc_op::InfNeg: SPOT_UNREACHABLE(); } SPOT_UNREACHABLE(); - return 0U; + return {}; } } @@ -387,7 +387,7 @@ namespace spot bool acc_cond::acc_code::inf_satisfiable(mark_t inf) const { - return !maybe_accepting(inf, 0U).is_false(); + return !maybe_accepting(inf, {}).is_false(); } @@ -397,7 +397,7 @@ namespace spot throw std::runtime_error ("Fin acceptance is not supported by this code path."); if (code_.empty()) - return 0U; + return {}; return eval_sets(inf, &code_.back()); } @@ -419,7 +419,7 @@ namespace spot pos -= 2; break; case acc_cond::acc_op::Fin: - if (code_[pos - 2].mark == 0U) // f + if (!code_[pos - 2].mark) // f { pos -= 2; break; @@ -458,8 +458,8 @@ namespace spot // Pretend we were in a unary highop. s = 5; } - acc_cond::mark_t seen_fin = 0U; - acc_cond::mark_t seen_inf = 0U; + acc_cond::mark_t seen_fin = {}; + acc_cond::mark_t seen_inf = {}; while (s) { if (code[--s].sub.op != lowop) @@ -481,7 +481,7 @@ namespace spot if (o1 != acc_cond::acc_op::Fin || o2 != acc_cond::acc_op::Inf || m1.count() != 1 - || m2.id != (m1.id << 1)) + || m2 != (m1 << 1)) return false; seen_fin |= m1; seen_inf |= m2; @@ -511,8 +511,8 @@ namespace spot if (mainop == singleop && m.count() != 1) return false; - acc_cond::mark_t fin(0U); - acc_cond::mark_t inf(0U); + acc_cond::mark_t fin = {}; + acc_cond::mark_t inf = {}; for (unsigned mark: m.sets()) { if (mainop == acc_cond::acc_op::Fin) @@ -543,8 +543,8 @@ namespace spot || op == acc_cond::acc_op::Inf) { auto m = code[--s].mark; - acc_cond::mark_t fin(0U); - acc_cond::mark_t inf(0U); + acc_cond::mark_t fin = {}; + acc_cond::mark_t inf = {}; if (op == singleop && m.count() != 1) { @@ -631,7 +631,7 @@ namespace spot return true; if (code_.is_f()) { - pairs.emplace_back(0U, 0U); + pairs.emplace_back(mark_t({}), mark_t({})); return true; } return is_rs_like(code_, acc_op::And, acc_op::Or, acc_op::Fin, pairs); @@ -644,7 +644,7 @@ namespace spot return true; if (code_.is_t()) { - pairs.emplace_back(0U, 0U); + pairs.emplace_back(mark_t({}), mark_t({})); return true; } return is_rs_like(code_, acc_op::Or, acc_op::And, acc_op::Inf, pairs); @@ -668,8 +668,8 @@ namespace spot return false; auto s = code_.back().sub.size; - acc_cond::mark_t seen_fin = 0U; - acc_cond::mark_t seen_inf = 0U; + acc_cond::mark_t seen_fin = {}; + acc_cond::mark_t seen_inf = {}; // Each pair is the position of a Fin followed // by the number of Inf. std::map p; @@ -752,8 +752,8 @@ namespace spot return false; auto s = code_.back().sub.size; - acc_cond::mark_t seen_fin = 0U; - acc_cond::mark_t seen_inf = 0U; + acc_cond::mark_t seen_fin = {}; + acc_cond::mark_t seen_inf = {}; // Each pairs is the position of a Inf followed // by the number of Fin. std::map p; @@ -1054,12 +1054,12 @@ namespace spot acc_code rescode = f(); while ((cube = isop.next()) != bddfalse) { - mark_t i = 0U; + mark_t i = {}; acc_code f; while (cube != bddtrue) { // The acceptance set associated to this BDD variable - mark_t s = 0U; + mark_t s = {}; s.set(sets[bdd_var(cube)]); bdd h = bdd_high(cube); @@ -1123,12 +1123,12 @@ namespace spot acc_code rescode; while ((cube = isop.next()) != bddfalse) { - mark_t m = 0U; + mark_t m = {}; acc_code i = f(); while (cube != bddtrue) { // The acceptance set associated to this BDD variable - mark_t s = 0U; + mark_t s = {}; s.set(sets[bdd_var(cube)]); bdd h = bdd_high(cube); @@ -1156,9 +1156,9 @@ namespace spot acc_cond::unsat_mark() const { if (is_t()) - return {false, 0U}; + return {false, mark_t({})}; if (!uses_fin_acceptance()) - return {true, 0U}; + return {true, mark_t({})}; auto used = code_.used_sets(); unsigned c = used.count(); @@ -1185,12 +1185,12 @@ namespace spot bdd res = to_bdd_rec(&code_.back(), &r[0]); if (res == bddtrue) - return {false, 0U}; + return {false, mark_t({})}; if (res == bddfalse) - return {true, 0U}; + return {true, mark_t({})}; bdd cube = bdd_satone(!res); - mark_t i = 0U; + mark_t i = {}; while (cube != bddtrue) { // The acceptance set associated to this BDD variable @@ -1483,8 +1483,8 @@ namespace spot acc_cond::acc_code::used_sets() const { if (is_t() || is_f()) - return 0U; - acc_cond::mark_t used_in_cond = 0U; + return {}; + acc_cond::mark_t used_in_cond = {}; auto pos = &back(); auto end = &front(); while (pos > end) @@ -1511,10 +1511,10 @@ namespace spot acc_cond::acc_code::used_inf_fin_sets() const { if (is_t() || is_f()) - return {0U, 0U}; + return {mark_t({}), mark_t({})}; - acc_cond::mark_t used_fin = 0U; - acc_cond::mark_t used_inf = 0U; + acc_cond::mark_t used_fin = {}; + acc_cond::mark_t used_inf = {}; auto pos = &back(); auto end = &front(); while (pos > end) diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index e194ac8d4..933b6a30a 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -51,8 +51,8 @@ namespace spot template mark_t(const iterator& begin, const iterator& end) noexcept + : mark_t(0U) { - id = 0U; for (iterator i = begin; i != end; ++i) set(*i); } @@ -62,16 +62,23 @@ namespace spot { } + static mark_t all() + { + mark_t res({}); + res.id -= 1; + return res; + } + bool operator==(unsigned o) const { SPOT_ASSERT(o == 0U); - return id == o; + return !id; } bool operator!=(unsigned o) const { SPOT_ASSERT(o == 0U); - return id != o; + return !!id; } bool operator==(mark_t o) const @@ -106,12 +113,12 @@ namespace spot explicit operator bool() const { - return id != 0; + return !!id; } bool has(unsigned u) const { - return id & (1U << u); + return !!this->operator&(mark_t({0}) << u); } void set(unsigned u) @@ -220,7 +227,7 @@ namespace spot bool subset(mark_t m) const { - return (*this) - m == 0U; + return !((*this) - m); } bool proper_subset(mark_t m) const @@ -302,11 +309,11 @@ namespace spot template void fill(iterator here) const { - auto a = id; + auto a = *this; unsigned level = 0; while (a) { - if (a & 1) + if (a.has(0)) *here++ = level; ++level; a >>= 1; @@ -437,21 +444,21 @@ namespace spot { unsigned s = size(); return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf - && (*this)[s - 2].mark == 0U); + && !((*this)[s - 2].mark)); } bool is_f() const { unsigned s = size(); return s > 1 - && (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0U; + && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark); } static acc_code f() { acc_code res; res.resize(2); - res[0].mark = 0U; + res[0].mark = {}; res[1].sub.op = acc_op::Fin; res[1].sub.size = 1; return res; @@ -534,17 +541,19 @@ namespace spot static acc_code generalized_buchi(unsigned n) { - acc_cond::mark_t m = (1U << n) - 1; - if (n == 8 * sizeof(mark_t::value_t)) - m = mark_t(-1U); + if (n == 0) + return inf({}); + acc_cond::mark_t m = mark_t::all(); + m >>= (8*sizeof(mark_t::value_t) - n); return inf(m); } static acc_code generalized_co_buchi(unsigned n) { - acc_cond::mark_t m = (1U << n) - 1; - if (n == 8 * sizeof(mark_t::value_t)) - m = mark_t(-1U); + if (n == 0) + return fin({}); + acc_cond::mark_t m = mark_t::all(); + m >>= (8*sizeof(mark_t::value_t) - n); return fin(m); } @@ -580,7 +589,7 @@ namespace spot for (Iterator i = begin; i != end; ++i) { unsigned f = n++; - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; for (unsigned ni = *i; ni > 0; --ni) m.set(n++); auto pair = inf(m) & fin({f}); @@ -666,7 +675,7 @@ namespace spot right_inf = right_end - 1; } - acc_cond::mark_t carry = 0U; + acc_cond::mark_t carry = {}; if (left_inf && right_inf) { carry = left_inf->mark; @@ -767,7 +776,7 @@ namespace spot right_fin = right_end - 1; } - acc_cond::mark_t carry = 0U; + acc_cond::mark_t carry = {}; if (left_fin && right_fin) { carry = left_fin->mark; @@ -817,7 +826,7 @@ namespace spot case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: pos -= 2; - (*this)[pos].mark.id <<= sets; + (*this)[pos].mark <<= sets; break; } } @@ -937,14 +946,14 @@ namespace spot }; acc_cond(unsigned n_sets = 0, const acc_code& code = {}) - : num_(0U), all_(0U), code_(code) + : num_(0U), all_({}), code_(code) { add_sets(n_sets); uses_fin_acceptance_ = check_fin_acceptance(); } acc_cond(const acc_code& code) - : num_(0U), all_(0U), code_(code) + : num_(0U), all_({}), code_(code) { add_sets(code.used_sets().max_set()); uses_fin_acceptance_ = check_fin_acceptance(); @@ -1205,7 +1214,7 @@ namespace spot return -1U; unsigned j = num_; num_ += num; - if (num_ > 8 * sizeof(mark_t::id)) + if (num_ > 8 * sizeof(mark_t::value_t)) throw std::runtime_error("Too many acceptance sets used."); all_ = all_sets_(); return j; @@ -1219,12 +1228,12 @@ namespace spot mark_t mark(unsigned u) const { SPOT_ASSERT(u < num_sets()); - return 1U << u; + return mark_t({0}) << u; } - mark_t comp(mark_t l) const + mark_t comp(const mark_t& l) const { - return all_ ^ l.id; + return all_ ^ l; } mark_t all_sets() const @@ -1252,7 +1261,7 @@ namespace spot std::ostream& format(std::ostream& os, mark_t m) const { auto a = m; - if (a == 0U) + if (!a) return os; return os << m; } @@ -1272,17 +1281,18 @@ namespace spot template mark_t useless(iterator begin, iterator end) const { - mark_t::value_t u = 0U; // The set of useless marks. + mark_t u = {}; // The set of useless marks + const mark_t one = {0}; for (unsigned x = 0; x < num_; ++x) { // Skip marks that are already known to be useless. - if (u & (1 << x)) + if (u & (one << x)) continue; - unsigned all = all_ ^ (u | (1 << x)); + auto all = all_ ^ (u | (one << x)); for (iterator y = begin; y != end; ++y) { - auto v = y->id; - if (v & (1 << x)) + const mark_t& v = *y; + if (!!(v & (one << x))) { all &= v; if (!all) @@ -1340,15 +1350,13 @@ namespace spot std::string name(const char* fmt = "alo") const; protected: - mark_t::value_t all_sets_() const + mark_t all_sets_() const { - if (num_ == 0) - return 0; - return -1U >> (8 * sizeof(mark_t::value_t) - num_); + return mark_t::all() >> (8*sizeof(mark_t::value_t) - num_); } unsigned num_; - mark_t::value_t all_; + mark_t all_; acc_code code_; bool uses_fin_acceptance_ = false; @@ -1363,13 +1371,13 @@ namespace spot // Creates view of pairs without restriction to marks explicit rs_pairs_view(const rs_pairs& p) - : rs_pairs_view(p, std::numeric_limits::max()) {} + : rs_pairs_view(p, acc_cond::mark_t::all()) {} acc_cond::mark_t infs() const { return do_view([&](const acc_cond::rs_pair& p) { - return visible(p.inf) ? p.inf : 0U; + return visible(p.inf) ? p.inf : acc_cond::mark_t({}); }); } @@ -1377,7 +1385,7 @@ namespace spot { return do_view([&](const acc_cond::rs_pair& p) { - return visible(p.fin) ? p.fin : 0U; + return visible(p.fin) ? p.fin : acc_cond::mark_t({}); }); } @@ -1385,7 +1393,8 @@ namespace spot { return do_view([&](const acc_cond::rs_pair& p) { - return !visible(p.inf) && visible(p.fin) ? p.fin : 0U; + return !visible(p.inf) && visible(p.fin) ? p.fin + : acc_cond::mark_t({}); }); } @@ -1393,13 +1402,14 @@ namespace spot { return do_view([&](const acc_cond::rs_pair& p) { - return !visible(p.fin) && visible(p.inf) ? p.inf : 0U; + return !visible(p.fin) && visible(p.inf) ? p.inf + : acc_cond::mark_t({}); }); } acc_cond::mark_t paired_with_fin(unsigned mark) const { - acc_cond::mark_t res = 0U; + acc_cond::mark_t res = {}; for (const auto& p: pairs_) if (p.fin.has(mark) && visible(p.fin) && visible(p.inf)) res |= p.inf; @@ -1415,7 +1425,7 @@ namespace spot template acc_cond::mark_t do_view(const filter& filt) const { - acc_cond::mark_t res = 0U; + acc_cond::mark_t res = {}; for (const auto& p: pairs_) res |= filt(p); return res; @@ -1423,7 +1433,7 @@ namespace spot bool visible(const acc_cond::mark_t& v) const { - return (view_marks_ & v) != 0; + return !!(view_marks_ & v); } const rs_pairs& pairs_; @@ -1446,7 +1456,7 @@ namespace spot typedef std::forward_iterator_tag iterator_category; mark_iterator() noexcept - : m_(0U) + : m_({}) { } @@ -1471,9 +1481,9 @@ namespace spot return m_.min_set() - 1; } - mark_iterator operator++() + mark_iterator& operator++() { - m_.id &= m_.id - 1; + m_.clear(this->operator*()); return *this; } diff --git a/spot/twa/taatgba.cc b/spot/twa/taatgba.cc index 27f15edcc..416028e37 100644 --- a/spot/twa/taatgba.cc +++ b/spot/twa/taatgba.cc @@ -132,7 +132,7 @@ namespace spot { taa_tgba::transition* t = new taa_tgba::transition; t->condition = bddtrue; - t->acceptance_conditions = 0U; + t->acceptance_conditions = {}; t->dst = new taa_tgba::state_set; succ_.emplace_back(t); return; @@ -155,7 +155,7 @@ namespace spot { taa_tgba::transition* t = new taa_tgba::transition; t->condition = bddtrue; - t->acceptance_conditions = 0U; + t->acceptance_conditions = {}; taa_tgba::state_set* ss = new taa_tgba::state_set; unsigned p; diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh index 80c753bbe..3d020af4f 100644 --- a/spot/twa/taatgba.hh +++ b/spot/twa/taatgba.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011-2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2009, 2011-2018 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -177,7 +177,7 @@ namespace spot transition* t = new transition; t->dst = dst; t->condition = bddtrue; - t->acceptance_conditions = 0U; + t->acceptance_conditions = {}; src->emplace_back(t); return t; } @@ -192,7 +192,7 @@ namespace spot void add_acceptance_condition(transition* t, formula f) { - auto p = acc_map_.emplace(f, 0); + auto p = acc_map_.emplace(f, acc_cond::mark_t({})); if (p.second) p.first->second = acc_cond::mark_t({acc().add_set()}); t->acceptance_conditions |= p.first->second; diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 07d26f100..cbd4a46dd 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -88,11 +88,13 @@ namespace spot acc_cond::mark_t acc; explicit twa_graph_edge_data() noexcept - : cond(bddfalse), acc(0) + : cond(bddfalse), acc({}) { } - twa_graph_edge_data(bdd cond, acc_cond::mark_t acc = 0U) noexcept + twa_graph_edge_data( + bdd cond, + acc_cond::mark_t acc = {}) noexcept : cond(cond), acc(acc) { } @@ -425,7 +427,8 @@ namespace spot } unsigned new_edge(unsigned src, unsigned dst, - bdd cond, acc_cond::mark_t acc = 0U) + bdd cond, + acc_cond::mark_t acc = {}) { return g_.new_edge(src, dst, cond, acc); } @@ -441,13 +444,15 @@ namespace spot template unsigned new_univ_edge(unsigned src, I begin, I end, - bdd cond, acc_cond::mark_t acc = 0U) + bdd cond, + acc_cond::mark_t acc = {}) { return g_.new_univ_edge(src, begin, end, cond, acc); } unsigned new_univ_edge(unsigned src, std::initializer_list dst, - bdd cond, acc_cond::mark_t acc = 0U) + bdd cond, + acc_cond::mark_t acc = {}) { return g_.new_univ_edge(src, dst.begin(), dst.end(), cond, acc); } @@ -613,7 +618,7 @@ namespace spot // Stop at the first edge, since the remaining should be // labeled identically. return t.acc; - return 0U; + return {}; } /// \brief Tell if a state is accepting. diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc index 0ebbb1667..63a7745cd 100644 --- a/spot/twaalgos/alternation.cc +++ b/spot/twaalgos/alternation.cc @@ -109,7 +109,7 @@ namespace spot { bool first = true; bool reject_cycle = false; - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; for (unsigned src: si_.states_of(scc)) for (auto& t: aut_->out(src)) for (unsigned d: aut_->univ_dests(t.dst)) @@ -280,7 +280,7 @@ namespace spot acc_cond::mark_t bdd_to_state(bdd b, std::vector& s) { - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; while (b != bddtrue) { assert(bdd_low(b) == bddfalse); @@ -649,7 +649,9 @@ namespace spot virtual acc_cond::mark_t acc() const override { assert(dst_); - return dst_->is_reset(); + return dst_->is_reset() ? + acc_cond::mark_t({0}) : + acc_cond::mark_t({}); } }; diff --git a/spot/twaalgos/cleanacc.cc b/spot/twaalgos/cleanacc.cc index a672f1cb5..34fdae9d9 100644 --- a/spot/twaalgos/cleanacc.cc +++ b/spot/twaalgos/cleanacc.cc @@ -31,7 +31,7 @@ namespace spot auto c = aut->get_acceptance(); acc_cond::mark_t used_in_cond = c.used_sets(); - acc_cond::mark_t used_in_aut = 0U; + acc_cond::mark_t used_in_aut = {}; acc_cond::mark_t used_on_all_edges = used_in_cond; for (auto& t: aut->edges()) { @@ -97,7 +97,7 @@ namespace spot else always_together[i] = acc_cond::mark_t({i}); - acc_cond::mark_t previous_a = 0U; + acc_cond::mark_t previous_a = {}; for (auto& t: aut->edges()) { acc_cond::mark_t a = t.acc & used_in_cond; @@ -116,7 +116,7 @@ namespace spot } } - acc_cond::mark_t to_remove = 0U; + acc_cond::mark_t to_remove = {}; for (unsigned i = 0; i < num_sets; ++i) { auto oldm = always_together[i]; @@ -168,8 +168,8 @@ namespace spot { --pos; auto res = acc_cond::acc_code::t(); - acc_cond::mark_t seen_fin = 0U; - auto inf = acc_cond::acc_code::inf(0U); + acc_cond::mark_t seen_fin = {}; + auto inf = acc_cond::acc_code::inf({}); do { auto tmp = remove_compl_rec(pos, complement); @@ -212,7 +212,7 @@ namespace spot { --pos; auto res = acc_cond::acc_code::f(); - acc_cond::mark_t seen_inf = 0U; + acc_cond::mark_t seen_inf = {}; auto fin = acc_cond::acc_code::f(); do { @@ -288,7 +288,7 @@ namespace spot // prev_acc that would allow us to fail the comparison on the // first edge (this was issue #315), so we have to deal with // that first edge specifically. - acc_cond::mark_t prev_acc = 0U; + acc_cond::mark_t prev_acc = {}; const auto& edges = aut->edges(); auto b = edges.begin(); auto e = edges.end(); diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 32129a196..634b3f6b2 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -170,7 +170,7 @@ namespace spot if (nca_is_inf_state[s]) { for (auto& e : res_->out(s)) - e.acc = 0U; + e.acc = {}; if (nca_info) save_inf_nca_st(s, nca_info); @@ -182,7 +182,7 @@ namespace spot if (si_.scc_of(e.dst) == src_scc || state_based_) e.acc = acc_cond::mark_t({0}); else - e.acc = 0u; + e.acc = {}; } } } @@ -318,7 +318,7 @@ namespace spot unsigned ns = si.scc_count(); for (unsigned s = 0; s < ns; ++s) { - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; if (si.is_rejecting_scc(s)) m = acc_cond::mark_t{0}; else diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc index 78ac48b7b..20be2ea06 100644 --- a/spot/twaalgos/complete.cc +++ b/spot/twaalgos/complete.cc @@ -153,7 +153,7 @@ namespace spot // in case the automaton uses state-based acceptance, propagate // the acceptance of the first edge to the one we add. if (!aut->prop_state_acc().is_true() && i != sink) - acc = 0U; + acc = {}; aut->new_edge(i, sink, missingcond, acc); } diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index 103431ec9..cf907779f 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -264,7 +264,7 @@ namespace spot // A simple struct representing an SCC. struct scc { - scc(int i): index(i), condition(0U) {} + scc(int i): index(i), condition({}) {} int index; acc_cond::mark_t condition; @@ -424,7 +424,7 @@ namespace spot acc_cond::mark_t less_acc = acc_to_traverse - st.acc; if (less_acc != acc_to_traverse - || (acc_to_traverse == 0U + || (!acc_to_traverse && T::from_state(ecs->aut, s) == ecs->cycle_seed)) { acc_to_traverse = less_acc; @@ -437,7 +437,7 @@ namespace spot substart = b.search(substart, run_->cycle); assert(substart); } - while (acc_to_traverse != 0U || substart != cycle_seed); + while (acc_to_traverse || substart != cycle_seed); } }; @@ -691,7 +691,7 @@ namespace spot ecs_->h[init] = 1; ecs_->root.push(1); if (strength == STRONG) - arc.push(0U); + arc.push({}); auto iter = T::succ(ecs_->aut, init); todo.emplace(init, iter); live.emplace_back(init); diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index d1dbdc633..397ec33da 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -80,7 +80,7 @@ namespace spot { unsigned s1 = scc_of(s); acc_cond::mark_t common = a_->acc().all_sets(); - acc_cond::mark_t union_ = 0U; + acc_cond::mark_t union_ = {}; bool has_acc_self_loop = false; bool is_true_state = false; bool seen = false; @@ -108,7 +108,7 @@ namespace spot seen = true; } if (!seen) - common = 0U; + common = {}; std::get<0>(cache_[s]) = common; std::get<1>(cache_[s]) = union_; std::get<3>(cache_[s]) = has_acc_self_loop; diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index f3826025f..4e0f44e8c 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -81,8 +81,8 @@ namespace spot std::string* name_ = nullptr; std::map, int> univ_done; - acc_cond::mark_t inf_sets_ = 0U; - acc_cond::mark_t fin_sets_ = 0U; + acc_cond::mark_t inf_sets_ = {}; + acc_cond::mark_t fin_sets_ = {}; unsigned opt_shift_sets_ = 0; enum { ShapeAuto = 0, ShapeCircle, ShapeEllipse } opt_shape_ = ShapeAuto; bool opt_force_acc_trans_ = false; @@ -591,7 +591,7 @@ namespace spot if (mark_states_ && !dcircles_) { - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; for (auto& t: aut_->out(s)) { acc = t.acc; diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index b1fd22b4b..ecde78e44 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -76,7 +76,7 @@ namespace spot path(unsigned src_ref) : src_ref(src_ref), dst_ref(src_ref), - acc_cand(0U), acc_ref(0U) + acc_cand({}), acc_ref({}) { } @@ -131,7 +131,7 @@ namespace spot auto pos = &acc.back(); if (pos->sub.op == acc_cond::acc_op::Or) --pos; - acc_cond::mark_t all_fin = 0U; + acc_cond::mark_t all_fin = {}; auto start = &acc.front(); while (pos > start) { @@ -145,8 +145,8 @@ namespace spot { // We have a conjunction of Fin and Inf sets. auto end = pos - pos->sub.size - 1; - acc_cond::mark_t fin = 0U; - acc_cond::mark_t inf = 0U; + acc_cond::mark_t fin = {}; + acc_cond::mark_t inf = {}; while (pos > end) { switch (pos->sub.op) @@ -291,8 +291,8 @@ namespace spot int pathid(unsigned src_cand, unsigned src_ref, unsigned dst_cand, - unsigned dst_ref, acc_cond::mark_t acc_cand = 0U, - acc_cond::mark_t acc_ref = 0U) + unsigned dst_ref, acc_cond::mark_t acc_cand = {}, + acc_cond::mark_t acc_ref = {}) { #if TRACE try @@ -352,8 +352,8 @@ namespace spot std::string fmt_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand, - unsigned dst_ref, acc_cond::mark_t acc_cand = 0U, - acc_cond::mark_t acc_ref = 0U) + unsigned dst_ref, acc_cond::mark_t acc_cand = {}, + acc_cond::mark_t acc_ref = {}) { return helper.format_p(debug_cand_acc, debug_ref_acc, src_cand, src_ref, dst_cand, dst_ref, acc_cand, acc_ref); @@ -405,7 +405,7 @@ namespace spot d.scc_marks.reserve(scccount); for (auto& v: tmp) { - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; for (auto i: v) m |= i; d.scc_marks.emplace_back(m); @@ -423,7 +423,7 @@ namespace spot d.cand_inf_trim_map = split_dnf_acc_by_inf(d.cand_acc); bdd_dict_ptr bd = aut->get_dict(); - d.all_cand_acc.emplace_back(0U); + d.all_cand_acc.emplace_back(acc_cond::mark_t({})); for (unsigned n = 0; n < d.cand_nacc; ++n) { auto c = d.cacc.mark(n); @@ -443,7 +443,7 @@ namespace spot } } - d.all_ref_acc.emplace_back(0U); + d.all_ref_acc.emplace_back(acc_cond::mark_t({})); unsigned ref_nacc = aut->num_sets(); for (unsigned n = 0; n < ref_nacc; ++n) { @@ -818,7 +818,7 @@ namespace spot d.cand_inf_trim (candhist_p | d.all_cand_acc[f]); - acc_cond::mark_t f2p = 0U; + acc_cond::mark_t f2p = {}; if (!is_weak) f2p = d.ref_inf_trim(refhist | curacc); @@ -906,7 +906,7 @@ namespace spot // Skip (s,l,d2) if we have already seen some (s,l,d1). if (seen_trans.insert(src_cond(i, satdict.alpha_vect[j])).second) { - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; if (state_based) { auto tmp = state_acc.find(i); diff --git a/spot/twaalgos/dualize.cc b/spot/twaalgos/dualize.cc index 1f8a436cf..4cc661dec 100644 --- a/spot/twaalgos/dualize.cc +++ b/spot/twaalgos/dualize.cc @@ -258,7 +258,7 @@ namespace spot // a universal transition. acc_cond::mark_t bdd_to_state(bdd b, std::vector& s) { - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; while (b != bddtrue) { assert(bdd_low(b) == bddfalse); @@ -281,7 +281,7 @@ namespace spot : sbacc(std::const_pointer_cast(aut))), state_to_var_(aut_->num_states(), bddfalse), true_state_(-1U), - acc_(0U), + acc_({}), has_sink(false) { } @@ -303,7 +303,7 @@ namespace spot { //Shortcut if dual is false res->new_states(1); - res->new_edge(0, 0, bddtrue, 0U); + res->new_edge(0, 0, bddtrue, {}); res->set_init_state(0); res->set_acceptance(0, acc_cond::acc_code::f()); diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc index f9b91f1a7..4ce6e02e9 100644 --- a/spot/twaalgos/emptiness.cc +++ b/spot/twaalgos/emptiness.cc @@ -358,7 +358,7 @@ namespace spot // Start from the end of the original cycle, and rewind until all // acceptance sets have been seen. - acc_cond::mark_t seen_acc = 0U; + acc_cond::mark_t seen_acc = {}; twa_run::steps::const_iterator seg = cycle.end(); do { @@ -371,7 +371,7 @@ namespace spot // Now go forward and ends the segment as soon as we have seen all // acceptance sets, cloning it in our result along the way. - seen_acc = 0U; + seen_acc = {}; do { assert(seg != cycle.end()); @@ -507,7 +507,7 @@ namespace spot int serial = 1; const twa_run::steps* l; std::string in; - acc_cond::mark_t all_acc = 0U; + acc_cond::mark_t all_acc = {}; bool all_acc_seen = false; state_map> seen; @@ -771,7 +771,7 @@ namespace spot unsigned src; unsigned dst; const twa_run::steps* l; - acc_cond::mark_t seen_acc = 0U; + acc_cond::mark_t seen_acc = {}; state_map seen; diff --git a/spot/twaalgos/gtec/ce.cc b/spot/twaalgos/gtec/ce.cc index c44bb3ebe..9b167d00c 100644 --- a/spot/twaalgos/gtec/ce.cc +++ b/spot/twaalgos/gtec/ce.cc @@ -207,7 +207,7 @@ namespace spot acc_cond::mark_t less_acc = acc_to_traverse - st.acc; if (less_acc != acc_to_traverse - || (acc_to_traverse == 0U + || (!acc_to_traverse && s == ecs->cycle_seed)) { acc_to_traverse = less_acc; @@ -221,7 +221,7 @@ namespace spot substart = b.search(substart, run_->cycle); assert(substart); } - while (acc_to_traverse != 0U || substart != ecs_->cycle_seed); + while (acc_to_traverse || substart != ecs_->cycle_seed); } void diff --git a/spot/twaalgos/gtec/gtec.cc b/spot/twaalgos/gtec/gtec.cc index 243ad8c91..f36d2fe3c 100644 --- a/spot/twaalgos/gtec/gtec.cc +++ b/spot/twaalgos/gtec/gtec.cc @@ -162,7 +162,7 @@ namespace spot const state* init = ecs_->aut->get_init_state(); ecs_->h[init] = 1; ecs_->root.push(1); - arc.push(0U); + arc.push({}); twa_succ_iterator* iter = ecs_->aut->succ_iter(init); iter->first(); todo.emplace(init, iter); diff --git a/spot/twaalgos/gtec/sccstack.cc b/spot/twaalgos/gtec/sccstack.cc index 34ec7493b..eb2c5e73e 100644 --- a/spot/twaalgos/gtec/sccstack.cc +++ b/spot/twaalgos/gtec/sccstack.cc @@ -28,7 +28,7 @@ namespace spot scc_stack::connected_component::connected_component(int i) { index = i; - condition = 0U; + condition = acc_cond::mark_t({}); } scc_stack::connected_component& diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc index a6e7e6b64..2ad80e796 100644 --- a/spot/twaalgos/gv04.cc +++ b/spot/twaalgos/gv04.cc @@ -364,7 +364,7 @@ namespace spot virtual bool match(twa_run::step& step, const state*) override { - return step.acc != 0U; + return !!step.acc; } }; diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index e70bf4d18..e17da320a 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -72,7 +72,7 @@ namespace spot emit_acc(std::ostream& os, acc_cond::mark_t b) { // FIXME: We could use a cache for this. - if (b == 0U) + if (!b) return os; os << " {"; bool notfirst = false; @@ -104,7 +104,7 @@ namespace spot bdd available = bddtrue; bool st_acc = true; bool notfirst = false; - acc_cond::mark_t prev = 0U; + acc_cond::mark_t prev = {}; bool has_succ = false; bdd lastcond = bddfalse; for (auto& t: aut->out(src)) @@ -636,7 +636,7 @@ namespace spot os << " \"" << (*sn)[i] << '"'; if (this_acc == Hoa_Acceptance_States) { - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; for (auto& t: aut->out(i)) { acc = t.acc; diff --git a/spot/twaalgos/lbtt.cc b/spot/twaalgos/lbtt.cc index c56f4a0f9..f7a0dda7f 100644 --- a/spot/twaalgos/lbtt.cc +++ b/spot/twaalgos/lbtt.cc @@ -66,7 +66,7 @@ namespace spot // is not terribly efficient since we have to create the // iterator. twa_succ_iterator* it = aut_->succ_iter(s); - acc_cond::mark_t res = 0U; + acc_cond::mark_t res = {}; if (it->first()) res = it->acc(); aut_->release_iter(it); diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 648c03b08..63b993434 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -238,7 +238,7 @@ namespace spot { bdd o = a; if (a == bddtrue) - return 0U; + return {}; assert(a != bddfalse); std::vector t; do diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index ac3a5bd37..1a86a154a 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -102,7 +102,7 @@ namespace spot const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, BLUE); - push(st_blue, s0, bddfalse, 0U); + push(st_blue, s0, bddfalse, {}); if (dfs_blue()) return std::make_shared(t, options()); } diff --git a/spot/twaalgos/ndfs_result.hxx b/spot/twaalgos/ndfs_result.hxx index 2cfb67fb6..9d9878fc0 100644 --- a/spot/twaalgos/ndfs_result.hxx +++ b/spot/twaalgos/ndfs_result.hxx @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de recherche +// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2018 Laboratoire de recherche // et développement de l'Epita (LRDE). // Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -111,7 +111,7 @@ namespace spot SPOT_ASSERT(!stb.empty()); - acc_cond::mark_t covered_acc = 0U; + acc_cond::mark_t covered_acc = {}; accepting_transitions_list acc_trans; const state* start; @@ -263,7 +263,7 @@ namespace spot seen.insert(start); twa_succ_iterator* i = a_->succ_iter(start); i->first(); - st1.emplace_front(start, i, bddfalse, 0U); + st1.emplace_front(start, i, bddfalse, acc_cond::mark_t({})); while (!st1.empty()) { @@ -608,7 +608,7 @@ namespace spot transition tmp; // Initialize to please GCC 4.0.1 (Darwin). tmp.source = tmp.dest = nullptr; - tmp.acc = 0U; + tmp.acc = {}; target.emplace(begin, tmp); min_path s(this, a_, target, h_); const state* res = s.search(current.dest->clone(), run->cycle); @@ -623,7 +623,7 @@ namespace spot m_source_trans target; transition tmp; tmp.source = tmp.dest = nullptr; // Initialize to please GCC 4.0. - tmp.acc = 0U; + tmp.acc = {}; // Register all states from the cycle as target of the BFS. for (twa_run::steps::const_iterator i = run->cycle.begin(); diff --git a/spot/twaalgos/rabin2parity.cc b/spot/twaalgos/rabin2parity.cc index 178981cad..c307b08bb 100644 --- a/spot/twaalgos/rabin2parity.cc +++ b/spot/twaalgos/rabin2parity.cc @@ -143,7 +143,7 @@ namespace spot auto colors = scc_.acc_sets_of(scc_num); std::set scc_pairs; for (unsigned k = 0; k != pairs_.size(); ++k) - if (inf(k) == 0U || (colors & (pairs_[k].fin | pairs_[k].inf))) + if (!inf(k) || (colors & (pairs_[k].fin | pairs_[k].inf))) scc_pairs.insert(k); perm_t p0; @@ -213,13 +213,13 @@ namespace spot for (unsigned k = 0; k != current.perm.size(); ++k) { unsigned pk = current.perm[k]; - if (inf(pk) == 0U || + if (!inf(pk) || (e.acc & (pairs_[pk].fin | pairs_[pk].inf))) // k increases in the loop, so k > maxint necessarily maxint = k; } - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; if (maxint == -1U) acc = {0}; else if (e.acc & fin(current.perm[maxint])) diff --git a/spot/twaalgos/randomgraph.cc b/spot/twaalgos/randomgraph.cc index 59e1c6bdf..32e624f81 100644 --- a/spot/twaalgos/randomgraph.cc +++ b/spot/twaalgos/randomgraph.cc @@ -80,7 +80,7 @@ namespace spot static acc_cond::mark_t random_acc(unsigned n_accs, float a) { - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; for (unsigned i = 0U; i < n_accs; ++i) if (drand() < a) m.set(i); @@ -194,7 +194,7 @@ namespace spot int possibilities = n; unsigned dst; - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; if (state_acc) m = colored ? random_acc1(n_accs) : random_acc(n_accs, a); diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 1becc427d..112d51c05 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -74,7 +74,7 @@ namespace spot const Edges& edges, const EdgeMask& mask) { - acc_cond::mark_t scc_mark = 0U; + acc_cond::mark_t scc_mark = {}; for_each_edge(aut, edges, mask, [&] (unsigned e) { scc_mark |= aut->edge_data(e).acc; @@ -89,7 +89,7 @@ namespace spot unsigned nst = aut->num_states(); for (unsigned s = 0; s < nst; ++s) { - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; for (auto& t: aut->out(s)) acc |= t.acc; for (auto& t: aut->out(s)) @@ -313,7 +313,7 @@ namespace spot for (const auto& e: si.edges_of(scc)) { - bool acc = (e.acc & scc_infs_alone) != 0; + bool acc = !!(e.acc & scc_infs_alone); res->new_acc_edge(e.src, e.dst, e.cond, acc); } @@ -331,7 +331,7 @@ namespace spot continue; auto src = state_map[e.src]; auto dst = state_map[e.dst]; - bool cacc = fins_alone.has(r) || (pairinf & e.acc) != 0; + bool cacc = fins_alone.has(r) || (pairinf & e.acc); res->new_acc_edge(src, dst, e.cond, cacc); // We need only one non-deterministic jump per // cycle. As an approximation, we only do @@ -339,7 +339,7 @@ namespace spot if (e.dst <= e.src) { deterministic = false; - bool jacc = ((e.acc & scc_infs_alone) != 0); + bool jacc = !!(e.acc & scc_infs_alone); res->new_acc_edge(e.src, dst, e.cond, jacc); } } @@ -379,7 +379,7 @@ namespace spot // only, the Fin() may encode a disjunction of sets. for (auto s: pos[-1].mark.sets()) { - acc_cond::mark_t fin = 0U; + acc_cond::mark_t fin = {}; fin.set(s); res[fin] = acc_cond::acc_code{}; } @@ -389,8 +389,8 @@ namespace spot { // We have a conjunction of Fin and Inf sets. auto end = pos - pos->sub.size - 1; - acc_cond::mark_t fin = 0U; - acc_cond::mark_t inf = 0U; + acc_cond::mark_t fin = {}; + acc_cond::mark_t inf = {}; while (pos > end) { switch (pos->sub.op) @@ -453,7 +453,7 @@ namespace spot { if (!si.reachable_state(src)) continue; - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; unsigned scc = si.scc_of(src); if (si.is_accepting_scc(scc) && !si.is_trivial(scc)) acc = all_acc; @@ -504,8 +504,8 @@ namespace spot std::vector keep; std::vector add; bool has_true_term = false; - acc_cond::mark_t allinf = 0U; - acc_cond::mark_t allfin = 0U; + acc_cond::mark_t allinf = {}; + acc_cond::mark_t allfin = {}; { auto acccode = aut->get_acceptance(); if (!acccode.is_dnf()) @@ -534,10 +534,10 @@ namespace spot for (auto p: split) { // The empty Fin should always come first - assert(p.first != 0U || rem.empty()); + assert(p.first || rem.empty()); rem.emplace_back(p.first); allfin |= p.first; - acc_cond::mark_t inf = 0U; + acc_cond::mark_t inf = {}; if (!p.second.empty()) { auto pos = &p.second.back(); @@ -562,14 +562,14 @@ namespace spot } } } - if (inf == 0U) + if (!inf) { has_true_term = true; } code.emplace_back(std::move(p.second)); keep.emplace_back(inf); allinf |= inf; - add.emplace_back(0U); + add.emplace_back(acc_cond::mark_t({})); } } assert(add.size() > 0); @@ -582,7 +582,7 @@ namespace spot bool interference = false; { auto sz = keep.size(); - acc_cond::mark_t sofar = 0U; + acc_cond::mark_t sofar = {}; for (unsigned i = 0; i < sz; ++i) { auto k = keep[i]; @@ -614,7 +614,7 @@ namespace spot } for (unsigned i = 0; i < sz; ++i) { - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; for (auto f: rem[i].sets()) m.set(exs[f]); trace << "rem[" << i << "] = " << rem[i] @@ -637,14 +637,15 @@ namespace spot continue; add[i] = m; code[i] &= std::move(c); - c = acc.fin(0U); // Use false for the other terms. + // Use false for the other terms. + c = acc.fin({}); trace << "code[" << i << "] = " << code[i] << '\n'; } } } - acc_cond::acc_code new_code = aut->acc().fin(0U); + acc_cond::acc_code new_code = aut->acc().fin({}); for (auto c: code) new_code |= std::move(c); @@ -662,7 +663,7 @@ namespace spot res->set_init_state(aut->get_init_state_number()); // If the input had no Inf, the output is a state-based automaton. - if (allinf == 0U) + if (!allinf) res->prop_state_acc(true); bool sbacc = res->prop_state_acc().is_true(); @@ -676,8 +677,8 @@ namespace spot trace << "SCC #" << n << " uses " << m << '\n'; // What to keep and add into the main copy - acc_cond::mark_t main_sets = 0U; - acc_cond::mark_t main_add = 0U; + acc_cond::mark_t main_sets = {}; + acc_cond::mark_t main_add = {}; bool intersects_fin = false; for (unsigned i = 0; i < cs; ++i) if (!(m & rem[i])) @@ -696,7 +697,7 @@ namespace spot for (auto s: states) for (auto& t: aut->out(s)) { - acc_cond::mark_t a = 0U; + acc_cond::mark_t a = {}; if (sbacc || SPOT_LIKELY(si.scc_of(t.dst) == n)) a = (t.acc & main_sets) | main_add; res->new_edge(s, t.dst, t.cond, a); @@ -732,7 +733,7 @@ namespace spot // them on back-links. if (t.dst <= s) { - acc_cond::mark_t a = 0U; + acc_cond::mark_t a = {}; if (sbacc) a = (t.acc & main_sets) | main_add; res->new_edge(s, nd, t.cond, a); diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index fe55d5fb8..52f9e7b63 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -52,9 +52,9 @@ namespace spot std::vector common_in(ns, all); std::vector common_out(ns, all); // Marks that label one incoming transition from the same SCC. - std::vector one_in(ns, 0U); + std::vector one_in(ns, acc_cond::mark_t({})); std::vector true_state(ns, false); - acc_cond::mark_t true_state_acc = 0U; + acc_cond::mark_t true_state_acc = {}; unsigned true_state_last; for (auto& e: old->edges()) for (unsigned d: old->univ_dests(e.dst)) @@ -95,7 +95,7 @@ namespace spot if (ts) { state = true_state_last; // Merge all true states. - m = 0U; + m = {}; } pair_t x(state, m); auto p = s2n.emplace(x, 0); @@ -126,7 +126,7 @@ namespace spot internal::univ_dest_mapper uniq(res->get_graph()); for (unsigned s: old_init) { - acc_cond::mark_t init_acc = 0U; + acc_cond::mark_t init_acc = {}; if (!si.is_rejecting_scc(si.scc_of(s))) // Use any edge going into the initial state to set the first // acceptance mark. @@ -148,7 +148,7 @@ namespace spot for (unsigned d: old->univ_dests(t.dst)) { unsigned scc_dst = si.scc_of(d); - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; bool dst_acc = !si.is_rejecting_scc(scc_dst); if (maybe_accepting && scc_src == scc_dst) acc = t.acc - common_out[t.src]; diff --git a/spot/twaalgos/sccfilter.cc b/spot/twaalgos/sccfilter.cc index d73e67b26..f24b96f7a 100644 --- a/spot/twaalgos/sccfilter.cc +++ b/spot/twaalgos/sccfilter.cc @@ -188,12 +188,12 @@ namespace spot if (!this->si->is_trivial(u)) acc &= accmask; // No choice. else if (RemoveAll) - acc = 0U; + acc = {}; } else if (!PreserveSBA) { if (RemoveAll) - acc = 0U; + acc = {}; else if (this->si->is_rejecting_scc(v)) acc &= accmask; } @@ -264,7 +264,7 @@ namespace spot unsigned u = this->si->scc_of(dst); if (this->si->is_rejecting_scc(u)) - acc = 0U; + acc = {}; else acc = acc.strip(strip_[u]); } diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 9f77bb313..df34e1f28 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -58,8 +58,9 @@ namespace spot } acc_cond::mark_t in_acc; // Acceptance sets on the incoming transition - acc_cond::mark_t acc = 0U; // union of all acceptance marks in the SCC - acc_cond::mark_t common = -1U; // intersection of all marks in the SCC + acc_cond::mark_t acc = {}; // union of all acceptance marks in the SCC + // intersection of all marks in the SCC + acc_cond::mark_t common = acc_cond::mark_t::all(); int index; // Index of the SCC bool trivial = true; // Whether the SCC has no cycle bool accepting = false; // Necessarily accepting @@ -205,7 +206,7 @@ namespace spot continue; assert(spi == 0); h_[init] = --num_; - root_.emplace_back(num_, 0U); + root_.emplace_back(num_, acc_cond::mark_t({})); todo_.emplace(stack_item{init, gr.state_storage(init).succ, 0}); live.emplace_back(init); @@ -568,7 +569,7 @@ namespace spot // Get all Fin acceptance set that appears in the SCC and does not have // their corresponding Inf appearing in the SCC. - acc_cond::mark_t m = 0u; + acc_cond::mark_t m = {}; if (fin) for (unsigned p = 0; p < nb_pairs; ++p) if (fin & pairs[p].fin && !(inf & pairs[p].inf)) @@ -617,8 +618,8 @@ namespace spot for (unsigned i = 0; i < nb_states; ++i) old.push_back(i); - acc_cond::mark_t all_fin = 0U; - acc_cond::mark_t all_inf = 0U; + acc_cond::mark_t all_fin = {}; + acc_cond::mark_t all_inf = {}; std::tie(all_inf, all_fin) = aut_->get_acceptance().used_inf_fin_sets(); states_on_acc_cycle_of_rec(scc, all_fin, all_inf, nb_pairs, pairs, res, diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 684a6e9c8..d71dd6194 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -230,7 +230,7 @@ namespace spot bool useful_:1; public: scc_info_node(): - acc_(0U), trivial_(true), accepting_(false), + acc_({}), trivial_(true), accepting_(false), rejecting_(false), useful_(false) { } diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index 89032f289..3c2d8dc00 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -101,7 +101,7 @@ namespace spot const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, CYAN); - push(st_blue, s0, bddfalse, 0U); + push(st_blue, s0, bddfalse, {}); if (dfs_blue()) return std::make_shared(t, options()); } diff --git a/spot/twaalgos/sepsets.cc b/spot/twaalgos/sepsets.cc index 2b246a06d..001e88f36 100644 --- a/spot/twaalgos/sepsets.cc +++ b/spot/twaalgos/sepsets.cc @@ -35,14 +35,14 @@ namespace spot bool has_separate_sets(const const_twa_graph_ptr& aut) { - return common_sets(aut) == 0U; + return !common_sets(aut); } twa_graph_ptr separate_sets_here(const twa_graph_ptr& aut) { auto common = common_sets(aut); - if (common == 0U) + if (!common) return aut; // Each Fin(first) should be replaced by Fin(second). std::vector> map; @@ -69,7 +69,7 @@ namespace spot break; case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: - if ((pos[-1].mark & common) == 0U) + if (!(pos[-1].mark & common)) break; for (auto p: map) if (pos[-1].mark & p.first) @@ -88,7 +88,7 @@ namespace spot // Fix the edges for (auto& t: aut->edges()) { - if ((t.acc & common) == 0U) + if (!(t.acc & common)) continue; for (auto p: map) if (t.acc & p.first) diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc index 724510d84..3c16e25b6 100644 --- a/spot/twaalgos/simulation.cc +++ b/spot/twaalgos/simulation.cc @@ -193,7 +193,7 @@ namespace spot // the destination state on its incoming arcs // (which now become outgoing arcs after // transposition). - acc = 0U; + acc = {}; for (auto& td: in->out(t.dst)) { acc = td.acc ^ all_inf; @@ -476,7 +476,7 @@ namespace spot // Acceptance of states. Only used if Sba && Cosimulation. std::vector accst; if (Sba && Cosimulation) - accst.resize(res->num_states(), 0U); + accst.resize(res->num_states(), acc_cond::mark_t({})); stat.states = bdd_lstate_.size(); stat.edges = 0; @@ -565,7 +565,7 @@ namespace spot // can't do this here, store this in a table // so we can fix it later. accst[gb->get_state(src.id())] = acc; - acc = 0U; + acc = {}; } gb->new_edge(dst.id(), src.id(), cond, acc); } @@ -592,7 +592,7 @@ namespace spot for (unsigned s = 0; s < ns; ++s) { acc_cond::mark_t acc = accst[s]; - if (acc == 0U) + if (!acc) continue; for (auto& t: res->out(s)) t.acc = acc; diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 36821c91e..736c0f0fd 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -50,7 +50,7 @@ namespace spot if (si->states_of(i).size() > 1) is_single_state_scc = false; bool first = true; - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; if (is_weak) for (auto& t: si->edges_of(i)) // In case of a universal edge we only need to check if @@ -294,7 +294,7 @@ namespace spot auto p = aut->acc().unsat_mark(); bool all_accepting = !p.first; - acc_cond::mark_t wacc = 0U; // acceptance for weak SCCs + acc_cond::mark_t wacc = {}; // acceptance for weak SCCs acc_cond::mark_t uacc = p.second; // Acceptance for "needed" SCCs, that // we only want to traverse. diff --git a/spot/twaalgos/stripacc.cc b/spot/twaalgos/stripacc.cc index 41634b409..1fc7f353c 100644 --- a/spot/twaalgos/stripacc.cc +++ b/spot/twaalgos/stripacc.cc @@ -28,7 +28,7 @@ namespace spot unsigned n = a->num_states(); for (unsigned s = 0; s < n; ++s) for (auto& t: a->out(s)) - t.acc = 0U; + t.acc = {}; a->set_generalized_buchi(0); a->release_named_properties(); a->prop_weak(true); diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index b2f2cbedb..abfd956e6 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -181,7 +181,7 @@ namespace spot acc() const override { if (loop_) - return 0U; + return {}; return it_->acc(); } @@ -329,7 +329,7 @@ namespace spot } if (self_loop_needed && s.second != bddfalse) - res->new_edge(src, src, s.second, 0U); + res->new_edge(src, src, s.second, {}); } res->merge_edges(); return res; @@ -381,10 +381,10 @@ namespace spot unsigned tmp = p.first->second; // intermediate state unsigned i = a->new_edge(src, tmp, one, acc); assert(i > num_edges); - i = a->new_edge(tmp, tmp, one, 0U); + i = a->new_edge(tmp, tmp, one, {}); assert(i > num_edges); // No acceptance here to preserve the state-based property. - i = a->new_edge(tmp, dst, one, 0U); + i = a->new_edge(tmp, dst, one, {}); assert(i > num_edges); (void)i; } diff --git a/spot/twaalgos/sum.cc b/spot/twaalgos/sum.cc index 85e579471..93476228e 100644 --- a/spot/twaalgos/sum.cc +++ b/spot/twaalgos/sum.cc @@ -56,7 +56,7 @@ namespace spot static void copy_union(const twa_graph_ptr& res, const const_twa_graph_ptr& graph, - acc_cond::mark_t mark = 0U, + acc_cond::mark_t mark = acc_cond::mark_t({}), unsigned offset = 0U) { unsigned state_offset = res->num_states(); @@ -95,8 +95,8 @@ namespace spot res->copy_ap_of(right); auto unsatl = left->acc().unsat_mark(); - acc_cond::mark_t markl = 0U; - acc_cond::mark_t markr = 0U; + acc_cond::mark_t markl = {}; + acc_cond::mark_t markr = {}; auto left_acc = left->get_acceptance(); unsigned left_num_sets = left->num_sets(); if (!unsatl.first) diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index ec7396949..059e14eda 100644 --- a/spot/twaalgos/tau03.cc +++ b/spot/twaalgos/tau03.cc @@ -93,7 +93,7 @@ namespace spot const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, BLUE); - push(st_blue, s0, bddfalse, 0U); + push(st_blue, s0, bddfalse, {}); auto t = std::static_pointer_cast (this->emptiness_check::shared_from_this()); if (dfs_blue()) @@ -350,7 +350,7 @@ namespace spot assert(h.find(s) == h.end()); h.emplace(std::piecewise_construct, std::forward_as_tuple(s), - std::forward_as_tuple(c, 0U)); + std::forward_as_tuple(c, acc_cond::mark_t({}))); } void pop_notify(const state*) const diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index 51f988854..494145afe 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -108,7 +108,7 @@ namespace spot const state* s0 = a_->get_init_state(); inc_states(); h.add_new_state(s0, CYAN, current_weight); - push(st_blue, s0, bddfalse, 0U); + push(st_blue, s0, bddfalse, {}); auto t = std::static_pointer_cast (this->emptiness_check::shared_from_this()); if (dfs_blue()) @@ -310,7 +310,7 @@ namespace spot typedef std::pair cond_level; std::stack condition_stack; unsigned depth = 1; - condition_stack.emplace(0U, 0); + condition_stack.emplace(acc_cond::mark_t({}), 0); while (!st_red.empty()) { @@ -340,7 +340,7 @@ namespace spot current_weight.diff(a_->acc(), c_prime. get_weight()) - : acc_cond::mark_t(0U)))) + : acc_cond::mark_t({})))) { trace << " It is cyan and acceptance condition " << "is reached, report cycle" << std::endl; @@ -526,7 +526,7 @@ namespace spot (void)c; hc.emplace(std::piecewise_construct, std::forward_as_tuple(s), - std::forward_as_tuple(w, 0U)); + std::forward_as_tuple(w, acc_cond::mark_t({}))); } void pop_notify(const state*) const diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index e9440f22e..6cefdf3d8 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -87,8 +87,8 @@ namespace spot { s = one_conjunction ? s + 1 : s; const unsigned short size = code[s].sub.size; - acc_cond::mark_t fin = 0u; - acc_cond::mark_t inf = 0u; + acc_cond::mark_t fin = {}; + acc_cond::mark_t inf = {}; for (unsigned i = 1; i <= size; i += 2) { if (code[s-i].sub.op == acc_cond::acc_op::Fin) @@ -107,14 +107,15 @@ namespace spot auto m1 = code[--s].mark; for (unsigned int s : m1.sets()) { - all_clauses_.emplace_back(acc_cond::mark_t({s}), 0u); + all_clauses_.emplace_back(acc_cond::mark_t({s}), + acc_cond::mark_t({})); set_to_keep_.emplace_back(acc_cond::mark_t({s})); } } else if (code[s].sub.op == acc_cond::acc_op::Inf) // Inf { auto m2 = code[--s].mark; - all_clauses_.emplace_back(0u, m2); + all_clauses_.emplace_back(acc_cond::mark_t({}), m2); set_to_keep_.emplace_back(m2); } else @@ -183,7 +184,7 @@ namespace spot { if (all_clauses_[clause].second) { - acc_cond::mark_t m = 0u; + acc_cond::mark_t m = {}; for (unsigned set = 0; set < max_set_in_; ++set) if (all_clauses_[clause].second.has(set)) { @@ -194,11 +195,11 @@ namespace spot } else { - set_to_add_.emplace_back(0u); + set_to_add_.emplace_back(acc_cond::mark_t({})); } } - all_set_to_add_ = 0u; + all_set_to_add_ = {}; for (unsigned s = 0; s < max_set_in_; ++s) if (all_inf_.has(s)) { @@ -358,7 +359,7 @@ namespace spot if (st == init_st_in_) { for (const auto& p_dst : st_repr_[e.dst]) - res_->new_edge(res_init_, p_dst.second, e.cond, 0u); + res_->new_edge(res_init_, p_dst.second, e.cond, {}); if (!init_reachable_) continue; } @@ -378,14 +379,14 @@ namespace spot res_->new_edge(p_src.second, p_dst.second, e.cond, state_based_ ? get_edge_mark(e.acc, p_src.first) - : 0u); + : acc_cond::mark_t({})); } else { assert(st_repr_[st].size() == 1); unsigned src = st_repr_[st][0].second; - acc_cond::mark_t m = 0u; + acc_cond::mark_t m = {}; if (same_scc || state_based_) m = all_set_to_add_; @@ -451,7 +452,7 @@ namespace spot acc_cond::mark_t pend; unsigned s; - st2gba_state(unsigned st, acc_cond::mark_t bv = -1U): + st2gba_state(unsigned st, acc_cond::mark_t bv = acc_cond::mark_t::all()): pend(bv), s(st) { } @@ -495,7 +496,7 @@ namespace spot bool inor = pos->sub.op == acc_cond::acc_op::Or; if (inor) --pos; - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; while (pos > term_end) { assert(pos->sub.op == acc_cond::acc_op::Inf); @@ -554,15 +555,17 @@ namespace spot unsigned p = inf.count(); // At some point we will remove anything that is not used as Inf. acc_cond::mark_t to_strip = in->acc().all_sets() - inf; - acc_cond::mark_t inf_alone = 0U; - acc_cond::mark_t fin_alone = 0U; + acc_cond::mark_t inf_alone = {}; + acc_cond::mark_t fin_alone = {}; if (!p) return remove_fin(in); unsigned numsets = in->acc().num_sets(); - std::vector fin_to_infpairs(numsets, 0U); - std::vector inf_to_finpairs(numsets, 0U); + std::vector fin_to_infpairs(numsets, + acc_cond::mark_t({})); + std::vector inf_to_finpairs(numsets, + acc_cond::mark_t({})); for (auto pair: pairs) { if (pair.fin) @@ -581,7 +584,7 @@ namespace spot // fin_alone, but we also have fin_to_infpair[0] = {1}. This should // really be simplified to Fin(0). for (auto mark: fin_alone.sets()) - fin_to_infpairs[mark] = 0U; + fin_to_infpairs[mark] = {}; scc_info si(in, scc_info_options::NONE); @@ -598,7 +601,7 @@ namespace spot // Fin sets that are alone either because the acceptance // condition has no matching Inf, or because the SCC does not // intersect the matching Inf. - acc_cond::mark_t fin_wo_inf = 0U; + acc_cond::mark_t fin_wo_inf = {}; for (unsigned mark: acc_fin.sets()) if (!fin_to_infpairs[mark] || (fin_to_infpairs[mark] - acc_inf)) fin_wo_inf.set(mark); @@ -606,13 +609,13 @@ namespace spot // Inf sets that *do* have a matching Fin in the acceptance // condition but without matching Fin in the SCC: they can be // considered as always present in the SCC. - acc_cond::mark_t inf_wo_fin = 0U; + acc_cond::mark_t inf_wo_fin = {}; for (unsigned mark: inf.sets()) if (inf_to_finpairs[mark] && (inf_to_finpairs[mark] - acc_fin)) inf_wo_fin.set(mark); sccfi.emplace_back(fin_wo_inf, inf_wo_fin, - acc_fin == 0U, acc_inf == 0U); + !acc_fin, !acc_inf); } auto out = make_twa_graph(in->get_dict()); @@ -637,7 +640,7 @@ namespace spot bool sbacc = in->prop_state_acc().is_true(); // States of the original automaton are marked with s.pend == -1U. - const acc_cond::mark_t orig_copy(-1U); + const acc_cond::mark_t orig_copy = acc_cond::mark_t::all(); while (!todo.empty()) { @@ -658,7 +661,7 @@ namespace spot for (auto& t: in->out(s.s)) { acc_cond::mark_t pend = s.pend; - acc_cond::mark_t acc = 0U; + acc_cond::mark_t acc = {}; bool maybe_acc = maybe_acc_scc && (scc_src == si.scc_of(t.dst)); if (pend != orig_copy) @@ -725,7 +728,7 @@ namespace spot // this has to occur at least once per cycle. if (pend == orig_copy && (t.src >= t.dst) && maybe_acc && !no_fin) { - acc_cond::mark_t stpend = 0U; + acc_cond::mark_t stpend = {}; if (sbacc) { auto a = in->state_acc_sets(t.dst); @@ -808,7 +811,7 @@ namespace spot // state without successor. if (cnf.is_f()) { - assert(cnf.front().mark == 0U); + assert(!cnf.front().mark); res = make_twa_graph(aut->get_dict()); res->set_init_state(res->new_state()); res->prop_state_acc(true); @@ -826,7 +829,7 @@ namespace spot for (auto& t: res->edges()) { acc_cond::mark_t cur_m = t.acc; - acc_cond::mark_t new_m = 0U; + acc_cond::mark_t new_m = {}; for (unsigned n = 0; n < nterms; ++n) if (cur_m & terms[n]) new_m.set(n); @@ -852,7 +855,7 @@ namespace spot std::vector> res; if (acc.empty()) { - res.emplace_back(0U, 0U); + res.emplace_back(acc_cond::mark_t({}), acc_cond::mark_t({})); return res; } auto pos = &acc.back(); @@ -866,15 +869,15 @@ namespace spot // We have only a Fin term, without Inf. In this case // only, the Fin() may encode a disjunction of sets. for (auto s: pos[-1].mark.sets()) - res.emplace_back(acc_cond::mark_t({s}), 0U); + res.emplace_back(acc_cond::mark_t({s}), acc_cond::mark_t({})); pos -= pos->sub.size + 1; } else { // We have a conjunction of Fin and Inf sets. auto end = pos - pos->sub.size - 1; - acc_cond::mark_t fin = 0U; - acc_cond::mark_t inf = 0U; + acc_cond::mark_t fin = {}; + acc_cond::mark_t inf = {}; while (pos > end) { switch (pos->sub.op) @@ -958,7 +961,7 @@ namespace spot fin_set = next_set++; } - acc_cond::mark_t infsets = 0U; + acc_cond::mark_t infsets = {}; if (share_inf) for (auto s: i.second.sets()) @@ -1007,7 +1010,7 @@ namespace spot res->set_acceptance(next_set, code); for (auto& e: res->edges()) { - acc_cond::mark_t m = 0U; + acc_cond::mark_t m = {}; for (auto s: e.acc.sets()) m |= rename[s]; e.acc = m; diff --git a/spot/twaalgos/toweak.cc b/spot/twaalgos/toweak.cc index af27b706b..01af20036 100644 --- a/spot/twaalgos/toweak.cc +++ b/spot/twaalgos/toweak.cc @@ -38,7 +38,8 @@ namespace spot unsigned rank; acc_cond::mark_t mark; - rc_state(unsigned state_id, unsigned state_rank, acc_cond::mark_t m = 0U) + rc_state(unsigned state_id, unsigned state_rank, + acc_cond::mark_t m = acc_cond::mark_t({})) : id(state_id), rank(state_rank), mark(m) { } @@ -129,7 +130,7 @@ namespace spot for (unsigned m = start_set; m < numsets_; ++m) levels |= state_to_var_[new_state(d, i, {m})]; else - levels |= state_to_var_[new_state(d, i, 0U)]; + levels |= state_to_var_[new_state(d, i, {})]; } dest &= levels; } @@ -160,7 +161,7 @@ namespace spot { std::vector states; for (unsigned d: aut_->univ_dests(aut_->get_init_state_number())) - states.push_back(new_state(d, aut_->num_states() * 2, 0U)); + states.push_back(new_state(d, aut_->num_states() * 2, {})); res_->set_univ_init_state(states.begin(), states.end()); @@ -168,7 +169,7 @@ namespace spot { rc_state st = todo_.front(); - acc_cond::mark_t mark = 0U; + acc_cond::mark_t mark = {}; if (st.rank % 2) mark = {0}; diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 40059d8c2..572e01074 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -64,7 +64,7 @@ int main() auto m2 = spot::acc_cond::mark_t({0, 3}); auto m3 = spot::acc_cond::mark_t({2, 1}); - spot::acc_cond::mark_t m0 = 0U; + spot::acc_cond::mark_t m0 = {}; std::cout << m0.max_set() << ' ' << m0.min_set() << '\n'; std::cout << m3.max_set() << ' ' << m3.min_set() << '\n'; @@ -160,7 +160,7 @@ int main() // {1} // {2, 3} std::cout << code3 << ' ' << "{0} true\n"; - spot::acc_cond::mark_t m = 0U; + spot::acc_cond::mark_t m = {}; m.set(0); print(code3.missing(m, true)); std::cout << code3 << ' ' << "{0} false\n"; diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index a7eae696e..b979da6e6 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -38,12 +38,12 @@ static void f1() auto s1 = tg->new_state(); auto s2 = tg->new_state(); auto s3 = tg->new_state(); - tg->new_edge(s1, s1, bddfalse, 0U); - tg->new_edge(s1, s2, p1, 0U); + tg->new_edge(s1, s1, bddfalse, {}); + tg->new_edge(s1, s2, p1, {}); tg->new_edge(s1, s3, p2, tg->acc().mark(1)); tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0)); tg->new_edge(s3, s1, p1 | p2, spot::acc_cond::mark_t({0, 1})); - tg->new_edge(s3, s2, p1 >> p2, 0U); + tg->new_edge(s3, s2, p1 >> p2, {}); tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1})); spot::print_dot(std::cout, tg); @@ -66,7 +66,7 @@ static void f1() spot::acc_cond::mark_t all({0, 1}); tg->new_edge(s3, s1, p1 | p2, all); - tg->new_edge(s3, s2, p1 >> p2, 0U); + tg->new_edge(s3, s2, p1 >> p2, {}); tg->new_edge(s3, s1, bddtrue, all); std::cerr << tg->num_edges() << '\n'; diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index 070318900..5d15e63fc 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -249,7 +249,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Internally, the `mark_t` stores the bit-vector as an integer. This also implies that we currently do not support more than 32 acceptance sets. The underlaying integer can be retrieved using `.id`." + "Internally, the `mark_t` stores the bit-vector as an integer. This implies that we currently do not support more than 32 acceptance sets. The underlying integer can be retrieved using `.id`. Note that this implementation may evolve in the future, so relying on it is not recommended." ] }, { @@ -281,7 +281,9 @@ "source": [ "`mark_t` can also be initialized using an integer: in that case the integer is interpreted as a bit vector.\n", "\n", - "A frequent error is to use `mark_t(n)` when we really mean `mark_t([n])` or `mark_t((n,))`." + "A frequent error is to use `mark_t(n)` when we really mean `mark_t([n])` or `mark_t((n,))`.\n", + "\n", + "As the underlying implementation of `mark_t` may change in the future, it is not recommended to rely on this interface." ] }, { @@ -313,7 +315,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The different sets can be iterated over with the `sets()` method, that returns a tuble with the index of all bits set." + "The different sets can be iterated over with the `sets()` method, that returns a tuple with the index of all bits set." ] }, {