diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index 43b7528f3..2cedfc660 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -440,8 +440,8 @@ namespace spot std::cerr << "Possible states are:"; for (ei = enum_map[type_num].begin(); ei != enum_map[type_num].end(); ++ei) - std::cerr << " " << ei->first; - std::cerr << std::endl; + std::cerr << ' ' << ei->first; + std::cerr << '\n'; free(name); ++errors; @@ -566,8 +566,8 @@ namespace spot std::cerr << "Possible states are:"; for (ei = enum_map[type_num].begin(); ei != enum_map[type_num].end(); ++ei) - std::cerr << " " << ei->first; - std::cerr << std::endl; + std::cerr << ' ' << ei->first; + std::cerr << '\n'; free(name); ++errors; @@ -906,7 +906,7 @@ namespace spot ++i; continue; } - res << vname_[i] << "=" << vars[i]; + res << vname_[i] << '=' << vars[i]; ++i; if (i == state_size_) break; @@ -993,7 +993,7 @@ namespace spot if (verbose) std::cerr << "Execution of `" << command.c_str() << "' returned exit code " << WEXITSTATUS(res) - << "." << std::endl; + << ".\n"; return true; } return false; @@ -1088,7 +1088,7 @@ namespace spot { if (verbose) std::cerr << "Failed to resolve some symbol while loading `" - << file << "'" << std::endl; + << file << "'\n"; delete d; lt_dlexit(); return 0; diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index 04ae7de62..897f69b54 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et // Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -186,7 +187,7 @@ main(int argc, char **argv) if (!echeck_inst) { std::cerr << "Failed to parse argument of -e/-E near `" - << err << "'" << std::endl; + << err << "'\n"; exit_code = 1; goto safe_exit; } diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index e97f46dde..b07efa972 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -242,10 +242,10 @@ output_formula(std::ostream& out, if (!format) { if (prefix) - out << prefix << ","; + out << prefix << ','; stream_escapable_formula(out, f, filename, linenum); if (suffix) - out << "," << suffix; + out << ',' << suffix; } else { diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index bc64f1a4e..d2985a6c8 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -347,7 +347,7 @@ namespace spot::never_claim_reachable(std::cout, aut); break; case Stats: - statistics.print(daut, aut, filename, conversion_time) << "\n"; + statistics.print(daut, aut, filename, conversion_time) << '\n'; break; } delete aut; diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index b9d6df095..0d59b79f0 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -262,7 +262,7 @@ namespace spot::never_claim_reachable(std::cout, aut, f); break; case Stats: - statistics.print(aut, f, translation_time) << "\n"; + statistics.print(aut, f, translation_time) << '\n'; break; } delete aut; diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 0d9846acf..94aedcacd 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -1061,11 +1061,11 @@ namespace std::ostream& err = global_error(); err << "error: "; if (icomp) - err << "Comp(N" << i << ")"; + err << "Comp(N" << i << ')'; else - err << "P" << i; + err << 'P' << i; if (jcomp) - err << "*Comp(P" << j << ")"; + err << "*Comp(P" << j << ')'; else err << "*N" << j; err << " is nonempty"; @@ -1079,12 +1079,12 @@ namespace << " "; spot::tgba_word w(runmin); w.simplify(); - w.print(example(), prod->get_dict()) << "\n"; + w.print(example(), prod->get_dict()) << '\n'; delete runmin; } else { - std::cerr << "\n"; + std::cerr << '\n'; } end_error(); } @@ -1142,7 +1142,7 @@ namespace } err << "} when evaluating "; if (products > 1) - err << "state-space #" << p << "/" << products << "\n"; + err << "state-space #" << p << '/' << products << '\n'; else err << "the state-space\n"; end_error(); @@ -1233,14 +1233,14 @@ namespace // complains. std::string fstr = runner.formula(); if (filename) - std::cerr << filename << ":"; + std::cerr << filename << ':'; if (linenum) - std::cerr << linenum << ":"; + std::cerr << linenum << ':'; if (filename || linenum) - std::cerr << " "; + std::cerr << ' '; if (color_opt) std::cerr << bright_white; - std::cerr << fstr << "\n"; + std::cerr << fstr << '\n'; if (color_opt) std::cerr << reset_color; @@ -1465,9 +1465,9 @@ namespace << " and N" << i; if (products > 1) err << " for state-space #" << p - << "/" << products << "\n"; + << '/' << products << '\n'; else - err << "\n"; + err << '\n'; end_error(); } } diff --git a/src/dstarparse/dra2ba.cc b/src/dstarparse/dra2ba.cc index f77a2cb13..43d41faa3 100644 --- a/src/dstarparse/dra2ba.cc +++ b/src/dstarparse/dra2ba.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -350,7 +351,7 @@ namespace spot bool scc_realizable = filter_states(dra->aut, dra, sl, final, nonfinal); dba_realizable &= scc_realizable; realizable[scc] = scc_realizable; - //std::cerr << "realizable[" << scc << "] = " << scc_realizable << "\n"; + //std::cerr << "realizable[" << scc << "] = " << scc_realizable << '\n'; } if (dba) diff --git a/src/dstarparse/fmterror.cc b/src/dstarparse/fmterror.cc index 67c468061..e4fe828d0 100644 --- a/src/dstarparse/fmterror.cc +++ b/src/dstarparse/fmterror.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -31,7 +32,7 @@ namespace spot for (it = error_list.begin(); it != error_list.end(); ++it) { if (filename != "-") - os << filename << ":"; + os << filename << ':'; os << it->first << ": "; os << it->second << std::endl; printed = true; diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc index f3ec6a5ca..cffb39e5f 100644 --- a/src/dstarparse/nsa2tgba.cc +++ b/src/dstarparse/nsa2tgba.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -222,7 +223,7 @@ namespace spot // bs2num_map::iterator i = bs2num.begin(); // while (i != bs2num.end()) // { - // std::cerr << i->second << ": (" << i->first.s << ","; + // std::cerr << i->second << ": (" << i->first.s << ','; // if (i->first.pend) // std::cerr << *i->first.pend << ")\n"; // else diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc index 564cd611d..a2d0b4f9d 100644 --- a/src/kripke/kripkeprint.cc +++ b/src/kripke/kripkeprint.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE) +// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -42,7 +42,7 @@ namespace spot void process_state(const state* s, int, tgba_succ_iterator* si) { const bdd_dict* d = aut_->get_dict(); - os_ << "\""; + os_ << '"'; escape_str(os_, aut_->format_state(s)); os_ << "\", \""; const kripke* automata = down_cast (aut_); @@ -56,7 +56,7 @@ namespace spot state* dest = si->current_state(); os_ << " \""; escape_str(os_, aut_->format_state(dest)); - os_ << "\""; + os_ << '"'; } os_ << ";\n"; } @@ -89,7 +89,7 @@ namespace spot notfirst = true; const bdd_dict* d = aut_->get_dict(); - os_ << "S" << in_s << ", \""; + os_ << 'S' << in_s << ", \""; const kripke* automata = down_cast(aut_); assert(automata); escape_str(os_, bdd_format_formula(d, diff --git a/src/kripkeparse/fmterror.cc b/src/kripkeparse/fmterror.cc index 5d8f7cc42..1142a2658 100644 --- a/src/kripkeparse/fmterror.cc +++ b/src/kripkeparse/fmterror.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE) // // This file is part of Spot, a model checking library. @@ -31,7 +32,7 @@ namespace spot for (it = error_list.begin(); it != error_list.end(); ++it) { if (filename != "-") - os << filename << ":"; + os << filename << ':'; os << it->first << ": "; os << it->second << std::endl; printed = true; diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 73db95249..8a7351697 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -112,7 +112,7 @@ namespace spot for (const auto& i: instances) os << i.second << " = " << i.second->ref_count_() << " * atomic_prop(" << i.first.first << ", " - << i.first.second->name() << ")" << std::endl; + << i.first.second->name() << ')' << std::endl; return os; } diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 2a43c4306..6dfb01e4c 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -89,7 +89,7 @@ namespace spot out << "unbounded"; else out << max_; - out << ")"; + out << ')'; return out.str(); } @@ -144,7 +144,7 @@ namespace spot out << max_; } } - out << "]"; + out << ']'; return out.str(); } diff --git a/src/ltltest/ltlrel.cc b/src/ltltest/ltlrel.cc index 45dd68df6..d97f322ef 100644 --- a/src/ltltest/ltlrel.cc +++ b/src/ltltest/ltlrel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Developement de -// l'Epita (LRDE). +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -47,7 +47,7 @@ main(int argc, char **argv) spot::ltl::relabeling_map* m = new spot::ltl::relabeling_map; const spot::ltl::formula* f2 = spot::ltl::relabel_bse(f1, spot::ltl::Pnn, m); f1->destroy(); - spot::ltl::to_string(f2, std::cout) << "\n"; + spot::ltl::to_string(f2, std::cout) << '\n'; typedef std::map map_t; @@ -59,7 +59,7 @@ main(int argc, char **argv) for (map_t::const_iterator i = sorted_map.begin(); i != sorted_map.end(); ++i) std::cout << " " << i->first << " -> " - << i->second << "\n"; + << i->second << '\n'; f2->destroy(); delete m; diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 2456e6fc3..89f884403 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -258,11 +258,11 @@ main(int argc, char** argv) // If -h is set, we want to print only formulae that have become larger. if (!f2 && (!hidereduc || (length_f1_after > length_f1_before))) { - std::cout << length_f1_before << " " << length_f1_after - << " '" << f1s_before << "' reduce to '" << f1s_after << "'"; + std::cout << length_f1_before << ' ' << length_f1_after + << " '" << f1s_before << "' reduce to '" << f1s_after << '\''; if (f1l != "" && f1l != f1s_after) - std::cout << " or (w/o rss) to '" << f1l << "'"; - std::cout << std::endl; + std::cout << " or (w/o rss) to '" << f1l << '\''; + std::cout << '\n'; } if (f2) @@ -311,7 +311,7 @@ main(int argc, char** argv) float before = sum_before; float after = sum_after; std::cout << "gain: " - << (1 - (after / before)) * 100 << "%" << std::endl; + << (1 - (after / before)) * 100 << '%' << std::endl; delete fin; } diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc index 26aecd8c8..dea1035e2 100644 --- a/src/ltltest/syntimpl.cc +++ b/src/ltltest/syntimpl.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -74,7 +74,7 @@ main(int argc, char** argv) std::cout << "Test f1 < f2" << std::endl; if (c->syntactic_implication(f1, f2)) { - std::cout << f1s << " < " << f2s << std::endl; + std::cout << f1s << " < " << f2s << '\n'; exit_return = 1; } break; @@ -83,7 +83,7 @@ main(int argc, char** argv) std::cout << "Test !f1 < f2" << std::endl; if (c->syntactic_implication_neg(f1, f2, false)) { - std::cout << "!(" << f1s << ") < " << f2s << std::endl; + std::cout << "!(" << f1s << ") < " << f2s << '\n'; exit_return = 1; } break; @@ -92,7 +92,7 @@ main(int argc, char** argv) std::cout << "Test f1 < !f2" << std::endl; if (c->syntactic_implication_neg(f1, f2, true)) { - std::cout << f1s << " < !(" << f2s << ")" << std::endl; + std::cout << f1s << " < !(" << f2s << ")\n"; exit_return = 1; } break; @@ -100,8 +100,8 @@ main(int argc, char** argv) break; } - spot::ltl::dump(std::cout, f1) << std::endl; - spot::ltl::dump(std::cout, f2) << std::endl; + spot::ltl::dump(std::cout, f1) << '\n'; + spot::ltl::dump(std::cout, f2) << '\n'; f1->destroy(); f2->destroy(); diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index 59bf1dc6b..b1172b9cb 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -160,7 +160,7 @@ namespace spot os_ << " [taillabel=\"L\"]"; else if (childnum == -2) os_ << " [taillabel=\"R\"]"; - os_ << ";" << std::endl; + os_ << ';' << std::endl; } father_ = node; @@ -190,7 +190,7 @@ namespace spot os << "digraph G {" << std::endl; f->accept(v); v.finish(); - os << "}" << std::endl; + os << '}' << std::endl; return os; } diff --git a/src/ltlvisit/lbt.cc b/src/ltlvisit/lbt.cc index 5d657656d..164c5a33a 100644 --- a/src/ltlvisit/lbt.cc +++ b/src/ltlvisit/lbt.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -88,10 +88,10 @@ namespace spot switch (c->val()) { case constant::False: - os_ << "f"; + os_ << 'f'; break; case constant::True: - os_ << "t"; + os_ << 't'; break; case constant::EmptyWord: assert(!"unsupported constant"); @@ -106,25 +106,25 @@ namespace spot switch (bo->op()) { case binop::Xor: - os_ << "^"; + os_ << '^'; break; case binop::Implies: - os_ << "i"; + os_ << 'i'; break; case binop::Equiv: - os_ << "e"; + os_ << 'e'; break; case binop::U: - os_ << "U"; + os_ << 'U'; break; case binop::R: - os_ << "V"; + os_ << 'V'; break; case binop::W: - os_ << "W"; + os_ << 'W'; break; case binop::M: - os_ << "M"; + os_ << 'M'; break; case binop::UConcat: case binop::EConcat: @@ -149,16 +149,16 @@ namespace spot switch (uo->op()) { case unop::Not: - os_ << "!"; + os_ << '!'; break; case unop::X: - os_ << "X"; + os_ << 'X'; break; case unop::F: - os_ << "F"; + os_ << 'F'; break; case unop::G: - os_ << "G"; + os_ << 'G'; break; case unop::Finish: case unop::Closure: diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 029e77692..51d5f43a2 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -291,7 +291,7 @@ namespace spot random_formula::dump_priorities(std::ostream& os) const { for (unsigned i = 0; i < proba_size_; ++i) - os << proba_[i].name << "\t" << proba_[i].proba << std::endl; + os << proba_[i].name << '\t' << proba_[i].proba << '\n'; return os; } diff --git a/src/ltlvisit/relabel.cc b/src/ltlvisit/relabel.cc index 0f06bc682..a269d1e31 100644 --- a/src/ltlvisit/relabel.cc +++ b/src/ltlvisit/relabel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -57,7 +57,7 @@ namespace spot const formula* next() { std::ostringstream s; - s << "p" << nn++; + s << 'p' << nn++; return default_environment::instance().require(s.str()); } }; @@ -401,7 +401,7 @@ namespace spot while (!s.empty()) { - // std::cerr << "-- visiting " << to_string(s.top().parent) << "\n"; + // std::cerr << "-- visiting " << to_string(s.top().parent) << '\n'; stack_entry& e = s.top(); if (e.current_child != e.last_child) { @@ -414,8 +414,8 @@ namespace spot continue; } // std::cerr << " grand parent is " - // << to_string(e.grand_parent) << "\n" - // << " child is " << to_string(child) << "\n"; + // << to_string(e.grand_parent) + // << "\n child is " << to_string(child) << '\n'; data_entry d = { num, num }; std::pair i = data.insert(fmap_t::value_type(child, d)); diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index af1d5d6ba..178374b52 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -4323,7 +4323,7 @@ namespace spot static int srec = 0; for (int i = srec; i; --i) trace << ' '; - trace << "** simplify_recursively(" << to_string(f) << ")"; + trace << "** simplify_recursively(" << to_string(f) << ')'; #endif const formula* result = c->lookup_simplified(f); diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index f0da9c113..dc1223452 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE) +// Copyright (C) 2008, 2010, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE) // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -333,7 +333,7 @@ namespace spot if (in_ratexp_) emit(KOpenSERE); else - os_ << "("; + os_ << '('; } void @@ -342,7 +342,7 @@ namespace spot if (in_ratexp_) emit(KCloseSERE); else - os_ << ")"; + os_ << ')'; } std::ostream& @@ -356,7 +356,7 @@ namespace spot { std::string str = ap->name(); if (full_parent_) - os_ << "("; + os_ << '('; if (!is_bare_word(str.c_str())) { // Spin 6 supports atomic propositions such as (a == 0) @@ -382,11 +382,11 @@ namespace spot os_ << "\\mathit{"; os_ << str.substr(0, s); if (s > 1) - os_ << "}"; + os_ << '}'; if (s != str.size()) os_ << "_{" << str.substr(s) - << "}"; + << '}'; } else { @@ -396,7 +396,7 @@ namespace spot if (kw_ == wring_kw) os_ << "=1"; if (full_parent_) - os_ << ")"; + os_ << ')'; } void @@ -492,7 +492,7 @@ namespace spot emit(KCloseSERE); if (bo->second() == constant::true_instance()) { - os_ << "!"; + os_ << '!'; in_ratexp_ = false; goto second_done; } @@ -501,7 +501,7 @@ namespace spot top_level_ = false; break; case binop::EConcatMarked: - os_ << "}"; + os_ << '}'; emit(onelast ? KSeqMarkedNext : KSeqMarked); in_ratexp_ = false; top_level_ = false; @@ -676,13 +676,13 @@ namespace spot need_parent = true; break; case unop::Closure: - os_ << "{"; + os_ << '{'; in_ratexp_ = true; top_level_ = true; break; case unop::NegClosure: emit(KNot); - os_ << "{"; + os_ << '{'; in_ratexp_ = true; top_level_ = true; break; @@ -704,7 +704,7 @@ namespace spot { case unop::Closure: case unop::NegClosure: - os_ << "}"; + os_ << '}'; in_ratexp_ = false; top_level_ = false; break; @@ -731,18 +731,18 @@ namespace spot bool top_level = top_level_; top_level_ = false; if (!top_level) - os_ << "("; - os_ << ao->get_nfa()->get_name() << "("; + os_ << '('; + os_ << ao->get_nfa()->get_name() << '('; unsigned max = ao->size(); ao->nth(0)->accept(*this); for (unsigned n = 1; n < max; ++n) { - os_ << ","; + os_ << ','; ao->nth(n)->accept(*this); } - os_ << ")"; + os_ << ')'; if (!top_level) - os_ << ")"; + os_ << ')'; } void @@ -767,7 +767,7 @@ namespace spot if (i + 2 < max && mo->nth(i) == mo->nth(i + 2)) { emit(KEqualBunop); - os_ << "1"; + os_ << '1'; emit(KCloseBunop); i += 2; } diff --git a/src/misc/bitvect.cc b/src/misc/bitvect.cc index 53039e7ed..874df0bf2 100644 --- a/src/misc/bitvect.cc +++ b/src/misc/bitvect.cc @@ -185,7 +185,7 @@ namespace spot os.width(w); os << i; os.width(1); - os << ": " << a.at(i) << "\n"; + os << ": " << a.at(i) << '\n'; } return os; } diff --git a/src/misc/optionmap.cc b/src/misc/optionmap.cc index ebe543039..95ead80bc 100644 --- a/src/misc/optionmap.cc +++ b/src/misc/optionmap.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -156,7 +156,7 @@ namespace spot { for (std::map::const_iterator it = m.options_.begin(); it != m.options_.end(); ++it) - os << "\"" << it->first << "\" = " << it->second << std::endl; + os << '"' << it->first << "\" = " << it->second << '\n'; return os; } } diff --git a/src/misc/timer.cc b/src/misc/timer.cc index 86e80c1c8..26474952d 100644 --- a/src/misc/timer.cc +++ b/src/misc/timer.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -61,15 +61,15 @@ namespace spot const char* sep = t.is_running() ? "+|" : " |"; os << std::setw(22) << name << sep - << std::setw(6) << t.utime() << " " + << std::setw(6) << t.utime() << ' ' << std::setw(8) << (total.utime ? 100.0 * t.utime() / total.utime : 0.) << sep - << std::setw(6) << t.stime() << " " + << std::setw(6) << t.stime() << ' ' << std::setw(8) << (total.stime ? 100.0 * t.stime() / total.stime : 0.) << sep - << std::setw(6) << t.utime() + t.stime() << " " + << std::setw(6) << t.utime() + t.stime() << ' ' << std::setw(8) << (grand_total ? (100.0 * (t.utime() + t.stime()) / grand_total) : 0.) @@ -80,13 +80,13 @@ namespace spot os << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl << std::setw(22) << "TOTAL" << " |" - << std::setw(6) << total.utime << " " + << std::setw(6) << total.utime << ' ' << std::setw(8) << 100. << " |" - << std::setw(6) << total.stime << " " + << std::setw(6) << total.stime << ' ' << std::setw(8) << 100. << " |" - << std::setw(6) << grand_total << " " + << std::setw(6) << grand_total << ' ' << std::setw(8) << 100. << " |" << std::endl; diff --git a/src/neverparse/fmterror.cc b/src/neverparse/fmterror.cc index 8984cecf1..092763153 100644 --- a/src/neverparse/fmterror.cc +++ b/src/neverparse/fmterror.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -31,7 +32,7 @@ namespace spot for (it = error_list.begin(); it != error_list.end(); ++it) { if (filename != "-") - os << filename << ":"; + os << filename << ':'; os << it->first << ": "; os << it->second << std::endl; printed = true; diff --git a/src/priv/freelist.cc b/src/priv/freelist.cc index dbfa8f432..9a2c4fce0 100644 --- a/src/priv/freelist.cc +++ b/src/priv/freelist.cc @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita. // Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -201,7 +204,7 @@ namespace spot { free_list_type::const_iterator i; for (i = fl.begin(); i != fl.end(); ++i) - os << " (" << i->first << ", " << i->second << ")"; + os << " (" << i->first << ", " << i->second << ')'; return os; } diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc index 204912b3c..ddb8fd5da 100644 --- a/src/saba/sabacomplementtgba.cc +++ b/src/saba/sabacomplementtgba.cc @@ -425,11 +425,11 @@ namespace spot dynamic_cast(state); assert(s); std::ostringstream ss; - ss << "{" - << "original: " << automaton_->format_state(s->get_state()) << std::endl - << "rank: " << s->get_rank() << "}" << std::endl - << "acc: " << bdd_format_accset(get_dict(), s->acceptance_conditions()) - << "}"; + ss << "{ original: " << automaton_->format_state(s->get_state()) + << "\n rank: " << s->get_rank() + << "\n acc: " << bdd_format_accset(get_dict(), + s->acceptance_conditions()) + << " }"; return ss.str(); } diff --git a/src/sabaalgos/sabadotty.cc b/src/sabaalgos/sabadotty.cc index abb09a3d2..7f3bf1fc7 100644 --- a/src/sabaalgos/sabadotty.cc +++ b/src/sabaalgos/sabadotty.cc @@ -1,4 +1,5 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -46,7 +47,7 @@ namespace spot void end() { - os_ << "}" << std::endl; + os_ << '}' << std::endl; } void @@ -57,9 +58,8 @@ namespace spot + "\\n" + bdd_format_accset(automata_->get_dict(), s->acceptance_conditions()); - os_ << " " << n << " " - << "[label=\"" << label << "\"];" - << std::endl; + os_ << " " << n << ' ' + << "[label=\"" << label << "\"];\n"; } void @@ -76,8 +76,7 @@ namespace spot si->current_condition()); os_ << " " << in << " -> s" << in << "sc" << sc_id - << " [label=\"" << label << "\", arrowhead=\"none\"];" - << std::endl; + << " [label=\"" << label << "\", arrowhead=\"none\"];\n"; } void @@ -88,8 +87,7 @@ namespace spot const saba_succ_iterator*) { os_ << " s" << in << "sc" << sc_id << " -> " << out - << " [label=\"\"];" - << std::endl; + << " [label=\"\"];\n"; } private: diff --git a/src/sanity/style.test b/src/sanity/style.test index f5caf5070..33416b6da 100755 --- a/src/sanity/style.test +++ b/src/sanity/style.test @@ -84,6 +84,13 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do grep Copyright $file >/dev/null || diag "missing copyright" + # If some grep implementation ignore LC_ALL=C, this rule might be + # a problem on utf-8 characters such as "δ" which really + # corresponds to multiple bytes, but might be matched as a single + # character by grep. + grep '<< *"\([^\\]\|\\.\)"' $file && + diag "Use << 'c' instead" 'of << "c".' + # A doxygen comments such as # # | \brief foo @@ -210,7 +217,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do grep '[ ];' $tmp && diag 'No space before semicolon.' - grep -v 'for (.*;;)' $tmp | grep ';[^ ")]' && + grep -v 'for (.*;;)' $tmp | grep ';[^ ")'"']" && diag 'Must have space or newline after semicolon.' grep '}.*}' $tmp && diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index 698f74645..2f9774e90 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developpement -// de l Epita (LRDE). +// Copyright (C) 2010, 2012, 2014 Laboratoire de Recherche et +// Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -72,7 +72,7 @@ namespace spot void end() { - os_ << "}" << std::endl; + os_ << '}' << std::endl; } void diff --git a/src/taalgos/minimize.cc b/src/taalgos/minimize.cc index 9c6484ebf..c8bb745da 100644 --- a/src/taalgos/minimize.cc +++ b/src/taalgos/minimize.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -51,14 +51,14 @@ namespace spot static std::ostream& dump_hash_set(const hash_set* hs, const ta* aut, std::ostream& out) { - out << "{"; + out << '{'; const char* sep = ""; for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i) { out << sep << aut->format_state(*i); sep = ", "; } - out << "}"; + out << '}'; return out; } @@ -475,7 +475,7 @@ namespace spot #ifdef TRACE trace << "Final partition: "; for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) - trace << format_hash_set(*i, ta_) << " "; + trace << format_hash_set(*i, ta_) << ' '; trace << std::endl; #endif diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index b65c40e18..af820e300 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -218,7 +218,7 @@ namespace spot std::ostringstream s; // FIXME: We could be smarter and reuse unused "$n" numbers. - s << ltl::to_string(i.f) << "$" << ++i.clone_counts; + s << ltl::to_string(i.f) << '$' << ++i.clone_counts; const ltl::formula* f = ltl::atomic_prop::instance(s.str(), ltl::default_environment::instance()); @@ -416,7 +416,7 @@ namespace spot unsigned s = bdd_map.size(); for (unsigned i = 0; i < s; ++i) { - os << " " << i << " "; + os << ' ' << i << ' '; const bdd_info& r = bdd_map[i]; switch (r.type) { @@ -424,16 +424,16 @@ namespace spot os << (r.refs.empty() ? "Free" : "Anon"); break; case now: - os << "Now[" << to_string(r.f) << "]"; + os << "Now[" << to_string(r.f) << ']'; break; case next: - os << "Next[" << to_string(r.f) << "]"; + os << "Next[" << to_string(r.f) << ']'; break; case acc: - os << "Acc[" << to_string(r.f) << "]"; + os << "Acc[" << to_string(r.f) << ']'; break; case var: - os << "Var[" << to_string(r.f) << "]"; + os << "Var[" << to_string(r.f) << ']'; break; } if (!r.refs.empty()) @@ -441,10 +441,10 @@ namespace spot os << " x" << r.refs.size() << " {"; for (ref_set::const_iterator si = r.refs.begin(); si != r.refs.end(); ++si) - os << " " << *si; + os << ' ' << *si; os << " }"; } - os << "\n"; + os << '\n'; } os << "Anonymous lists:\n"; bdd_dict_priv::free_anonymous_list_of_type::const_iterator ai; @@ -456,7 +456,7 @@ namespace spot } os << "Free list:\n"; priv_->dump_free_list(os); - os << std::endl; + os << '\n'; return os; } diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 589003c14..2a8e32866 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2012, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 +// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université +// Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -63,24 +64,24 @@ namespace spot if (want_acc) { o << "Acc["; - print_ltl(ref.f, o) << "]"; + print_ltl(ref.f, o) << ']'; } else { - o << "\""; - print_ltl(ref.f, o) << "\""; + o << '"'; + print_ltl(ref.f, o) << '"'; } break; case bdd_dict::now: o << "Now["; - print_ltl(ref.f, o) << "]"; + print_ltl(ref.f, o) << ']'; break; case bdd_dict::next: o << "Next["; - print_ltl(ref.f, o) << "]"; + print_ltl(ref.f, o) << ']'; break; case bdd_dict::anon: - o << "?" << v; + o << '?' << v; } } @@ -95,13 +96,11 @@ namespace spot if (varset[v] < 0) continue; if (not_first) - *where << " "; + *where << ' '; else not_first = true; if (varset[v] == 0) - // The space is important for LBTT, but we have to hide it - // from our style checking droid. - *where << "!"" "; + *where << "! "; print_handler(*where, v); } } @@ -123,7 +122,7 @@ namespace spot for (int v = 0; v < size; ++v) if (varset[v] > 0) { - *where << " "; + *where << ' '; print_handler(*where, v); } } @@ -160,7 +159,7 @@ namespace spot first_done = false; bdd_allsat(b, print_accset_handler); if (first_done) - *where << "}"; + *where << '}'; return os; } diff --git a/src/tgba/futurecondcol.cc b/src/tgba/futurecondcol.cc index 019eff8b3..547623fbb 100644 --- a/src/tgba/futurecondcol.cc +++ b/src/tgba/futurecondcol.cc @@ -1,4 +1,6 @@ -// Copyright (C) 2009 Laboratoire de recherche et développement de l'Epita. +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2014 Laboratoire de recherche et développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -81,7 +83,7 @@ namespace spot str << ", "; bdd_print_formula(str, get_dict(), *i); } - str << "]"; + str << ']'; return str.str(); } } diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index 4e5e08d11..50e5e4fba 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -242,7 +242,7 @@ namespace spot os << "State: " << label_to_string(i->first) << std::endl; for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) { - os << " " << format_state_set((*i2)->dst) + os << ' ' << format_state_set((*i2)->dst) << ", C:" << (*i2)->condition << ", A:" << (*i2)->acceptance_conditions << std::endl; } diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc index 8e18897e9..c9f953c53 100644 --- a/src/tgba/tgbakvcomplement.cc +++ b/src/tgba/tgbakvcomplement.cc @@ -82,7 +82,7 @@ namespace spot << bdd_format_accset(a->get_dict(), condition.get_bdd()) << "} "; } - ss << "}"; + ss << '}'; return ss.str(); } }; @@ -652,14 +652,14 @@ namespace spot ++i) { ss << " {" << automaton_->format_state(i->first.get()) - << ", " << i->second.format(this) << "}" << std::endl; + << ", " << i->second.format(this) << "}\n"; } ss << "} odd-less: {"; for (shared_state_set::const_iterator i = state_filter.begin(); i != state_filter.end(); ++i) - ss << " " << automaton_->format_state(i->get()) << std::endl; + ss << " " << automaton_->format_state(i->get()) << '\n'; ss << "} }"; return ss.str(); } diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 9655650aa..14fd488fd 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -755,7 +755,7 @@ namespace spot } std::cout << "node" << this_node << "[label=\""; - std::cout << this_node->name << "|"; + std::cout << this_node->name << '|'; for (auto j: this_node->nodes) { stnum_t::const_iterator it = node_names.find(j); @@ -799,16 +799,16 @@ namespace spot i != a->automaton.rend(); ++i) { - std::cout << "subgraph sg" << i->first << "{" << std::endl; + std::cout << "subgraph sg" << i->first << '{' << std::endl; print_safra_tree(i->first, node_names, current_node, nb_accepting_conditions); - std::cout << "}" << std::endl; + std::cout << "}\n"; // Successors. for (const auto& j: i->second) std::cout << "node" << i->first << "->" << "node" << j.second << - " [label=\"" << bddset << j.first << "\"];" << std::endl; + " [label=\"" << bddset << j.first << "\"];\n"; } // Output the real name of all states. @@ -819,10 +819,7 @@ namespace spot std::cout << "" << nn.second << "" << a->get_sba()->format_state(nn.first) << "\n"; - std::cout << "\n" - << ">]}" << std::endl; - - std::cout << "}" << std::endl; + std::cout << "\n>]}\n}\n"; } } // test diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index 4f6bd839f..d78fa0c2a 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -183,9 +183,9 @@ namespace spot return ltl::unop::instance(ltl::unop::G, i->second->clone()); std::ostringstream s; - s << "["; + s << '['; to_string(f, s); - s << "]"; + s << ']'; res = suspenv.require(s.str()); // We have to clone f, because it is not always a sub-tree // of the original formula. (Think n-ary operators.) diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc index f5537ca87..974a9a724 100644 --- a/src/tgbaalgos/cycles.cc +++ b/src/tgbaalgos/cycles.cc @@ -182,11 +182,11 @@ namespace spot ++i; do { - std::cout << aut_->format_state(i->ts->first) << " "; + std::cout << aut_->format_state(i->ts->first) << ' '; ++i; } while (i != dfs_.end()); - std::cout << "\n"; + std::cout << '\n'; return true; } diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index ec5636be2..2cd13d5bc 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -56,7 +57,7 @@ namespace spot void end() { - os_ << "}" << std::endl; + os_ << '}' << std::endl; } void @@ -83,7 +84,7 @@ namespace spot accepting = false; } - os_ << " " << n << " " + os_ << " " << n << ' ' << dd_->state_decl(aut_, s, n, si, escape_str(aut_->format_state(s)), accepting) @@ -109,7 +110,7 @@ namespace spot label += s; } - os_ << " " << in << " -> " << out << " " + os_ << " " << in << " -> " << out << ' ' << dd_->link_decl(aut_, in_s, in, out_s, out, si, escape_str(label)) << '\n'; diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index 95303447d..eaa6c06ca 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -177,25 +177,25 @@ namespace spot std::ostream& operator<<(std::ostream& os, const state_pair& p) { - os << "<" << p.a << "," << p.b << ">"; + os << '<' << p.a << ',' << p.b << '>'; return os; } std::ostream& operator<<(std::ostream& os, const transition& t) { - os << "<" << t.src << "," + os << '<' << t.src << ',' << bdd_format_formula(debug_dict, t.cond) - << "," << t.dst << ">"; + << ',' << t.dst << '>'; return os; } std::ostream& operator<<(std::ostream& os, const path& p) { - os << "<" - << p.src_cand << "," - << p.src_ref << "," - << p.dst_cand << "," - << p.dst_ref << ">"; + os << '<' + << p.src_cand << ',' + << p.src_ref << ',' + << p.dst_cand << ',' + << p.dst_ref << '>'; return os; } @@ -366,8 +366,8 @@ namespace spot #if DEBUG debug_dict = ref->get_dict(); - dout << "ref_size: " << ref_size << "\n"; - dout << "cand_size: " << d.cand_size << "\n"; + dout << "ref_size: " << ref_size << '\n'; + dout << "cand_size: " << d.cand_size << '\n'; #endif dout << "symmetry-breaking clauses\n"; @@ -382,7 +382,7 @@ namespace spot { transition t(i, s, k); int ti = d.transid[t]; - dout << "¬" << t << "\n"; + dout << "¬" << t << '\n'; out << -ti << " 0\n"; ++nclauses; } @@ -409,7 +409,7 @@ namespace spot if (q2 != d.cand_size) out << " ∨ "; } - out << "\n"; + out << '\n'; #endif for (int q2 = 1; q2 <= d.cand_size; q2++) @@ -417,7 +417,7 @@ namespace spot transition t(q1, s, q2); int ti = d.transid[t]; - out << ti << " "; + out << ti << ' '; } out << "0\n"; @@ -426,7 +426,7 @@ namespace spot } dout << "(2) the initial state is reachable\n"; - dout << state_pair(1, 1) << "\n"; + dout << state_pair(1, 1) << '\n'; out << d.prodid[state_pair(1, 1)] << " 0\n"; ++nclauses; @@ -461,8 +461,8 @@ namespace spot if (pit->second == succ) continue; - dout << pit->first << " ∧ " << t << "δ → " << p2 << "\n"; - out << -pit->second << " " << -ti << " " + dout << pit->first << " ∧ " << t << "δ → " << p2 << '\n'; + out << -pit->second << ' ' << -ti << ' ' << succ << " 0\n"; ++nclauses; } @@ -492,7 +492,7 @@ namespace spot path p1(q1, q1p, q2, q2p); dout << "(4&5) matching paths from reference based on " - << p1 << "\n"; + << p1 << '\n'; int pid1; if (q1 == q2 && q1p == q2p) @@ -530,7 +530,7 @@ namespace spot dout << p1 << "R ∧ " << t << "δ → ¬" << t << "F\n"; - out << -pid1 << " " << -ti << " " + out << -pid1 << ' ' << -ti << ' ' << -ta << " 0\n"; ++nclauses; } @@ -556,7 +556,7 @@ namespace spot dout << p1 << "R ∧ " << t << "δ → " << p2 << "R\n"; - out << -pid1 << " " << -ti << " " + out << -pid1 << ' ' << -ti << ' ' << pid2 << " 0\n"; ++nclauses; } @@ -585,7 +585,7 @@ namespace spot { path p1(q1, q1p, q2, q2p); dout << "(6&7) matching paths from candidate based on " - << p1 << "\n"; + << p1 << '\n'; int pid1; if (q1 == q2 && q1p == q2p) @@ -625,7 +625,7 @@ namespace spot dout << p1 << "C ∧ " << t << "δ → " << t << "F\n"; - out << -pid1 << " " << -ti << " " << ta + out << -pid1 << ' ' << -ti << ' ' << ta << " 0\n"; ++nclauses; } @@ -651,8 +651,8 @@ namespace spot dout << p1 << "C ∧ " << t << "δ ∧ ¬" << t << "F → " << p2 << "C\n"; - out << -pid1 << " " << -ti << " " - << ta << " " << pid2 << " 0\n"; + out << -pid1 << ' ' << -ti << ' ' + << ta << ' ' << pid2 << " 0\n"; ++nclauses; } } @@ -662,7 +662,7 @@ namespace spot } } out.seekp(0); - out << "p cnf " << d.nvars << " " << nclauses.nb_clauses(); + out << "p cnf " << d.nvars << ' ' << nclauses.nb_clauses(); return std::make_pair(d.nvars, nclauses.nb_clauses()); } @@ -719,7 +719,7 @@ namespace spot last_aut_trans->condition = t->second.cond; last_sat_trans = &t->second; - dout << v << "\t" << t->second << "δ\n"; + dout << v << '\t' << t->second << "δ\n"; // Mark the transition as accepting if the source is. if (state_based @@ -732,7 +732,7 @@ namespace spot t = satdict.revtransacc.find(v); if (t != satdict.revtransacc.end()) { - dout << v << "\t" << t->second << "F\n"; + dout << v << '\t' << t->second << "F\n"; if (last_sat_trans && t->second == *last_sat_trans) { assert(!state_based); @@ -757,7 +757,7 @@ namespace spot for (std::map::const_iterator pit = satdict.prodid.begin(); pit != satdict.prodid.end(); ++pit) if (positive.find(pit->second) != positive.end()) - dout << pit->second << "\t" << pit->first << "\n"; + dout << pit->second << '\t' << pit->first << "C\n"; else dout << -pit->second << "\t¬" << pit->first << "C\n"; @@ -766,17 +766,16 @@ namespace spot satdict.pathid_cand.begin(); pit != satdict.pathid_cand.end(); ++pit) if (positive.find(pit->second) != positive.end()) - dout << pit->second << "\t" << pit->first << "C\n"; + dout << pit->second << '\t' << pit->first << "C\n"; else dout << -pit->second << "\t¬" << pit->first << "C\n"; - dout << "--- pathid_ref variables ---\n"; for (std::map::const_iterator pit = satdict.pathid_ref.begin(); pit != satdict.pathid_ref.end(); ++pit) if (positive.find(pit->second) != positive.end()) - dout << pit->second << "\t" << pit->first << "R\n"; + dout << pit->second << '\t' << pit->first << "R\n"; else dout << -pit->second << "\t¬" << pit->first << "C\n"; @@ -785,7 +784,7 @@ namespace spot satdict.pathcand.begin(); pit != satdict.pathcand.end(); ++pit) if (positive.find(pit->second) != positive.end()) - dout << pit->second << "\t" << pit->first << "C\n"; + dout << pit->second << '\t' << pit->first << "C\n"; else dout << -pit->second << "\t¬" << pit->first << "C\n"; @@ -850,7 +849,7 @@ namespace spot if (show && res) dotty_reachable(std::cout, res); - trace << "dtba_sat_synthetize(...) = " << res << "\n"; + trace << "dtba_sat_synthetize(...) = " << res << '\n'; return res; } diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index f0aca39e2..067ad9046 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -213,31 +213,31 @@ namespace spot std::ostream& operator<<(std::ostream& os, const transition& t) { - os << "<" << t.src << "," + os << '<' << t.src << ',' << bdd_format_formula(debug_dict, t.cond) - << "," << t.dst << ">"; + << ',' << t.dst << '>'; return os; } std::ostream& operator<<(std::ostream& os, const transition_acc& t) { - os << "<" << t.src << "," - << bdd_format_formula(debug_dict, t.cond) << "," + os << '<' << t.src << ',' + << bdd_format_formula(debug_dict, t.cond) << ',' << bdd_format_accset(debug_dict, t.acc) - << "," << t.dst << ">"; + << ',' << t.dst << '>'; return os; } std::ostream& operator<<(std::ostream& os, const path& p) { - os << "<" - << p.src_cand << "," - << p.src_ref << "," - << p.dst_cand << "," + os << '<' + << p.src_cand << ',' + << p.src_ref << ',' + << p.dst_cand << ',' << p.dst_ref << ", " << bdd_format_accset(debug_dict, p.acc_cand) << ", " - << bdd_format_accset(debug_dict, p.acc_ref) << ">"; + << bdd_format_accset(debug_dict, p.acc_ref) << '>'; return os; } @@ -511,8 +511,8 @@ namespace spot #if DEBUG debug_dict = ref->get_dict(); - dout << "ref_size: " << ref_size << "\n"; - dout << "cand_size: " << d.cand_size << "\n"; + dout << "ref_size: " << ref_size << '\n'; + dout << "cand_size: " << d.cand_size << '\n'; #endif dout << "symmetry-breaking clauses\n"; @@ -527,7 +527,7 @@ namespace spot { transition t(i, s, k); int ti = d.transid[t]; - dout << "¬" << t << "\n"; + dout << "¬" << t << '\n'; out << -ti << " 0\n"; ++nclauses; } @@ -554,7 +554,7 @@ namespace spot if (q2 != d.cand_size) out << " ∨ "; } - out << "\n"; + out << '\n'; #endif for (int q2 = 1; q2 <= d.cand_size; q2++) @@ -562,7 +562,7 @@ namespace spot transition t(q1, s, q2); int ti = d.transid[t]; - out << ti << " "; + out << ti << ' '; } out << "0\n"; ++nclauses; @@ -570,7 +570,7 @@ namespace spot } dout << "(9) the initial state is reachable\n"; - dout << path(1, 1) << "\n"; + dout << path(1, 1) << '\n'; out << d.pathid[path(1, 1)] << " 0\n"; ++nclauses; @@ -605,8 +605,8 @@ namespace spot if (p1id == succ) continue; - dout << p1 << " ∧ " << t << "δ → " << p2 << "\n"; - out << -p1id << " " << -ti << " " << succ << " 0\n"; + dout << p1 << " ∧ " << t << "δ → " << p2 << '\n'; + out << -p1id << ' ' << -ti << ' ' << succ << " 0\n"; ++nclauses; } } @@ -639,7 +639,7 @@ namespace spot path p(q1, q1p, q2, q2p, d.all_cand_acc[f], d.all_ref_acc[fp]); - dout << "(11&12&13) paths from " << p << "\n"; + dout << "(11&12&13) paths from " << p << '\n'; int pid = d.pathid[p]; @@ -698,7 +698,7 @@ namespace spot } out << ")\n"; #endif // DEBUG - out << -pid << " " << -ti; + out << -pid << ' ' << -ti; // 11 bdd all_f = d.all_cand_acc.back(); @@ -712,7 +712,7 @@ namespace spot one, q1); int tai = d.transaccid[ta]; assert(tai != 0); - out << " " << -tai; + out << ' ' << -tai; } out << " 0\n"; ++nclauses; @@ -754,8 +754,8 @@ namespace spot int tai = d.transaccid[ta]; assert(tai != 0); - out << -pid << " " << -ti - << " " << tai << " 0\n"; + out << -pid << ' ' << -ti + << ' ' << tai << " 0\n"; ++nclauses; } } @@ -799,9 +799,9 @@ namespace spot transition_acc ta(q2, l, a, q3); out << " ∧ ¬" << ta << "FC"; } - out << " → " << p2 << "\n"; + out << " → " << p2 << '\n'; #endif - out << -pid << " " << -ti << " "; + out << -pid << ' ' << -ti << ' '; bdd biga = d.all_cand_acc[f]; while (biga != bddfalse) { @@ -810,7 +810,7 @@ namespace spot transition_acc ta(q2, l, a, q3); int tai = d.transaccid[ta]; - out << -tai << " "; + out << -tai << ' '; } biga = d.all_cand_acc.back() - d.all_cand_acc[f]; @@ -821,7 +821,7 @@ namespace spot transition_acc ta(q2, l, a, q3); int tai = d.transaccid[ta]; - out << tai << " "; + out << tai << ' '; } out << p2id << " 0\n"; @@ -836,7 +836,7 @@ namespace spot } } out.seekp(0); - out << "p cnf " << d.nvars << " " << nclauses.nb_clauses(); + out << "p cnf " << d.nvars << ' ' << nclauses.nb_clauses(); return std::make_pair(d.nvars, nclauses.nb_clauses()); } @@ -891,7 +891,7 @@ namespace spot last_aut_trans->condition = t->second.cond; last_sat_trans = &t->second; - dout << v << "\t" << t->second << "δ\n"; + dout << v << '\t' << t->second << "δ\n"; if (state_based) { @@ -910,7 +910,7 @@ namespace spot // increasing order. if (ta != satdict.revtransaccid.end()) { - dout << v << "\t" << ta->second << "F\n"; + dout << v << '\t' << ta->second << "F\n"; if (last_sat_trans && ta->second.src == last_sat_trans->src && @@ -933,7 +933,7 @@ namespace spot satdict.pathid.begin(); pit != satdict.pathid.end(); ++pit) if (positive.find(pit->second) != positive.end()) - dout << pit->second << "\t" << pit->first << "C\n"; + dout << pit->second << '\t' << pit->first << "C\n"; #endif a->merge_transitions(); @@ -999,7 +999,7 @@ namespace spot if (show && res) dotty_reachable(std::cout, res); - trace << "dtgba_sat_synthetize(...) = " << res << "\n"; + trace << "dtgba_sat_synthetize(...) = " << res << '\n'; return res; } diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 3ded8d290..3308ffb20 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.cc @@ -89,7 +89,7 @@ namespace spot os << " " << a->format_state(i->s) << std::endl; os << " | "; bdd_print_formula(os, d, i->label); - os << "\t"; + os << '\t'; bdd_print_accset(os, d, i->acc); os << std::endl; } @@ -100,9 +100,9 @@ namespace spot os << " " << a->format_state(i->s) << std::endl; os << " | "; bdd_print_formula(os, d, i->label); - os << "\t"; + os << '\t'; bdd_print_accset(os, d, i->acc); - os << std::endl; + os << '\n'; } return os; } @@ -288,7 +288,7 @@ namespace spot std::string format_state(const tgba* a, const state* s, int n) { std::ostringstream os; - os << a->format_state(s) << " (" << n << ")"; + os << a->format_state(s) << " (" << n << ')'; return os.str(); } } diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 6e84d67f3..0fc7b1ea9 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -392,7 +392,7 @@ namespace spot for (todo_list::const_iterator ti = todo.begin(); ti != todo.end(); ++ti) { ++pos; - os << "#" << pos << " s:" << ti->s << " n:" << ti->n + os << '#' << pos << " s:" << ti->s << " n:" << ti->n << " q:{"; for (succ_queue::const_iterator qi = ti->q.begin(); qi != ti->q.end();) { @@ -401,7 +401,7 @@ namespace spot if (qi != ti->q.end()) os << ", "; } - os << "}" << std::endl; + os << '}' << std::endl; } } diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 5b65d66cd..88b7fe6a0 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -103,7 +103,7 @@ namespace spot trace << "Main iteration (top = " << top << ", dftop = " << dftop << ", s = " << a_->format_state(stack[dftop].s) - << ")" << std::endl; + << ')' << std::endl; tgba_succ_iterator* iter = stack[dftop].lasttr; bool cont; @@ -170,7 +170,7 @@ namespace spot push(const state* s, bool accepting) { trace << " push(s = " << a_->format_state(s) - << ", accepting = " << accepting << ")" << std::endl; + << ", accepting = " << accepting << ")\n"; h[s] = ++top; @@ -194,7 +194,7 @@ namespace spot void pop() { - trace << " pop()" << std::endl; + trace << " pop()\n"; int p = stack[dftop].pre; if (p >= 0) @@ -217,10 +217,9 @@ namespace spot lowlinkupdate(int f, int t) { trace << " lowlinkupdate(f = " << f << ", t = " << t - << ")" << std::endl - << " t.lowlink = " << stack[t].lowlink << std::endl - << " f.lowlink = " << stack[f].lowlink << std::endl - << " f.acc = " << stack[f].acc << std::endl; + << ")\n t.lowlink = " << stack[t].lowlink + << "\n f.lowlink = " << stack[f].lowlink + << "\n f.acc = " << stack[f].acc << '\n'; int stack_t_lowlink = stack[t].lowlink; if (stack_t_lowlink <= stack[f].lowlink) { @@ -228,16 +227,16 @@ namespace spot violation = true; stack[f].lowlink = stack_t_lowlink; trace << " f.lowlink updated to " - << stack[f].lowlink << std::endl; + << stack[f].lowlink << '\n'; } } virtual std::ostream& print_stats(std::ostream& os) const { - os << h.size() << " unique states visited" << std::endl; - os << transitions() << " transitions explored" << std::endl; - os << max_depth() << " items max on stack" << std::endl; + os << h.size() << " unique states visited\n"; + os << transitions() << " transitions explored\n"; + os << max_depth() << " items max on stack\n"; return os; } diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 44dd11d64..2b5f64e49 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -60,7 +60,7 @@ namespace spot { bdd acc = bdd_satone(b); b -= acc; - os << sm[acc] << " "; + os << sm[acc] << ' '; } return os; } @@ -126,14 +126,14 @@ namespace spot else body_ << " -1"; } - body_ << "\n"; + body_ << '\n'; } void process_link(const state*, int, const state*, int out, const tgba_succ_iterator* si) { - body_ << out - 1 << " "; + body_ << out - 1 << ' '; if (!sba_format_) { acs_.split(body_, si->current_acceptance_conditions()); @@ -143,18 +143,18 @@ namespace spot aut_->get_dict()); to_lbt_string(f, body_); f->destroy(); - body_ << "\n"; + body_ << '\n'; } void end() { - os_ << seen.size() << " "; + os_ << seen.size() << ' '; if (sba_format_) - os_ << "1"; + os_ << '1'; else - os_ << aut_->number_of_acceptance_conditions() << "t"; - os_ << "\n" << body_.str() << "-1" << std::endl; + os_ << aut_->number_of_acceptance_conditions() << 't'; + os_ << '\n' << body_.str() << "-1" << std::endl; } private: diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 167495ba7..173436a6e 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -309,7 +309,7 @@ namespace spot for (auto& fi: next_map) { os << " " << fi.second << ": Next["; - to_string(fi.first, os) << "]" << std::endl; + to_string(fi.first, os) << ']' << std::endl; } os << "Shared Dict:" << std::endl; dict->dump(os); @@ -447,7 +447,7 @@ namespace spot trace_ltl_bdd(const translate_dict& d, bdd f) { std::cerr << "Displaying BDD "; - bdd_print_set(std::cerr, d.dict, f) << ":" << std::endl; + bdd_print_set(std::cerr, d.dict, f) << ":\n"; minato_isop isop(f); bdd cube; @@ -459,7 +459,7 @@ namespace spot bdd_print_set(std::cerr, d.dict, label) << " => "; bdd_print_set(std::cerr, d.dict, dest_bdd) << " = " << to_string(dest) - << std::endl; + << '\n'; dest->destroy(); } return std::cerr; @@ -970,7 +970,7 @@ namespace spot // std::cerr << "translate_ratexp[" << to_string(f); // if (to_concat) // std::cerr << ", " << to_string(to_concat); - // std::cerr << "]" << std::endl; + // std::cerr << ']' << std::endl; // ++indent; bdd res; if (!f->is_boolean()) @@ -1690,7 +1690,7 @@ namespace spot // the case handling G. bdd res = recurse(sub, recurring_); //std::cerr << "== in And (" << to_string(sub) - // << ")" << std::endl; + // << ')' << std::endl; // trace_ltl_bdd(dict_, res); res_ &= res; } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index fefffdbb9..69b1115a5 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -64,14 +64,14 @@ namespace spot static std::ostream& dump_hash_set(const hash_set* hs, const tgba* aut, std::ostream& out) { - out << "{"; + out << '{'; const char* sep = ""; for (hash_set::const_iterator i = hs->begin(); i != hs->end(); ++i) { out << sep << aut->format_state(*i); sep = ", "; } - out << "}"; + out << '}'; return out; } @@ -453,7 +453,7 @@ namespace spot #ifdef TRACE trace << "Final partition: "; for (partition_t::const_iterator i = done.begin(); i != done.end(); ++i) - trace << format_hash_set(*i, det_a) << " "; + trace << format_hash_set(*i, det_a) << ' '; trace << std::endl; #endif diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 9db285494..ecc6dfce2 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -67,7 +67,7 @@ namespace spot os_ << " fi;\n"; if (accept_all_ != -1) os_ << "accept_all:\n skip\n"; - os_ << "}" << std::endl; + os_ << '}' << std::endl; init_->destroy(); } @@ -138,7 +138,7 @@ namespace spot { if (fi_needed_ != 0) os_ << " fi;\n"; - os_ << get_state_label(s, n) << ":"; + os_ << get_state_label(s, n) << ':'; if (comments_) os_ << " /* " << aut_->format_state(s) << " */"; os_ << "\n if\n :: (0) -> goto " @@ -157,7 +157,7 @@ namespace spot { if (fi_needed_) os_ << " fi;\n"; - os_ << get_state_label(s, n) << ":"; + os_ << get_state_label(s, n) << ':'; if (comments_) os_ << " /* " << aut_->format_state(s) << " */"; os_ << "\n if\n"; diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc index 1dd2c5e0d..214d3db90 100644 --- a/src/tgbaalgos/powerset.cc +++ b/src/tgbaalgos/powerset.cc @@ -157,16 +157,16 @@ namespace spot cycles_left_ = threshold_; run(m); -// std::cerr << "SCC #" << m << "\n"; +// std::cerr << "SCC #" << m << '\n'; // std::cerr << "REJECT: "; -// print_set(std::cerr, reject_) << "\n"; +// print_set(std::cerr, reject_) << '\n'; // std::cerr << "ALL: "; -// print_set(std::cerr, all_) << "\n"; +// print_set(std::cerr, all_) << '\n'; // for (set_set::const_iterator j = accept_.begin(); // j != accept_.end(); ++j) // { // std::cerr << "ACCEPT: "; -// print_set(std::cerr, *j) << "\n"; +// print_set(std::cerr, *j) << '\n'; // } bdd acc = aut_->all_acceptance_conditions(); @@ -232,8 +232,8 @@ namespace spot { o << "{ "; for (auto i: s) - o << i << " "; - o << "}"; + o << i << ' '; + o << '}'; return o; } @@ -247,13 +247,13 @@ namespace spot bool is_acc = is_cycle_accepting(i, ts); do { - // std::cerr << aut_->format_state(i->ts->first) << " "; + // std::cerr << aut_->format_state(i->ts->first) << ' '; ++i; } while (i != dfs_.end()); // std::cerr << " acc=" << is_acc << " ("; // bdd_print_accset(std::cerr, aut_->get_dict(), s) << ") "; - // print_set(std::cerr, ts) << "\n"; + // print_set(std::cerr, ts) << '\n'; if (is_acc) { accept_.push_back(ts); diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc index 15bbae629..64f4308e6 100644 --- a/src/tgbaalgos/replayrun.cc +++ b/src/tgbaalgos/replayrun.cc @@ -38,7 +38,7 @@ namespace spot std::string s = a->transition_annotation(i); if (s == "") return; - os << " " << s; + os << ' ' << s; } } @@ -210,7 +210,7 @@ namespace spot os << " | "; print_annotation(os, a, j); bdd_print_formula(os, a->get_dict(), label); - os << "\t"; + os << '\t'; bdd_print_accset(os, a->get_dict(), acc); os << std::endl; } diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 327e478bc..9afd34c8c 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -56,7 +56,7 @@ namespace spot do { state* dest = si->current_state(); - os_ << "\"" << cur << "\", \""; + os_ << '"' << cur << "\", \""; escape_str(os_, aut_->format_state(dest)); os_ << "\", \""; escape_str(os_, bdd_format_formula(d, si->current_condition())); @@ -87,7 +87,7 @@ namespace spot s.resize(s.size() - 1); } os_ << " \""; - escape_str(os_, s) << "\""; + escape_str(os_, s) << '"'; } return os_; } diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 786dbc77d..ef9f259b7 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -493,7 +493,7 @@ namespace spot size_t n = m.states_of(state).size(); ostr << " (" << n << " state"; if (n > 1) - ostr << "s"; + ostr << 's'; ostr << ")\\naccs="; escape_str(ostr, bdd_format_accset(m.get_aut()->get_dict(), m.acc_set_of(state))); @@ -515,7 +515,7 @@ namespace spot m.aprec_set_of(state))); ostr << "]\\n useful=["; escape_str(ostr, bdd_format_accset(m.get_aut()->get_dict(), - m.useful_acc_of(state))) << "]"; + m.useful_acc_of(state))) << ']'; } out << " " << state << " [shape=box," @@ -543,7 +543,7 @@ namespace spot } } - out << "}" << std::endl; + out << '}' << std::endl; return out; } diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index 7188e7ac2..0be2216f8 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -166,7 +166,7 @@ namespace spot for (unsigned n = 0; n < c; ++n) { - //std::cerr << "SCC #" << n << "\n"; + //std::cerr << "SCC #" << n << '\n'; if (!sm.accepting(n)) continue; @@ -191,7 +191,7 @@ namespace spot one = bdd_high(one); } int id = resacc.id(); - //std::cerr << resacc << " -> " << res << "\n"; + //std::cerr << resacc << " -> " << res << '\n'; remap_[n][id] = res; } } @@ -447,7 +447,7 @@ namespace spot { if (!sm->accepting(n)) continue; - //std::cerr << "SCC " << n << "\n"; + //std::cerr << "SCC " << n << '\n'; bdd useful = useful_table[n]; int missing = max_num - max_table[n]; diff --git a/src/tgbaalgos/weight.cc b/src/tgbaalgos/weight.cc index 285713feb..87fd3ced1 100644 --- a/src/tgbaalgos/weight.cc +++ b/src/tgbaalgos/weight.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita. +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement +// de l'Epita. // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -114,7 +115,7 @@ namespace spot { weight::weight_vector::const_iterator it; for (it = w.m.begin(); it != w.m.end(); ++it) - os << "(" << it->first << "," << it->second << ")"; + os << '(' << it->first << ',' << it->second << ')'; return os; } diff --git a/src/tgbaalgos/word.cc b/src/tgbaalgos/word.cc index 1b8d9e3b4..ad5d6e614 100644 --- a/src/tgbaalgos/word.cc +++ b/src/tgbaalgos/word.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -102,7 +102,7 @@ namespace spot notfirst = true; bdd_print_formula(os, d, *i); } - os << "}"; + os << '}'; return os; } diff --git a/src/tgbaparse/fmterror.cc b/src/tgbaparse/fmterror.cc index 5a8a19f39..a9493053d 100644 --- a/src/tgbaparse/fmterror.cc +++ b/src/tgbaparse/fmterror.cc @@ -1,5 +1,8 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -32,7 +35,7 @@ namespace spot for (it = error_list.begin(); it != error_list.end(); ++it) { if (filename != "-") - os << filename << ":"; + os << filename << ':'; os << it->first << ": "; os << it->second << std::endl; printed = true; diff --git a/src/tgbatest/bitvect.cc b/src/tgbatest/bitvect.cc index 09b6ae608..3e88efabd 100644 --- a/src/tgbatest/bitvect.cc +++ b/src/tgbatest/bitvect.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -27,14 +27,14 @@ void ruler() if (x % 10 == 0) std::cout << x / 10; else - std::cout << "_"; + std::cout << '_'; std::cout << "\n "; for (size_t x = 0; x < 76; ++x) std::cout << x % 10; std::cout << "\n\n"; } -#define ECHO(name) std::cout << #name": " << *name << "\n" +#define ECHO(name) std::cout << #name": " << *name << '\n' int main() { diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc index 6a4c4af40..d82bd8695 100644 --- a/src/tgbatest/complementation.cc +++ b/src/tgbatest/complementation.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -110,7 +111,7 @@ int main(int argc, char* argv[]) print_formula = true; break; default: std::cerr << "unrecognized option `-" << argv[i][1] - << "'" << std::endl; + << '\'' << std::endl; return 2; } } diff --git a/src/tgbatest/intvcmp2.cc b/src/tgbatest/intvcmp2.cc index 39a5ace20..6e6e821b5 100644 --- a/src/tgbatest/intvcmp2.cc +++ b/src/tgbatest/intvcmp2.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -29,7 +30,7 @@ int check_aa(int* data, int size, unsigned expected = 0) std::cout << "AC[" << csize << "] "; for (size_t i = 0; i < csize; ++i) - std::cout << comp[i] << " "; + std::cout << comp[i] << ' '; std::cout << std::endl; int* decomp = new int[size + 30]; @@ -37,7 +38,7 @@ int check_aa(int* data, int size, unsigned expected = 0) std::cout << "AD[" << size << "] "; for (int i = 0; i < size; ++i) - std::cout << decomp[i] << " "; + std::cout << decomp[i] << ' '; std::cout << std::endl; int res = memcmp(data, decomp, size * sizeof(int)); @@ -47,7 +48,7 @@ int check_aa(int* data, int size, unsigned expected = 0) std::cout << "*** cmp error *** " << res << std::endl; std::cout << "AE[" << size << "] "; for (int i = 0; i < size; ++i) - std::cout << data[i] << " "; + std::cout << data[i] << ' '; std::cout << std::endl; } diff --git a/src/tgbatest/intvcomp.cc b/src/tgbatest/intvcomp.cc index 09b37ec3e..7c66efb9a 100644 --- a/src/tgbatest/intvcomp.cc +++ b/src/tgbatest/intvcomp.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -33,16 +34,16 @@ int check_vv(int* data, int size, unsigned expected = 0) std::cout << "WC[" << output.size() << "] "; for (size_t i = 0; i < output.size(); ++i) - std::cout << output[i] << " "; - std::cout << std::endl; + std::cout << output[i] << ' '; + std::cout << '\n'; std::vector decomp; spot::int_vector_vector_decompress(output, decomp, size); std::cout << "WD[" << decomp.size() << "] "; for (size_t i = 0; i < decomp.size(); ++i) - std::cout << decomp[i] << " "; - std::cout << std::endl; + std::cout << decomp[i] << ' '; + std::cout << '\n'; int res = (decomp != input); @@ -51,8 +52,8 @@ int check_vv(int* data, int size, unsigned expected = 0) std::cout << "*** cmp error *** " << std::endl; std::cout << "WE[" << size << "] "; for (int i = 0; i < size; ++i) - std::cout << data[i] << " "; - std::cout << std::endl; + std::cout << data[i] << ' '; + std::cout << '\n'; } if (expected && (output.size() * sizeof(int) != expected)) @@ -63,7 +64,7 @@ int check_vv(int* data, int size, unsigned expected = 0) res = 1; } - std::cout << std::endl; + std::cout << '\n'; return !!res; } @@ -75,16 +76,16 @@ int check_av(int* data, int size, unsigned expected = 0) std::cout << "VC[" << v->size() << "] "; for (size_t i = 0; i < v->size(); ++i) - std::cout << (*v)[i] << " "; - std::cout << std::endl; + std::cout << (*v)[i] << ' '; + std::cout << '\n'; int* decomp = new int[size]; spot::int_vector_array_decompress(v, decomp, size); std::cout << "VD[" << size << "] "; for (int i = 0; i < size; ++i) - std::cout << decomp[i] << " "; - std::cout << std::endl; + std::cout << decomp[i] << ' '; + std::cout << '\n'; int res = memcmp(data, decomp, size * sizeof(int)); @@ -93,8 +94,8 @@ int check_av(int* data, int size, unsigned expected = 0) std::cout << "*** cmp error *** " << res << std::endl; std::cout << "VE[" << size << "] "; for (int i = 0; i < size; ++i) - std::cout << data[i] << " "; - std::cout << std::endl; + std::cout << data[i] << ' '; + std::cout << '\n'; } if (expected && (v->size() * sizeof(int) != expected)) @@ -105,7 +106,7 @@ int check_av(int* data, int size, unsigned expected = 0) res = 1; } - std::cout << std::endl; + std::cout << '\n'; delete v; delete[] decomp; @@ -120,16 +121,16 @@ int check_aa(int* data, int size, unsigned expected = 0) std::cout << "AC[" << csize << "] "; for (size_t i = 0; i < csize; ++i) - std::cout << comp[i] << " "; - std::cout << std::endl; + std::cout << comp[i] << ' '; + std::cout << '\n'; int* decomp = new int[size]; spot::int_array_array_decompress(comp, csize, decomp, size); std::cout << "AD[" << size << "] "; for (int i = 0; i < size; ++i) - std::cout << decomp[i] << " "; - std::cout << std::endl; + std::cout << decomp[i] << ' '; + std::cout << '\n'; int res = memcmp(data, decomp, size * sizeof(int)); @@ -138,8 +139,8 @@ int check_aa(int* data, int size, unsigned expected = 0) std::cout << "*** cmp error *** " << res << std::endl; std::cout << "AE[" << size << "] "; for (int i = 0; i < size; ++i) - std::cout << data[i] << " "; - std::cout << std::endl; + std::cout << data[i] << ' '; + std::cout << '\n'; } if (expected && (csize * sizeof(int) != expected)) @@ -150,7 +151,7 @@ int check_aa(int* data, int size, unsigned expected = 0) res = 1; } - std::cout << std::endl; + std::cout << '\n'; delete[] comp; delete[] decomp; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 6c52e4f2b..2ed34f5f9 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1,8 +1,8 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire -// de Recherche et Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de -// Paris 6 (LIP6), département Systèmes Répartis +// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 +// Laboratoire de Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire +// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // Coopératifs (SRC), Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. @@ -529,7 +529,7 @@ main(int argc, char** argv) if (!echeck_inst) { std::cerr << "Failed to parse argument of -e near `" - << err << "'" << std::endl; + << err << '\'' << std::endl; exit(2); } expect_counter_example = true; @@ -547,7 +547,7 @@ main(int argc, char** argv) if (!echeck_inst) { std::cerr << "Failed to parse argument of -e near `" - << err << "'" << std::endl; + << err << '\'' << std::endl; exit(2); } expect_counter_example = false; diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 2520f47a6..79909e100 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -316,7 +317,7 @@ struct stat_collector { std::ios::fmtflags old = os.flags(); os << std::setw(25) << "" << " | " - << std::setw(30) << std::left << title << std::right << "|" << std::endl + << std::setw(30) << std::left << title << std::right << '|' << std::endl << std::setw(25) << "algorithm" << " | min < mean < max | total | n" << std::endl @@ -328,10 +329,10 @@ struct stat_collector { os << std::setw(25) << i->first << " |" << std::setw(6) << i->second.min - << " " + << ' ' << std::setw(8) << static_cast(i->second.tot) / i->second.n - << " " + << ' ' << std::setw(6) << i->second.max << " |"; if (total) @@ -436,17 +437,17 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string& s) i != ar_stats.end(); ++i) std::cout << std::setw(25) << i->first << " |" << std::setw(6) << i->second.min_prefix - << " " + << ' ' << std::setw(8) << static_cast(i->second.tot_prefix) / i->second.n - << " " + << ' ' << std::setw(6) << i->second.max_prefix << " |" << std::setw(6) << i->second.min_cycle - << " " + << ' ' << std::setw(8) << static_cast(i->second.tot_cycle) / i->second.n - << " " + << ' ' << std::setw(6) << i->second.max_cycle << " |" << std::setw(4) << i->second.n @@ -466,18 +467,18 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string& s) std::cout << std::setw(25) << i->first << " |" << std::setw(6) << i->second.min_run - << " " + << ' ' << std::setw(8) << static_cast(i->second.tot_prefix + i->second.tot_cycle) / i->second.n - << " " + << ' ' << std::setw(6) << i->second.max_run << " |" << std::setw(6) << i->second.tot_prefix - << " " + << ' ' << std::setw(6) << i->second.tot_cycle - << " " + << ' ' << std::setw(8) << i->second.tot_prefix + i->second.tot_cycle << " |" << std::setw(4) << i->second.n @@ -796,14 +797,14 @@ main(int argc, char** argv) if (tok) { std::cerr << "failed to parse probabilities near `" - << tok << "'" << std::endl; + << tok << '\'' << std::endl; exit(2); } if (opt_l > opt_f) { std::cerr << "-l's argument (" << opt_l << ") should not be larger than " - << "-f's (" << opt_f << ")" << std::endl; + << "-f's (" << opt_f << ')' << std::endl; exit(2); } @@ -840,7 +841,7 @@ main(int argc, char** argv) &err); if (ec_algos[i].inst == 0) { - std::cerr << "Parse error after `" << err << "'" << std::endl; + std::cerr << "Parse error after `" << err << '\'' << std::endl; exit(1); } ec_algos[i].inst->options().set(options); @@ -1059,8 +1060,8 @@ main(int argc, char** argv) } if (opt_z && !opt_paper) std::cout << " [" << run->prefix.size() - << "+" << run->cycle.size() - << "]"; + << '+' << run->cycle.size() + << ']'; if (opt_reduce) { @@ -1088,9 +1089,9 @@ main(int argc, char** argv) { std::cout << " [" << redrun->prefix.size() - << "+" + << '+' << redrun->cycle.size() - << "]"; + << ']'; } delete redrun; } @@ -1234,7 +1235,7 @@ main(int argc, char** argv) int n = -1; - std::cout << std::setw(25) << algo << " " << std::setw(8); + std::cout << std::setw(25) << algo << ' ' << std::setw(8); ec_iter i = stats["states"].find(algo); if (i != stats["states"].end()) @@ -1244,7 +1245,7 @@ main(int argc, char** argv) } else std::cout << ""; - std::cout << " " << std::setw(8); + std::cout << ' ' << std::setw(8); i = stats["transitions"].find(algo); if (i != stats["transitions"].end()) @@ -1254,7 +1255,7 @@ main(int argc, char** argv) } else std::cout << ""; - std::cout << " " << std::setw(8); + std::cout << ' ' << std::setw(8); i = stats["max. depth"].find(algo); if (i != stats["max. depth"].end()) @@ -1265,7 +1266,7 @@ main(int argc, char** argv) else std::cout << ""; if (n >= 0) - std::cout << " " << std::setw(8) << n; + std::cout << ' ' << std::setw(8) << n; std::cout << std::endl; } @@ -1277,14 +1278,14 @@ main(int argc, char** argv) { const std::string algo = ec_algos[ai].name; - std::cout << std::setw(25) << algo << " " << std::setw(8); + std::cout << std::setw(25) << algo << ' ' << std::setw(8); ec_iter i = stats2["search space states"].find(algo); if (i != stats2["search space states"].end()) std::cout << i->second.tot / i->second.n; else std::cout << ""; - std::cout << " " << std::setw(8); + std::cout << ' ' << std::setw(8); i = stats2["(non unique) states for cycle"].find(algo); if (i != stats2["(non unique) states for cycle"].end()) @@ -1301,7 +1302,7 @@ main(int argc, char** argv) std::cout << "The check failed for the following seeds:"; for (std::set::const_iterator i = failed_seeds.begin(); i != failed_seeds.end(); ++i) - std::cout << " " << *i; + std::cout << ' ' << *i; std::cout << std::endl; }