From d7a3914a9417702761b2d779944751387269a2c6 Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 19:13:43 +0100 Subject: [PATCH] print certain movement guards only when necessary --- util/PrismModulesPrinter.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 9912f79..04ec02d 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -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 &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector 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 &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector 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 {