From 2b7d5bc9a93a6c8137fbfc66d7dd3db8f1c95138 Mon Sep 17 00:00:00 2001 From: sp Date: Mon, 8 Jan 2024 14:06:24 +0100 Subject: [PATCH] removed dead code --- util/PrismModulesPrinter.cpp | 311 +---------------------------------- 1 file changed, 1 insertion(+), 310 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index da7bb8a..7d274c9 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -478,315 +478,6 @@ namespace prism { return os; } - std::ostream& PrismModulesPrinter::printSlipperyTurn(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation) { - // constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 9; - - // std::array positionTransition = { - // /* north */ "(y" + agentName + "'=y" + agentName + "-1)", - // /* north east */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "-1)", - // /* east */ "(x" + agentName + "'=x" + agentName + "+1)", - // /* east south */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "+1)", - // /* south */ "(y" + agentName + "'=y" + agentName + "+1)", - // /* south west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "+1)", - // /* west */ "(x" + agentName + "'=x" + agentName + "-1)", - // /* north west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "-1)", - // /* own position */ "(x" + agentName + "'=x" + agentName + ") & (y" + agentName + "'=y" + agentName + ")" - // }; - - // // view transition appdx in form (guard, update part) - // // IMPORTANT: No mod() usage for turn left due to bug in mod() function for decrement - - - // std::array, 3> viewTransition = { - // std::make_tuple(" & " + agentName + "SlipperyTurnRightAllowed ", " & (view" + agentName + "'=mod(view" + agentName + " + 1, 4))", "_right]"), - // std::make_tuple(" & " + agentName + "SlipperyTurnLeftAllowed & view" + agentName + ">0", " & (view" + agentName + "'=view" + agentName + " - 1)", "_left]"), - // std::make_tuple(" & " + agentName + "SlipperyTurnLeftAllowed & view" + agentName + "=0", " & (view" + agentName + "'=3)", "_left]") - // }; - - // // direction specifics - - // std::string actionName; - // std::string positionGuard; - // std::size_t remainPosIndex = 8; - // std::array prob_piece_dir; // { n, ne, e, se, s, sw, w, nw, CURRENT POS } - // std::array prob_piece_dir_constants; - - // switch (orientation) - // { - // case SlipperyType::North: - // actionName = "\t[" + agentName + "turn_at_slip_north"; - // positionGuard = "\t" + agentName + "IsOnSlipperyNorth"; - // prob_piece_dir = { 0, 0, 0, 0, 1, 0, 0, 0, 0 /* <- R */ }; - // prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_turn_displacement" /* <- R */, "prop_zero", "prop_zero", "prop_zero","prop_zero" }; - // break; - - // case SlipperyType::South: - // actionName = "\t[" + agentName + "turn_at_slip_south"; - // positionGuard = "\t" + agentName + "IsOnSlipperySouth"; - // prob_piece_dir = { 1, 0, 0, 0, 0, 0, 0, 0, 0 /* <- R */ }; - // prob_piece_dir_constants = { "prop_turn_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" }; - // break; - - // case SlipperyType::East: - // actionName = "\t[" + agentName + "turn_at_slip_east"; - // positionGuard = "\t" + agentName + "IsOnSlipperyEast"; - // prob_piece_dir = { 0, 0, 0, 0, 0, 0, 1, 0, 0 /* <- R */ }; - // prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_turn_displacement", "prop_zero", "prop_zero" }; - // break; - - // case SlipperyType::West: - // actionName = "\t[" + agentName + "turn_at_slip_west"; - // positionGuard = "\t" + agentName + "IsOnSlipperyWest"; - // prob_piece_dir = { 0, 0, 1, 0, 0, 0, 0, 0, 0 /* <- R */ }; - // prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_turn_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" }; - // break; - // } - - // slipperyActions.insert(actionName + "_left]"); - // slipperyActions.insert(actionName + "_right]"); - - // // override probability to 0 if corresp. direction is blocked - - // for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS - 1; i++) { - // if (!neighborhood.at(i)) - // prob_piece_dir.at(i) = 0; - // } - - // // determine residual probability (R) by replacing 0 with (1 - overall sum) - - // prob_piece_dir.at(remainPosIndex) = PROB_PIECES - std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0); - // prob_piece_dir_constants.at(remainPosIndex) = "prop_turn_intended"; - // // - // { - // assert(prob_piece_dir.at(remainPosIndex) <= 9 && prob_piece_dir.at(remainPosIndex) >= 6 && "Value not in Range!"); - // assert(std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0) == PROB_PIECES && "Does not sum up to 1!"); - // } - // // - - // // generic output (for every view transition) - // for (std::size_t v = 0; v < viewTransition.size(); v++) { - // os << actionName << std::get<2>(viewTransition.at(v)) << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << std::get<0>(viewTransition.at(v)); - // for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - // if (i == remainPosIndex) { - // os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants.at(i) << " : " << positionTransition.at(i) << std::get<1>(viewTransition.at(v)) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - // } else { - // os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - // } - // } - // } - - return os; - } - - std::ostream& PrismModulesPrinter::printSlipperyMove(std::ostream &os, const AgentName &agentName, const size_t &agentIndex, const coordinates &c, std::set &slipperyActions, const std::array& neighborhood, SlipperyType orientation) { - //constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 8; - - //std::array positionTransition = { - // /* north */ "(y" + agentName + "'=y" + agentName + "-1)", - // /* north east */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "-1)", - // /* east */ "(x" + agentName + "'=x" + agentName + "+1)", - // /* east south */ "(x" + agentName + "'=x" + agentName + "+1) & (y" + agentName + "'=y" + agentName + "+1)", - // /* south */ "(y" + agentName + "'=y" + agentName + "+1)", - // /* south west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "+1)", - // /* west */ "(x" + agentName + "'=x" + agentName + "-1)", - // /* north west */ "(x" + agentName + "'=x" + agentName + "-1) & (y" + agentName + "'=y" + agentName + "-1)" - //}; - - //// direction specifics - - //std::size_t straightPosIndex, straightPosIndex_east, straightPosIndex_south, straightPosIndex_west, straightPosIndex_north; - //std::string actionName, specialTransition; // if straight ahead is blocked - //std::string positionGuard; - //std::array prob_piece_dir; // { n, ne, e, se, s, sw, w, nw } - //std::array prob_piece_dir_agent_north; // { n, ne, e, se, s, sw, w, nw } - //std::array prob_piece_dir_agent_east; // { n, ne, e, se, s, sw, w, nw } - //std::array prob_piece_dir_agent_south; // { n, ne, e, se, s, sw, w, nw } - //std::array prob_piece_dir_agent_west; // { n, ne, e, se, s, sw, w, nw } - - //std::array prob_piece_dir_constants; - //std::array prob_piece_dir_constants_agent_north; - //std::array prob_piece_dir_constants_agent_east; - //std::array prob_piece_dir_constants_agent_south; - //std::array prob_piece_dir_constants_agent_west; - - //switch (orientation) - //{ - // case SlipperyType::North: - // actionName = "\t[" + agentName + "move_on_slip_north]"; - // positionGuard = "\t" + agentName + "IsOnSlipperyNorth"; - // prob_piece_dir = { 0, 0, 1, 2, 0 /* <- R */, 2, 1, 0 }; - - // prob_piece_dir_agent_south = { 0 , 0, 0, 1, 0 /*s <- R */, 1, 0, 0}; - // prob_piece_dir_agent_east = { 0, 0, 0 /*e <- R */, 2, 0, 0, 0, 0 }; - // prob_piece_dir_agent_north = { 0 /*n <- R */, 0, 0, 0, 2 , 0, 0, 0 }; - // prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 2, 0 /* <- R */, 0 }; - - // prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero" }; - - // prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_zero", "prop_zero" }; - // prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_displacement", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - // prob_piece_dir_constants_agent_south = { "prop_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - // prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement", "prop_zero", "prop_zero" } ; - - - // straightPosIndex = 4; - // straightPosIndex_east = 2; - // straightPosIndex_south = 4; - // straightPosIndex_west = 6; - // straightPosIndex_north = 0; - - // specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)"); - // break; - - // case SlipperyType::South: - // actionName = "\t[" + agentName + "move_on_slip_south]"; - // positionGuard = "\t" + agentName + "IsOnSlipperySouth"; - - // prob_piece_dir = { 0 /* <- R */, 2, 1, 0, 0, 0, 1, 2 }; - // // { n, ne, e, se, s, sw, w, nw } - // prob_piece_dir_agent_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1}; - // prob_piece_dir_agent_east = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 }; - // prob_piece_dir_agent_south = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 }; - // prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; - - // prob_piece_dir_constants = { "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement" }; - - // prob_piece_dir_constants_agent_north = { "prop_zero", "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_displacement * 1/2" }; - // prob_piece_dir_constants_agent_east = { "prop_zero", "prop_displacement", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - // prob_piece_dir_constants_agent_south = { "prop_displacement", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - // prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_displacement" } ; - - - // straightPosIndex = 0; // always north - // straightPosIndex_east = 2; - // straightPosIndex_south = 4; - // straightPosIndex_west = 6; - // straightPosIndex_north = 0; - // specialTransition = "(y" + agentName + "'=y" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)"); - // break; - - // case SlipperyType::East: - // actionName = "\t[" + agentName + "move_on_slip_east]"; - // positionGuard = "\t" + agentName + "IsOnSlipperyEast"; - // // { n, ne, e, se, s, sw, w, nw } - - // prob_piece_dir = { 1, 0, 0, 0, 1, 2, 0 /* <- R */, 2 }; - // // TODO - // prob_piece_dir_agent_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1}; - // prob_piece_dir_agent_east = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 }; - // prob_piece_dir_agent_south = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 }; - // prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; - - // prob_piece_dir_constants = { "prop_displacement * 1/2", "prop_zero", "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement" }; - - // prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2" }; - // prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_displacement", "prop_zero" }; - // prob_piece_dir_constants_agent_south = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero" } ; - // prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_displacement * 1/2", "prop_zero", "prop_displacement * 1/2" } ; - - - // straightPosIndex = 6; - // straightPosIndex_east = 2; - // straightPosIndex_south = 4; - // straightPosIndex_west = 6; - // straightPosIndex_north = 0; - - // specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "-1)"); - // break; - - // case SlipperyType::West: - // actionName = "\t[" + agentName + "move_on_slip_west]"; - // positionGuard = "\t" + agentName + "IsOnSlipperyWest"; - // prob_piece_dir = { 1, 2, 0 /* <- R */, 2, 1, 0, 0, 0 }; - // // TODO - // // { n, ne, e, se, s, sw, w, nw } - - // prob_piece_dir_agent_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1}; - // prob_piece_dir_agent_east = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 }; - // prob_piece_dir_agent_south = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 }; - // prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; - - // prob_piece_dir_constants = {"prop_displacement * 1/2", "prop_displacement", "prop_zero" /* <- R */, "prop_displacement", "prop_displacement * 1/2", "prop_zero","prop_zero", "prop_zero" }; - - // prob_piece_dir_constants_agent_north = { "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - // prob_piece_dir_constants_agent_east = { "prop_zero", "prop_displacement * 1/2", "prop_zero", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; - // prob_piece_dir_constants_agent_south = { "prop_zero", "prop_zero", "prop_displacement * 1/2", "prop_displacement * 1/2", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - // prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_displacement", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; - - - // straightPosIndex = 2; - // straightPosIndex_east = 2; - // straightPosIndex_south = 4; - // straightPosIndex_west = 6; - // straightPosIndex_north = 0; - // specialTransition = "(x" + agentName + "'=x" + agentName + (!neighborhood.at(straightPosIndex) ? ")" : "+1)"); - // break; - //} - - //slipperyActions.insert(actionName); - - //// override probability to 0 if corresp. direction is blocked - - //for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - // if (!neighborhood.at(i)) - // prob_piece_dir.at(i) = 0; - //} - - //// determine residual probability (R) by replacing 0 with (1 - overall sum) - //prob_piece_dir.at(straightPosIndex) = PROB_PIECES - std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0); - //prob_piece_dir_constants.at(straightPosIndex) = "prop_intended"; - //prob_piece_dir_constants_agent_east.at(straightPosIndex_east) = "prop_intended"; - //prob_piece_dir_constants_agent_south.at(straightPosIndex_south) = "prop_intended"; - //prob_piece_dir_constants_agent_west.at(straightPosIndex_west) = "prop_intended"; - //prob_piece_dir_constants_agent_north.at(straightPosIndex_north) = "prop_intended"; - //// - //{ - // assert(prob_piece_dir.at(straightPosIndex) <= 9 && prob_piece_dir.at(straightPosIndex) >= 3 && "Value not in Range!"); - // assert(std::accumulate(prob_piece_dir.begin(), prob_piece_dir.end(), 0) == PROB_PIECES && "Does not sum up to 1!"); - // assert(orientation != SlipperyType::North || (prob_piece_dir.at(7) == 0 && prob_piece_dir.at(0) == 0 && prob_piece_dir.at(1) == 0 && "Slippery up should be impossible!")); - // assert(orientation != SlipperyType::South || (prob_piece_dir.at(3) == 0 && prob_piece_dir.at(4) == 0 && prob_piece_dir.at(5) == 0 && "Slippery down should be impossible!")); - // assert(orientation != SlipperyType::East || (prob_piece_dir.at(1) == 0 && prob_piece_dir.at(2) == 0 && prob_piece_dir.at(3) == 0 && "Slippery right should be impossible!")); - // assert(orientation != SlipperyType::West || (prob_piece_dir.at(5) == 0 && prob_piece_dir.at(6) == 0 && prob_piece_dir.at(7) == 0 && "Slippery left should be impossible!")); - //} - //// - - //// special case: straight forward is blocked (then remain in same position) - - //positionTransition.at(straightPosIndex) = specialTransition; - - //// generic output (for every view and every possible view direction) - //size_t current_dir = 0; // East - //os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - - //for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - // os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_east.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - //} - - //current_dir = 1; // South - //os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - - //for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - // os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_south.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - //} - - //current_dir = 2; // West - - //os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - //for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - // os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_west.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - //} - - - //current_dir = 3; // North - - //os << actionName << moveGuard(agentIndex) << " x" << agentName << "=" << c.second << " & y" << agentName << "=" << c.first << " & " << agentName << "SlipperyMoveForwardAllowed " << "& " << "view" << agentName << "=" << current_dir; - //for (std::size_t i = 0; i < ALL_POSS_DIRECTIONS; i++) { - // os << (i == 0 ? " -> " : " + ") << prob_piece_dir_constants_agent_north.at(i) << " : " << positionTransition.at(i) << moveUpdate(agentIndex) << (i == ALL_POSS_DIRECTIONS - 1 ? ";\n" : "\n"); - //} - - return os; - } - std::ostream& PrismModulesPrinter::printPlayerStruct(std::ostream &os, const AgentName &agentName, const bool agentWithView, const std::vector &probabilities, const std::set &slipperyActions) { os << "player " << agentName << "\n\t"; bool first = true; @@ -926,7 +617,7 @@ namespace prism { if(first) first = false; else updatesString += " + "; updatesString += updateToString(update); - if(faultyBehaviour()) updatesString += "&" + faultyBehaviourUpdate(a, actionId); + //if(faultyBehaviour()) updatesString += "&" + faultyBehaviourUpdate(a, actionId); } return updatesString; }