From e65a46e99a6d6aeace830c5c8c3055d50c963048 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sat, 13 Jan 2024 18:24:04 +0100
Subject: [PATCH 01/21] fixed indentation

---
 main.cpp | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/main.cpp b/main.cpp
index 2760259..7b70a81 100644
--- a/main.cpp
+++ b/main.cpp
@@ -23,15 +23,15 @@ std::vector<std::string> parseCommaSeparatedString(std::string const& str) {
 
 
 struct printer {
-    typedef boost::spirit::utf8_string string;
+  typedef boost::spirit::utf8_string string;
 
-    void element(string const& tag, string const& value, int depth) const {
-        for (int i = 0; i < (depth*4); ++i) std::cout << ' ';
+  void element(string const& tag, string const& value, int depth) const {
+    for (int i = 0; i < (depth*4); ++i) std::cout << ' ';
 
-        std::cout << "tag: " << tag;
-        if (value != "") std::cout << ", value: " << value;
-        std::cout << std::endl;
-    }
+    std::cout << "tag: " << tag;
+    if (value != "") std::cout << ", value: " << value;
+    std::cout << std::endl;
+  }
 };
 
 void print_info(boost::spirit::info const& what) {

From aa6fd9219e5b71545d535115ebe1875ede6e6fe4 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sat, 13 Jan 2024 18:24:55 +0100
Subject: [PATCH 02/21] removed GridOptions

---
 main.cpp      |  8 +++-----
 util/Grid.cpp | 16 +++-------------
 util/Grid.h   | 15 +++------------
 3 files changed, 9 insertions(+), 30 deletions(-)

diff --git a/main.cpp b/main.cpp
index 7b70a81..16a752d 100644
--- a/main.cpp
+++ b/main.cpp
@@ -83,7 +83,6 @@ int main(int argc, char* argv[]) {
 		return EXIT_FAILURE;
 	}
 
-  GridOptions gridOptions = { {}, {} };
   std::fstream file {outputFilename->value(0), file.trunc | file.out};
   std::fstream infile {inputFilename->value(0), infile.in};
   std::string line, content, background, rewards, properties;
@@ -164,12 +163,11 @@ int main(int argc, char* argv[]) {
       setProbability(properties, probabilities, probTurnIntendedIdentifier, probTurnIntended);
     }
     if(ok) {
-      Grid grid(contentCells, backgroundCells, gridOptions, stateRewards, probIntended, faultyProbability);
+      Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability);
 
-      // grid.printToPrism(std::cout, configurations , gridOptions.getModelType());
+      grid.printToPrism(std::cout, configurations);
       std::stringstream ss;
-      // grid.printToPrism(file, configurations ,prism::ModelType::MDP);
-      grid.printToPrism(ss, configurations , gridOptions.getModelType());
+      grid.printToPrism(ss, configurations);
       std::string str = ss.str();
       grid.applyOverwrites(str, configurations);
       file << str;
diff --git a/util/Grid.cpp b/util/Grid.cpp
index f9ebdac..d5e454e 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -3,16 +3,8 @@
 
 #include <algorithm>
 
-prism::ModelType GridOptions::getModelType() const
-{
-  if (agentsWithView.size() > 1) {
-    return prism::ModelType::SMG;
-  }
-  return prism::ModelType::MDP;
-}
-
-Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability)
-  : allGridCells(gridCells), background(background), gridOptions(gridOptions), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
+Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards, const float probIntended, const float faultyProbability)
+  : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
 {
   cell max = allGridCells.at(allGridCells.size() - 1);
   maxBoundaries = std::make_pair(max.row - 1, max.column - 1);
@@ -38,7 +30,6 @@ Grid::Grid(cells gridCells, cells background, const GridOptions &gridOptions, co
     std::string color = adversary.getColor();
     color.at(0) = std::toupper(color.at(0));
     try {
-      if(gridOptions.agentsToBeConsidered.size() != 0 && std::find(gridOptions.agentsToBeConsidered.begin(), gridOptions.agentsToBeConsidered.end(), color) == gridOptions.agentsToBeConsidered.end()) continue;
       auto success = agentNameAndPositionMap.insert({ color, adversary.getCoordinates() });
       floor.push_back(adversary);
       if(!success.second) {
@@ -130,9 +121,8 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
       }
   }
 }
-void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration ,const prism::ModelType& modelType) {
+void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration) {
   cells northRestriction, eastRestriction, southRestriction, westRestriction;
-
   cells walkable = floor;
   walkable.insert(walkable.end(), goals.begin(), goals.end());
   walkable.insert(walkable.end(), boxes.begin(), boxes.end());
diff --git a/util/Grid.h b/util/Grid.h
index eb95437..7e890d3 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -6,29 +6,20 @@
 #include <utility>
 
 #include "MinigridGrammar.h"
+#include "PrismPrinter.h"
 #include "PrismModulesPrinter.h"
 #include "PrismFormulaPrinter.h"
 #include "ConfigYaml.h"
 
-struct GridOptions {
-  std::vector<AgentName> agentsToBeConsidered;
-  std::vector<AgentName> agentsWithView;
-  std::vector<AgentName> agentsWithProbabilisticBehaviour;
-  std::vector<float>     probabilitiesForActions;
-  bool                   enforceOneWays;
-
-  prism::ModelType getModelType() const;
-};
-
 class Grid {
   public:
-    Grid(cells gridCells, cells background, const GridOptions &gridOptions, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
+    Grid(cells gridCells, cells background, const std::map<coordinates, float> &stateRewards = {}, const float probIntended = 1.0, const float faultyProbability = 0);
 
     cells getGridCells();
 
     bool isBlocked(coordinates p);
     bool isWall(coordinates p);
-    void printToPrism(std::ostream &os, std::vector<Configuration>& configuration, const prism::ModelType& modelType);
+    void printToPrism(std::ostream &os, std::vector<Configuration>& configuration);
     void applyOverwrites(std::string& str, std::vector<Configuration>& configuration);
 
     std::array<bool, 8> getWalkableDirOf8Neighborhood(cell c);

From 12b08ab068d44c3c95b7b946d25bbe415e4ef588 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sat, 13 Jan 2024 18:25:14 +0100
Subject: [PATCH 03/21] set modelType based on the amount of agents

---
 util/Grid.cpp | 8 +++++++-
 util/Grid.h   | 4 ++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/util/Grid.cpp b/util/Grid.cpp
index d5e454e..8a02c5e 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -61,6 +61,12 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
       backgroundTiles.emplace(color, cellsOfColor);
     }
   }
+
+  if(adversaries.empty()) {
+    modelType = prism::ModelType::MDP;
+  } else {
+    modelType = prism::ModelType::SMG;
+  }
 }
 
 std::ostream& operator<<(std::ostream& os, const Grid& grid) {
@@ -97,7 +103,7 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
     }
       for (auto& index : config.indexes_) {
         size_t start_pos;
-        std::string search;      
+        std::string search;
 
         if (config.type_ == ConfigType::Formula) {
           search = "formula " + config.identifier_;
diff --git a/util/Grid.h b/util/Grid.h
index 7e890d3..da593ba 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -27,12 +27,12 @@ class Grid {
     friend std::ostream& operator<<(std::ostream& os, const Grid &grid);
 
   private:
-    GridOptions gridOptions;
-
     cells allGridCells;
     cells background;
     coordinates maxBoundaries;
 
+    prism::ModelType modelType;
+
     cell agent;
     cells adversaries;
     AgentNameAndPositionMap agentNameAndPositionMap;

From eda22afaa98328e8a8198808e7ae43ddbe9f8f43 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sat, 13 Jan 2024 18:25:23 +0100
Subject: [PATCH 04/21] removed some ws

---
 main.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/main.cpp b/main.cpp
index 16a752d..b68cf3f 100644
--- a/main.cpp
+++ b/main.cpp
@@ -48,14 +48,14 @@ void setProbability(const std::string& gridProperties, const std::vector<Probabi
 
   if (start_pos != std::string::npos) {
     auto end_pos = gridProperties.find('\n', start_pos);
-    auto value = gridProperties.substr(start_pos + identifier.length()  + seperator.size(), end_pos - start_pos - identifier.length()); 
+    auto value = gridProperties.substr(start_pos + identifier.length()  + seperator.size(), end_pos - start_pos - identifier.length());
     prop = std::stod(value);
   }
 
   auto yaml_config_prop = std::find_if(configProperties.begin(), configProperties.end(), [&identifier](const Probability&  obj) -> bool {return obj.probability_ == identifier;} );
 
   if (yaml_config_prop != configProperties.end()) {
-    prop = (*yaml_config_prop).value_;    
+    prop = (*yaml_config_prop).value_;
   }
 }
 

From fd2cc9e07fb04ef82c4a649380809a7948422936 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 14 Jan 2024 09:19:20 +0100
Subject: [PATCH 05/21] set defaults for probIntended and faultyProb

---
 main.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/main.cpp b/main.cpp
index b68cf3f..e26762e 100644
--- a/main.cpp
+++ b/main.cpp
@@ -129,9 +129,9 @@ int main(int argc, char* argv[]) {
   std::vector<Configuration> configurations;
   std::vector<Probability> probabilities;
   std::map<coordinates, float> stateRewards;
-  float faultyProbability = 0.1;
-  float probIntended = 0.9;
-  float probTurnIntended = 1;
+  float faultyProbability = 0.0;
+  float probIntended = 1.0;
+  float probTurnIntended = 1.0;
 
   try {
     bool ok = phrase_parse(contentIter, contentLast, contentParser, qi::space, contentCells);

From 370740349ca2da8c1e31bb2d8ac5234ee803be5a Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 14 Jan 2024 10:08:57 +0100
Subject: [PATCH 06/21] fixed turn guards regarding IsOnSlippery

---
 util/PrismModulesPrinter.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index f360cbc..ad8617c 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -276,7 +276,10 @@ namespace prism {
   std::string PrismModulesPrinter::printTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::string &cond) {
     std::string actionName = "[" + a + "_turn_" + direction + "]";
     agentNameActionMap.at(a).insert({actionId, actionName});
-    return "  " + actionName + " " + cond + " -> ";
+    std::string guard = "  " + actionName;
+    if(slipperyBehaviour()) guard += " !" + a + "IsOnSlippery & ";
+    guard += cond + " -> ";
+    return guard;
   }
 
   std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const {
@@ -459,7 +462,7 @@ namespace prism {
   std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector<std::string> &guards, const std::string &cond) {
     std::string actionName = "[" + a + "_turn_" + direction + "]";
     agentNameActionMap.at(a).insert({actionId, actionName});
-    return "  " + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> ";
+    return "  " + actionName + " " + a + "IsOnSlippery & " + buildConjunction(a, guards) + " & " + cond + " -> ";
   }
 
   std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) {

From 11658eb01fd098c4a7e128a48a0d9bfe19c6edfa Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 14 Jan 2024 10:21:40 +0100
Subject: [PATCH 07/21] fixed multiple column row issues

---
 util/Grid.cpp                |  2 +-
 util/PrismModulesPrinter.cpp | 18 +++++++++---------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/util/Grid.cpp b/util/Grid.cpp
index 8a02c5e..d87fcc0 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -7,7 +7,7 @@ Grid::Grid(cells gridCells, cells background, const std::map<coordinates, float>
   : allGridCells(gridCells), background(background), stateRewards(stateRewards), probIntended(probIntended), faultyProbability(faultyProbability)
 {
   cell max = allGridCells.at(allGridCells.size() - 1);
-  maxBoundaries = std::make_pair(max.row - 1, max.column - 1);
+  maxBoundaries = std::make_pair(max.column - 1, max.row - 1);
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(walls),         [](cell c) { return c.type == Type::Wall; });
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(lava),          [](cell c) { return c.type == Type::Lava; });
   std::copy_if(gridCells.begin(),  gridCells.end(),  std::back_inserter(floor),         [](cell c) { return c.type == Type::Floor; }); // TODO CHECK IF ALL AGENTS ARE ADDED TO FLOOR
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index ad8617c..fb1803a 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -104,8 +104,8 @@ namespace prism {
   void PrismModulesPrinter::printPortableObjectModule(const cell &object) {
     std::string identifier = capitalize(object.getColor()) + object.getType();
     os << "\nmodule " << identifier << std::endl;
-    os << "  x" << identifier << " : [-1.." << maxBoundaries.second  << "] init " << object.column << ";\n";
-    os << "  y" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n";
+    os << "  col" << identifier << " : [-1.." << maxBoundaries.first  << "] init " << object.column << ";\n";
+    os << "  row" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.row << ";\n";
     os << "  " << identifier << "PickedUp : bool;\n";
     os << "\n";
 
@@ -118,19 +118,19 @@ namespace prism {
   void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) {
     std::string actionName = "[" + agentName + "_pickup_" + identifier + "]";
     agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
+    os << "  " << actionName << " true -> (col" << identifier << "'=-1) & (row" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
     actionName = "[" + agentName + "_drop_" + identifier + "_north]";
     agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ")   & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
+    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ")   & (row" << identifier << "'=row" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
     actionName = "[" + agentName + "_drop_" + identifier + "_west]";
     agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
+    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "-1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
     actionName = "[" + agentName + "_drop_" + identifier + "_south]";
     agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ")   & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
+    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ")   & (row" << identifier << "'=row" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
     actionName = "[" + agentName + "_drop_" + identifier + "_east]";
     agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
+    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "+1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
   }
 
   void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) {
@@ -171,8 +171,8 @@ namespace prism {
 
   void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) {
     os << "\nmodule " << agentName << std::endl;
-    os << "  col"    << agentName << " : [1.." << maxBoundaries.second  << "] init " << initialPosition.second << ";\n";
-    os << "  row"    << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n";
+    os << "  col"    << agentName << " : [1.." << maxBoundaries.first  << "] init " << initialPosition.first << ";\n";
+    os << "  row"    << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
     os << "  view" << agentName << " : [0..3] init 1;\n";
 
     printTurnActionsForRobot(agentName);

From 8c5ff31ad36577f41e433f664cca21323da04ee0 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 14 Jan 2024 13:11:04 +0100
Subject: [PATCH 08/21] NOFAULT is 3 instead of -1

---
 util/PrismModulesPrinter.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index fb1803a..68b19ee 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -3,7 +3,7 @@
 #include <map>
 #include <string>
 
-#define NOFAULT -1
+#define NOFAULT 3
 #define LEFT 0
 #define RIGHT 1
 #define FORWARD 2
@@ -471,7 +471,7 @@ namespace prism {
 
   void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) {
     os << "\nmodule " << a << "FaultyBehaviour" << std::endl;
-    os << "  previousAction" << a << " : [-1..2] init -1;\n";
+    os << "  previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "] init " + std::to_string(NOFAULT) + ";\n";
 
     for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
       os << "  " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";

From 5d373c5cb815f34019ebbaf8895a547d22fd4b13 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sun, 14 Jan 2024 16:26:04 +0100
Subject: [PATCH 09/21] remove debug printout to std::cout

---
 main.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/main.cpp b/main.cpp
index e26762e..012f2e6 100644
--- a/main.cpp
+++ b/main.cpp
@@ -165,7 +165,7 @@ int main(int argc, char* argv[]) {
     if(ok) {
       Grid grid(contentCells, backgroundCells, stateRewards, probIntended, faultyProbability);
 
-      grid.printToPrism(std::cout, configurations);
+      //grid.printToPrism(std::cout, configurations);
       std::stringstream ss;
       grid.printToPrism(ss, configurations);
       std::string str = ss.str();

From 969dd87adaefabb8121b9034e7f5fdea043f9afc Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Tue, 16 Jan 2024 14:53:11 +0100
Subject: [PATCH 10/21] changed behaviour of slippery tiles

---
 util/PrismModulesPrinter.cpp | 24 ++++++++----------------
 1 file changed, 8 insertions(+), 16 deletions(-)

diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index 68b19ee..aa2a7bc 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -325,10 +325,8 @@ namespace prism {
     actionStream << printSlipperyMovementGuard(a, "North", 0, {"!"+a+"CannotSlipEast",     a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a) } }) << ";\n";
     actionStream << printSlipperyMovementGuard(a, "North", 0, {    a+"CannotSlipEast",     a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n";
 
-    actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "North", 1, {    a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, northUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth",     a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, southUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "North", 1, {    a+"CannotSlipSouth",     a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, "true" }, {1 - probIntended, northUpdate(a)} }) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "North", 1, {    a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, "true"} }) << ";\n";
   }
 
   void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) {
@@ -351,10 +349,8 @@ namespace prism {
     actionStream << printSlipperyMovementGuard(a, "East", 1, {"!"+a+"CannotSlipSouth",     a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", { {1, southUpdate(a) } }) << ";\n";
     actionStream << printSlipperyMovementGuard(a, "East", 1, {    a+"CannotSlipSouth",     a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n";
 
-    actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipWest", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, westUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "East", 2, {    a+"CannotSlipWest", "!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, eastUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipWest",     a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, westUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "East", 2, {    a+"CannotSlipWest",     a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", {}) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "East", 2, {"!"+a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {probIntended, eastUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "East", 2, {    a+"CannotSlipEast"}) << printSlipperyMovementUpdate(a, "East", { {1, "true"} }) << ";\n";
   }
 
   void PrismModulesPrinter::printSlipperyMovementActionsForSouth(const AgentName &a) {
@@ -377,10 +373,8 @@ namespace prism {
     actionStream << printSlipperyMovementGuard(a, "South", 0, {"!"+a+"CannotSlipEast",     a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a) } }) << ";\n";
     actionStream << printSlipperyMovementGuard(a, "South", 0, {    a+"CannotSlipEast",     a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n";
 
-    actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, northUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "South", 3, {    a+"CannotSlipSouth", "!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, northUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth",     a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", { {1, southUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "South", 3, {    a+"CannotSlipSouth",     a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "South", 3, {    a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "South", { {1, "true"} }) << ";\n";
   }
 
   void PrismModulesPrinter::printSlipperyMovementActionsForWest(const AgentName &a) {
@@ -403,10 +397,8 @@ namespace prism {
     actionStream << printSlipperyMovementGuard(a, "West", 1, {"!"+a+"CannotSlipSouth",     a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", { {1, southUpdate(a) } }) << ";\n";
     actionStream << printSlipperyMovementGuard(a, "West", 1, {    a+"CannotSlipSouth",     a+"CannotSlipSouthWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n";
 
-    actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, eastUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "West", 0, {    a+"CannotSlipEast", "!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, westUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipEast",     a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {1, eastUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "West", 0, {    a+"CannotSlipEast",     a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {}) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "West", 0, {"!"+a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", { {probIntended, westUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "West", 0, {    a+"CannotSlipWest"}) << printSlipperyMovementUpdate(a, "West", {{1, "true"}}) << ";\n";
   }
 
   void PrismModulesPrinter::printSlipperyTurnActionsForNorth(const AgentName &a) {

From ba348a95f291107149699e2aa8e9446362236ab8 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Wed, 17 Jan 2024 15:23:58 +0100
Subject: [PATCH 11/21] fixed bugs in slippery updates

---
 util/PrismModulesPrinter.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index aa2a7bc..5e27ad7 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -325,8 +325,8 @@ namespace prism {
     actionStream << printSlipperyMovementGuard(a, "North", 0, {"!"+a+"CannotSlipEast",     a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", { {1, eastUpdate(a) } }) << ";\n";
     actionStream << printSlipperyMovementGuard(a, "North", 0, {    a+"CannotSlipEast",     a+"CannotSlipNorthEast"}) << printSlipperyMovementUpdate(a, "North", {}) << ";\n";
 
-    actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, "true" }, {1 - probIntended, northUpdate(a)} }) << ";\n";
-    actionStream << printSlipperyMovementGuard(a, "North", 1, {    a+"CannotSlipNorth"}) << printSlipperyMovementUpdate(a, "North", { {1, "true"} }) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "North", 1, {"!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "North", { {probIntended, southUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "North", 1, {    a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "North", { {1, "true"} }) << ";\n";
   }
 
   void PrismModulesPrinter::printSlipperyMovementActionsForEast(const AgentName &a) {
@@ -373,7 +373,7 @@ namespace prism {
     actionStream << printSlipperyMovementGuard(a, "South", 0, {"!"+a+"CannotSlipEast",     a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", { {1, eastUpdate(a) } }) << ";\n";
     actionStream << printSlipperyMovementGuard(a, "South", 0, {    a+"CannotSlipEast",     a+"CannotSlipSouthEast"}) << printSlipperyMovementUpdate(a, "South", {}) << ";\n";
 
-    actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, southUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
+    actionStream << printSlipperyMovementGuard(a, "South", 3, {"!"+a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "South", { {probIntended, northUpdate(a) }, {1 - probIntended, "true"} }) << ";\n";
     actionStream << printSlipperyMovementGuard(a, "South", 3, {    a+"CannotSlipSouth"}) << printSlipperyMovementUpdate(a, "South", { {1, "true"} }) << ";\n";
   }
 

From 4b8444f6aa0b8551f5b51fa96321bb3b0e7b6d68 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Wed, 17 Jan 2024 15:24:08 +0100
Subject: [PATCH 12/21] the agent cannot turn in lava

---
 util/PrismModulesPrinter.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index 5e27ad7..cf91edc 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -278,6 +278,7 @@ namespace prism {
     agentNameActionMap.at(a).insert({actionId, actionName});
     std::string guard = "  " + actionName;
     if(slipperyBehaviour()) guard += " !" + a + "IsOnSlippery & ";
+    if(anyLava)             guard += " !" + a + "IsOnLava &";
     guard += cond + " -> ";
     return guard;
   }

From ec5480f670ed1593a493e385ef27b484bcf542d2 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Thu, 18 Jan 2024 13:07:39 +0100
Subject: [PATCH 13/21] use init struct

We do not know the view direction of all of the agents, hence we
iterate over all possible combinations as initial states
---
 util/Grid.cpp                | 14 +++-------
 util/PrismFormulaPrinter.cpp | 52 ++++++++++++++++++++++++++++++++++--
 util/PrismFormulaPrinter.h   | 11 +++++++-
 util/PrismModulesPrinter.cpp | 27 ++++++++-----------
 util/PrismPrinter.h          |  6 +++++
 5 files changed, 81 insertions(+), 29 deletions(-)

diff --git a/util/Grid.cpp b/util/Grid.cpp
index d87fcc0..0fcf24e 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -154,22 +154,16 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
                  [](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;});
   std::string agentName = agentNames.at(0);
 
-  prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals);
+  prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0);
   prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty());
 
   modules.printModelType(modelType);
   for(const auto &agentName : agentNames) {
     formulas.print(agentName);
   }
-  //std::vector<std::string> constants {"const double prop_zero = 0/9;",
-  //                                    "const double prop_intended = 6/9;",
-  //                                    "const double prop_turn_intended = 6/9;",
-  //                                    "const double prop_displacement = 3/9;",
-  //                                    "const double prop_turn_displacement = 3/9;",
-  //                                    "const int width = " + std::to_string(maxBoundaries.first) + ";",
-  //                                    "const int height = " + std::to_string(maxBoundaries.second) + ";"
-  //                                    };
-  //modules.printConstants(os, constants);
+  formulas.printCollisionFormula(agentName);
+  formulas.printInitStruct();
+
   modules.print();
 
 
diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index 1317fe3..29b4a07 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -57,8 +57,8 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
 }
 
 namespace prism {
-  PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals)
-    : os(os),  restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals)
+  PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty)
+    : os(os),  restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals), agentNameAndPositionMap(agentNameAndPositionMap), faulty(faulty)
   { }
 
   void PrismFormulaPrinter::print(const AgentName &agentName) {
@@ -159,6 +159,54 @@ namespace prism {
     if(!semicolon) os << ";\n";
   }
 
+  void PrismFormulaPrinter::printCollisionFormula(const AgentName &agentName) {
+    if(!agentNameAndPositionMap.empty()) {
+      os << "formula collision = ";
+      bool first = true;
+      for(auto const [name, coordinates] : agentNameAndPositionMap) {
+        if(name == agentName) continue;
+        if(first) first = false;
+        else os << " | ";
+        os << "(col"+agentName+"=col"+name+"&row"+agentName+"=row"+name+")";
+      }
+      os << ";\n";
+      printCollisionLabel();
+    }
+  }
+
+  void PrismFormulaPrinter::printCollisionLabel() {
+    if(!agentNameAndPositionMap.empty()) {
+      os << "label \"collision\" = collision;\n";
+    }
+  }
+
+  void PrismFormulaPrinter::printInitStruct() {
+    os << "init\n";
+    bool first = true;
+    for(auto const [a, coordinates] : agentNameAndPositionMap) {
+      if(first) first = false;
+      else os << " & ";
+      os << "(col"+a+"="+std::to_string(coordinates.first)+"&row"+a+"="+std::to_string(coordinates.second)+" & ";
+      os << "(view"+a+"=0|view"+a+"=1|view"+a+"=2|view"+a+"=3) ";
+      if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT);
+      os << ")";
+    }
+    for(auto const ball : balls) {
+      std::string identifier = capitalize(ball.getColor()) + ball.getType();
+      os << " & (col"+identifier+"="+std::to_string(ball.column)+"&row"+identifier+"="+std::to_string(ball.row)+") ";
+    }
+    for(auto const key : keys) {
+      std::string identifier = capitalize(key.getColor()) + key.getType();
+      os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+") ";
+    }
+    for(auto const box : boxes) {
+      std::string identifier = capitalize(box.getColor()) + box.getType();
+      os << " & (col"+identifier+"="+std::to_string(box.column)+"&row"+identifier+"="+std::to_string(box.row)+") ";
+    }
+    os << "endinit\n\n";
+  }
+
+
   std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon) {
     return "formula " + formulaName + " = " + formula + (semicolon ? ";\n": "");
   }
diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h
index f1def2d..8e24578 100644
--- a/util/PrismFormulaPrinter.h
+++ b/util/PrismFormulaPrinter.h
@@ -21,7 +21,7 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells();
 namespace prism {
   class PrismFormulaPrinter {
     public:
-      PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals);
+      PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty);
 
       void print(const AgentName &agentName);
 
@@ -31,6 +31,11 @@ namespace prism {
       void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition);
       void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition);
       void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction);
+
+      void printCollisionFormula(const std::string &agentName);
+      void printCollisionLabel();
+
+      void printInitStruct();
     private:
       std::string buildFormula(const std::string &formulaName, const std::string &formula, const bool semicolon = true);
       std::string buildLabel(const std::string &labelName, const std::string &label);
@@ -55,7 +60,11 @@ namespace prism {
       cells lava;
       cells goals;
 
+      AgentNameAndPositionMap agentNameAndPositionMap;
+
       std::vector<std::string> conditionalMovementRestrictions;
       std::vector<std::string> portableObjects;
+
+      bool faulty;
   };
 }
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index cf91edc..a12353b 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -3,11 +3,6 @@
 #include <map>
 #include <string>
 
-#define NOFAULT 3
-#define LEFT 0
-#define RIGHT 1
-#define FORWARD 2
-
 
 std::string northUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"-1)"; }
 std::string southUpdate(const AgentName &a) { return "(row"+a+"'=row"+a+"+1)"; }
@@ -104,8 +99,8 @@ namespace prism {
   void PrismModulesPrinter::printPortableObjectModule(const cell &object) {
     std::string identifier = capitalize(object.getColor()) + object.getType();
     os << "\nmodule " << identifier << std::endl;
-    os << "  col" << identifier << " : [-1.." << maxBoundaries.first  << "] init " << object.column << ";\n";
-    os << "  row" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.row << ";\n";
+    os << "  col" << identifier << " : [-1.." << maxBoundaries.first  << "];\n";
+    os << "  row" << identifier << " : [-1.." << maxBoundaries.second << "];\n";
     os << "  " << identifier << "PickedUp : bool;\n";
     os << "\n";
 
@@ -136,7 +131,7 @@ namespace prism {
   void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) {
     std::string identifier = capitalize(door.getColor()) + door.getType();
     os << "\nmodule " << identifier << std::endl;
-    os << "  " << identifier << "Open : bool init false;\n";
+    os << "  " << identifier << "Open : bool;\n";
     os << "\n";
 
     if(opened) {
@@ -171,9 +166,9 @@ namespace prism {
 
   void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) {
     os << "\nmodule " << agentName << std::endl;
-    os << "  col"    << agentName << " : [1.." << maxBoundaries.first  << "] init " << initialPosition.first << ";\n";
-    os << "  row"    << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n";
-    os << "  view" << agentName << " : [0..3] init 1;\n";
+    os << "  col"    << agentName << " : [1.." << maxBoundaries.first  << "];\n";
+    os << "  row"    << agentName << " : [1.." << maxBoundaries.second << "];\n";
+    os << "  view" << agentName << " : [0..3];\n";
 
     printTurnActionsForRobot(agentName);
     printMovementActionsForRobot(agentName);
@@ -192,19 +187,19 @@ namespace prism {
 
     for(const auto &key : keys) {
       std::string identifier = capitalize(key.getColor()) + key.getType();
-      os << "  " << agentName << "Carrying" << identifier << " : bool init false;\n";
+      os << "  " << agentName << "Carrying" << identifier << " : bool;\n";
       printPortableObjectActionsForRobot(agentName, identifier);
     }
 
     for(const auto &ball : balls) {
       std::string identifier = capitalize(ball.getColor()) + ball.getType();
-      os << "  " << agentName << "Carrying" << identifier << " : bool init false;\n";
+      os << "  " << agentName << "Carrying" << identifier << " : bool;\n";
       printPortableObjectActionsForRobot(agentName, identifier);
     }
 
     for(const auto &box : boxes) {
       std::string identifier = capitalize(box.getColor()) + box.getType();
-      os << "  " << agentName << "Carrying" << identifier << " : bool init false;\n";
+      os << "  " << agentName << "Carrying" << identifier << " : bool;\n";
       printPortableObjectActionsForRobot(agentName, identifier);
     }
 
@@ -464,7 +459,7 @@ namespace prism {
 
   void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) {
     os << "\nmodule " << a << "FaultyBehaviour" << std::endl;
-    os << "  previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "] init " + std::to_string(NOFAULT) + ";\n";
+    os << "  previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "];\n";
 
     for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
       os << "  " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
@@ -474,7 +469,7 @@ namespace prism {
 
   void PrismModulesPrinter::printMoveModule() {
     os << "\nmodule " << "Arbiter" << std::endl;
-    os << "  clock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n";
+    os << "  clock : [0.." << agentIndexMap.size() - 1 << "];\n";
 
     for(const auto [agentName, actions] : agentNameActionMap) {
       for(const auto [actionId, actionName] : actions) {
diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h
index 572cb40..a75e9f1 100644
--- a/util/PrismPrinter.h
+++ b/util/PrismPrinter.h
@@ -5,6 +5,12 @@
 
 #include "cell.h"
 
+#define NOFAULT 3
+#define LEFT 0
+#define RIGHT 1
+#define FORWARD 2
+
+
 typedef std::string AgentName;
 typedef size_t ViewDirection;
 typedef std::pair<std::string, coordinates> AgentNameAndPosition;

From a1ac41b01b9bd0ff43e0c6f114e31ecc20dae004 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Thu, 18 Jan 2024 21:12:39 +0100
Subject: [PATCH 14/21] fix bug with conditional movement formulas

---
 util/PrismFormulaPrinter.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index 29b4a07..c8bc460 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -62,6 +62,7 @@ namespace prism {
   { }
 
   void PrismFormulaPrinter::print(const AgentName &agentName) {
+    conditionalMovementRestrictions.clear();
     for(const auto& [direction, cells] : restrictions) {
       printRestrictionFormula(agentName, direction, cells);
     }

From af2ee862e650dbefb5e0152bcf0485a71c3ee4a4 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Thu, 18 Jan 2024 21:13:07 +0100
Subject: [PATCH 15/21] objects are initially not picked up

---
 util/PrismFormulaPrinter.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index c8bc460..e50b2f4 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -194,15 +194,15 @@ namespace prism {
     }
     for(auto const ball : balls) {
       std::string identifier = capitalize(ball.getColor()) + ball.getType();
-      os << " & (col"+identifier+"="+std::to_string(ball.column)+"&row"+identifier+"="+std::to_string(ball.row)+") ";
+      os << " & (col"+identifier+"="+std::to_string(ball.column)+"&row"+identifier+"="+std::to_string(ball.row)+"&"+identifier+"PickedUp=false) ";
     }
     for(auto const key : keys) {
       std::string identifier = capitalize(key.getColor()) + key.getType();
-      os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+") ";
+      os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) ";
     }
     for(auto const box : boxes) {
       std::string identifier = capitalize(box.getColor()) + box.getType();
-      os << " & (col"+identifier+"="+std::to_string(box.column)+"&row"+identifier+"="+std::to_string(box.row)+") ";
+      os << " & (col"+identifier+"="+std::to_string(box.column)+"&row"+identifier+"="+std::to_string(box.row)+"&"+identifier+"PickedUp=false) ";
     }
     os << "endinit\n\n";
   }

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 16/21] 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";
   }
 

From bd8bf2eca5115c723343902d865f1f3d0bef2b24 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Thu, 18 Jan 2024 21:56:03 +0100
Subject: [PATCH 17/21] print collision formula when other agents present

---
 util/Grid.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/util/Grid.cpp b/util/Grid.cpp
index 0fcf24e..91366b2 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -161,7 +161,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
   for(const auto &agentName : agentNames) {
     formulas.print(agentName);
   }
-  formulas.printCollisionFormula(agentName);
+  if(agentNameAndPositionMap.size() > 1) formulas.printCollisionFormula(agentName);
   formulas.printInitStruct();
 
   modules.print();

From 7d7649bd0611ed4b1da98b6513366efb500d0b14 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Fri, 19 Jan 2024 10:40:23 +0100
Subject: [PATCH 18/21] include all action with indices

---
 util/PrismModulesPrinter.h | 1 +
 util/PrismPrinter.h        | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index c0d192a..bfdd58f 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -109,6 +109,7 @@ namespace prism {
       std::vector<Configuration> configuration;
       std::vector<ViewDirection> viewDirections = {0, 1, 2, 3};
       std::map<ViewDirection, std::string> viewDirectionToString = {{0, "East"}, {1, "South"}, {2, "West"}, {3, "North"}};
+      std::vector<std::pair<size_t, std::string>> nonMovementActions = { {PICKUP, "pickup"}, {DROP, "drop"}, {TOGGLE, "toggle"}, {DONE, "done"} };
 
       std::map<AgentName, std::set<std::pair<ActionId, std::string>>> agentNameActionMap;
   };
diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h
index a75e9f1..1f82cf4 100644
--- a/util/PrismPrinter.h
+++ b/util/PrismPrinter.h
@@ -9,6 +9,10 @@
 #define LEFT 0
 #define RIGHT 1
 #define FORWARD 2
+#define PICKUP 3
+#define DROP 4
+#define TOGGLE 5
+#define DONE 6
 
 
 typedef std::string AgentName;

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 19/21] 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);

From 8cc2b0c4da9abcc17edf54d9414fed0cb6da225e Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sat, 20 Jan 2024 13:09:22 +0100
Subject: [PATCH 20/21] portable objects are now traversable

This is also changes keys to not be dropable anymore.
---
 util/Grid.cpp                |  4 +--
 util/PrismFormulaPrinter.cpp | 44 ++++-------------------
 util/PrismFormulaPrinter.h   |  6 ++--
 util/PrismModulesPrinter.cpp | 70 +++++++++++++++---------------------
 util/PrismModulesPrinter.h   |  8 ++---
 5 files changed, 41 insertions(+), 91 deletions(-)

diff --git a/util/Grid.cpp b/util/Grid.cpp
index 91366b2..8f83703 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -154,8 +154,8 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
                  [](const std::map<AgentNameAndPosition::first_type,AgentNameAndPosition::second_type>::value_type &pair){return pair.first;});
   std::string agentName = agentNames.at(0);
 
-  prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0);
-  prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty());
+  prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals, agentNameAndPositionMap, faultyProbability > 0.0);
+  prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability, !lava.empty(), !goals.empty());
 
   modules.printModelType(modelType);
   for(const auto &agentName : agentNames) {
diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
index e50b2f4..bbb9a0c 100644
--- a/util/PrismFormulaPrinter.cpp
+++ b/util/PrismFormulaPrinter.cpp
@@ -57,8 +57,8 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells() {
 }
 
 namespace prism {
-  PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty)
-    : os(os),  restrictions(restrictions), walls(walls), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals), agentNameAndPositionMap(agentNameAndPositionMap), faulty(faulty)
+  PrismFormulaPrinter::PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty)
+    : os(os),  restrictions(restrictions), walls(walls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), lava(lava), goals(goals), agentNameAndPositionMap(agentNameAndPositionMap), faulty(faulty)
   { }
 
   void PrismFormulaPrinter::print(const AgentName &agentName) {
@@ -83,21 +83,10 @@ namespace prism {
     if(!lava.empty())  printIsOnFormula(agentName, "Lava", lava);
     if(!goals.empty()) printIsOnFormula(agentName, "Goal", goals);
 
-    for(const auto& ball : balls) {
-      std::string identifier = capitalize(ball.getColor()) + ball.getType();
-      printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
-      portableObjects.push_back(agentName + "Carrying" + identifier);
-    }
-
-    for(const auto& box : boxes) {
-      std::string identifier = capitalize(box.getColor()) + box.getType();
-      printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
-      portableObjects.push_back(agentName + "Carrying" + identifier);
-    }
 
     for(const auto& key : keys) {
       std::string identifier = capitalize(key.getColor()) + key.getType();
-      printRelativeRestrictionFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
+      printRelativeIsInFrontOfFormulaWithCondition(agentName, identifier, "!" + identifier + "PickedUp");
       portableObjects.push_back(agentName + "Carrying" + identifier);
     }
 
@@ -136,27 +125,14 @@ namespace prism {
     conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
   }
 
-  void PrismFormulaPrinter::printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) {
-    os << buildFormula(agentName + "CannotMove" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition);
-    conditionalMovementRestrictions.push_back(agentName + "CannotMove" + reason);
+  void PrismFormulaPrinter::printRelativeIsInFrontOfFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition) {
+    os << buildFormula(agentName + "IsInFrontOf" + reason, "(" + buildDisjunction(agentName, reason) + ") & " + condition);
   }
 
   void PrismFormulaPrinter::printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction) {
     std::pair<int, int> slipCell = getRelativeSurroundingCells().at(direction);
     bool semicolon = anyPortableObject() ? false : true;
     os << buildFormula(agentName + "CannotSlip" + direction, buildDisjunction(agentName, walls, slipCell), semicolon);
-    for(auto const key : keys) {
-      std::string identifier = capitalize(key.getColor()) + key.getType();
-      os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
-    }
-    for(auto const ball : balls) {
-      std::string identifier = capitalize(ball.getColor()) + ball.getType();
-      os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
-    }
-    for(auto const box : boxes) {
-      std::string identifier = capitalize(box.getColor()) + box.getType();
-      os << " | " << objectPositionToConjunction(agentName, identifier, slipCell);
-    }
     if(!semicolon) os << ";\n";
   }
 
@@ -192,18 +168,10 @@ namespace prism {
       if(faulty) os << " & previousAction"+a+"="+std::to_string(NOFAULT);
       os << ")";
     }
-    for(auto const ball : balls) {
-      std::string identifier = capitalize(ball.getColor()) + ball.getType();
-      os << " & (col"+identifier+"="+std::to_string(ball.column)+"&row"+identifier+"="+std::to_string(ball.row)+"&"+identifier+"PickedUp=false) ";
-    }
     for(auto const key : keys) {
       std::string identifier = capitalize(key.getColor()) + key.getType();
       os << " & (col"+identifier+"="+std::to_string(key.column)+"&row"+identifier+"="+std::to_string(key.row)+"&"+identifier+"PickedUp=false) ";
     }
-    for(auto const box : boxes) {
-      std::string identifier = capitalize(box.getColor()) + box.getType();
-      os << " & (col"+identifier+"="+std::to_string(box.column)+"&row"+identifier+"="+std::to_string(box.row)+"&"+identifier+"PickedUp=false) ";
-    }
     os << "endinit\n\n";
   }
 
@@ -264,6 +232,6 @@ namespace prism {
     return !slipperyTiles.at("North").empty() || !slipperyTiles.at("East").empty() || !slipperyTiles.at("South").empty() || !slipperyTiles.at("West").empty();
   }
   bool PrismFormulaPrinter::anyPortableObject() const {
-    return !keys.empty() || !boxes.empty() || !balls.empty();
+    return !keys.empty();
   }
 }
diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h
index 8e24578..e0c5a62 100644
--- a/util/PrismFormulaPrinter.h
+++ b/util/PrismFormulaPrinter.h
@@ -21,7 +21,7 @@ std::map<std::string, std::pair<int, int>> getRelativeSurroundingCells();
 namespace prism {
   class PrismFormulaPrinter {
     public:
-      PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty);
+      PrismFormulaPrinter(std::ostream &os, const std::map<std::string, cells> &restrictions, const cells &walls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const cells &lava, const cells &goals, const AgentNameAndPositionMap &agentNameAndPositionMap, const bool faulty);
 
       void print(const AgentName &agentName);
 
@@ -29,7 +29,7 @@ namespace prism {
       void printIsOnFormula(const AgentName &agentName, const std::string &type, const cells &grid_cells, const std::string &direction = "");
       void printIsNextToFormula(const AgentName &agentName, const std::string &type, const std::map<ViewDirection, coordinates> &coordinates);
       void printRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::map<ViewDirection, coordinates> &coordinates, const std::string &condition);
-      void printRelativeRestrictionFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition);
+      void printRelativeIsInFrontOfFormulaWithCondition(const AgentName &agentName, const std::string &reason, const std::string &condition);
       void printSlipRestrictionFormula(const AgentName &agentName, const std::string &direction);
 
       void printCollisionFormula(const std::string &agentName);
@@ -51,8 +51,6 @@ namespace prism {
       std::ostream &os;
       std::map<std::string, cells> restrictions;
       cells walls;
-      cells boxes;
-      cells balls;
       cells lockedDoors;
       cells unlockedDoors;
       cells keys;
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index 5b6ddd1..01c8431 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -11,8 +11,8 @@ std::string westUpdate(const AgentName &a)  { return "(col"+a+"'=col"+a+"-1)"; }
 
 namespace prism {
 
-  PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals)
-    : os(os), modelType(modelType), maxBoundaries(maxBoundaries), boxes(boxes), balls(balls), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) {
+  PrismModulesPrinter::PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals)
+    : os(os), modelType(modelType), maxBoundaries(maxBoundaries), lockedDoors(lockedDoors), unlockedDoors(unlockedDoors), keys(keys), slipperyTiles(slipperyTiles), agentNameAndPositionMap(agentNameAndPositionMap), configuration(config), probIntended(probIntended), faultyProbability(faultyProbability), anyLava(anyLava), anyGoals(anyGoals) {
       numberOfPlayer = agentNameAndPositionMap.size();
       size_t index = 0;
       for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) {
@@ -40,12 +40,6 @@ namespace prism {
     for(const auto &key : keys) {
       printPortableObjectModule(key);
     }
-    for(const auto &ball : balls) {
-      printPortableObjectModule(ball);
-    }
-    for(const auto &box : boxes) {
-      printPortableObjectModule(box);
-    }
     for(const auto &door : unlockedDoors) {
       printDoorModule(door, true);
     }
@@ -110,22 +104,24 @@ namespace prism {
     os << "endmodule\n\n";
   }
 
-  void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier) {
+  void PrismModulesPrinter::printPortableObjectActions(const std::string &agentName, const std::string &identifier, const bool canBeDroped) {
     std::string actionName = "[" + agentName + "_pickup_" + identifier + "]";
-    agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
+    agentNameActionMap.at(agentName).insert({PICKUP, actionName});
     os << "  " << actionName << " true -> (col" << identifier << "'=-1) & (row" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n";
-    actionName = "[" + agentName + "_drop_" + identifier + "_north]";
-    agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ")   & (row" << identifier << "'=row" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
-    actionName = "[" + agentName + "_drop_" + identifier + "_west]";
-    agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "-1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
-    actionName = "[" + agentName + "_drop_" + identifier + "_south]";
-    agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ")   & (row" << identifier << "'=row" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
-    actionName = "[" + agentName + "_drop_" + identifier + "_east]";
-    agentNameActionMap.at(agentName).insert({NOFAULT, actionName});
-    os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "+1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
+    if(canBeDroped) {
+      actionName = "[" + agentName + "_drop_" + identifier + "_north]";
+      agentNameActionMap.at(agentName).insert({DROP, actionName});
+      os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ")   & (row" << identifier << "'=row" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n";
+      actionName = "[" + agentName + "_drop_" + identifier + "_west]";
+      agentNameActionMap.at(agentName).insert({DROP, actionName});
+      os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "-1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
+      actionName = "[" + agentName + "_drop_" + identifier + "_south]";
+      agentNameActionMap.at(agentName).insert({DROP, actionName});
+      os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << ")   & (row" << identifier << "'=row" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n";
+      actionName = "[" + agentName + "_drop_" + identifier + "_east]";
+      agentNameActionMap.at(agentName).insert({DROP, actionName});
+      os << "  " << actionName << " " << " true -> (col" << identifier << "'=col" << agentName << "+1) & (row" << identifier << "'=row" << agentName << ") & (" << identifier << "PickedUp'=false);\n";
+    }
   }
 
   void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) {
@@ -191,18 +187,6 @@ namespace prism {
       printPortableObjectActionsForRobot(agentName, identifier);
     }
 
-    for(const auto &ball : balls) {
-      std::string identifier = capitalize(ball.getColor()) + ball.getType();
-      os << "  " << agentName << "Carrying" << identifier << " : bool;\n";
-      printPortableObjectActionsForRobot(agentName, identifier);
-    }
-
-    for(const auto &box : boxes) {
-      std::string identifier = capitalize(box.getColor()) + box.getType();
-      os << "  " << agentName << "Carrying" << identifier << " : bool;\n";
-      printPortableObjectActionsForRobot(agentName, identifier);
-    }
-
     printNonMovementActionsForRobot(agentName);
 
 
@@ -213,13 +197,15 @@ namespace prism {
     os << "endmodule\n\n";
   }
 
-  void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) {
-    actionStream << "  [" << a << "_pickup_" << i << "] "      << " !" << a << "IsCarrying & " <<  a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n";
-	  actionStream << "  [" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n";
-	  actionStream << "  [" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall  -> (" << a << "Carrying" << i << "'=false);\n";
-	  actionStream << "  [" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n";
-	  actionStream << "  [" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall  -> (" << a << "Carrying" << i << "'=false);\n";
-    actionStream << "\n";
+  void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i, const bool canBeDroped) {
+    actionStream << "  [" << a << "_pickup_" << i << "] "      << " !" << a << "IsCarrying & " <<  a << "IsInFrontOf" << i << " -> (" << a << "Carrying" << i << "'=true);\n";
+    if(canBeDroped) {
+	    actionStream << "  [" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n";
+	    actionStream << "  [" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall  -> (" << a << "Carrying" << i << "'=false);\n";
+	    actionStream << "  [" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n";
+	    actionStream << "  [" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall  -> (" << a << "Carrying" << i << "'=false);\n";
+      actionStream << "\n";
+    }
   }
 
   void PrismModulesPrinter::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) {
@@ -636,7 +622,7 @@ namespace prism {
   }
 
   bool PrismModulesPrinter::anyPortableObject() const {
-    return !keys.empty() || !boxes.empty() || !balls.empty();
+    return !keys.empty();
   }
 
   bool PrismModulesPrinter::faultyBehaviour() const {
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index 16d562b..618833a 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -16,7 +16,7 @@ std::string westUpdate(const AgentName &a);
 namespace prism {
   class PrismModulesPrinter {
     public:
-      PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &boxes, const cells &balls, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals);
+      PrismModulesPrinter(std::ostream& os, const ModelType &modelType, const coordinates &maxBoundaries, const cells &lockedDoors, const cells &unlockedDoors, const cells &keys, const std::map<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> config, const float probIntended, const float faultyProbability, const bool anyLava, const bool anyGoals);
 
       std::ostream& print();
 
@@ -26,14 +26,14 @@ namespace prism {
       bool isGame() const;
     private:
       void printPortableObjectModule(const cell &object);
-      void printPortableObjectActions(const std::string &agentName, const std::string &identifier);
+      void printPortableObjectActions(const std::string &agentName, const std::string &identifier, const bool canBeDroped = false);
 
       void printDoorModule(const cell &object, const bool &opened);
       void printLockedDoorActions(const std::string &agentName, const std::string &identifier);
       void printUnlockedDoorActions(const std::string &agentName, const std::string &identifier);
 
       void printRobotModule(const AgentName &agentName, const coordinates &initialPosition);
-      void printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier);
+      void printPortableObjectActionsForRobot(const std::string &agentName, const std::string &identifier, const bool canBeDroped = false);
       void printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier);
       void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key);
       void printMovementActionsForRobot(const std::string &a);
@@ -92,8 +92,6 @@ namespace prism {
       ModelType const &modelType;
       coordinates const &maxBoundaries;
       AgentName agentName;
-      cells boxes;
-      cells balls;
       cells lockedDoors;
       cells unlockedDoors;
       cells keys;

From 82849e5f67ab162917bdd2fd7a9e6c996f18af0a Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Sat, 20 Jan 2024 13:12:28 +0100
Subject: [PATCH 21/21] changed NOFAULT constant

---
 util/PrismPrinter.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/util/PrismPrinter.h b/util/PrismPrinter.h
index 1f82cf4..c12b585 100644
--- a/util/PrismPrinter.h
+++ b/util/PrismPrinter.h
@@ -5,7 +5,7 @@
 
 #include "cell.h"
 
-#define NOFAULT 3
+#define NOFAULT 7
 #define LEFT 0
 #define RIGHT 1
 #define FORWARD 2