Browse Source

add nonmovement action to modules

This is needed to correctly shield when staying at a certain place
should not be allowed
pull/16/head
sp 10 months ago
parent
commit
43aebc463c
  1. 16
      util/PrismModulesPrinter.cpp
  2. 1
      util/PrismModulesPrinter.h

16
util/PrismModulesPrinter.cpp

@ -203,6 +203,8 @@ namespace prism {
printPortableObjectActionsForRobot(agentName, identifier);
}
printNonMovementActionsForRobot(agentName);
os << "\n" << actionStream.str();
actionStream.str(std::string());
@ -285,6 +287,14 @@ namespace prism {
return updateToString(u) + ";\n";
}
void PrismModulesPrinter::printNonMovementActionsForRobot(const AgentName &agentName) {
for(auto const [actionId, action] : nonMovementActions) {
std::string actionName = "[" + agentName + "_" + action + "]";
agentNameActionMap.at(agentName).insert({actionId, actionName});
actionStream << " " << actionName << " true -> true;\n";
}
}
void PrismModulesPrinter::printSlipperyMovementActionsForRobot(const AgentName &a) {
if(!slipperyTiles.at("North").empty()) {
printSlipperyMovementActionsForNorth(a);
@ -464,7 +474,9 @@ namespace prism {
os << "\nmodule " << a << "FaultyBehaviour" << std::endl;
os << " previousAction" << a << " : [0.." + std::to_string(NOFAULT) + "];\n";
std::set<size_t> exclude = {PICKUP, DROP, TOGGLE, DONE};
for(const auto [actionId, actionName] : agentNameActionMap.at(a)) {
if(exclude.count(actionId) > 0) continue;
os << " " << actionName << faultyBehaviourGuard(a, actionId) << " -> " << faultyBehaviourUpdate(a, actionId) << ";\n";
}
os << "endmodule\n\n";
@ -493,7 +505,7 @@ namespace prism {
}
void PrismModulesPrinter::printDoneActions(const AgentName &agentName) {
os << " [" << agentName << "_done]" << agentName << "IsOnGoal & clock=0 -> true;\n";
os << " [" << agentName << "_on_goal]" << agentName << "IsOnGoal & clock=0 -> true;\n";
}
void PrismModulesPrinter::printPlayerStruct(const AgentName &agentName) {
@ -504,7 +516,7 @@ namespace prism {
else os << ", ";
os << actionName;
}
if(agentName == "Agent") os << ", [Agent_done]";
if(agentName == "Agent") os << ", [Agent_on_goal]";
os << "\nendplayer\n";
}

1
util/PrismModulesPrinter.h

@ -38,6 +38,7 @@ namespace prism {
void printLockedDoorActionsForRobot(const std::string &agentName, const std::string &identifier, const std::string &key);
void printMovementActionsForRobot(const std::string &a);
void printTurnActionsForRobot(const std::string &a);
void printNonMovementActionsForRobot(const AgentName &agentName);
void printSlipperyMovementActionsForRobot(const AgentName &a);
void printSlipperyMovementActionsForNorth(const AgentName &a);
void printSlipperyMovementActionsForEast(const AgentName &a);

Loading…
Cancel
Save