From a3413fe990500a5f273fa32dc473590fbaad512f Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Tue, 29 Apr 2025 14:17:23 +0200
Subject: [PATCH] changed behaviour when moving against wall
---
util/Grid.cpp | 5 ++---
util/PrismModulesPrinter.cpp | 10 +++++-----
2 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/util/Grid.cpp b/util/Grid.cpp
index d276c7b..0c9db49 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -181,12 +181,11 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
}
if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName);
formulas.printInitStruct();
+ os << "const int WIDTH = " << maxBoundaries.first << ";\n";
+ os << "const int HEIGHT = " << maxBoundaries.second << ";\n";
modules.print();
-
-
-
//if(!stateRewards.empty()) {
// modules.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
//}
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index a2855da..ffe8a7b 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -5,10 +5,10 @@
#include <stdexcept>
-std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; }
-std::string southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; }
-std::string eastUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"+1)"; }
-std::string westUpdate(const AgentName &a) { return "(col"+a+"'=col"+a+"-1)"; }
+std::string northUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"-1))"; }
+std::string southUpdate(const AgentName &a) { return "min(WIDTH, max(1, row"+a+"'=row"+a+"+1))"; }
+std::string eastUpdate(const AgentName &a) { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"+1))"; }
+std::string westUpdate(const AgentName &a) { return "min(HEIGHT, max(1, col"+a+"'=col"+a+"-1))"; }
namespace prism {
@@ -250,7 +250,7 @@ namespace prism {
if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery";
if(anyLava) guard += " & !" + a + "IsOnLava";
if(anyGoals && a == "Agent") guard += " & !" + a + "IsOnGoal";
- guard += " & !" + a + "CannotMove" + direction + "Wall";
+ //guard += " & !" + a + "CannotMove" + direction + "Wall";
if(anyPortableObject() || !lockedDoors.empty() || !unlockedDoors.empty()) guard += " & !" + a + "CannotMoveConditionally";
guard += " -> ";
return guard;