add MONA DFA printing to stdout

whitemech · Feb 17, 2021 · 80bbdf8 · 80bbdf8
1 parent a567384
commit 80bbdf8
Show file tree

Hide file tree

Showing 3 changed files with 83 additions and 4 deletions.
diff --git a/app/lydia/src/main.cpp b/app/lydia/src/main.cpp
@@ -40,7 +40,7 @@ std::string dump_formula(const std::filesystem::path &filename) {
 
 int main(int argc, char **argv) {
   whitemech::lydia::Logger logger("main");
-  whitemech::lydia::Logger::level(whitemech::lydia::LogLevel::debug);
+  whitemech::lydia::Logger::level(whitemech::lydia::LogLevel::error);
 
   CLI::App app{"A tool for LDLf automata translation and LDLf synthesis."};
   bool verbose = false;
@@ -169,9 +169,13 @@ int main(int argc, char **argv) {
     if(my_mona_dfa){
       std::vector<unsigned> x(my_mona_dfa->get_nb_variables());
       std::iota(std::begin(x), std::end(x), 0);
-      whitemech::lydia::dfaPrintGraphvizToFile(my_mona_dfa->get_dfa(),
-                                               my_mona_dfa->get_nb_variables(),
-                                               x.data(), std::cout);
+      whitemech::lydia::dfaPrint(my_mona_dfa->get_dfa(),
+                                 my_mona_dfa->get_nb_variables(),
+                                 my_mona_dfa->names,
+                                 x.data(), std::cout);
+//      whitemech::lydia::dfaPrintGraphvizToFile(my_mona_dfa->get_dfa(),
+//                                               my_mona_dfa->get_nb_variables(),
+//                                               x.data(), std::cout);
     }
   }
   if (!dot_option->empty()) {

diff --git a/lib/include/lydia/dfa/mona_dfa.hpp b/lib/include/lydia/dfa/mona_dfa.hpp
@@ -109,6 +109,8 @@ DFA *dfaPropositionalTrue();
 bool is_sink(DFA *automaton, bool is_positive = true);
 
 void print_mona_dfa(DFA *a, const std::string &name, int num = 1);
+void dfaPrint(DFA *a, int no_free_vars, std::vector<std::string> free_variables,
+              unsigned *offsets, std::ostream &o = std::cout);
 void dfaPrintGraphvizToFile(DFA *a, int no_free_vars, unsigned *offsets,
                             std::ostream &o = std::cout);
 

diff --git a/lib/src/dfa/mona_dfa.cpp b/lib/src/dfa/mona_dfa.cpp
@@ -351,6 +351,79 @@ void print_mona_dfa(DFA *a, const std::string &name, int num) {
       std::string("dot -Tsvg '" + name + ".dot' > '" + name + ".svg'").c_str());
 }
 
+void dfaPrint(DFA *a, int no_free_vars, std::vector<std::string> free_variables,
+              unsigned *offsets, std::ostream &o) {
+  paths state_paths, pp;
+  trace_descr tp;
+  int i, j, any = 0;
+
+  o << "DFA for formula with free variables: ";
+
+  for (i = 0; i < no_free_vars; i++)
+    o << free_variables[i] << " ";
+
+  o << "\nInitial state: " << a->s << "\n"
+                                      "Accepting states: ";
+
+  for (i = 0; i < a->ns; i++)
+    if (a->f[i] == 1)
+      o << i << " ";
+
+  o << "\n"
+       "Rejecting states: ";
+
+  for (i = 0; i < a->ns; i++)
+    if (a->f[i] == -1)
+      o << i << " ";
+
+  o << "\n";
+
+  for (i = 0; i < a->ns; i++)
+    if (a->f[i] == 0) {
+      any = 1;
+      break;
+    }
+  if (any) {
+    printf("Don't-care states: ");
+    for (i = 0; i < a->ns; i++)
+      if (a->f[i] == 0)
+        o << i << " ";
+
+    o << "\n";
+  }
+
+  o << "\nAutomaton has "
+    << a->ns << " state(s) and "
+    << bdd_size(a->bddm) << " BDD-node(s)\n";
+
+  o << "Transitions:\n";
+
+  for (i = 0; i < a->ns; i++) {
+    state_paths = pp = make_paths(a->bddm, a->q[i]);
+
+    while (pp) {
+      o << "State " << i << ": ";
+
+      for (j = 0; j < no_free_vars; j++) {
+        for (tp = pp->trace; tp && (tp->index != offsets[j]); tp = tp->next);
+
+        if (tp) {
+          if (tp->value) o << "1";
+          else o << "0";
+        }
+        else
+          o << "X";
+      }
+
+      o << " -> state " << pp->to << "\n";
+
+      pp = pp->next;
+    }
+
+    kill_paths(state_paths);
+  }
+}
+
 void dfaPrintGraphvizToFile(DFA *a, int no_free_vars, unsigned *offsets,
                             std::ostream &o) {
   paths state_paths, pp;