From 70c70a63a3a9e751ecb9e80764bbf7651445d229 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 1 Feb 2017 14:09:18 +0100 Subject: [PATCH] do not use non-standard anonymous structs For #214, as observed by Thibaud Michaud. * spot/twa/acc.hh: Name the anonymous struct. * spot/twa/acc.hh, spot/twa/acc.cc, spot/parseaut/parseaut.yy, spot/twaalgos/dtwasat.cc, spot/twaalgos/remfin.cc, spot/twaalgos/sepsets.cc, spot/twaalgos/totgba.cc: Adjust all usages. * NEWS: Mention the renaming. --- NEWS | 6 ++ spot/parseaut/parseaut.yy | 16 ++--- spot/twa/acc.cc | 104 +++++++++++++++---------------- spot/twa/acc.hh | 126 ++++++++++++++++++++------------------ spot/twaalgos/dtwasat.cc | 10 +-- spot/twaalgos/remfin.cc | 34 +++++----- spot/twaalgos/sepsets.cc | 6 +- spot/twaalgos/totgba.cc | 24 ++++---- 8 files changed, 169 insertions(+), 157 deletions(-) diff --git a/NEWS b/NEWS index 5e3f3a134..fcbc50fbc 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,12 @@ New in spot 2.3.0.dev (not yet released) - spot::ltsmin_model::kripke() forgot to register the "dead" proposition. + - The spot::acc_word type (used to construct acceptance condition) + was using some non-standard anonymous struct. It is unlikely that + this type was actually used outside Spot, but if you do use it, + spot::acc_word::op and spot::acc_word::type had to be renamed as + spot::acc_word::sub.op and spot::acc_word::sub.type. + New in spot 2.3 (2017-01-19) Build: diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index af2eeb487..63de3bf1d 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1,5 +1,5 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +** Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et ** Développement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -2048,33 +2048,33 @@ fix_acceptance_aux(spot::acc_cond& acc, unsigned base) { auto& w = in[pos]; - switch (w.op) + switch (w.sub.op) { case spot::acc_cond::acc_op::And: { - unsigned sub = pos - w.size; + unsigned sub = pos - w.sub.size; --pos; auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base); - pos -= in[pos].size; + pos -= in[pos].sub.size; while (sub < pos) { --pos; c &= fix_acceptance_aux(acc, in, pos, onlyneg, both, base); - pos -= in[pos].size; + pos -= in[pos].sub.size; } return c; } case spot::acc_cond::acc_op::Or: { - unsigned sub = pos - w.size; + unsigned sub = pos - w.sub.size; --pos; auto c = fix_acceptance_aux(acc, in, pos, onlyneg, both, base); - pos -= in[pos].size; + pos -= in[pos].sub.size; while (sub < pos) { --pos; c |= fix_acceptance_aux(acc, in, pos, onlyneg, both, base); - pos -= in[pos].size; + pos -= in[pos].sub.size; } return c; } diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index cede10035..350020286 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -73,14 +73,14 @@ namespace spot auto& w = code[pos]; const char* negated = ""; bool top = pos == code.size() - 1; - switch (w.op) + switch (w.sub.op) { case acc_cond::acc_op::And: op = html ? " & " : " & "; SPOT_FALLTHROUGH; case acc_cond::acc_op::Or: { - unsigned sub = pos - w.size; + unsigned sub = pos - w.sub.size; if (!top) os << '('; bool first = true; @@ -92,7 +92,7 @@ namespace spot else os << op; print_code(os, code, pos, set_printer); - pos -= code[pos].size; + pos -= code[pos].sub.size; } if (!top) os << ')'; @@ -177,29 +177,29 @@ namespace spot static bool eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: { - auto sub = pos - pos->size; + auto sub = pos - pos->sub.size; while (sub < pos) { --pos; if (!eval(inf, pos)) return false; - pos -= pos->size; + pos -= pos->sub.size; } return true; } case acc_cond::acc_op::Or: { - auto sub = pos - pos->size; + auto sub = pos - pos->sub.size; while (sub < pos) { --pos; if (eval(inf, pos)) return true; - pos -= pos->size; + pos -= pos->sub.size; } return false; } @@ -218,29 +218,29 @@ namespace spot static bool inf_eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: { - auto sub = pos - pos->size; + auto sub = pos - pos->sub.size; while (sub < pos) { --pos; if (!inf_eval(inf, pos)) return false; - pos -= pos->size; + pos -= pos->sub.size; } return true; } case acc_cond::acc_op::Or: { - auto sub = pos - pos->size; + auto sub = pos - pos->sub.size; while (sub < pos) { --pos; if (inf_eval(inf, pos)) return true; - pos -= pos->size; + pos -= pos->sub.size; } return false; } @@ -259,11 +259,11 @@ namespace spot static acc_cond::mark_t eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: { - auto sub = pos - pos->size; + auto sub = pos - pos->sub.size; acc_cond::mark_t m = 0U; while (sub < pos) { @@ -272,19 +272,19 @@ namespace spot m |= s; else return 0U; - pos -= pos->size; + pos -= pos->sub.size; } return m; } case acc_cond::acc_op::Or: { - auto sub = pos - pos->size; + auto sub = pos - pos->sub.size; while (sub < pos) { --pos; if (auto s = eval_sets(inf, pos)) return s; - pos -= pos->size; + pos -= pos->sub.size; } return 0U; } @@ -334,7 +334,7 @@ namespace spot unsigned pos = code_.size(); do { - switch (code_[pos - 1].op) + switch (code_[pos - 1].sub.op) { case acc_cond::acc_op::And: case acc_cond::acc_op::Or: @@ -369,8 +369,8 @@ namespace spot acc_cond::acc_op lowop, acc_cond::mark_t all_sets) { - unsigned s = code.back().size; - auto mainop = code.back().op; + unsigned s = code.back().sub.size; + auto mainop = code.back().sub.op; if (mainop == highop) { // The size must be a multiple of 5. @@ -388,11 +388,11 @@ namespace spot acc_cond::mark_t seen_inf = 0U; while (s) { - if (code[--s].op != lowop) + if (code[--s].sub.op != lowop) return false; - auto o1 = code[--s].op; + auto o1 = code[--s].sub.op; auto m1 = code[--s].mark; - auto o2 = code[--s].op; + auto o2 = code[--s].sub.op; auto m2 = code[--s].mark; // We assume @@ -454,10 +454,10 @@ namespace spot return true; } if (code_.is_t() - || code_.back().op != acc_op::Or) + || code_.back().sub.op != acc_op::Or) return false; - auto s = code_.back().size; + auto s = code_.back().sub.size; acc_cond::mark_t seen_fin = 0U; acc_cond::mark_t seen_inf = 0U; // Each pairs is the position of a Fin followed @@ -466,11 +466,11 @@ namespace spot while (s) { --s; - if (code_[s].op == acc_op::And) + if (code_[s].sub.op == acc_op::And) { - auto o1 = code_[--s].op; + auto o1 = code_[--s].sub.op; auto m1 = code_[--s].mark; - auto o2 = code_[--s].op; + auto o2 = code_[--s].sub.op; auto m2 = code_[--s].mark; // We assume @@ -503,7 +503,7 @@ namespace spot seen_fin |= m1; seen_inf |= m2; } - else if (code_[s].op == acc_op::Fin) + else if (code_[s].sub.op == acc_op::Fin) { auto m1 = code_[--s].mark; for (auto s: m1.sets()) @@ -597,9 +597,9 @@ namespace spot { bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map) { - auto sz = c->size; + auto sz = c->sub.size; auto start = c - sz - 1; - auto op = c->op; + auto op = c->sub.op; switch (op) { case acc_cond::acc_op::Or: @@ -609,7 +609,7 @@ namespace spot do { res |= to_bdd_rec(c, map); - c -= c->size + 1; + c -= c->sub.size + 1; } while (c > start); return res; @@ -621,7 +621,7 @@ namespace spot do { res &= to_bdd_rec(c, map); - c -= c->size + 1; + c -= c->sub.size + 1; } while (c > start); return res; @@ -1005,16 +1005,16 @@ namespace spot auto pos = &back(); auto start = &front(); auto and_scope = pos + 1; - if (pos->op == acc_cond::acc_op::Or) + if (pos->sub.op == acc_cond::acc_op::Or) --pos; while (pos > start) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::Or: return false; case acc_cond::acc_op::And: - and_scope = std::min(and_scope, pos - pos->size); + and_scope = std::min(and_scope, pos - pos->sub.size); --pos; break; case acc_cond::acc_op::Fin: @@ -1038,16 +1038,16 @@ namespace spot auto pos = &back(); auto start = &front(); auto or_scope = pos + 1; - if (pos->op == acc_cond::acc_op::And) + if (pos->sub.op == acc_cond::acc_op::And) --pos; while (pos > start) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: return false; case acc_cond::acc_op::Or: - or_scope = std::min(or_scope, pos - pos->size); + or_scope = std::min(or_scope, pos - pos->sub.size); --pos; break; case acc_cond::acc_op::Inf: @@ -1068,8 +1068,8 @@ namespace spot { acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos) { - auto start = pos - pos->size; - switch (pos->op) + auto start = pos - pos->sub.size; + switch (pos->sub.op) { case acc_cond::acc_op::And: { @@ -1079,7 +1079,7 @@ namespace spot { auto tmp = complement_rec(pos) | std::move(res); std::swap(tmp, res); - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } while (pos > start); return res; @@ -1092,7 +1092,7 @@ namespace spot { auto tmp = complement_rec(pos) & std::move(res); std::swap(tmp, res); - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } while (pos > start); return res; @@ -1125,8 +1125,8 @@ namespace spot static acc_cond::acc_code strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing) { - auto start = pos - pos->size; - switch (pos->op) + auto start = pos - pos->sub.size; + switch (pos->sub.op) { case acc_cond::acc_op::And: { @@ -1136,7 +1136,7 @@ namespace spot { auto tmp = strip_rec(pos, rem, missing) & std::move(res); std::swap(tmp, res); - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } while (pos > start); return res; @@ -1149,7 +1149,7 @@ namespace spot { auto tmp = strip_rec(pos, rem, missing) | std::move(res); std::swap(tmp, res); - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } while (pos > start); return res; @@ -1190,7 +1190,7 @@ namespace spot auto end = &front(); while (pos > end) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: case acc_cond::acc_op::Or: @@ -1220,7 +1220,7 @@ namespace spot auto end = &front(); while (pos > end) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: case acc_cond::acc_op::Or: diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index edcc08ff4..2ecff352f 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -294,7 +294,7 @@ namespace spot acc_op op; // Operator unsigned short size; // Size of the subtree (number of acc_word), // not counting this node. - }; + } sub; }; struct SPOT_API acc_code: public std::vector @@ -306,10 +306,10 @@ namespace spot return false; while (pos > 0) { - auto op = (*this)[pos - 1].op; - auto sz = (*this)[pos - 1].size; - if (other[pos - 1].op != op || - other[pos - 1].size != sz) + auto op = (*this)[pos - 1].sub.op; + auto sz = (*this)[pos - 1].sub.size; + if (other[pos - 1].sub.op != op || + other[pos - 1].sub.size != sz) return false; switch (op) { @@ -340,14 +340,14 @@ namespace spot return false; while (pos > 0) { - auto op = (*this)[pos - 1].op; - auto oop = other[pos - 1].op; + auto op = (*this)[pos - 1].sub.op; + auto oop = other[pos - 1].sub.op; if (op < oop) return true; if (op > oop) return false; - auto sz = (*this)[pos - 1].size; - auto osz = other[pos - 1].size; + auto sz = (*this)[pos - 1].sub.size; + auto osz = other[pos - 1].sub.size; if (sz < osz) return true; if (sz > osz) @@ -398,15 +398,15 @@ namespace spot bool is_t() const { unsigned s = size(); - return s == 0 - || ((*this)[s - 1].op == acc_op::Inf && (*this)[s - 2].mark == 0U); + return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf + && (*this)[s - 2].mark == 0U); } bool is_f() const { unsigned s = size(); return s > 1 - && (*this)[s - 1].op == acc_op::Fin && (*this)[s - 2].mark == 0U; + && (*this)[s - 1].sub.op == acc_op::Fin && (*this)[s - 2].mark == 0U; } static acc_code f() @@ -414,8 +414,8 @@ namespace spot acc_code res; res.resize(2); res[0].mark = 0U; - res[1].op = acc_op::Fin; - res[1].size = 1; + res[1].sub.op = acc_op::Fin; + res[1].sub.size = 1; return res; } @@ -429,8 +429,8 @@ namespace spot acc_code res; res.resize(2); res[0].mark = m; - res[1].op = acc_op::Fin; - res[1].size = 1; + res[1].sub.op = acc_op::Fin; + res[1].sub.size = 1; return res; } @@ -444,8 +444,8 @@ namespace spot acc_code res; res.resize(2); res[0].mark = m; - res[1].op = acc_op::FinNeg; - res[1].size = 1; + res[1].sub.op = acc_op::FinNeg; + res[1].sub.size = 1; return res; } @@ -459,8 +459,8 @@ namespace spot acc_code res; res.resize(2); res[0].mark = m; - res[1].op = acc_op::Inf; - res[1].size = 1; + res[1].sub.op = acc_op::Inf; + res[1].sub.size = 1; return res; } @@ -474,8 +474,8 @@ namespace spot acc_code res; res.resize(2); res[0].mark = m; - res[1].op = acc_op::InfNeg; - res[1].size = 1; + res[1].sub.op = acc_op::InfNeg; + res[1].sub.size = 1; return res; } @@ -572,8 +572,10 @@ namespace spot unsigned rs = r.size() - 1; // We want to group all Inf(x) operators: // Inf(a) & Inf(b) = Inf(a & b) - if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf) - || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg)) + if (((*this)[s].sub.op == acc_op::Inf + && r[rs].sub.op == acc_op::Inf) + || ((*this)[s].sub.op == acc_op::InfNeg + && r[rs].sub.op == acc_op::InfNeg)) { (*this)[s - 1].mark |= r[rs - 1].mark; return *this; @@ -585,43 +587,43 @@ namespace spot // left_inf points to the left Inf mark if any. // right_inf points to the right Inf mark if any. acc_word* left_inf = nullptr; - if ((*this)[s].op == acc_op::And) + if ((*this)[s].sub.op == acc_op::And) { - auto start = &(*this)[s] - (*this)[s].size; + auto start = &(*this)[s] - (*this)[s].sub.size; auto pos = &(*this)[s] - 1; pop_back(); while (pos > start) { - if (pos->op == acc_op::Inf) + if (pos->sub.op == acc_op::Inf) { left_inf = pos - 1; break; } - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } } - else if ((*this)[s].op == acc_op::Inf) + else if ((*this)[s].sub.op == acc_op::Inf) { left_inf = &(*this)[s - 1]; } acc_word* right_inf = nullptr; auto right_end = &r.back(); - if (right_end->op == acc_op::And) + if (right_end->sub.op == acc_op::And) { auto start = &r[0]; auto pos = --right_end; while (pos > start) { - if (pos->op == acc_op::Inf) + if (pos->sub.op == acc_op::Inf) { right_inf = pos - 1; break; } - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } } - else if (right_end->op == acc_op::Inf) + else if (right_end->sub.op == acc_op::Inf) { right_inf = right_end - 1; } @@ -645,8 +647,8 @@ namespace spot } acc_word w; - w.op = acc_op::And; - w.size = size(); + w.sub.op = acc_op::And; + w.sub.size = size(); emplace_back(w); return *this; } @@ -663,8 +665,10 @@ namespace spot unsigned s = size() - 1; unsigned rs = r.size() - 1; // Inf(a) & Inf(b) = Inf(a & b) - if (((*this)[s].op == acc_op::Inf && r[rs].op == acc_op::Inf) - || ((*this)[s].op == acc_op::InfNeg && r[rs].op == acc_op::InfNeg)) + if (((*this)[s].sub.op == acc_op::Inf + && r[rs].sub.op == acc_op::Inf) + || ((*this)[s].sub.op == acc_op::InfNeg + && r[rs].sub.op == acc_op::InfNeg)) { (*this)[s - 1].mark |= r[rs - 1].mark; return *this; @@ -676,43 +680,43 @@ namespace spot // left_inf points to the left Inf mark if any. // right_inf points to the right Inf mark if any. acc_word* left_inf = nullptr; - if ((*this)[s].op == acc_op::And) + if ((*this)[s].sub.op == acc_op::And) { - auto start = &(*this)[s] - (*this)[s].size; + auto start = &(*this)[s] - (*this)[s].sub.size; auto pos = &(*this)[s] - 1; pop_back(); while (pos > start) { - if (pos->op == acc_op::Inf) + if (pos->sub.op == acc_op::Inf) { left_inf = pos - 1; break; } - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } } - else if ((*this)[s].op == acc_op::Inf) + else if ((*this)[s].sub.op == acc_op::Inf) { left_inf = &(*this)[s - 1]; } const acc_word* right_inf = nullptr; auto right_end = &r.back(); - if (right_end->op == acc_op::And) + if (right_end->sub.op == acc_op::And) { auto start = &r[0]; auto pos = --right_end; while (pos > start) { - if (pos->op == acc_op::Inf) + if (pos->sub.op == acc_op::Inf) { right_inf = pos - 1; break; } - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } } - else if (right_end->op == acc_op::Inf) + else if (right_end->sub.op == acc_op::Inf) { right_inf = right_end - 1; } @@ -736,8 +740,8 @@ namespace spot } acc_word w; - w.op = acc_op::And; - w.size = size(); + w.sub.op = acc_op::And; + w.sub.size = size(); emplace_back(w); return *this; } @@ -768,20 +772,22 @@ namespace spot unsigned s = size() - 1; unsigned rs = r.size() - 1; // Fin(a) | Fin(b) = Fin(a | b) - if (((*this)[s].op == acc_op::Fin && r[rs].op == acc_op::Fin) - || ((*this)[s].op == acc_op::FinNeg && r[rs].op == acc_op::FinNeg)) + if (((*this)[s].sub.op == acc_op::Fin + && r[rs].sub.op == acc_op::Fin) + || ((*this)[s].sub.op == acc_op::FinNeg + && r[rs].sub.op == acc_op::FinNeg)) { (*this)[s - 1].mark |= r[rs - 1].mark; return *this; } - if ((*this)[s].op == acc_op::Or) + if ((*this)[s].sub.op == acc_op::Or) pop_back(); - if (r.back().op == acc_op::Or) + if (r.back().sub.op == acc_op::Or) r.pop_back(); insert(this->end(), r.begin(), r.end()); acc_word w; - w.op = acc_op::Or; - w.size = size(); + w.sub.op = acc_op::Or; + w.sub.size = size(); emplace_back(w); return *this; } @@ -812,7 +818,7 @@ namespace spot unsigned pos = size(); do { - switch ((*this)[pos - 1].op) + switch ((*this)[pos - 1].sub.op) { case acc_cond::acc_op::And: case acc_cond::acc_op::Or: @@ -1008,7 +1014,7 @@ namespace spot { unsigned s = code_.size(); return num_ == 1 && - s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets(); + s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets(); } bool is_co_buchi() const @@ -1024,15 +1030,15 @@ namespace spot bool is_generalized_buchi() const { unsigned s = code_.size(); - return (s == 0 && num_ == 0) || - (s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets()); + return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf + && code_[0].mark == all_sets()); } bool is_generalized_co_buchi() const { unsigned s = code_.size(); return (s == 2 && - code_[1].op == acc_op::Fin && code_[0].mark == all_sets()); + code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets()); } // Returns a number of pairs (>=0) if Rabin, or -1 else. diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 38547ebbf..e5ad46210 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -128,27 +128,27 @@ namespace spot trimming_map res; auto acc = input_acc.to_dnf(); auto pos = &acc.back(); - if (pos->op == acc_cond::acc_op::Or) + if (pos->sub.op == acc_cond::acc_op::Or) --pos; acc_cond::mark_t all_fin = 0U; auto start = &acc.front(); while (pos > start) { - if (pos->op == acc_cond::acc_op::Fin) + if (pos->sub.op == acc_cond::acc_op::Fin) { // We have only a Fin term, without Inf. // There is nothing to do about it. - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } else { // We have a conjunction of Fin and Inf sets. - auto end = pos - pos->size - 1; + auto end = pos - pos->sub.size - 1; acc_cond::mark_t fin = 0U; acc_cond::mark_t inf = 0U; while (pos > end) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: --pos; diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index f02faaa2c..26c6919e4 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -318,12 +318,12 @@ namespace spot { std::map res; auto pos = &acc.back(); - if (pos->op == acc_cond::acc_op::Or) + if (pos->sub.op == acc_cond::acc_op::Or) --pos; auto start = &acc.front(); while (pos > start) { - if (pos->op == acc_cond::acc_op::Fin) + if (pos->sub.op == acc_cond::acc_op::Fin) { // We have only a Fin term, without Inf. In this case // only, the Fin() may encode a disjunction of sets. @@ -333,17 +333,17 @@ namespace spot fin.set(s); res[fin] = acc_cond::acc_code{}; } - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } else { // We have a conjunction of Fin and Inf sets. - auto end = pos - pos->size - 1; + auto end = pos - pos->sub.size - 1; acc_cond::mark_t fin = 0U; acc_cond::mark_t inf = 0U; while (pos > end) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: --pos; @@ -367,8 +367,8 @@ namespace spot assert(pos == end); acc_cond::acc_word w[2]; w[0].mark = inf; - w[1].op = acc_cond::acc_op::Inf; - w[1].size = 1; + w[1].sub.op = acc_cond::acc_op::Inf; + w[1].sub.size = 1; acc_cond::acc_code c; c.insert(c.end(), w, w + 2); auto p = res.emplace(fin, c); @@ -428,27 +428,27 @@ namespace spot acc_cond::mark_t inf_alone = 0U; acc_cond::mark_t fin_alone = 0U; - auto s = code.back().size; + auto s = code.back().sub.size; // Rabin 1 - if (code.back().op == acc_cond::acc_op::And && s == 4) + if (code.back().sub.op == acc_cond::acc_op::And && s == 4) goto start_and; // Co-Büchi - else if (code.back().op == acc_cond::acc_op::Fin && s == 1) + else if (code.back().sub.op == acc_cond::acc_op::Fin && s == 1) goto start_fin; // Rabin >1 - else if (code.back().op != acc_cond::acc_op::Or) + else if (code.back().sub.op != acc_cond::acc_op::Or) return nullptr; while (s) { --s; - if (code[s].op == acc_cond::acc_op::And) + if (code[s].sub.op == acc_cond::acc_op::And) { start_and: - auto o1 = code[--s].op; + auto o1 = code[--s].sub.op; auto m1 = code[--s].mark; - auto o2 = code[--s].op; + auto o2 = code[--s].sub.op; auto m2 = code[--s].mark; // We expect // Fin({n}) & Inf({n+1}) @@ -460,12 +460,12 @@ namespace spot return nullptr; inf_pairs |= m2; } - else if (code[s].op == acc_cond::acc_op::Fin) + else if (code[s].sub.op == acc_cond::acc_op::Fin) { start_fin: fin_alone |= code[--s].mark; } - else if (code[s].op == acc_cond::acc_op::Inf) + else if (code[s].sub.op == acc_cond::acc_op::Inf) { auto m1 = code[--s].mark; if (m1.count() != 1) @@ -551,7 +551,7 @@ namespace spot auto end = &p.second.front(); while (pos > end) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: case acc_cond::acc_op::Or: diff --git a/spot/twaalgos/sepsets.cc b/spot/twaalgos/sepsets.cc index fbb2a7fb6..2e9f95f42 100644 --- a/spot/twaalgos/sepsets.cc +++ b/spot/twaalgos/sepsets.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -60,7 +60,7 @@ namespace spot acc_cond::acc_word* start = &code.front(); while (pos > start) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::Or: case acc_cond::acc_op::And: diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 33fa52390..146b8ab3d 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -70,17 +70,17 @@ namespace spot terms_t res; auto pos = &code.back(); auto end = &code.front(); - if (pos->op == acc_cond::acc_op::And) + if (pos->sub.op == acc_cond::acc_op::And) --pos; while (pos >= end) { - auto term_end = pos - 1 - pos->size; - if (pos->op == acc_cond::acc_op::Or) + auto term_end = pos - 1 - pos->sub.size; + if (pos->sub.op == acc_cond::acc_op::Or) --pos; acc_cond::mark_t m = 0U; while (pos > term_end) { - assert(pos->op == acc_cond::acc_op::Inf); + assert(pos->sub.op == acc_cond::acc_op::Inf); m |= pos[-1].mark; pos -= 2; } @@ -319,7 +319,7 @@ namespace spot auto cnf = res->get_acceptance().to_cnf(); // If we are very lucky, building a CNF actually gave us a GBA... if (cnf.empty() || - (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Inf)) + (cnf.size() == 2 && cnf.back().sub.op == acc_cond::acc_op::Inf)) { res->set_acceptance(res->num_sets(), cnf); cleanup_acceptance_here(res); @@ -379,28 +379,28 @@ namespace spot return res; } auto pos = &acc.back(); - if (pos->op == acc_cond::acc_op::Or) + if (pos->sub.op == acc_cond::acc_op::Or) --pos; auto start = &acc.front(); while (pos > start) { - if (pos->op == acc_cond::acc_op::Fin) + if (pos->sub.op == acc_cond::acc_op::Fin) { // 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); - pos -= pos->size + 1; + pos -= pos->sub.size + 1; } else { // We have a conjunction of Fin and Inf sets. - auto end = pos - pos->size - 1; + auto end = pos - pos->sub.size - 1; acc_cond::mark_t fin = 0U; acc_cond::mark_t inf = 0U; while (pos > end) { - switch (pos->op) + switch (pos->sub.op) { case acc_cond::acc_op::And: --pos;