Browse Source

fix player ostream output

main
Stefan Pranger 5 years ago
parent
commit
271ed284a6
  1. 5
      src/storm/storage/prism/Player.cpp

5
src/storm/storage/prism/Player.cpp

@ -21,7 +21,7 @@ namespace storm {
std::ostream& operator<<(std::ostream& stream, Player const& player) { std::ostream& operator<<(std::ostream& stream, Player const& player) {
stream << "player"; stream << "player";
if (player.getName() != "") { if (player.getName() != "") {
stream << " \"" << player.getName() << "\"";
stream << " " << player.getName();
} }
stream << std::endl; stream << std::endl;
for (auto const& module : player.getModules()) { for (auto const& module : player.getModules()) {
@ -33,7 +33,8 @@ namespace storm {
stream << "[" << command.getActionName() << "] "; stream << "[" << command.getActionName() << "] ";
//&command != (player.getCommands()).back ? std::cout << "," : std::cout << std::endl; //&command != (player.getCommands()).back ? std::cout << "," : std::cout << std::endl;
} }
stream << "player" << std::endl;
stream << std::endl;
stream << "endplayer" << std::endl;
return stream; return stream;
} }
} // namespace prism } // namespace prism

Loading…
Cancel
Save