Skip to content

Commit

Permalink
to_mata and to_dot with filename
Browse files Browse the repository at this point in the history
  • Loading branch information
koniksedy committed Nov 16, 2024
1 parent 3c05423 commit 5a388f7
Show file tree
Hide file tree
Showing 2 changed files with 47 additions and 13 deletions.
41 changes: 29 additions & 12 deletions include/mata/nfa/nfa.hh
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ public:
BoolVector get_useful_states() const;

/**
* @brief Structure for storing callback functions (event handlers) utilizing
* @brief Structure for storing callback functions (event handlers) utilizing
* Tarjan's SCC discover algorithm.
*/
struct TarjanDiscoverCallback {
Expand All @@ -189,7 +189,7 @@ public:

/**
* @brief Tarjan's SCC discover algorihm.
*
*
* @param callback Callbacks class to instantiate callbacks for the Tarjan's algorithm.
*/
void tarjan_scc_discover(const TarjanDiscoverCallback& callback) const;
Expand Down Expand Up @@ -218,9 +218,9 @@ public:

/**
* @brief Get some shortest accepting run from state @p q
*
*
* Assumes that @p q is a state of this automaton and that there is some accepting run from @p q
*
*
* @param distances_to_final Vector of the lengths of the shortest runs from states (can be computed using distances_to_final())
*/
Run get_shortest_accepting_run_from_state(State q, const std::vector<State>& distances_to_final) const;
Expand Down Expand Up @@ -280,6 +280,12 @@ public:
*/
void print_to_dot(std::ostream &output) const;

/**
* @brief Prints the automaton to the file in DOT format
* @param filename Name of the file to print the automaton to
*/
void print_to_dot(const std::string& filename) const;

/**
* @brief Prints the automaton in mata format
*
Expand All @@ -289,6 +295,7 @@ public:
* TODO handle alphabet of the automaton, currently we print the exact value of the symbols
*/
std::string print_to_mata() const;

/**
* @brief Prints the automaton to the output stream in mata format
*
Expand All @@ -298,20 +305,30 @@ public:
*/
void print_to_mata(std::ostream &output) 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 filename Name of the file to print the automaton to
*/
void print_to_mata(const std::string& filename) 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;

/**
* Check whether the language of NFA is empty.
* Currently calls is_lang_empty_scc if cex is null
* Check whether the language of NFA is empty.
* Currently calls is_lang_empty_scc if cex is null
* @param[out] cex Counter-example path for a case the language is not empty.
* @return True if the language is empty, false otherwise.
*/
bool is_lang_empty(Run* cex = nullptr) const;

/**
* @brief Check if the language is empty using Tarjan's SCC discover algorithm.
*
*
* @return Language empty <-> True
*/
bool is_lang_empty_scc() const;
Expand All @@ -334,17 +351,17 @@ public:

/**
* @brief Is the automaton graph acyclic? Used for checking language finiteness.
*
*
* @return true <-> Automaton graph is acyclic.
*/
bool is_acyclic() const;

/**
* @brief Is the automaton flat?
*
* Flat automaton is an NFA whose every SCC is a simple loop. Basically each state in an
*
* Flat automaton is an NFA whose every SCC is a simple loop. Basically each state in an
* SCC has at most one successor within this SCC.
*
*
* @return true <-> Automaton graph is flat.
*/
bool is_flat() const;
Expand Down Expand Up @@ -374,7 +391,7 @@ public:

/**
* @brief Get the set of all words in the language of the automaton whose length is <= @p max_length
*
*
* If you have an automaton with finite language (can be checked using @ref is_acyclic),
* you can get all words by calling
* get_words(aut.num_of_states())
Expand Down
19 changes: 18 additions & 1 deletion src/nfa/nfa.cc
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
#include <list>
#include <optional>
#include <iterator>
#include <fstream>

// MATA headers
#include "mata/utils/sparse-set.hh"
Expand Down Expand Up @@ -404,7 +405,7 @@ bool Nfa::is_flat() const {
mata::nfa::Nfa::TarjanDiscoverCallback callback {};
callback.scc_discover = [&](const std::vector<mata::nfa::State>& scc, const std::vector<mata::nfa::State>& tarjan_stack) -> bool {
(void)tarjan_stack;

for(const mata::nfa::State& st : scc) {
bool one_input_visited = false;
for (const mata::nfa::SymbolPost& sp : this->delta[st]) {
Expand Down Expand Up @@ -459,6 +460,14 @@ void Nfa::print_to_dot(std::ostream &output) const {
output << "}" << std::endl;
}

void Nfa::print_to_dot(const std::string& filename) const {
std::ofstream output(filename);
if (!output) {
throw std::ios_base::failure("Failed to open file: " + filename);
}
print_to_dot(output);
}

std::string Nfa::print_to_mata() const {
std::stringstream output;
print_to_mata(output);
Expand Down Expand Up @@ -492,6 +501,14 @@ void Nfa::print_to_mata(std::ostream &output) const {
}
}

void Nfa::print_to_mata(const std::string& filename) const {
std::ofstream output(filename);
if (!output) {
throw std::ios_base::failure("Failed to open file: " + filename);
}
print_to_mata(output);
}

Nfa Nfa::get_one_letter_aut(Symbol abstract_symbol) const {
Nfa digraph{num_of_states(), StateSet(initial), StateSet(final) };
// Add directed transitions for digraph.
Expand Down

0 comments on commit 5a388f7

Please sign in to comment.