diff --git a/util/Grid.cpp b/util/Grid.cpp
index 0b9fd23..fa17d6c 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -249,7 +249,7 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
   }
   size_t agentIndex  = 0;
 
-  printer.printInitStruct(os, agentNameAndPositionMap, keyNameAndPositionMap, lockedDoors, unlockedDoors);
+  printer.printInitStruct(os, agentNameAndPositionMap, keyNameAndPositionMap, lockedDoors, unlockedDoors, modelType);
 
 
   for(auto agentNameAndPosition = agentNameAndPositionMap.begin(); agentNameAndPosition != agentNameAndPositionMap.end(); ++agentNameAndPosition, agentIndex++) {
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index 4688b59..757683b 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -418,7 +418,7 @@ namespace prism {
     return os;
   }
 
-  std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors) {
+  std::ostream& PrismModulesPrinter::printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType) {
     os << "init\n";
     os << "\t";
     
@@ -453,7 +453,10 @@ namespace prism {
       os << " & (!Door" << unlocked.getColor() << "locked & !Door" << unlocked.getColor() << "open)";
     }
 
-    // os << " & ( !" << agentName << "_is_carrying_object" << ")";
+    if (modelType == ModelType::SMG) {
+      os << " & move=0"; 
+    }
+
 
     os << "\nendinit\n\n";
 
@@ -691,7 +694,8 @@ namespace prism {
         break;
     }
 
-    slipperyActions.insert(actionName);
+    slipperyActions.insert(actionName + "_left]");
+    slipperyActions.insert(actionName + "_right]");
 
     // override probability to 0 if corresp. direction is blocked
 
@@ -847,12 +851,14 @@ namespace prism {
     for(auto const& action : slipperyActions) {
       os << ", " << action;
     }
+
+    os << ", [" << agentName << "_done]";
     os << "\nendplayer\n";
     return os;
   }
 
   std::ostream& PrismModulesPrinter::printGlobalMoveVariable(std::ostream &os, const size_t &numberOfPlayer) {
-    os << "\nglobal move : [0.." << std::to_string(numberOfPlayer - 1) << "] init 0;\n\n";
+    os << "\nglobal move : [0.." << std::to_string(numberOfPlayer - 1) << "];\n\n";
     return os;
   }
 
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index dd57a8c..07f67bd 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -77,7 +77,7 @@ namespace prism {
       std::ostream& printActionsForKeys(std::ostream &os, const AgentName &agentName, const cells &keys);
       std::ostream& printBooleansForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles);
       std::ostream& printActionsForBackground(std::ostream &os, const AgentName &agentName, const std::map<Color, cells> &backgroundTiles);
-      std::ostream& printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors);
+      std::ostream& printInitStruct(std::ostream &os, const AgentNameAndPositionMap &agents, const KeyNameAndPositionMap &keys, const cells &lockedDoors, const cells &unlockedDoors, prism::ModelType modelType);
       std::ostream& printModule(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &boundaries, const coordinates& initialPosition, const cells &keys, const std::map<Color, cells> &backgroundTiles, const bool agentWithView, const std::vector<float> &probabilities = {});
       std::ostream& printMovementActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const bool agentWithView, const float &probability = 1.0);
       std::ostream& printDoneActions(std::ostream &os, const AgentName &agentName, const size_t &agentIndex);