Skip to content

Commit

Permalink
Merge pull request #419 from VeriFIT/get_symbols_to_work_with
Browse files Browse the repository at this point in the history
Get symbols to work with #patch
  • Loading branch information
Adda0 authored Jul 9, 2024
2 parents a377851 + c106e3b commit 9deba89
Show file tree
Hide file tree
Showing 6 changed files with 170 additions and 100 deletions.
3 changes: 2 additions & 1 deletion bindings/python/libmata/nfa/nfa.pxd
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
from libcpp cimport bool
from libcpp.optional cimport optional
from libcpp.set cimport set as cset
from libcpp.unordered_set cimport unordered_set as uset
from libcpp.unordered_map cimport unordered_map as umap
Expand Down Expand Up @@ -178,7 +179,7 @@ cdef extern from "mata/nfa/nfa.hh" namespace "mata::nfa":
bool is_in_lang(CRun&)
bool is_prfx_in_lang(CRun&)
pair[CRun, bool] get_word_for_path(CRun&)
void make_complete(CAlphabet&, State) except +
void make_complete(CAlphabet*, optional[State]) except +

# Automata tests
cdef bool c_is_included "mata::nfa::is_included" (CNfa&, CNfa&, CAlphabet*, ParameterMap&)
Expand Down
3 changes: 2 additions & 1 deletion bindings/python/libmata/nfa/nfa.pyx
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import networkx as nx

from libc.stdint cimport uint8_t
from libcpp cimport bool
from libcpp.optional cimport make_optional
from libcpp.list cimport list as clist
from libcpp.memory cimport shared_ptr, make_shared
from libcpp.set cimport set as cset
Expand Down Expand Up @@ -792,7 +793,7 @@ cdef class Nfa:
"""
if not self.thisptr.get().is_state(sink_state):
self.thisptr.get().add_state(self.thisptr.get().num_of_states())
self.thisptr.get().make_complete(<CAlphabet&>dereference(alphabet.as_base()), sink_state)
self.thisptr.get().make_complete(alphabet.as_base(), make_optional[State](sink_state))

def get_symbols(self):
"""Return a set of symbols used on the transitions in NFA.
Expand Down
36 changes: 15 additions & 21 deletions include/mata/nfa/nfa.hh
Original file line number Diff line number Diff line change
Expand Up @@ -367,11 +367,12 @@ public:
* to the NFA, it is added to it, but only in the case that some transition to @p sink_state was added.
* In the case that NFA does not contain any states, this function does nothing.
*
* @param[in] alphabet Alphabet to use for computing "missing" symbols.
* @param[in] sink_state The state into which new transitions are added.
* @return True if some new transition was added to the NFA.
* @param[in] alphabet Alphabet to use for computing "missing" symbols. If @c nullptr, use @c this->alphabet when
* defined, otherwise use @c this->delta.get_used_symbols().
* @param[in] sink_state The state into which new transitions are added. If @c std::nullopt, add a new sink state.
* @return @c true if a new transition was added to the NFA.
*/
bool make_complete(const Alphabet& alphabet, State sink_state);
bool make_complete(const Alphabet* alphabet = nullptr, std::optional<State> sink_state = std::nullopt);

/**
* @brief Make NFA complete in place.
Expand All @@ -385,24 +386,11 @@ public:
* complete to from the alphabet. Prefer this version when you already have the set of symbols precomputed or plan
* to complete multiple automata over the same set of symbols.
*
* @param[in] symbols Symbols to compute missing symbols from.
* @param[in] sink_state The state into which new transitions are added.
* @return True if some new transition was added to the automaton.
* @param[in] symbols Symbols to compute "missing" symbols from.
* @param[in] sink_state The state into which new transitions are added. If @c std::nullopt, add a new sink state.
* @return @c true if a new transition was added to the NFA.
*/
bool make_complete(const utils::OrdVector<Symbol>& symbols, State sink_state);

/**
* @brief Make NFA complete in place.
*
* For each state 0,...,this->num_of_states()-1, add transitions with "missing" symbols from @p alphabet
* (symbols that do not occur on transitions from given state) to new sink state (if no new transitions are added,
* this sink state is not created).
* In the case that NFA does not contain any states, this function does nothing.
*
* @param[in] alphabet Alphabet to use for computing "missing" symbols.
* @return True if some new transition (and sink state) was added to the automaton.
*/
bool make_complete(const Alphabet& alphabet) { return this->make_complete(alphabet, this->num_of_states()); }
bool make_complete(const utils::OrdVector<Symbol>& symbols, std::optional<State> sink_state = std::nullopt);

/**
* Complement deterministic automaton in-place by adding a sink state and swapping final and non-final states.
Expand Down Expand Up @@ -682,6 +670,12 @@ Nfa remove_epsilon(const Nfa& aut, Symbol epsilon = EPSILON);
// What are the symbol names and their sequences?
Run encode_word(const Alphabet* alphabet, const std::vector<std::string>& input);

/**
* Get the set of symbols to work with during operations.
* @param[in] shared_alphabet Optional alphabet shared between NFAs passed as an argument to a function.
*/
utils::OrdVector<Symbol> get_symbols_to_work_with(const nfa::Nfa& nfa, const Alphabet* const shared_alphabet = nullptr);

} // namespace mata::nfa.

namespace std {
Expand Down
2 changes: 1 addition & 1 deletion include/mata/utils/synchronized-iterator.hh
Original file line number Diff line number Diff line change
Expand Up @@ -239,7 +239,7 @@ public:
/**
* @brief Returns the vector of current still active positions.
*
* Beware, thy will be ordered differently from how there were input into the iterator.
* Beware, they will be ordered differently from how there were input into the iterator.
* This is due to swapping of the emptied positions with positions at the end.
*/
const std::vector<Iterator>& get_current() const override { return this->currently_synchronized; };
Expand Down
60 changes: 30 additions & 30 deletions src/nfa/operations.cc
Original file line number Diff line number Diff line change
Expand Up @@ -481,33 +481,35 @@ std::ostream &std::operator<<(std::ostream &os, const mata::nfa::Transition &tra
return os << result;
}

bool mata::nfa::Nfa::make_complete(const Alphabet& alphabet, State sink_state) {
return this->make_complete(alphabet.get_alphabet_symbols(), sink_state);
bool mata::nfa::Nfa::make_complete(const Alphabet* const alphabet, const std::optional<State> sink_state) {
return make_complete(get_symbols_to_work_with(*this, alphabet), sink_state);
}

bool mata::nfa::Nfa::make_complete(const mata::utils::OrdVector<Symbol>& symbols, State sink_state) {
bool was_something_added{ false };

bool mata::nfa::Nfa::make_complete(const OrdVector<Symbol>& symbols, const std::optional<State> sink_state) {
bool transition_added{ false };
const size_t num_of_states{ this->num_of_states() };
for (State state = 0; state < num_of_states; ++state) {
OrdVector<Symbol> used_symbols{};
for (auto const &move : this->delta[state]) {
used_symbols.insert(move.symbol);
const State sink_state_val{ sink_state.value_or(num_of_states) };

OrdVector<Symbol> used_symbols{};
for (State state{ 0 }; state < num_of_states; ++state) {
for (const SymbolPost& symbol_post: delta[state]) {
used_symbols.insert(symbol_post.symbol);
}
mata::utils::OrdVector<Symbol> unused_symbols{ symbols.difference(used_symbols) };
for (Symbol symb : unused_symbols) {
this->delta.add(state, symb, sink_state);
was_something_added = true;
const OrdVector<Symbol> unused_symbols{ symbols.difference(used_symbols) };
for (const Symbol symbol: unused_symbols) {
delta.add(state, symbol, sink_state_val);
transition_added = true;
}
used_symbols.clear();
}

if (was_something_added && num_of_states <= sink_state) {
for (Symbol symbol : symbols) {
this->delta.add(sink_state, symbol, sink_state);
if (transition_added && num_of_states <= sink_state_val) {
for (const Symbol symbol: symbols) {
delta.add(sink_state_val, symbol, sink_state_val);
}
}

return was_something_added;
return transition_added;
}

//TODO: based on the comments inside, this function needs to be rewritten in a more optimal way.
Expand Down Expand Up @@ -772,18 +774,10 @@ bool mata::nfa::Nfa::is_deterministic() const {
return true;
}
bool mata::nfa::Nfa::is_complete(Alphabet const* alphabet) const {
if (alphabet == nullptr) {
if (this->alphabet != nullptr) {
alphabet = this->alphabet;
} else {
throw std::runtime_error("Checking for completeness without any alphabet to check againts.");
}
}
utils::OrdVector<Symbol> symbs_ls = alphabet->get_alphabet_symbols();
utils::OrdVector<Symbol> symbs(symbs_ls);
utils::OrdVector<Symbol> symbols{ get_symbols_to_work_with(*this, alphabet) };
utils::OrdVector<Symbol> symbs_ls{ symbols };

// TODO: make a general function for traversal over reachable states that can
// be shared by other functions?
// TODO: make a general function for traversal over reachable states that can be shared by other functions?
std::list<State> worklist(initial.begin(), initial.end());
std::unordered_set<State> processed(initial.begin(), initial.end());

Expand All @@ -795,7 +789,7 @@ bool mata::nfa::Nfa::is_complete(Alphabet const* alphabet) const {
if (!delta.empty()) {
for (const auto &symb_stateset: delta[state]) {
++n;
if (!haskey(symbs, symb_stateset.symbol)) {
if (!haskey(symbols, symb_stateset.symbol)) {
throw std::runtime_error(std::to_string(__func__) +
": encountered a symbol that is not in the provided alphabet");
}
Expand All @@ -808,7 +802,7 @@ bool mata::nfa::Nfa::is_complete(Alphabet const* alphabet) const {
}
}

if (symbs.size() != n) { return false; }
if (symbols.size() != n) { return false; }
}

return true;
Expand Down Expand Up @@ -1199,6 +1193,12 @@ std::set<mata::Word> mata::nfa::Nfa::get_words(unsigned max_length) {
return result;
}

OrdVector<Symbol> mata::nfa::get_symbols_to_work_with(const Nfa& nfa, const mata::Alphabet *const shared_alphabet) {
if (shared_alphabet != nullptr) { return shared_alphabet->get_alphabet_symbols(); }
else if (nfa.alphabet != nullptr) { return nfa.alphabet->get_alphabet_symbols(); }
else { return nfa.delta.get_used_symbols(); }
}

std::optional<mata::Word> Nfa::get_word(const Symbol first_epsilon) const {
if (initial.empty() || final.empty()) { return std::nullopt; }

Expand Down
Loading

0 comments on commit 9deba89

Please sign in to comment.