From ff0369cfb14a3071844ae2b62934a332f21a91f0 Mon Sep 17 00:00:00 2001 From: sp Date: Mon, 8 Jan 2024 15:54:40 +0100 Subject: [PATCH] added move module as arbiter --- util/PrismModulesPrinter.cpp | 27 ++++++++++++++++++--------- util/PrismModulesPrinter.h | 1 + 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp index 988df47..2c9af3f 100644 --- a/util/PrismModulesPrinter.cpp +++ b/util/PrismModulesPrinter.cpp @@ -494,6 +494,18 @@ namespace prism { os << "endmodule\n\n"; } + void PrismModulesPrinter::printMoveModule() { + os << "\nmodule " << "Arbiter" << std::endl; + os << "\tclock : [0.." << agentIndexMap.size() - 1 << "] init 0;\n"; + + for(const auto [agentName, actions] : agentNameActionMap) { + for(const auto [actionId, actionName] : actions) { + os << "\t" << actionName << " " << moveGuard(agentName) << " -> " << moveUpdate(agentName) << ";\n"; + } + } + os << "endmodule\n\n"; + } + std::ostream& PrismModulesPrinter::printConfiguredActions(std::ostream &os, const AgentName &agentName) { for (auto& config : configuration) { if (config.type_ == ConfigType::Module && !config.overwrite_ && agentName == config.module_) { @@ -613,10 +625,6 @@ namespace prism { return os; } - std::string PrismModulesPrinter::moveGuard(const AgentName &agentName) const { - return isGame() ? " move=" + std::to_string(agentIndexMap.at(agentName)) + " & " : " "; - } - std::string PrismModulesPrinter::faultyBehaviourGuard(const AgentName &agentName, const ActionId &actionId) const { if(faultyBehaviour()) { if(actionId == NOFAULT) { @@ -637,13 +645,14 @@ namespace prism { } } + std::string PrismModulesPrinter::moveGuard(const AgentName &agentName) const { + return "clock=" + std::to_string(agentIndexMap.at(agentName)); + } + std::string PrismModulesPrinter::moveUpdate(const AgentName &agentName) const { size_t agentIndex = agentIndexMap.at(agentName); - return isGame() ? - (agentIndex == numberOfPlayer - 1) ? - " & (move'=0) " : - " & (move'=" + std::to_string(agentIndex + 1) + ") " : - ""; + return (agentIndex == numberOfPlayer - 1) ? " & (clock'=0) " : " & (clock'=" + std::to_string(agentIndex + 1) + ") "; + } std::string PrismModulesPrinter::updatesToString(const updates &updates) const { diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h index 4c5eb8e..3284cfe 100644 --- a/util/PrismModulesPrinter.h +++ b/util/PrismModulesPrinter.h @@ -94,6 +94,7 @@ namespace prism { std::string printSlipperyTurnUpdate(const AgentName &a, const updates &u); void printFaultyMovementModule(const AgentName &a); + void printMoveModule(); bool anyPortableObject() const; bool faultyBehaviour() const;