alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Don't flush the stream on each new line, when writing automata.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2011-11-27 23:35:31 +01:00
parent ba3108f98d
commit 9c4adf1eb4
5 changed files with 54 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2011-11-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2011-11-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Add an ltl2tgba option to read Kripke structure. Add an ltl2tgba option to read Kripke structure.

60
src/ltltest/genltl.cc
View file

@ -108,37 +108,35 @@ environment& env(default_environment::instance());
void void
syntax(char* prog) syntax(char* prog)
{ {
std::cerr std::cerr <<
<< "Usage: "<< prog << " [-s] F N" << std::endl "Usage: " << prog << " [-s] F N\n"
<< std::endl "\n"
<< "-s output using Spin's syntax" << std::endl "-s output using Spin's syntax\n"
<< "F specifies the familly of LTL formula to build" << std::endl "F specifies the familly of LTL formula to build\n"
<< "N is the size parameter of the familly" << std::endl "N is the size parameter of the familly\n"
<< std::endl "\n"
<< "Available families (F):" << std::endl "Available families (F):\n"
<< " 1: F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))" " 1: F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))"
<< std::endl "\n"
<< " 2: F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))" << std::endl " 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)))" " 3: F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q)))\n"
<< std::endl " 4: GF(p1)&GF(p2)&...&GF(pn)\n"
<< " 4: GF(p1)&GF(p2)&...&GF(pn)" << std::endl " 5: FG(p1)|FG(p2)|...|FG(pn)\n"
<< " 5: FG(p1)|FG(p2)|...|FG(pn)" << std::endl " 6: GF(p1)|GF(p2)|...|GF(pn)\n"
<< " 6: GF(p1)|GF(p2)|...|GF(pn)" << std::endl " 7: FG(p1)&FG(p2)&...&FG(pn)\n"
<< " 7: FG(p1)&FG(p2)&...&FG(pn)" << std::endl " 8: (((p1 U p2) U p3) ... U pn)\n"
<< " 8: (((p1 U p2) U p3) ... U pn)" << std::endl " 9: (p1 U (p2 U (... U pn)))\n"
<< " 9: (p1 U (p2 U (... U pn)))" << std::endl " 10: (((p1 R p2) R p3) ... R pn)\n"
<< " 10: (((p1 R p2) R p3) ... R pn)" << std::endl " 11: (p1 R (p2 R (... R pn)))\n"
<< " 11: (p1 R (p2 R (... R pn)))" << std::endl " 12: (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))\n"
<< " 12: (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))" " 13: (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))\n"
<< std::endl " 14: G(p1)|G(p2)|...|G(pn)\n"
<< " 13: (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))" << std::endl " 15: F(p1)&F(p2)&...&F(pn)\n"
<< " 14: G(p1)|G(p2)|...|G(pn)" << std::endl " 16: !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))\n"
<< " 15: F(p1)&F(p2)&...&F(pn)" << std::endl " 17: LTLcounter(n)\n"
<< " 16: !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))" << std::endl " 18: LTLcounterLinear(n)\n"
<< " 17: LTLcounter(n)" << std::endl " 19: LTLcounterCarry(n)\n"
<< " 18: LTLcounterLinear(n)" << std::endl " 20: LTLcounterCarryLinear(n)" << std::endl;
<< " 19: LTLcounterCarry(n)" << std::endl
<< " 20: LTLcounterCarryLinear(n)" << std::endl;
exit(2); exit(2);
} }

10
src/tgbaalgos/dotty.cc
View file

@ -47,9 +47,9 @@ namespace spot
void void
start() start()
{ {
os_ << "digraph G {" << std::endl; os_ << ("digraph G {\n"
os_ << " 0 [label=\"\", style=invis, height=0]" << std::endl; " 0 [label=\"\", style=invis, height=0]\n"
os_ << " 0 -> 1" << std::endl; " 0 -> 1\n");
} }
void void
@ -86,7 +86,7 @@ namespace spot
<< dd_->state_decl(automata_, s, n, si, << dd_->state_decl(automata_, s, n, si,
escape_str(automata_->format_state(s)), escape_str(automata_->format_state(s)),
accepting) accepting)
<< std::endl; << '\n';
} }
void void
@ -111,7 +111,7 @@ namespace spot
os_ << " " << in << " -> " << out << " " os_ << " " << in << " -> " << out << " "
<< dd_->link_decl(automata_, in_s, in, out_s, out, si, << dd_->link_decl(automata_, in_s, in, out_s, out, si,
escape_str(label)) escape_str(label))
<< std::endl; << '\n';
} }
private: private:

23
src/tgbaalgos/neverclaim.cc
View file

@ -57,7 +57,7 @@ namespace spot
to_string(f_, os_); to_string(f_, os_);
os_ << " */"; os_ << " */";
} }
os_ << std::endl; os_ << '\n';
init_ = automata_->get_init_state(); init_ = automata_->get_init_state();
} }
@ -65,12 +65,9 @@ namespace spot
end() end()
{ {
if (fi_needed_) if (fi_needed_)
os_ << " fi;" << std::endl; os_ << " fi;\n";
if (accept_all_ != -1) if (accept_all_ != -1)
{ os_ << "accept_all:\n skip\n";
os_ << "accept_all:" << std::endl;
os_ << " skip" << std::endl;
}
os_ << "}" << std::endl; os_ << "}" << std::endl;
init_->destroy(); init_->destroy();
} }
@ -144,13 +141,12 @@ namespace spot
if (it->done()) if (it->done())
{ {
if (fi_needed_ != 0) if (fi_needed_ != 0)
os_ << " fi;" << std::endl; os_ << " fi;\n";
os_ << get_state_label(s, n) << ":"; os_ << get_state_label(s, n) << ":";
if (comments_) if (comments_)
os_ << " /* " << automata_->format_state(s) << " */"; os_ << " /* " << automata_->format_state(s) << " */";
os_ << std::endl; os_ << "\n if\n :: (0) -> goto "
os_ << " if" << std::endl; << get_state_label(s, n) << '\n';
os_ << " :: (0) -> goto " << get_state_label(s, n) << std::endl;
fi_needed_ = true; fi_needed_ = true;
} }
else else
@ -164,12 +160,11 @@ namespace spot
else else
{ {
if (fi_needed_) if (fi_needed_)
os_ << " fi;" << std::endl; os_ << " fi;\n";
os_ << get_state_label(s, n) << ":"; os_ << get_state_label(s, n) << ":";
if (comments_) if (comments_)
os_ << " /* " << automata_->format_state(s) << " */"; os_ << " /* " << automata_->format_state(s) << " */";
os_ << std::endl; os_ << "\n if\n";
os_ << " if" << std::endl;
fi_needed_ = true; fi_needed_ = true;
} }
current->destroy(); current->destroy();
@ -189,7 +184,7 @@ namespace spot
to_spin_string(f, os_, true); to_spin_string(f, os_, true);
f->destroy(); f->destroy();
state* current = si->current_state(); state* current = si->current_state();
os_ << ") -> goto " << get_state_label(current, out) << std::endl; os_ << ") -> goto " << get_state_label(current, out) << '\n';
current->destroy(); current->destroy();
} }
} }

4
src/tgbaalgos/save.cc
View file

@ -45,7 +45,7 @@ namespace spot
start() start()
{ {
os_ << "acc ="; os_ << "acc =";
print_acc(automata_->all_acceptance_conditions()) << ";" << std::endl; print_acc(automata_->all_acceptance_conditions()) << ";\n";
} }
void void
@ -61,7 +61,7 @@ namespace spot
os_ << "\", \""; os_ << "\", \"";
escape_str(os_, bdd_format_formula(d, si->current_condition())); escape_str(os_, bdd_format_formula(d, si->current_condition()));
os_ << "\","; os_ << "\",";
print_acc(si->current_acceptance_conditions()) << ";" << std::endl; print_acc(si->current_acceptance_conditions()) << ";\n";
dest->destroy(); dest->destroy();
} }
} }