|  |  | @ -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<std::string> &slipperyActions, const std::array<bool, 8>& neighborhood, SlipperyType orientation) { | 
			
		
	
		
			
				
					|  |  |  |    // constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 9;
 | 
			
		
	
		
			
				
					|  |  |  | 
 | 
			
		
	
		
			
				
					|  |  |  |    // std::array<std::string, ALL_POSS_DIRECTIONS> 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<std::tuple<std::string, std::string, std::string>, 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<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir; // { n, ne, e, se, s, sw, w, nw, CURRENT POS }
 | 
			
		
	
		
			
				
					|  |  |  |    // std::array<std::string, ALL_POSS_DIRECTIONS> 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";
 | 
			
		
	
		
			
				
					|  |  |  |    // // <DEBUG_AREA>
 | 
			
		
	
		
			
				
					|  |  |  |    // {
 | 
			
		
	
		
			
				
					|  |  |  |    //   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!");
 | 
			
		
	
		
			
				
					|  |  |  |    // }
 | 
			
		
	
		
			
				
					|  |  |  |    // // </DEBUG_AREA>
 | 
			
		
	
		
			
				
					|  |  |  | 
 | 
			
		
	
		
			
				
					|  |  |  |    // // 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<std::string> &slipperyActions, const std::array<bool, 8>& neighborhood, SlipperyType orientation) { | 
			
		
	
		
			
				
					|  |  |  |     //constexpr std::size_t PROB_PIECES = 9, ALL_POSS_DIRECTIONS = 8;
 | 
			
		
	
		
			
				
					|  |  |  | 
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::string, ALL_POSS_DIRECTIONS> 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<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir; // { n, ne, e, se, s, sw, w, nw }
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir_agent_north; // { n, ne, e, se, s, sw, w, nw }
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir_agent_east; // { n, ne, e, se, s, sw, w, nw }
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir_agent_south; // { n, ne, e, se, s, sw, w, nw }
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::size_t, ALL_POSS_DIRECTIONS> prob_piece_dir_agent_west; // { n, ne, e, se, s, sw, w, nw }
 | 
			
		
	
		
			
				
					|  |  |  | 
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::string, ALL_POSS_DIRECTIONS> prob_piece_dir_constants;
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::string, ALL_POSS_DIRECTIONS> prob_piece_dir_constants_agent_north;
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::string, ALL_POSS_DIRECTIONS> prob_piece_dir_constants_agent_east;
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::string, ALL_POSS_DIRECTIONS> prob_piece_dir_constants_agent_south;
 | 
			
		
	
		
			
				
					|  |  |  |     //std::array<std::string, ALL_POSS_DIRECTIONS> 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";
 | 
			
		
	
		
			
				
					|  |  |  |     //// <DEBUG_AREA>
 | 
			
		
	
		
			
				
					|  |  |  |     //{
 | 
			
		
	
		
			
				
					|  |  |  |     //  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!"));
 | 
			
		
	
		
			
				
					|  |  |  |     //}
 | 
			
		
	
		
			
				
					|  |  |  |     //// </DEBUG_AREA>
 | 
			
		
	
		
			
				
					|  |  |  | 
 | 
			
		
	
		
			
				
					|  |  |  |     //// 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<float> &probabilities, const std::set<std::string> &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; | 
			
		
	
		
			
				
					|  |  |  |   } | 
			
		
	
	
		
			
				
					|  |  | 
 |