From 43aebc463c4d0fb048beddd0e133286c299b1de0 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Fri, 19 Jan 2024 10:47:18 +0100
Subject: [PATCH] add nonmovement action to modules

This is needed to correctly shield when staying at a certain place
should not be allowed
---
 util/PrismModulesPrinter.cpp | 16 ++++++++++++++--
 util/PrismModulesPrinter.h   |  1 +
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index 7fcdd4a..5b6ddd1 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -203,6 +203,8 @@ namespace prism {
       printPortableObjectActionsForRobot(agentName, identifier);
     }
 
+    printNonMovementActionsForRobot(agentName);
+
 
     os << "\n" << actionStream.str();
     actionStream.str(std::string());
@@ -285,6 +287,14 @@ namespace prism {
     return updateToString(u) + ";\n";
   }
 
+  void PrismModulesPrinter::printNonMovementActionsForRobot(const AgentName &agentName) {
+    for(auto const [actionId, action] : nonMovementActions) {
+      std::string actionName = "[" + agentName + "_" + action + "]";
+      agentNameActionMap.at(agentName).insert({actionId, actionName});
+      actionStream << "  " << actionName << " true -> true;\n";
+    }
+  }
+
   void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) {
     if(!slipperyTiles.at("North").empty()) {
       printSlipperyMovementActionsForNorth(a);
@@ -464,7 +474,9 @@ namespace prism {
     os << "\nmodule " << a << "FaultyBehaviour" << std::endl;
     os << "  previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "];\n";
 
+    std::set<size_t> exclude = {PICKUP, DROP, TOGGLE, DONE};
     for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
+      if(exclude.count(actionId) > 0) continue;
       os << "  " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
     }
     os << "endmodule\n\n";
@@ -493,7 +505,7 @@ namespace prism {
   }
 
   void PrismModulesPrinter::printDoneActions(const AgentName &agentName) {
-    os << "  [" << agentName << "_done]" << agentName << "IsOnGoal & clock=0 -> true;\n";
+    os << "  [" << agentName << "_on_goal]" << agentName << "IsOnGoal & clock=0 -> true;\n";
   }
 
   void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) {
@@ -504,7 +516,7 @@ namespace prism {
       else os << ", ";
       os << actionName;
     }
-    if(agentName == "Agent") os << ", [Agent_done]";
+    if(agentName == "Agent") os << ", [Agent_on_goal]";
     os << "\nendplayer\n";
   }
 
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index bfdd58f..16d562b 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -38,6 +38,7 @@ namespace prism {
       void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key);
       void printMovementActionsForRobot(const std::string &a);
       void printTurnActionsForRobot(const std::string &a);
+      void printNonMovementActionsForRobot(const AgentName &agentName);
       void printSlipperyMovementActionsForRobot(const AgentName &a);
       void printSlipperyMovementActionsForNorth(const AgentName &a);
       void printSlipperyMovementActionsForEast(const AgentName &a);