From 0a0d836968de3964287f56d1be6dd75b32efbead Mon Sep 17 00:00:00 2001
From: Thomas Knoll <thomas.knolł@student.tugraz.at>
Date: Thu, 31 Aug 2023 09:29:40 +0200
Subject: [PATCH] added config print

---
 main.cpp                     |  5 ++---
 util/ConfigGrammar.h         | 32 ++++++++++++++++++++++++--------
 util/Grid.cpp                |  6 +++++-
 util/Grid.h                  |  3 ++-
 util/PrismModulesPrinter.cpp | 21 +++++++++++++++++++++
 util/PrismModulesPrinter.h   |  3 +++
 6 files changed, 57 insertions(+), 13 deletions(-)

diff --git a/main.cpp b/main.cpp
index aa6b336..19d3c25 100644
--- a/main.cpp
+++ b/main.cpp
@@ -133,7 +133,7 @@ int main(int argc, char* argv[]) {
   if (configFilename->is_set()) {
     std::fstream configFile {configFilename->value(0), configFile.in};
     while (std::getline(configFile, line) && !line.empty()) {
-      std::cout << "Configuration   :\t" << line << "\n";
+      std::cout << "Configuration:\t" << line << "\n";
       config += line + "\n";
     }
   }
@@ -164,7 +164,6 @@ int main(int argc, char* argv[]) {
       ok &= phrase_parse(configIter, configLast, configParser, qi::space, configurations);
     }
 
-    std::cout << "Found " << configurations.size() << "configs" << std::endl;
     for (auto& config : configurations) {
       std::cout << config << std::endl;
     }
@@ -180,7 +179,7 @@ int main(int argc, char* argv[]) {
     if(ok) {
       Grid grid(contentCells, backgroundCells, gridOptions, stateRewards);
       //grid.printToPrism(std::cout, prism::ModelType::MDP);
-      grid.printToPrism(file, prism::ModelType::MDP);
+      grid.printToPrism(file, configurations ,prism::ModelType::MDP);
     }
   } catch(qi::expectation_failure<pos_iterator_t> const& e) {
     std::cout << "expected: "; print_info(e.what_);
diff --git a/util/ConfigGrammar.h b/util/ConfigGrammar.h
index 597df96..71aa54d 100644
--- a/util/ConfigGrammar.h
+++ b/util/ConfigGrammar.h
@@ -17,30 +17,37 @@ namespace phoenix = boost::phoenix;
 
 typedef std::vector<std::string> expressions;
 
+enum class ConfigType : char {
+  Label = 'L',
+  Formula = 'F',
+};
+
 struct Configuration
 {
   expressions expressions_;
   std::string derivation_;
+  ConfigType type_ {ConfigType::Label};
 
   Configuration() = default;
-  Configuration(expressions expressions, std::string derivation) : expressions_(expressions), derivation_(derivation) {}
+  Configuration(expressions expressions, std::string derivation, ConfigType type) : expressions_(expressions), derivation_(derivation), type_(type) {}
   ~Configuration() = default;
   Configuration(const Configuration&) = default;
 
   friend std::ostream& operator << (std::ostream& os, const Configuration& config) {
-    os << "Configuration" << std::endl; 
+    os << "Configuration with Type: " << static_cast<char>(config.type_) << std::endl; 
 
     for (auto& expression : config.expressions_) {
-      os << "Expression=" << expression << std::endl;
+      os << "\tExpression=" << expression << std::endl;
     }
 
-    return os << "Derviation=" << config.derivation_;
+    return os << "\tDerviation=" << config.derivation_;
   }
 };
 
 
 BOOST_FUSION_ADAPT_STRUCT(
     Configuration,
+    (ConfigType, type_)
     (expressions, expressions_)
     (std::string, derivation_)
 )
@@ -52,21 +59,30 @@ template <typename It>
   ConfigParser(It first) : ConfigParser::base_type(config_)
   {
     using namespace qi;
-   
-    expression_ = +char_("a-zA-Z_0-9");
+   //F:(AgentCannotMoveSouth & AgentCannotMoveNorth)  | (AgentCannotMoveEast & AgentCannotMoveWest) ;AgentCannotTurn
+    configType_.add
+      ("L", ConfigType::Label)
+      ("F", ConfigType::Formula);
+
+    expression_ = -qi::char_('!') > + char_("a-zA-Z_0-9");
     expressions_ = (expression_ % ',');
-    row_ = (expressions_ > ';' > expression_);
+    row_ = (configType_ > ':' > expressions_ > ';' > expression_);
+    // row_ = (expressions_ > ';' > expression_);
     config_ = (row_ % "\n");
 
+    BOOST_SPIRIT_DEBUG_NODE(configType_);
     BOOST_SPIRIT_DEBUG_NODE(expression_);
     BOOST_SPIRIT_DEBUG_NODE(expressions_);
     BOOST_SPIRIT_DEBUG_NODE(config_);
   }
 
   private:
+
+    qi::symbols<char, ConfigType>  configType_;
+
   
     qi::rule<It, expressions()> expressions_;
     qi::rule<It, std::string()> expression_;
     qi::rule<It, Configuration()> row_;
     qi::rule<It, std::vector<Configuration>>  config_;
-};
\ No newline at end of file
+};
diff --git a/util/Grid.cpp b/util/Grid.cpp
index 3036503..b45266c 100644
--- a/util/Grid.cpp
+++ b/util/Grid.cpp
@@ -129,7 +129,7 @@ bool Grid::isBox(coordinates p) {
       }) != boxes.end();
 }
 
-void Grid::printToPrism(std::ostream& os, const prism::ModelType& modelType) {
+void Grid::printToPrism(std::ostream& os, std::vector<Configuration>& configuration ,const prism::ModelType& modelType) {
   cells northRestriction;
   cells eastRestriction;
   cells southRestriction;
@@ -225,6 +225,10 @@ void Grid::printToPrism(std::ostream& os, const prism::ModelType& modelType) {
     //if(!stateRewards.empty()) {
     printer.printRewards(os, agentName, stateRewards, lava, goals, backgroundTiles);
     //}
+
+    if (!configuration.empty()) {
+      printer.printConfiguration(os, configuration);
+    }
   }
 }
 
diff --git a/util/Grid.h b/util/Grid.h
index a17fb42..4aaab9a 100644
--- a/util/Grid.h
+++ b/util/Grid.h
@@ -7,6 +7,7 @@
 
 #include "MinigridGrammar.h"
 #include "PrismModulesPrinter.h"
+#include "ConfigGrammar.h"
 
 struct GridOptions {
   std::vector<AgentName> agentsToBeConsidered;
@@ -28,7 +29,7 @@ class Grid {
     bool isUnlockedDoor(coordinates p);
     bool isKey(coordinates p);
     bool isBox(coordinates p);
-    void printToPrism(std::ostream &os, const prism::ModelType& modelType);
+    void printToPrism(std::ostream &os, std::vector<Configuration>& configuration, const prism::ModelType& modelType);
 
     std::array<bool, 8> getWalkableDirOf8Neighborhood(cell c);
 
diff --git a/util/PrismModulesPrinter.cpp b/util/PrismModulesPrinter.cpp
index 12c0c4e..9d50860 100644
--- a/util/PrismModulesPrinter.cpp
+++ b/util/PrismModulesPrinter.cpp
@@ -218,6 +218,27 @@ namespace prism {
     return os;
   }
 
+  std::ostream& PrismModulesPrinter::printConfiguration(std::ostream& os, const std::vector<Configuration>& configurations) {
+    os << "\n// Configuration\n";
+    
+    for (auto& configuration : configurations) {
+      if (configuration.type_ == ConfigType::Label) {
+        os << "label \"" << configuration.derivation_ << "\" = ";
+      }
+      else if (configuration.type_ == ConfigType::Formula) {
+        os << "formula " << configuration.derivation_ << " = ";
+      }
+
+      for (auto& expr : configuration.expressions_) {
+        os << expr;
+      }
+      
+      os << ";\n";
+    }
+
+    return os;
+  }
+
   std::ostream& PrismModulesPrinter::printAvoidanceLabel(std::ostream &os, const std::vector<AgentName> agentNames, const int &distance) {
     os << "label avoidance = ";
     bool first = true;
diff --git a/util/PrismModulesPrinter.h b/util/PrismModulesPrinter.h
index 12dc99f..22031d3 100644
--- a/util/PrismModulesPrinter.h
+++ b/util/PrismModulesPrinter.h
@@ -3,6 +3,7 @@
 #include <iostream>
 #include <functional>
 #include "MinigridGrammar.h"
+#include "ConfigGrammar.h"
 #include "PrismPrinter.h"
 
 namespace prism {
@@ -76,6 +77,8 @@ namespace prism {
 
       std::ostream& printRewards(std::ostream &os, const AgentName &agentName, const std::map<coordinates, float> &stateRewards, const cells &lava, const cells &goals, const std::map<Color, cells> &backgroundTiles);
 
+      std::ostream& printConfiguration(std::ostream &os, const std::vector<Configuration>& configurations);
+
       std::string moveGuard(const size_t &agentIndex);
       std::string moveUpdate(const size_t &agentIndex);