Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Concat problem #347

Closed
wants to merge 9 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions include/mata/nfa/algorithms.hh
Original file line number Diff line number Diff line change
Expand Up @@ -105,15 +105,15 @@ Simlib::Util::BinaryRelation compute_relation(
/**
* @brief Compute intersection of two NFAs with a possibility of using multiple epsilons.
*
* @param[in] lhs First NFA to compute intersection for.
* @param[in] lhs_source First NFA to compute intersection for.
* @param[in] rhs Second NFA to compute intersection for.
* @param[in] preserve_epsilon Whether to compute intersection preserving epsilon transitions.
* @param[in] epsilons Set of symbols to be considered as epsilons
* @param[out] prod_map Mapping of pairs of the original states (lhs_state, rhs_state) to new product states.
* @return NFA as a product of NFAs @p lhs and @p rhs with ε-transitions preserved.
*/
Nfa intersection_eps(const Nfa& lhs, const Nfa& rhs, bool preserve_epsilon, const std::set<Symbol>& epsilons,
std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr);
Nfa product(const Nfa& lhs_source, const Nfa& rhs, const std::function<bool(State,State)> && final_condition,
const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State,State>, State> *prod_map = nullptr);

/**
* @brief Concatenate two NFAs.
Expand Down
4 changes: 4 additions & 0 deletions include/mata/nfa/delta.hh
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,10 @@ public:
iterator find(const Symbol symbol) { return super::find({ symbol, {} }); }
const_iterator find(const Symbol symbol) const { return super::find({ symbol, {} }); }

//returns an iterator to the smallest epsilon, or end() if there is no epsilon
const_iterator first_epsilon_it(Symbol first_epsilon) const;


/**
* @brief Iterator over moves represented as @c Move instances.
*
Expand Down
2 changes: 1 addition & 1 deletion include/mata/nfa/nfa.hh
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,7 @@ Nfa uni(const Nfa &lhs, const Nfa &rhs);
* @return NFA as a product of NFAs @p lhs and @p rhs with ε-transitions preserved.
*/
Nfa intersection(const Nfa& lhs, const Nfa& rhs,
bool preserve_epsilon = false, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr);
const Symbol first_epsilon = EPSILON, std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr);

/**
* @brief Concatenate two NFAs.
Expand Down
4 changes: 2 additions & 2 deletions include/mata/nfa/plumbing.hh
Original file line number Diff line number Diff line change
Expand Up @@ -86,9 +86,9 @@ inline void uni(Nfa *unionAutomaton, const Nfa &lhs, const Nfa &rhs) { *unionAut
* Automata must share alphabets.
*/
inline void intersection(Nfa* res, const Nfa& lhs, const Nfa& rhs,
bool preserve_epsilon = false,
std::unordered_map<std::pair<State, State>, State> *prod_map = nullptr) {
*res = intersection(lhs, rhs, preserve_epsilon, prod_map);
//TODO: first_epsilon should also be a parameter, optional parameter?
*res = intersection(lhs, rhs, EPSILON, prod_map);
}

/**
Expand Down
20 changes: 20 additions & 0 deletions src/nfa/delta.cc
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ void SymbolPost::insert(State s) {
}
}

//TODO: slow! This should be doing merge, not inserting one by one.
void SymbolPost::insert(const StateSet& states) {
for (State s : states) {
insert(s);
Expand Down Expand Up @@ -374,6 +375,24 @@ bool Delta::operator==(const Delta& other) const {
return other_transitions_it == other_transitions_end;
}

//Returns an iterator to the smallest epsilon, or end() if there is no epsilon
//Searches from the end of the vector of SymbolPosts, since epsilons are at the end and they are typically few, mostly 1.
StatePost::const_iterator StatePost::first_epsilon_it(Symbol first_epsilon) const {
auto it = end();
while (it != begin()) {
--it;
if (it->symbol < first_epsilon) { //is it a normal symbol already?
++it; // go step back, to the smallest epsilon or end(), and return it
return it;
}
}

if (it != end() && it->symbol >= first_epsilon) //special case when begin is the smallest epsilon (since the while loop ended before the step back)
return it;

return end();
}

StatePost::Moves::const_iterator::const_iterator(
const StatePost& state_post, const StatePost::const_iterator symbol_post_it,
const StatePost::const_iterator symbol_post_end)
Expand Down Expand Up @@ -478,6 +497,7 @@ StatePost::Moves StatePost::moves_epsilons(const Symbol first_epsilon) const {
return { *this, symbol_post_begin, symbol_post_end };
}

//TODO: some comments, my brain hurts. Can we use first_epsilon_it above (or rewrite its code as below)
StatePost::const_iterator previous_symbol_post_it{ std::prev(symbol_post_end) };
StatePost::const_iterator symbol_post_it{ previous_symbol_post_it };
while (previous_symbol_post_it != symbol_post_begin && first_epsilon < previous_symbol_post_it->symbol) {
Expand Down
2 changes: 1 addition & 1 deletion src/nfa/inclusion.cc
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ bool mata::nfa::algorithms::is_included_naive(
} else {
bigger_cmpl = complement(bigger, *alphabet);
}
Nfa nfa_isect = intersection(smaller, bigger_cmpl, false, nullptr);
Nfa nfa_isect = intersection(smaller, bigger_cmpl);

return nfa_isect.is_lang_empty(cex);
} // is_included_naive }}}
Expand Down
Loading
Loading