From cfb0d5da6f497cd4795cde891cd1d284ae4b7c06 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Thu, 18 Jan 2024 21:13:23 +0100
Subject: [PATCH] add done actions for smg models
---
util/PrismModulesPrinter.cpp | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
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";
}