diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index a12353b..7fcdd4a 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -203,8 +203,11 @@ namespace prism { printPortableObjectActionsForRobot(agentName, identifier); } + os << "\n" << actionStream.str(); actionStream.str(std::string()); + + if(agentNameAndPositionMap.size() > 1 && agentName == "Agent") printDoneActions(agentName); os << "endmodule\n\n"; } @@ -490,7 +493,7 @@ namespace prism { } void PrismModulesPrinter::printDoneActions(const AgentName &agentName) { - os << " [" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n"; + os << " [" << agentName << "_done]" << agentName << "IsOnGoal & clock=0 -> true;\n"; } void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) { @@ -501,6 +504,7 @@ namespace prism { else os << ", "; os << actionName; } + if(agentName == "Agent") os << ", [Agent_done]"; os << "\nendplayer\n"; }