feat(alphabet): Print to mata format with symbol names on transitions (…

…#473) #patch
VeriFIT · Nov 26, 2024 · e953d8c · e953d8c
1 parent 1bd84b4
commit e953d8c
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 12 deletions.
diff --git a/include/mata/nfa/nfa.hh b/include/mata/nfa/nfa.hh
@@ -299,29 +299,29 @@ public:
      *
      * If you need to parse the automaton again, use IntAlphabet in construct()
      *
+     * @param[in] alphabet If specified, translates the symbols to their symbol names in the @p alphabet.
      * @return automaton in mata format
-     * TODO handle alphabet of the automaton, currently we print the exact value of the symbols
      */
-    std::string print_to_mata() const;
+    std::string print_to_mata(const Alphabet* alphabet = nullptr) const;
 
     /**
      * @brief Prints the automaton to the output stream in mata format
      *
      * If you need to parse the automaton again, use IntAlphabet in construct()
      *
-     * TODO handle alphabet of the automaton, currently we print the exact value of the symbols
+     * @param[in] alphabet If specified, translates the symbols to their symbol names in the @p alphabet.
      */
-    void print_to_mata(std::ostream &output) const;
+    void print_to_mata(std::ostream &output, const Alphabet* alphabet = nullptr) const;
 
     /**
      * @brief Prints the automaton to the file in mata format
      *
      * If you need to parse the automaton again, use IntAlphabet in construct()
      *
-     * TODO handle alphabet of the automaton, currently we print the exact value of the symbols
+     * @param[in] alphabet If specified, translates the symbols to their symbol names in the @p alphabet.
      * @param filename Name of the file to print the automaton to
      */
-    void print_to_mata(const std::string& filename) const;
+    void print_to_mata(const std::string& filename, const Alphabet* alphabet = nullptr) const;
 
     // TODO: Relict from VATA. What to do with inclusion/ universality/ this post function? Revise all of them.
     StateSet post(const StateSet& states, const Symbol& symbol) const;

diff --git a/src/nfa/nfa.cc b/src/nfa/nfa.cc
@@ -6,8 +6,10 @@
 #include <optional>
 #include <iterator>
 #include <fstream>
+#include <string>
 
 // MATA headers
+#include "mata/alphabet.hh"
 #include "mata/utils/sparse-set.hh"
 #include "mata/nfa/nfa.hh"
 #include "mata/nfa/algorithms.hh"
@@ -468,13 +470,13 @@ void Nfa::print_to_dot(const std::string& filename) const {
     print_to_dot(output);
 }
 
-std::string Nfa::print_to_mata() const {
+std::string Nfa::print_to_mata(const Alphabet* alphabet) const {
     std::stringstream output;
-    print_to_mata(output);
+    print_to_mata(output, alphabet);
     return output.str();
 }
 
-void Nfa::print_to_mata(std::ostream &output) const {
+void Nfa::print_to_mata(std::ostream &output, const Alphabet* alphabet) const {
     output << "@NFA-explicit" << std::endl
            << "%Alphabet-auto" << std::endl;
            // TODO should be this, but we cannot parse %Alphabet-numbers yet
@@ -497,16 +499,18 @@ void Nfa::print_to_mata(std::ostream &output) const {
     }
 
     for (const Transition& trans: delta.transitions()) {
-        output << "q" << trans.source << " " << trans.symbol << " q" << trans.target << std::endl;
+        output << "q" << trans.source << " "
+        << ((alphabet != nullptr) ? alphabet->reverse_translate_symbol(trans.symbol) : std::to_string(trans.symbol))
+        << " q" << trans.target << std::endl;
     }
 }
 
-void Nfa::print_to_mata(const std::string& filename) const {
+void Nfa::print_to_mata(const std::string& filename, const Alphabet* alphabet) const {
     std::ofstream output(filename);
     if (!output) {
         throw std::ios_base::failure("Failed to open file: " + filename);
     }
-    print_to_mata(output);
+    print_to_mata(output, alphabet);
 }
 
 Nfa Nfa::get_one_letter_aut(Symbol abstract_symbol) const {