|
|
@ -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<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> 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<std::string, cells> &slipperyTiles, const AgentNameAndPositionMap &agentNameAndPositionMap, std::vector<Configuration> 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 { |
|
|
|