sp
/
Minigrid2PRISM
1
0
Fork 0
Code Issues 5 Pull Requests 1 Projects Releases Wiki Activity
Browse Source

probability changes

pull/3/head
Thomas Knoll 11 months ago
parent
55c14a3c23
commit
e0c1807c71
2 changed files with 38 additions and 25 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 7
      util/Grid.cpp
  2. 54
      util/PrismModulesPrinter.cpp

7
util/Grid.cpp
View File

@ -168,6 +168,10 @@ void Grid::applyOverwrites(std::string& str, std::vector<Configuration>& configu
} }
else if (config.type_ == ConfigType::Constant) { else if (config.type_ == ConfigType::Constant) {
start_pos = str.find(config.identifier_); start_pos = str.find(config.identifier_);
if (start_pos == std::string::npos) {
std::cout << "Couldn't find overwrite:" << config.expression_ << std::endl;
}
} }
size_t end_pos = str.find(';', start_pos) + 1; size_t end_pos = str.find(';', start_pos) + 1;
@ -245,8 +249,9 @@ void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configurat
} }
std::vector<std::string> constants {"const double prop_zero = 0/9;", std::vector<std::string> constants {"const double prop_zero = 0/9;",
"const double prop_next_neighbour = 1/9;", "const double prop_next_neighbour = 1/9;",
"const double prop_slippery_move_forward = 3/9;",
"const double prop_slippery_move_forward = 7/9;",
"const double prop_slippery_turn = 6/9;", "const double prop_slippery_turn = 6/9;",
"const double prop_next_neighbour_turn = 1/9;",
"const double prop_direct_neighbour = 2/9;", "const double prop_direct_neighbour = 2/9;",
"const double total_prop = 9;"}; "const double total_prop = 9;"};
printer.printConstants(os, constants); printer.printConstants(os, constants);

54
util/PrismModulesPrinter.cpp
View File

@ -483,7 +483,7 @@ namespace prism {
if(enforceOneWays) { if(enforceOneWays) {
os << " & ( !AgentCannotTurn ) "; os << " & ( !AgentCannotTurn ) ";
} else { } else {
os << " & ( !AgentIsOnSlippery ) ";
// os << " & ( !AgentIsOnSlippery ) ";
} }
for (auto const& key : keys) { for (auto const& key : keys) {
@ -730,28 +730,28 @@ namespace prism {
actionName = "\t[" + agentName + "turn_at_slip_north"; actionName = "\t[" + agentName + "turn_at_slip_north";
positionGuard = "\t" + agentName + "IsOnSlipperyNorth"; positionGuard = "\t" + agentName + "IsOnSlipperyNorth";
prob_piece_dir = { 0, 0, 0, 1, 1, 1, 0, 0, 0 /* <- R */ }; prob_piece_dir = { 0, 0, 0, 1, 1, 1, 0, 0, 0 /* <- R */ };
prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_next_neighbour" /* <- R */, "prop_next_neighbour", "prop_zero", "prop_zero","prop_zero" };
prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour_turn", "prop_next_neighbour_turn" /* <- R */, "prop_next_neighbour_turn", "prop_zero", "prop_zero","prop_zero" };
break; break;
case SlipperyType::South: case SlipperyType::South:
actionName = "\t[" + agentName + "turn_at_slip_south"; actionName = "\t[" + agentName + "turn_at_slip_south";
positionGuard = "\t" + agentName + "IsOnSlipperySouth"; positionGuard = "\t" + agentName + "IsOnSlipperySouth";
prob_piece_dir = { 1, 1, 0, 0, 0, 0, 0, 1, 0 /* <- R */ }; prob_piece_dir = { 1, 1, 0, 0, 0, 0, 0, 1, 0 /* <- R */ };
prob_piece_dir_constants = { "prop_next_neighbour", "prop_next_neighbour", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_zero" };
prob_piece_dir_constants = { "prop_next_neighbour_turn", "prop_next_neighbour_turn", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour_turn", "prop_zero" };
break; break;
case SlipperyType::East: case SlipperyType::East:
actionName = "\t[" + agentName + "turn_at_slip_east"; actionName = "\t[" + agentName + "turn_at_slip_east";
positionGuard = "\t" + agentName + "IsOnSlipperyEast"; positionGuard = "\t" + agentName + "IsOnSlipperyEast";
prob_piece_dir = { 0, 0, 0, 0, 0, 1, 1, 1, 0 /* <- R */ }; prob_piece_dir = { 0, 0, 0, 0, 0, 1, 1, 1, 0 /* <- R */ };
prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_next_neighbour", "prop_next_neighbour", "prop_zero" };
prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour_turn", "prop_next_neighbour_turn", "prop_next_neighbour_turn", "prop_zero" };
break; break;
case SlipperyType::West: case SlipperyType::West:
actionName = "\t[" + agentName + "turn_at_slip_west"; actionName = "\t[" + agentName + "turn_at_slip_west";
positionGuard = "\t" + agentName + "IsOnSlipperyWest"; positionGuard = "\t" + agentName + "IsOnSlipperyWest";
prob_piece_dir = { 0, 1, 1, 1, 0, 0, 0, 0, 0 /* <- R */ }; prob_piece_dir = { 0, 1, 1, 1, 0, 0, 0, 0, 0 /* <- R */ };
prob_piece_dir_constants = { "prop_zero", "prop_next_neighbour", "prop_next_neighbour", "prop_next_neighbour", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" };
prob_piece_dir_constants = { "prop_zero", "prop_next_neighbour_turn", "prop_next_neighbour_turn", "prop_next_neighbour_turn", "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" };
break; break;
} }
@ -833,11 +833,12 @@ namespace prism {
prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_next_neighbour", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_direct_neighbour", "prop_next_neighbour", "prop_zero" }; prob_piece_dir_constants = { "prop_zero", "prop_zero", "prop_next_neighbour", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_direct_neighbour", "prop_next_neighbour", "prop_zero" };
prob_piece_dir_constants_agent_south = { "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_zero" /* <- R */, "prop_next_neighbour", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_zero" /* <- R */, "prop_next_neighbour", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_direct_neighbour" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ;
prob_piece_dir_constants_agent_south = { "prop_direct_neighbour", "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_direct_neighbour", "prop_zero", "prop_zero" } ; prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_direct_neighbour", "prop_zero", "prop_zero" } ;
straightPosIndex = 4; straightPosIndex = 4;
straightPosIndex_east = 2; straightPosIndex_east = 2;
straightPosIndex_south = 4; straightPosIndex_south = 4;
@ -850,6 +851,7 @@ namespace prism {
case SlipperyType::South: case SlipperyType::South:
actionName = "\t[" + agentName + "move_on_slip_south]"; actionName = "\t[" + agentName + "move_on_slip_south]";
positionGuard = "\t" + agentName + "IsOnSlipperySouth"; positionGuard = "\t" + agentName + "IsOnSlipperySouth";
prob_piece_dir = { 0 /* <- R */, 2, 1, 0, 0, 0, 1, 2 }; prob_piece_dir = { 0 /* <- R */, 2, 1, 0, 0, 0, 1, 2 };
// { n, ne, e, se, s, sw, w, nw } // { 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_north = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1};
@ -858,11 +860,13 @@ namespace prism {
prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 }; prob_piece_dir_agent_west = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 };
prob_piece_dir_constants = { "prop_zero" /* <- R */, "prop_direct_neighbour", "prop_next_neighbour", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_direct_neighbour" }; prob_piece_dir_constants = { "prop_zero" /* <- R */, "prop_direct_neighbour", "prop_next_neighbour", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_direct_neighbour" };
prob_piece_dir_constants_agent_north = { "prop_zero", "prop_next_neighbour", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_next_neighbour" }; prob_piece_dir_constants_agent_north = { "prop_zero", "prop_next_neighbour", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_next_neighbour" };
prob_piece_dir_constants_agent_east = { "prop_zero", "prop_direct_neighbour", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" }; prob_piece_dir_constants_agent_east = { "prop_zero", "prop_direct_neighbour", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_south = { "prop_direct_neighbour", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ; prob_piece_dir_constants_agent_south = { "prop_direct_neighbour", "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_direct_neighbour" } ; prob_piece_dir_constants_agent_west ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_direct_neighbour" } ;
straightPosIndex = 0; // always north straightPosIndex = 0; // always north
straightPosIndex_east = 2; straightPosIndex_east = 2;
straightPosIndex_south = 4; straightPosIndex_south = 4;
@ -874,18 +878,21 @@ namespace prism {
case SlipperyType::East: case SlipperyType::East:
actionName = "\t[" + agentName + "move_on_slip_east]"; actionName = "\t[" + agentName + "move_on_slip_east]";
positionGuard = "\t" + agentName + "IsOnSlipperyEast"; positionGuard = "\t" + agentName + "IsOnSlipperyEast";
// { n, ne, e, se, s, sw, w, nw }
prob_piece_dir = { 1, 0, 0, 0, 1, 2, 0 /* <- R */, 2 }; prob_piece_dir = { 1, 0, 0, 0, 1, 2, 0 /* <- R */, 2 };
// TODO // TODO
// prob_piece_dir_zero = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1};
// prob_piece_dir_ninety = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 };
// prob_piece_dir_oneeighty = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 };
// prob_piece_dir_twoseventy = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 };
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_next_neighbour", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_direct_neighbour" }; prob_piece_dir_constants = { "prop_next_neighbour", "prop_zero", "prop_zero", "prop_zero", "prop_next_neighbour", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_direct_neighbour" };
// prob_piece_dir_constants_zero = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
// prob_piece_dir_constants_ninety = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
// prob_piece_dir_constants_oneeighty = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ;
// prob_piece_dir_constants_twoseventy ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ;
prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_south = { "prop_zero", "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_zero" } ;
straightPosIndex = 6; straightPosIndex = 6;
@ -897,16 +904,17 @@ namespace prism {
positionGuard = "\t" + agentName + "IsOnSlipperyWest"; positionGuard = "\t" + agentName + "IsOnSlipperyWest";
prob_piece_dir = { 1, 2, 0 /* <- R */, 2, 1, 0, 0, 0 }; prob_piece_dir = { 1, 2, 0 /* <- R */, 2, 1, 0, 0, 0 };
// TODO // TODO
// prob_piece_dir_zero = { 0 /*n <- R */, 1, 0, 0, 0, 0, 0, 1};
// prob_piece_dir_ninety = { 0, 2, 0 /*e <- R */, 0, 0, 0, 0, 0 };
// prob_piece_dir_oneeighty = { 2, 0, 0, 0, 0 /*s <- R */, 0, 0, 0 };
// prob_piece_dir_twoseventy = { 0, 0, 0, 0, 0, 0, 0 /* <- R */, 2 };
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_next_neighbour", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_direct_neighbour", "prop_next_neighbour", "prop_zero","prop_zero", "prop_zero" }; prob_piece_dir_constants = {"prop_next_neighbour", "prop_direct_neighbour", "prop_zero" /* <- R */, "prop_direct_neighbour", "prop_next_neighbour", "prop_zero","prop_zero", "prop_zero" };
// prob_piece_dir_constants_zero = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
// prob_piece_dir_constants_ninety = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
// prob_piece_dir_constants_oneeighty = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ;
// prob_piece_dir_constants_twoseventy ={ "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" } ;
prob_piece_dir_constants_agent_north = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_east = { "prop_zero", "prop_zero", "prop_zero", "prop_zero", "prop_zero" /* <- R */, "prop_zero", "prop_zero", "prop_zero" };
prob_piece_dir_constants_agent_south = { "prop_zero", "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_zero" } ;
straightPosIndex = 2; straightPosIndex = 2;

Write Preview
Loading…
Cancel
Save