From 9f03a14347d8322d736ef4f350f39da9e4058ced Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Fri, 5 Jan 2024 21:12:49 +0100
Subject: [PATCH] init PrismFormulaPrinter

first attempt to enforce DRY for formulas in PrismModulesPrinter
---
 util/PrismFormulaPrinter.cpp | 46 ++++++++++++++++++++++++++++++++++++
 util/PrismFormulaPrinter.h   | 21 ++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 util/PrismFormulaPrinter.cpp
 create mode 100644 util/PrismFormulaPrinter.h

diff --git a/util/PrismFormulaPrinter.cpp b/util/PrismFormulaPrinter.cpp
new file mode 100644
index 0000000..a54233d
--- /dev/null
+++ b/util/PrismFormulaPrinter.cpp
@@ -0,0 +1,46 @@
+#include "PrismFormulaPrinter.h"
+
+#include <map>
+#include <string>
+
+
+std::string cellToConjunction(const AgentName &agentName, const cell &c) {
+  return "x" + agentName + "=" + std::to_string(c.column) + "&y" + agentName + "=" + std::to_string(c.row);
+}
+
+namespace prism {
+  PrismFormulaPrinter::PrismFormulaPrinter() {}
+
+  std::ostream& PrismFormulaPrinter::printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells) {
+    os << buildFormula(agentName + "CannotMove" + direction, buildDisjunction(agentName, grid_cells));
+    return os;
+  }
+  std::ostream& PrismFormulaPrinter::printRestrictionFormulaWithCondition(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const std::vector<std::string> conditions) {
+    os << buildFormula(agentName + "Something", buildDisjunction(agentName, grid_cells, conditions));
+    return os;
+  }
+
+  std::string PrismFormulaPrinter::buildFormula(const std::string &formulaName, const std::string &formula) {
+    return "formula " + formulaName + " = " + formula + ";\n";
+  }
+
+  std::string PrismFormulaPrinter::buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions) {
+    bool first = true;
+    std::string disjunction = "";
+    if(!conditions.empty()) {
+      for(uint index = 0; index < cells.size(); index++) {
+        if(first) first = false;
+        else disjunction += " | ";
+        disjunction += "(" + cellToConjunction(agentName, cells.at(index)) + "&" + conditions.at(index) + ")";
+      }
+
+    } else {
+      for(auto const cell : cells) {
+        if(first) first = false;
+        else disjunction += " | ";
+        disjunction += "(" + cellToConjunction(agentName, cell) + ")";
+      }
+    }
+    return disjunction;
+  }
+}
diff --git a/util/PrismFormulaPrinter.h b/util/PrismFormulaPrinter.h
new file mode 100644
index 0000000..a9b5df4
--- /dev/null
+++ b/util/PrismFormulaPrinter.h
@@ -0,0 +1,21 @@
+#pragma once
+
+#include <iostream>
+#include <functional>
+#include "MinigridGrammar.h"
+#include "PrismPrinter.h"
+#include "ConfigYaml.h"
+
+namespace prism {
+  class PrismFormulaPrinter {
+    public:
+      PrismFormulaPrinter();
+
+      std::ostream& printRestrictionFormula(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells);
+      std::ostream& printRestrictionFormulaWithCondition(std::ostream& os, const AgentName &agentName, const std::string &direction, const cells &grid_cells, const std::vector<std::string> conditions);
+    private:
+      std::string buildFormula(const std::string &formulaName, const std::string &formula);
+      std::string buildLabel(const std::string &labelName, const std::string &label);
+      std::string buildDisjunction(const AgentName &agentName, const cells &cells, const std::vector<std::string> &conditions = {});
+  };
+}