diff --git a/ChangeLog b/ChangeLog index bba8d2eb3..78e087a9f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2011-11-27 Alexandre Duret-Lutz + + Don't flush the stream on each new line, when writing automata. + + * src/tgbaalgos/neverclaim.cc, src/tgbaalgos/dotty.cc, + src/tgbaalgos/save.cc: Prefer '\n' over std::endl to speedup I/O. + * src/ltltest/genltl.cc (syntax): Use '\n' too, although it won't + make a big difference. + 2011-11-27 Alexandre Duret-Lutz Add an ltl2tgba option to read Kripke structure. diff --git a/src/ltltest/genltl.cc b/src/ltltest/genltl.cc index 2bc8f7290..1e2240e3f 100644 --- a/src/ltltest/genltl.cc +++ b/src/ltltest/genltl.cc @@ -108,37 +108,35 @@ environment& env(default_environment::instance()); void syntax(char* prog) { - std::cerr - << "Usage: "<< prog << " [-s] F N" << std::endl - << std::endl - << "-s output using Spin's syntax" << std::endl - << "F specifies the familly of LTL formula to build" << std::endl - << "N is the size parameter of the familly" << std::endl - << std::endl - << "Available families (F):" << std::endl - << " 1: F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))" - << std::endl - << " 2: F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))" << std::endl - << " 3: F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q)))" - << std::endl - << " 4: GF(p1)&GF(p2)&...&GF(pn)" << std::endl - << " 5: FG(p1)|FG(p2)|...|FG(pn)" << std::endl - << " 6: GF(p1)|GF(p2)|...|GF(pn)" << std::endl - << " 7: FG(p1)&FG(p2)&...&FG(pn)" << std::endl - << " 8: (((p1 U p2) U p3) ... U pn)" << std::endl - << " 9: (p1 U (p2 U (... U pn)))" << std::endl - << " 10: (((p1 R p2) R p3) ... R pn)" << std::endl - << " 11: (p1 R (p2 R (... R pn)))" << std::endl - << " 12: (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))" - << std::endl - << " 13: (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))" << std::endl - << " 14: G(p1)|G(p2)|...|G(pn)" << std::endl - << " 15: F(p1)&F(p2)&...&F(pn)" << std::endl - << " 16: !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))" << std::endl - << " 17: LTLcounter(n)" << std::endl - << " 18: LTLcounterLinear(n)" << std::endl - << " 19: LTLcounterCarry(n)" << std::endl - << " 20: LTLcounterCarryLinear(n)" << std::endl; + std::cerr << + "Usage: " << prog << " [-s] F N\n" + "\n" + "-s output using Spin's syntax\n" + "F specifies the familly of LTL formula to build\n" + "N is the size parameter of the familly\n" + "\n" + "Available families (F):\n" + " 1: F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))" + "\n" + " 2: F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))\n" + " 3: F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q)))\n" + " 4: GF(p1)&GF(p2)&...&GF(pn)\n" + " 5: FG(p1)|FG(p2)|...|FG(pn)\n" + " 6: GF(p1)|GF(p2)|...|GF(pn)\n" + " 7: FG(p1)&FG(p2)&...&FG(pn)\n" + " 8: (((p1 U p2) U p3) ... U pn)\n" + " 9: (p1 U (p2 U (... U pn)))\n" + " 10: (((p1 R p2) R p3) ... R pn)\n" + " 11: (p1 R (p2 R (... R pn)))\n" + " 12: (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))\n" + " 13: (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))\n" + " 14: G(p1)|G(p2)|...|G(pn)\n" + " 15: F(p1)&F(p2)&...&F(pn)\n" + " 16: !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))\n" + " 17: LTLcounter(n)\n" + " 18: LTLcounterLinear(n)\n" + " 19: LTLcounterCarry(n)\n" + " 20: LTLcounterCarryLinear(n)" << std::endl; exit(2); } diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 919665a0a..970d4ac91 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -47,9 +47,9 @@ namespace spot void start() { - os_ << "digraph G {" << std::endl; - os_ << " 0 [label=\"\", style=invis, height=0]" << std::endl; - os_ << " 0 -> 1" << std::endl; + os_ << ("digraph G {\n" + " 0 [label=\"\", style=invis, height=0]\n" + " 0 -> 1\n"); } void @@ -86,7 +86,7 @@ namespace spot << dd_->state_decl(automata_, s, n, si, escape_str(automata_->format_state(s)), accepting) - << std::endl; + << '\n'; } void @@ -111,7 +111,7 @@ namespace spot os_ << " " << in << " -> " << out << " " << dd_->link_decl(automata_, in_s, in, out_s, out, si, escape_str(label)) - << std::endl; + << '\n'; } private: diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 4ff700bd7..9bbb1d949 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -57,7 +57,7 @@ namespace spot to_string(f_, os_); os_ << " */"; } - os_ << std::endl; + os_ << '\n'; init_ = automata_->get_init_state(); } @@ -65,12 +65,9 @@ namespace spot end() { if (fi_needed_) - os_ << " fi;" << std::endl; + os_ << " fi;\n"; if (accept_all_ != -1) - { - os_ << "accept_all:" << std::endl; - os_ << " skip" << std::endl; - } + os_ << "accept_all:\n skip\n"; os_ << "}" << std::endl; init_->destroy(); } @@ -144,13 +141,12 @@ namespace spot if (it->done()) { if (fi_needed_ != 0) - os_ << " fi;" << std::endl; + os_ << " fi;\n"; os_ << get_state_label(s, n) << ":"; if (comments_) os_ << " /* " << automata_->format_state(s) << " */"; - os_ << std::endl; - os_ << " if" << std::endl; - os_ << " :: (0) -> goto " << get_state_label(s, n) << std::endl; + os_ << "\n if\n :: (0) -> goto " + << get_state_label(s, n) << '\n'; fi_needed_ = true; } else @@ -164,12 +160,11 @@ namespace spot else { if (fi_needed_) - os_ << " fi;" << std::endl; + os_ << " fi;\n"; os_ << get_state_label(s, n) << ":"; if (comments_) os_ << " /* " << automata_->format_state(s) << " */"; - os_ << std::endl; - os_ << " if" << std::endl; + os_ << "\n if\n"; fi_needed_ = true; } current->destroy(); @@ -189,7 +184,7 @@ namespace spot to_spin_string(f, os_, true); f->destroy(); state* current = si->current_state(); - os_ << ") -> goto " << get_state_label(current, out) << std::endl; + os_ << ") -> goto " << get_state_label(current, out) << '\n'; current->destroy(); } } diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index a17cc232f..c30ed95b9 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -45,7 +45,7 @@ namespace spot start() { os_ << "acc ="; - print_acc(automata_->all_acceptance_conditions()) << ";" << std::endl; + print_acc(automata_->all_acceptance_conditions()) << ";\n"; } void @@ -61,7 +61,7 @@ namespace spot os_ << "\", \""; escape_str(os_, bdd_format_formula(d, si->current_condition())); os_ << "\","; - print_acc(si->current_acceptance_conditions()) << ";" << std::endl; + print_acc(si->current_acceptance_conditions()) << ";\n"; dest->destroy(); } }