From 34a399972de15b5985be1b05982e75ed9f4531a9 Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 19:13:43 +0100 Subject: [PATCH 1/4] 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 4d63f98..b8b95c1 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++) { @@ -259,7 +259,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 { -- 2.20.1 From 92d7d11daa74d5681a86dfb4c3f88464764e790c Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 19:13:49 +0100 Subject: [PATCH 2/4] switched most tabs to two whitespaces in output --- util/PrismModulesPrinter.cpp | 76 ++++++++++++++++++------------------ util/PrismModulesPrinter.h | 5 ++- 2 files changed, 42 insertions(+), 39 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index b8b95c1..f360cbc 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -104,9 +104,9 @@ namespace prism { void PrismModulesPrinter::printPortableObjectModule(const cell &object) { std::string identifier = capitalize(object.getColor()) + object.getType(); os << "\nmodule " << identifier << std::endl; - os << "\tx" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n"; - os << "\ty" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n"; - os << "\t" << identifier << "PickedUp : bool;\n"; + os << " x" << identifier << " : [-1.." << maxBoundaries.second << "] init " << object.column << ";\n"; + os << " y" << identifier << " : [-1.." << maxBoundaries.first << "] init " << object.row << ";\n"; + os << " " << identifier << "PickedUp : bool;\n"; os << "\n"; for(const auto [name, position] : agentNameAndPositionMap) { @@ -118,25 +118,25 @@ 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 << "\t" << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n"; + os << " " << actionName << " true -> (x" << identifier << "'=-1) & (y" << identifier << "'=-1) & (" << identifier << "PickedUp'=true);\n"; actionName = "[" + agentName + "_drop_" + identifier + "_north]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; + os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "-1) & (" << identifier << "PickedUp'=false);\n"; actionName = "[" + agentName + "_drop_" + identifier + "_west]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << "-1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; actionName = "[" + agentName + "_drop_" + identifier + "_south]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t" << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; + os << " " << actionName << " " << " true -> (x" << identifier << "'=x" << agentName << ") & (y" << identifier << "'=y" << agentName << "+1) & (" << identifier << "PickedUp'=false);\n"; actionName = "[" + agentName + "_drop_" + identifier + "_east]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t" << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; + os << " " << actionName << " " << " ttrue -> (x" << identifier << "'=x" << agentName << "+1) & (y" << identifier << "'=y" << agentName << ") & (" << identifier << "PickedUp'=false);\n"; } void PrismModulesPrinter::printDoorModule(const cell &door, const bool &opened) { std::string identifier = capitalize(door.getColor()) + door.getType(); os << "\nmodule " << identifier << std::endl; - os << "\t" << identifier << "Open : bool init false;\n"; + os << " " << identifier << "Open : bool init false;\n"; os << "\n"; if(opened) { @@ -154,26 +154,26 @@ namespace prism { void PrismModulesPrinter::printLockedDoorActions(const std::string &agentName, const std::string &identifier) { std::string actionName = "[" + agentName + "_unlock_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t" << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; + os << " " << actionName << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; actionName = "[" + agentName + "_close_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t" << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; + os << " " << actionName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; } void PrismModulesPrinter::printUnlockedDoorActions(const std::string &agentName, const std::string &identifier) { std::string actionName = "[" + agentName + "_open_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; + os << " !" << identifier << "Open -> (" << identifier << "Open'=true);\n"; actionName = "[" + agentName + "_close_" + identifier + "]"; agentNameActionMap.at(agentName).insert({NOFAULT, actionName}); - os << "\t" << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; + os << " " << agentName << " " << identifier << "Open -> (" << identifier << "Open'=false);\n"; } void PrismModulesPrinter::printRobotModule(const AgentName &agentName, const coordinates &initialPosition) { os << "\nmodule " << agentName << std::endl; - os << "\tcol" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n"; - os << "\trow" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; - os << "\tview" << agentName << " : [0..3] init 1;\n"; + os << " col" << agentName << " : [1.." << maxBoundaries.second << "] init " << initialPosition.second << ";\n"; + os << " row" << agentName << " : [1.." << maxBoundaries.first << "] init " << initialPosition.first << ";\n"; + os << " view" << agentName << " : [0..3] init 1;\n"; printTurnActionsForRobot(agentName); printMovementActionsForRobot(agentName); @@ -192,19 +192,19 @@ namespace prism { for(const auto &key : keys) { std::string identifier = capitalize(key.getColor()) + key.getType(); - os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + os << " " << agentName << "Carrying" << identifier << " : bool init false;\n"; printPortableObjectActionsForRobot(agentName, identifier); } for(const auto &ball : balls) { std::string identifier = capitalize(ball.getColor()) + ball.getType(); - os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + os << " " << agentName << "Carrying" << identifier << " : bool init false;\n"; printPortableObjectActionsForRobot(agentName, identifier); } for(const auto &box : boxes) { std::string identifier = capitalize(box.getColor()) + box.getType(); - os << "\t" << agentName << "Carrying" << identifier << " : bool init false;\n"; + os << " " << agentName << "Carrying" << identifier << " : bool init false;\n"; printPortableObjectActionsForRobot(agentName, identifier); } @@ -214,23 +214,23 @@ namespace prism { } void PrismModulesPrinter::printPortableObjectActionsForRobot(const std::string &a, const std::string &i) { - actionStream << "\t[" << a << "_pickup_" << i << "] " << " !" << a << "IsCarrying & " << a << "CannotMove" << i << " -> (" << a << "Carrying" << i << "'=true);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_north]\t" << a << "Carrying" << i << " & view" << a << "=3 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveNorthWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_west] \t" << a << "Carrying" << i << " & view" << a << "=2 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveWestWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_south]\t" << a << "Carrying" << i << " & view" << a << "=1 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveSouthWall -> (" << a << "Carrying" << i << "'=false);\n"; - actionStream << "\t[" << a << "_drop_" << i << "_east] \t" << a << "Carrying" << i << " & view" << a << "=0 & !" << a << "CannotMoveConditionally & !" << a << "CannotMoveEastWall -> (" << a << "Carrying" << i << "'=false);\n"; + 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::printUnlockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier) { - actionStream << "\t[" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n"; - actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n"; + actionStream << " [" << agentName << "_open_" << identifier << "] " << agentName << "CannotMove" << identifier << " -> true;\n"; + actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " -> true;\n"; actionStream << "\n"; } void PrismModulesPrinter::printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key) { - actionStream << "\t[" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; - actionStream << "\t[" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << " [" << agentName << "_unlock_" << identifier << "] " << agentName << "CannotMove" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; + actionStream << " [" << agentName << "_close_" << identifier << "] " << agentName << "IsNextTo" << identifier << " & " << agentName << "Carrying" << key << " -> true;\n"; actionStream << "\n"; } @@ -248,7 +248,7 @@ namespace prism { if(faultyBehaviour()) { std::string actionName = "[" + a + "_stuck]"; agentNameActionMap.at(a).insert({FORWARD, actionName}); - actionStream << "\t" << actionName << " " << "previousAction" << a << "=" << std::to_string(FORWARD); + actionStream << " " << actionName << " " << "previousAction" << a << "=" << std::to_string(FORWARD); actionStream << " & ((view" << a << "=0 & " << a << "CannotMoveEastWall) |"; actionStream << " (view" << a << "=1 & " << a << "CannotMoveSouthWall) |"; actionStream << " (view" << a << "=2 & " << a << "CannotMoveWestWall) |"; @@ -276,7 +276,7 @@ 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 "\t" + actionName + " " + cond + " -> "; + return " " + actionName + " " + cond + " -> "; } std::string PrismModulesPrinter::printTurnUpdate(const AgentName &a, const update &u, const ActionId &actionId) const { @@ -449,7 +449,7 @@ namespace prism { std::string PrismModulesPrinter::printSlipperyMovementGuard(const AgentName &a, const std::string &direction, const ViewDirection &viewDirection, const std::vector &guards) { std::string actionName = "[" + a + "_move_" + viewDirectionToString.at(viewDirection) + "]"; agentNameActionMap.at(a).insert({FORWARD, actionName}); - return "\t" + actionName + " " + viewVariable(a, viewDirection) + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> "; + return " " + actionName + " " + viewVariable(a, viewDirection) + " & " + a + "IsOnSlippery" + direction + " & " + buildConjunction(a, guards) + " -> "; } std::string PrismModulesPrinter::printSlipperyMovementUpdate(const AgentName &a, const std::string &direction, const updates &u) const { @@ -459,7 +459,7 @@ namespace prism { std::string PrismModulesPrinter::printSlipperyTurnGuard(const AgentName &a, const std::string &direction, const ActionId &actionId, const std::vector &guards, const std::string &cond) { std::string actionName = "[" + a + "_turn_" + direction + "]"; agentNameActionMap.at(a).insert({actionId, actionName}); - return "\t" + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> "; + return " " + actionName + " " + buildConjunction(a, guards) + " & " + cond + " -> "; } std::string PrismModulesPrinter::printSlipperyTurnUpdate(const AgentName &a, const updates &u) { @@ -468,21 +468,21 @@ namespace prism { void PrismModulesPrinter::printFaultyMovementModule(const AgentName &a) { os << "\nmodule " << a << "FaultyBehaviour" << std::endl; - os << "\tpreviousAction" << a << " : [-1..2] init -1;\n"; + os << " previousAction" << a << " : [-1..2] init -1;\n"; for(const auto [actionId, actionName] : agentNameActionMap.at(a)) { - os << "\t" << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n"; + os << " " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n"; } os << "endmodule\n\n"; } void PrismModulesPrinter::printMoveModule() { os << "\nmodule " << "Arbiter" << std::endl; - os << "\tclock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n"; + os << " clock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n"; for(const auto [agentName, actions] : agentNameActionMap) { for(const auto [actionId, actionName] : actions) { - os << "\t" << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n"; + os << " " << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n"; } } os << "endmodule\n\n"; @@ -499,7 +499,7 @@ namespace prism { } void PrismModulesPrinter::printDoneActions(const AgentName &agentName) { - os << "\t[" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n"; + os << " [" << agentName << "_done]" << moveGuard(agentName) << agentName << "IsInGoal | " << agentName << "IsInLava -> (" << agentName << "Done'=true);\n"; } void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) { @@ -625,7 +625,7 @@ namespace prism { } std::string PrismModulesPrinter::viewVariable(const AgentName &agentName, const size_t &agentDirection) const { - return "view" + agentName + "=" + std::to_string(agentDirection) + " & "; + return "view" + agentName + "=" + std::to_string(agentDirection); } bool PrismModulesPrinter::anyPortableObject() const { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 368b667..c0d192a 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 &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector config, const float probIntended, const float faultyProbability); + 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); std::ostream& print(); @@ -98,6 +98,9 @@ namespace prism { cells keys; std::map slipperyTiles; + const bool anyLava; + const bool anyGoals; + AgentNameAndPositionMap agentNameAndPositionMap; std::map agentIndexMap; size_t numberOfPlayer; -- 2.20.1 From 76d4295f731abf5b1aae33e1f4c5902ecb9cebd9 Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 19:15:37 +0100 Subject: [PATCH 3/4] removed printing of unnecessary formulas --- util/PrismFormulaPrinter.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp index a873b38..1317fe3 100644 --- a/util/PrismFormulaPrinter.cpp +++ b/util/PrismFormulaPrinter.cpp @@ -79,8 +79,8 @@ namespace prism { } else { os << buildFormula(agentName + "IsOnSlippery", "false"); } - printIsOnFormula(agentName, "Lava", lava); - printIsOnFormula(agentName, "Goal", goals); + 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(); @@ -115,8 +115,6 @@ namespace prism { if(conditionalMovementRestrictions.size() > 0) { os << buildFormula(agentName + "CannotMoveConditionally", vectorToDisjunction(conditionalMovementRestrictions)); os << buildFormula(agentName + "IsCarrying", vectorToDisjunction(portableObjects)); - } else { - os << buildFormula(agentName + "CannotMoveConditionally", "false"); } } -- 2.20.1 From 46b4d5f9f397d3168bb02f3e280e7d13f5edb5c5 Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 10 Jan 2024 19:17:08 +0100 Subject: [PATCH 4/4] adapted call to PrismModulesPrinter --- util/Grid.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/util/Grid.cpp b/util/Grid.cpp index 6f057cc..f9ebdac 100644 --- a/util/Grid.cpp +++ b/util/Grid.cpp @@ -159,7 +159,7 @@ void Grid::printToPrism(std::ostream& os, std::vector& configurat std::string agentName = agentNames.at(0); prism::PrismFormulaPrinter formulas(os, wallRestrictions, walls, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, lava, goals); - prism::PrismModulesPrinter modules(os, modelType, maxBoundaries, boxes, balls, lockedDoors, unlockedDoors, keys, slipperyTiles, agentNameAndPositionMap, configuration, probIntended, faultyProbability); + 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) { -- 2.20.1