| 
						
						
							
								
							
						
						
					 | 
				
				 | 
				
					@ -16,8 +16,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) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    : 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) { | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					  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) { | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					      numberOfPlayer = agentNameAndPositionMap.size(); | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					      size_t index = 0; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					      for(auto begin = agentNameAndPositionMap.begin(); begin != agentNameAndPositionMap.end(); begin++, index++) { | 
				
			
			
		
	
	
		
			
				
					| 
						
							
								
							
						
						
							
								
							
						
						
					 | 
				
				 | 
				
					@ -255,7 +255,14 @@ namespace prism { | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					  std::string PrismModulesPrinter::printMovementGuard(const AgentName &a, const std::string &direction, const size_t &viewDirection) { | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    std::string actionName = "[" + a + "_move_" + direction + "]"; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    agentNameActionMap.at(a).insert({FORWARD, actionName}); | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    return "\t" + actionName + " " + viewVariable(a, viewDirection) + " !" + a + "IsOnSlippery & !" + a + "IsOnLava & !" + a + "IsOnGoal & !" + a + "CannotMove" + direction + "Wall &!" + a + "CannotMoveConditionally -> "; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    std::string guard = "  " + actionName + " " + viewVariable(a, viewDirection); | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    if(slipperyBehaviour()) guard += " & !" + a + "IsOnSlippery"; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    if(anyLava)             guard += " & !" + a + "IsOnLava"; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    if(anyGoals)            guard += " & !" + a + "IsOnGoal"; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    guard += " & !" + a + "CannotMove" + direction + "Wall"; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    if(anyPortableObject()) guard += " & !" + a + "CannotMoveConditionally"; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    guard += " -> "; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    return guard; | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					  } | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					  std::string PrismModulesPrinter::printMovementUpdate(const AgentName &a, const update &u) const { | 
				
			
			
		
	
	
		
			
				
					| 
						
							
								
							
						
						
						
					 | 
				
				 | 
				
					
  |