diff --git a/examples/nft.cc b/examples/nft.cc index 70f9721f3..a9ac513f1 100644 --- a/examples/nft.cc +++ b/examples/nft.cc @@ -37,7 +37,7 @@ int main() { Nfa nfa = nfa::builder::create_from_regex("ABCDEFggg"); // Compute the pre-image of an NFA (applies NFA to the image tape, i.e., tape 1) - Nft backward_applied_nft = nft.apply(nfa, 1); + Nft backward_applied_nft = nft.apply(nfa, 1, true, mata::nft::JumpMode::NoJump); // Extract a pre-image NFA. Nfa nfa_pre_image{ backward_applied_nft.to_nfa_move() }; // Minimize the result pre-image using hopcroft minimization. diff --git a/include/mata/nft/algorithms.hh b/include/mata/nft/algorithms.hh index b30659158..13ec7a213 100644 --- a/include/mata/nft/algorithms.hh +++ b/include/mata/nft/algorithms.hh @@ -132,6 +132,47 @@ Nft product(const Nft& lhs, const Nft& rhs, const std::function& lhs_sync_levels, const utils::OrdVector& rhs_sync_levels, + bool project_out_sync_levels = true, + JumpMode jump_mode = JumpMode::RepeatSymbol); + +/** + * @brief Composes two NFTs (lhs || rhs; read as "rhs after lhs") with a single synchronization level and no jumps. + * + * @param[in] lhs First transducer to compose. + * @param[in] rhs Second transducer to compose. + * @param[in] lhs_sync_level The synchronization level of the @p lhs. + * @param[in] rhs_sync_level The synchronization level of the @p rhs. + * @param[in] project_out_sync_levels Whether we wont to project out the synchronization levels. + * + * @return A new NFT after the composition. + */ +Nft compose_fast_no_jump(const Nft& lhs, const Nft& rhs, Level lhs_sync_level = 1, Level rhs_sync_level = 0, bool project_out_sync_levels = true); + } #endif diff --git a/include/mata/nft/nft.hh b/include/mata/nft/nft.hh index b5d2cfaf9..4500b437b 100644 --- a/include/mata/nft/nft.hh +++ b/include/mata/nft/nft.hh @@ -340,6 +340,45 @@ public: */ State add_transition(State source, const std::vector& symbols); + /** + * @brief Add a single NFT transition with a length @p length from a source state @p source + * to a newly created target state, creating as many inner states as needed for the transition + * @p length and the jump mode. + * + * @param source The source state where the transition begins. @p source must already exist. + * @param symbol The symbol used for the transition. + * @param length The length of the transition. + * @param jump_mode Specifies the semantic of jump transitions (transitions with a length greater than 1). + */ + State add_transition_with_length(State source, Symbol symbol, size_t length, JumpMode jump_mode = JumpMode::RepeatSymbol); + + /** + * @brief Add a single NFT transition from a source state @p source to a target state @p target + * creating as many inner states as needed for the transition length and the jump mode. + * + * @param source The source state where the transition begins. @p source must already exist. + * @param symbol The symbol used for the transition. + * @param target The target state where the transition ends. @p target must already exist. + * @param jump_mode Specifies the semantic of jump transitions (transitions with a length greater than 1). + */ + void add_transition_with_target(const State source, const Symbol symbol, const State target, const JumpMode jump_mode = JumpMode::RepeatSymbol) { + add_transition_with_same_level_targets(source, symbol, { target }, jump_mode); + } + + /** + * @brief Add a NFT transition from a source state @p source to a set of target states @p targets + * creating as many inner states as needed for the transition length and the jump mode. + * + * For transitions with a length `l` greater than 1, the common part (before the `l`-th symbol) of the + * is shared for all targets and only at the `l`-th symbol the transition branches to each target. + * + * @param source The source state where the transition begins. @p source must already exist. + * @param symbol The symbol used for the transition. + * @param targets The set of target states where the transition ends. Each target must already exist. + * @param jump_mode Specifies the semantic of jump transitions (transitions with a length greater than 1). + */ + void add_transition_with_same_level_targets(State source, Symbol symbol, const StateSet& targets, JumpMode jump_mode = JumpMode::RepeatSymbol); + /** * @brief Inserts a word, which is created by interleaving parts from @p word_parts_on_levels, into the NFT * from a source state @p source to a target state @p target, creating new states along the path of @p word. @@ -913,13 +952,6 @@ Nft intersection(const Nft& lhs, const Nft& rhs, /** * @brief Composes two NFTs (lhs || rhs; read as "rhs after lhs"). * - * This function computes the composition of two NFTs, `lhs` and `rhs`, by aligning their synchronization levels. - * Transitions between two synchronization levels are ordered as follows: first the transitions of `lhs`, then - * the transitions of `rhs` followed by next synchronization level (if exists). By default, synchronization - * levels are projected out from the resulting NFT. - * - * Vectors of synchronization levels have to be non-empty and of the same size. - * * @param[in] lhs First transducer to compose. * @param[in] rhs Second transducer to compose. * @param[in] lhs_sync_levels Ordered vector of synchronization levels of the @p lhs. @@ -927,31 +959,49 @@ Nft intersection(const Nft& lhs, const Nft& rhs, * @param[in] project_out_sync_levels Whether we want to project out the synchronization levels. * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1) * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE. + * @param[in] composition_mode Mode of composition to use. Default is Auto, which selects the best mode based + * on the presence of jump transitions. General mode supports all NFTs, while FastNoJump + * mode is optimized for NFTs without jump transitions and with only one synchronization level. + * * @return A new NFT after the composition. */ Nft compose(const Nft& lhs, const Nft& rhs, const utils::OrdVector& lhs_sync_levels, const utils::OrdVector& rhs_sync_levels, bool project_out_sync_levels = true, - JumpMode jump_mode = JumpMode::RepeatSymbol); + JumpMode jump_mode = JumpMode::RepeatSymbol, + CompositionMode composition_mode = CompositionMode::Auto); /** * @brief Composes two NFTs (lhs || rhs; read as "rhs after lhs"). * - * This function computes the composition of two NFTs, `lhs` and `rhs`, by aligning their synchronization levels. - * Transitions between two synchronization levels are ordered as follows: first the transitions of `lhs`, then - * the transitions of `rhs` followed by next synchronization level (if exists). By default, synchronization - * levels are projected out from the resulting NFT. - * * @param[in] lhs First transducer to compose. * @param[in] rhs Second transducer to compose. * @param[in] lhs_sync_level The synchronization level of the @p lhs. * @param[in] rhs_sync_level The synchronization level of the @p rhs. - * @param[in] project_out_sync_levels Whether we wont to project out the synchronization levels. + * @param[in] project_out_sync_levels Whether we want to project out the synchronization levels. * @param[in] jump_mode Specifies if the symbol on a jump transition (a transition with a length greater than 1) * is interpreted as a sequence repeating the same symbol or as a single instance of the symbol followed by a sequence of @c DONT_CARE. + * @param[in] composition_mode Mode of composition to use. Default is Auto, which selects the best mode based + * on the presence of jump transitions. General mode supports all NFTs, while FastNoJump + * mode is optimized for NFTs without jump transitions and with only one synchronization level. + * * @return A new NFT after the composition. */ -Nft compose(const Nft& lhs, const Nft& rhs, Level lhs_sync_level = 1, Level rhs_sync_level = 0, bool project_out_sync_levels = true, JumpMode jump_mode = JumpMode::RepeatSymbol); +inline Nft compose(const Nft& lhs, const Nft& rhs, + const Level lhs_sync_level = 1, const Level rhs_sync_level = 0, + const bool project_out_sync_levels = true, + const JumpMode jump_mode = JumpMode::RepeatSymbol, + const CompositionMode composition_mode = CompositionMode::Auto) +{ + return compose( + lhs, rhs, + utils::OrdVector{ lhs_sync_level }, + utils::OrdVector{ rhs_sync_level }, + project_out_sync_levels, + jump_mode, + composition_mode + ); +} /** * @brief Concatenate two NFTs. diff --git a/include/mata/nft/types.hh b/include/mata/nft/types.hh index 12e1c359f..4febdb1b1 100644 --- a/include/mata/nft/types.hh +++ b/include/mata/nft/types.hh @@ -56,7 +56,14 @@ class Nft; ///< A non-deterministic finite transducer. enum class JumpMode { RepeatSymbol, ///< Repeat the symbol on the jump. - AppendDontCares ///< Append a sequence of DONT_CAREs to the symbol on the jump. + AppendDontCares, ///< Append a sequence of DONT_CAREs to the symbol on the jump. + NoJump ///< No jumps are allowed. +}; + +enum class CompositionMode { + General, ///< General composition mode for arbitrary number or synchronization levels and jump modes. + FastNoJump, ///< Fast composition mode for a single synchronization level and no jumps. + Auto ///< Automatically select the best composition mode based on the parameters. }; using ProductFinalStateCondition = mata::nfa::ProductFinalStateCondition; @@ -99,8 +106,9 @@ public: */ size_t num_of_levels{ DEFAULT_NUM_OF_LEVELS }; - // explicit Levels(const std::vector& levels): super{ levels }, num_of_levels{ num_of_levels_of(levels).value_or(DEFAULT_NUM_OF_LEVELS) } {} - // explicit Levels(std::vector&& levels): super{ std::move(levels) } { num_of_levels = num_of_levels_of(*this).value_or(DEFAULT_NUM_OF_LEVELS); } + // explicit Levels(std::initializer_list levels): super{ levels }, num_of_levels{ num_of_levels_of(levels).value_or(DEFAULT_NUM_OF_LEVELS) } {} + explicit Levels(const std::vector& levels): super{ levels }, num_of_levels{ num_of_levels_of(levels).value_or(DEFAULT_NUM_OF_LEVELS) } {} + explicit Levels(std::vector&& levels): super{ std::move(levels) } { num_of_levels = num_of_levels_of(*this).value_or(DEFAULT_NUM_OF_LEVELS); } explicit Levels(const size_t num_of_levels, std::vector levels = {}): super{ std::move(levels) }, num_of_levels{ num_of_levels } {} Levels() = default; Levels(size_t num_of_levels, size_t count, Level value = DEFAULT_LEVEL); diff --git a/src/applications/strings/noodlification.cc b/src/applications/strings/noodlification.cc index 824dbf770..ffe74776c 100644 --- a/src/applications/strings/noodlification.cc +++ b/src/applications/strings/noodlification.cc @@ -469,9 +469,9 @@ std::vector seg_nfa::noodlify_for_transducer( // we can do the following optimization. Let I1, ..., In be the input automata. Because T is homomorphic, // we can take the concatenation T(I1).T(I2)...T(In) connected with INPUT_DELIMITER instead of computing // the composition with concatenated_input_nft. - mata::nft::Nft concatenation{ mata::nft::compose(mata::nft::Nft(*input_automata[0]), *nft, 0, 0, false) }; + mata::nft::Nft concatenation{ mata::nft::compose(mata::nft::Nft(*input_automata[0]), *nft, 0, 0, false, mata::nft::JumpMode::NoJump) }; for (size_t i = 1; i < input_automata.size(); ++i) { - mata::nft::Nft composition = mata::nft::compose(mata::nft::Nft(*input_automata[i]), *nft, 0, 0, false); + mata::nft::Nft composition = mata::nft::compose(mata::nft::Nft(*input_automata[i]), *nft, 0, 0, false, mata::nft::JumpMode::NoJump); concatenation = mata::nft::algorithms::concatenate_eps(concatenation, composition, input_delimiter, true); } intersection = std::move(concatenation); @@ -480,7 +480,7 @@ std::vector seg_nfa::noodlify_for_transducer( // we intersect input nfa with nft on the input track, but we need to add INPUT_DELIMITER as an "epsilon transition" of nft add_self_loop_for_every_default_state(intersection, input_delimiter); - intersection = mata::nft::compose(concatenated_input_nft, intersection, 0, 0, false); + intersection = mata::nft::compose(concatenated_input_nft, intersection, 0, 0, false, mata::nft::JumpMode::NoJump); } intersection.trim(); @@ -491,7 +491,7 @@ std::vector seg_nfa::noodlify_for_transducer( // We also need to INPUT_DELIMITER as "epsilon transition" of the output nfa, so that we do not lose it. add_self_loop_for_every_default_state(concatenated_output_nft, input_delimiter); add_self_loop_for_every_default_state(intersection, output_delimiter); - intersection = mata::nft::compose(concatenated_output_nft, intersection, 0, 1, false); + intersection = mata::nft::compose(concatenated_output_nft, intersection, 0, 1, false, mata::nft::JumpMode::NoJump); intersection.trim(); if (intersection.final.empty()) { return {}; } diff --git a/src/applications/strings/replace.cc b/src/applications/strings/replace.cc index aed588ae6..075ee57a2 100644 --- a/src/applications/strings/replace.cc +++ b/src/applications/strings/replace.cc @@ -516,7 +516,7 @@ Nft ReluctantReplace::replace_regex(nfa::Nfa aut, const Word& replacement, Alpha const Nft dft_begin_marker{ begin_marker_nft(begin_marker_nfa(aut, alphabet), begin_marker) }; const Nft nft_reluctant_replace{ reluctant_leftmost_nft(std::move(aut), alphabet, begin_marker, replacement, replace_mode) }; - return compose(dft_begin_marker, nft_reluctant_replace); + return compose(dft_begin_marker, nft_reluctant_replace, 1, 0, true, mata::nft::JumpMode::NoJump); } Nft ReluctantReplace::replace_literal(const Word& literal, const Word& replacement, Alphabet const* const alphabet, @@ -551,7 +551,7 @@ Nft ReluctantReplace::replace_literal(const Word& literal, const Word& replaceme const Nft nft_literal_replace{ replace_literal_nft(literal, replacement, alphabet, end_marker, replace_mode) }; - return compose(nft_end_marker, nft_literal_replace); + return compose(nft_end_marker, nft_literal_replace, 1, 0, true, mata::nft::JumpMode::NoJump); } Nft ReluctantReplace::replace_symbol( diff --git a/src/nft/composition.cc b/src/nft/composition.cc index 1bf25bff0..cf39ffc59 100644 --- a/src/nft/composition.cc +++ b/src/nft/composition.cc @@ -2,14 +2,1031 @@ * @brief Composition of two NFTs. */ +#include +#include +#include #include "mata/nft/nft.hh" +#include "mata/nft/algorithms.hh" +#include "mata/utils/two-dimensional-map.hh" + using namespace mata::utils; -namespace mata::nft { -Nft compose( - const Nft& lhs, const Nft& rhs, const OrdVector& lhs_sync_levels, const OrdVector& rhs_sync_levels, - const bool project_out_sync_levels, const JumpMode jump_mode) { + +namespace { + using mata::Symbol; + using namespace mata::nft; + + /** + * Enum class for a state flag to indicate which synchronization + * types (synchronization on epsilon or symbol) can be reached from the state. + * The synchronization type helps to determine if a state from lhs can + * at some point in the next levels synchronize with a state from rhs. + * The following table shows all possible combinations of synchronization types + * for lhs and rhs states, and whether they can synchronize or if one of them will wait + * because there is an EPSILON on the synchronization in the other that it + * could not synchronize with. + * + * You can nottice that we do not want to synchronize on EPSILONs. + * This is a part of the optimization to avoid creating redundant EPSILON transitions. + * For more defails, see https://cs.nyu.edu/~mohri/pub/nway.pdf Figure 3. + * || RHS sync type + * LHS sync type || ONLY_ON_SYMBOL | ONLY_ON_EPSILON | ON_EPSILON_AND_SYMBOL + * ======================||================|=================|====================== + * || synchornize | | synchornize + * ONLY_ON_SYMBOL || | wait on LHS | wait on LHS + * || | | + * ----------------------||----------------|-----------------|---------------------- + * || | | + * ONLY_ON_EPSILON || | lait on LHS | lait on LHS + * || wait on RHS | wait on RHS | wait on RHS + * ----------------------||----------------|-----------------|---------------------- + * || synchronize | | synchornize + * ON_EPSILON_AND_SYMBOL || | wait on LHS | wait on LHS + * || wait on RHS | wait on RHS | wait on RHS + * ================================================================================= + */ + enum class SynchronizationType : uint8_t { + UNDEFINED = 0b0000'0000, ///< Default value. Or used if we are past the synchronization. + ONLY_ON_SYMBOL = 0b0000'0001, ///< Synchronization on EPSILON. + ONLY_ON_EPSILON = 0b0000'0010, ///< Synchronization on symbol. + ON_EPSILON_AND_SYMBOL = 0b0000'0011, ///< Synchronization on EPSILON and symbol. + UNDER_COMPUTATION = 0b0000'0100 ///< The synchronization is being computed (only a helper value). + }; + inline SynchronizationType operator|(SynchronizationType lhs, SynchronizationType rhs) { + return static_cast(static_cast(lhs) | static_cast(rhs)); + } + inline SynchronizationType& operator|=(SynchronizationType& lhs, SynchronizationType rhs) { + lhs = lhs | rhs; + return lhs; + } + inline bool exist_intersection(SynchronizationType lhs, SynchronizationType rhs) { + return (static_cast(lhs) & static_cast(rhs)) != 0; + } + inline bool exist_synchronization(SynchronizationType lhs, SynchronizationType rhs) { + return lhs != SynchronizationType::ONLY_ON_EPSILON && rhs != SynchronizationType::ONLY_ON_EPSILON; + } + inline bool exist_epsilon(SynchronizationType s) { + return s != SynchronizationType::ONLY_ON_SYMBOL; + } + + /** + * @brief A class to hold properties related to synchronization during the composition of NFTs. + * This simplifies passing multiple synchronization-related parameters. + */ + class SynchronizationProperties { + public: + const Nft& nft; + const Level sync_level; + const size_t num_of_levels_before_sync; + const size_t num_of_levels_after_sync; + std::vector sync_types_v; + + SynchronizationProperties(const Nft& nft, const Level sync_level) + : nft(nft), + sync_level(sync_level), + num_of_levels_before_sync(sync_level), + num_of_levels_after_sync(nft.levels.num_of_levels - sync_level - 1), + sync_types_v(nft.num_of_states(), SynchronizationType::UNDEFINED) + { + get_synchronization_types(); + } + + private: + /** + * @brief For each state, sets the type of synchronization that follows. + * + * The scope of the synchronization type ends at the next zero-level state. + * Each state has a synchronization type that is a combination of the + * synchronization types of its children. + */ + void get_synchronization_types() { + const size_t num_of_states = nft.num_of_states(); + for (State root = 0; root < num_of_states; ++root) { + if (nft.levels[root] != 0) { + continue; // Skip states not on the zero level. + } + + // To perform the computation, which is a post-order traversal, we do not + // use recursion but a stack for better performance. To determine if a parent state + // has already been visited, we use the helper value SynchronizationType::UNDER_COMPUTATION. + std::stack stack; + stack.push(root); + while (!stack.empty()) { + const State state = stack.top(); + stack.pop(); + const Level state_level = nft.levels[state]; + const StatePost& state_post = nft.delta[state]; + SynchronizationType current_sync_type = sync_types_v[state]; + assert(current_sync_type == SynchronizationType::UNDEFINED || current_sync_type == SynchronizationType::UNDER_COMPUTATION); + + // If it has been visited, then we know that it has already been computed for its children. + if (current_sync_type == SynchronizationType::UNDER_COMPUTATION) { + // Combine the synchronization types of its children. + current_sync_type = SynchronizationType::UNDEFINED; + for (const SymbolPost& symbol_post : state_post) { + for (const State target : symbol_post.targets) { + // Skip fast EPSILON transitions. + if (symbol_post.symbol == EPSILON && nft.levels.num_of_levels != 1 && nft.levels[target] == 0) { + assert(state_level == 0); + continue; + } + assert(nft.levels[target] > nft.levels[state]); + current_sync_type |= sync_types_v[target]; + } + } + sync_types_v[state] = current_sync_type; + continue; // We already visited its children. + } + + // If we are on the sync level, we can determine the synchronization type. + if (state_level == sync_level) { + const auto epsilon_post_it = state_post.find(EPSILON); + if (epsilon_post_it != state_post.end()) { + // We don't want to count fast EPSILON transitions. + const bool has_not_only_fast_epsilon = ( + state_level != 0 || nft.levels.num_of_levels == 1 || + std::any_of( + epsilon_post_it->targets.cbegin(), + epsilon_post_it->targets.cend(), + [this](State target) { + return nft.levels[target] != 0; + } + ) + ); + if (has_not_only_fast_epsilon) { + current_sync_type = SynchronizationType::ONLY_ON_EPSILON; + } + if (state_post.size() > 1) { + current_sync_type |= SynchronizationType::ONLY_ON_SYMBOL; + } + } else if (!state_post.empty()) { + current_sync_type = SynchronizationType::ONLY_ON_SYMBOL; + } + sync_types_v[state] = current_sync_type; + continue; // No need to visit its children. + } + + // We need to visit its children. + sync_types_v[state] = SynchronizationType::UNDER_COMPUTATION; // Mark this state as under computation. + stack.push(state); // Push it back to the stack to compute it later. + for (const SymbolPost& symbol_post : state_post) { + for (const State target : symbol_post.targets) { + // Skip fast EPSILON transitions. + if (symbol_post.symbol == EPSILON && nft.levels.num_of_levels != 1 && nft.levels[target] == 0) { + assert(state_level == 0); + continue; + } + assert(nft.levels[target] > nft.levels[state]); + assert(sync_types_v[target] != SynchronizationType::UNDER_COMPUTATION); + if (sync_types_v[target] != SynchronizationType::UNDEFINED) { + current_sync_type |= sync_types_v[target]; + } else { + stack.push(target); // Push the target state onto the stack to visit it. + } + } + } + } + } + + assert(std::all_of(sync_types_v.begin(), sync_types_v.end(), + [](SynchronizationType type) { return type != SynchronizationType::UNDER_COMPUTATION; })); + } + }; +} + +namespace mata::nft +{ + +// Dispatch function for composition modes. +Nft compose(const Nft& lhs, + const Nft& rhs, + const utils::OrdVector& lhs_sync_levels, + const utils::OrdVector& rhs_sync_levels, + const bool project_out_sync_levels, + const JumpMode jump_mode, + const CompositionMode composition_mode) +{ + switch (composition_mode) { + case CompositionMode::FastNoJump: + if (jump_mode != JumpMode::NoJump) { + throw std::invalid_argument("FastNoJump composition mode only supports NoJump jump mode."); + } + if (lhs_sync_levels.size() != 1 || rhs_sync_levels.size() != 1) { + throw std::invalid_argument("FastNoJump composition mode only supports a single synchronization level per NFT."); + } + return algorithms::compose_fast_no_jump(lhs, rhs, lhs_sync_levels.front(), rhs_sync_levels.front(), project_out_sync_levels); + case CompositionMode::Auto: + if (jump_mode == JumpMode::NoJump && lhs_sync_levels.size() == 1) { + return algorithms::compose_fast_no_jump(lhs, rhs, lhs_sync_levels.front(), rhs_sync_levels.front(), project_out_sync_levels); + } + [[fallthrough]]; + case CompositionMode::General: + default: + return algorithms::compose_general(lhs, rhs, lhs_sync_levels, rhs_sync_levels, project_out_sync_levels, jump_mode); + } +} + +Nft algorithms::compose_fast_no_jump(const Nft& lhs, const Nft& rhs, const Level lhs_sync_level, const Level rhs_sync_level, const bool project_out_sync_levels) { + assert(lhs_sync_level < lhs.levels.num_of_levels && rhs_sync_level < rhs.levels.num_of_levels); + + // Check that there are only explicit synchronization transitions of length 1 with exception for fast EPSILON transitions. + assert( + std::all_of( + lhs.delta.transitions().begin(), + lhs.delta.transitions().end(), + [&](const Transition& transition) { + return static_cast((lhs.levels[transition.source] + 1) % lhs.levels.num_of_levels) == lhs.levels[transition.target] || + (lhs.levels[transition.source] == 0 && lhs.levels[transition.target] == 0 && transition.symbol == EPSILON); + } + ) + ); + + // Check that there are only explicit synchronization transitions of length 1 with exception for fast EPSILON transitions. + assert( + std::all_of( + rhs.delta.transitions().begin(), + rhs.delta.transitions().end(), + [&](const Transition& transition) { + return static_cast((rhs.levels[transition.source] + 1) % rhs.levels.num_of_levels) == rhs.levels[transition.target] || + (rhs.levels[transition.source] == 0 && rhs.levels[transition.target] == 0 && transition.symbol == EPSILON); + } + ) + ); + + // Number of Levels and States + const size_t lhs_num_of_states = lhs.num_of_states(); + const size_t rhs_num_of_states = rhs.num_of_states(); + const size_t result_num_of_levels = lhs.levels.num_of_levels + rhs.levels.num_of_levels - (project_out_sync_levels ? (2) : 1); + assert(result_num_of_levels > 0); + + // Initialize the synchronization properties for both NFTs. + const SynchronizationProperties lhs_sync_props(lhs, lhs_sync_level); + const SynchronizationProperties rhs_sync_props(rhs, rhs_sync_level); + + Nft result; + result.levels.num_of_levels = result_num_of_levels; + // Use composition storage without tracking inverted indices, + // because waiting in virtual states would spoil the inverse mapping. + TwoDimensionalMap composition_storage(lhs_num_of_states, rhs_num_of_states); + std::unordered_map waiting_state_storage; + // I use a queue for the worklist to process states in a breadth-first manner. + // This helps the branch prediction in the CPU because all processed states + // are likely to be at the same level and thus enter the same branch. + std::queue> worklist; + + /** + * @brief Efficiently inserts a symbol post into the delta of the result NFT. + * + * @param source The source state of the transition. + * @param symbol_post The symbol post to insert. + */ + auto insert_symbol_post_to_delta = [&](const State source, const SymbolPost& symbol_post) { + assert(!symbol_post.targets.empty()); + auto &mutable_state_post = result.delta.mutable_state_post(source); + auto symbol_post_it = mutable_state_post.find(symbol_post.symbol); + if (symbol_post_it != mutable_state_post.end()) { + // The symbol post already exists, just add the targets. + symbol_post_it->targets.insert(symbol_post.targets); + return; + } + // The symbol post does not exist. + if (mutable_state_post.empty() || mutable_state_post.back().symbol < symbol_post.symbol) { + // It is the greatest symbol, just add it to the end. + mutable_state_post.push_back(std::move(symbol_post)); + return; + } + // Use insert method to insert at the correct position. + mutable_state_post.insert(std::move(symbol_post)); + }; + + /** + * @brief Creates a chain of EPSILON transitions of the given length starting from the source state. + * + * @param source The source state from which the EPSILON transitions will start. + * @param common_path_length The length of the EPSILON transition chain to create. + * @return The last state in the created EPSILON transition chain. + */ + auto create_epsilon_transition_with_common_path = [&](const State source, const size_t common_path_length) { + assert(source < result.num_of_states()); + State current_source = source; + Level current_level = result.levels[current_source]; + for (size_t i = 0; i < common_path_length; ++i) { + SymbolPost symbol_post{ EPSILON }; + const State new_composition_state = result.add_state_with_level(++current_level); + assert(current_level < result.levels.num_of_levels); + symbol_post.push_back(new_composition_state); + insert_symbol_post_to_delta(current_source, symbol_post); + current_source = new_composition_state; + } + return current_source; + }; + + /** + * @brief Creates an EPSILON transition from source to target, possibly with a common path in between. + * @param source The source state of the EPSILON transition. + * @param target The target state of the EPSILON transition. + */ + auto create_epsilon_transition_with_target = [&](const State source, const State target) { + assert(source < result.num_of_states() && target < result.num_of_states()); + const Level source_level = result.levels[source]; + const Level target_level = result.levels[target]; + const size_t common_path_length = (target_level == 0 ? result.levels.num_of_levels : target_level) - source_level - 1; + State internal_state = create_epsilon_transition_with_common_path(source, common_path_length); + SymbolPost symbol_post{ EPSILON }; + symbol_post.insert(target); + insert_symbol_post_to_delta(internal_state, symbol_post); + }; + + /** + * @brief Creates a new composition state for the given pair of states, if it does not already exist. + * + * @param first The first state (from lhs or rhs). + * @param second The second state (from rhs or lhs). + * @param level The level of the new composition state. + * @param is_first_lhs If true, @p first is from the lhs NFT; otherwise, it is from the rhs NFT. + * @param composition_state_to_add If provided, this is the state to be added to the result NFT; + * if not provided, a new state will be created. + * + * @return The composition state for the given pair of states. + */ + auto create_composition_state = [&](const State first, + const State second, + const Level level, + const bool is_first_lhs = true, + const State composition_state_to_add = Limits::max_state) + { + const auto key = is_first_lhs ? std::make_pair(first, second) + : std::make_pair(second, first); + + // Try to find the entry in the state map. + const State found_state = composition_storage.get(key.first, key.second); + if (found_state != Limits::max_state) { + assert(result.levels[found_state] == level); + return found_state; + } + assert(composition_state_to_add == Limits::max_state || result.levels[composition_state_to_add] == level); + + // If not found, add a new state to the result NFT. + // Since the key pair was not found in the map, we can be certain that the state is not yet in the worklist. + const State new_state = (composition_state_to_add != Limits::max_state) ? composition_state_to_add + : result.add_state_with_level(level); + composition_storage.insert(key.first, key.second, new_state); + if (level == 0) { + // If the level is zero, check for final states and add the state to the worklist. + if ((is_first_lhs && lhs.final.contains(first) && rhs.final.contains(second)) || + (!is_first_lhs && rhs.final.contains(first) && lhs.final.contains(second))) + { + result.final.insert(new_state); + } + } + worklist.push(key); + return new_state; + }; + + /** + * @brief Perform the synchronization of the LHS and RHS at the given state pair. + * + * @param composition_state The state in the composition NFT from which the synchronization result will proceed. + * @param lhs_state The state in the LHS NFT being synchronized. + * @param rhs_state The state in the RHS NFT being synchronized. + * @param reconnect If true, the synchronization will use the specified symbol on the resulting + * synchronization transition, virtually reconnecting the predecessors of + * the synchronization level to its successors; otherwise, it will simply + * synchronize and keep or remove the synchronization level depending on + * the project_out_sync_levels flag. + * @param reconnection_symbol The symbol to use for the reconnection transition if reconnect is true. + */ + auto synchronize = [&](const State composition_state, + const State lhs_state, + const State rhs_state, + const bool reconnect = false, + const Symbol reconnection_symbol = Limits::max_symbol) + { + const Level composition_state_level = result.levels[composition_state]; + const Level composition_target_level = static_cast((composition_state_level + 1) % result.levels.num_of_levels); + // When projecting out the synchronization levels, and we do not want to connect their + // predecessors to their successors, we simply perform the synchronization, note the reached targets, + // and remove (vanish) the synchronization level and its transition from the result NFT. + const bool vanish_sync_level = !reconnect && project_out_sync_levels; + + // Helper function to combine LHS and RHS targets over the given symbol. + auto combine_targets = [&](const StateSet& lhs_sync_targets, const StateSet& rhs_sync_targets, const Symbol symbol) { + if (!vanish_sync_level) { + // Do a standard combination of targets. + SymbolPost symbol_post{ symbol }; + for (const State lhs_sync_target : lhs_sync_targets) { + for (const State rhs_sync_target : rhs_sync_targets) { + symbol_post.insert(create_composition_state(lhs_sync_target, + rhs_sync_target, + composition_target_level)); + } + } + insert_symbol_post_to_delta(composition_state, symbol_post); + return; + } + + // The synchronization level will vanish. + // We know that there is at least one transition in LHS or RHS after the synchronization. + // We are going to use those transitions to connect composition_state to their targets. + const bool is_remainging_transition_in_lhs = lhs_sync_level + 1 < lhs.levels.num_of_levels; + assert(is_remainging_transition_in_lhs || rhs_sync_level + 1 < rhs.levels.num_of_levels); + + + const StateSet& moving_sync_targets = is_remainging_transition_in_lhs ? lhs_sync_targets : rhs_sync_targets; + const StateSet& static_sync_targets = is_remainging_transition_in_lhs ? rhs_sync_targets : lhs_sync_targets; + const Nft& moving_nft = is_remainging_transition_in_lhs ? lhs : rhs; + + mata::utils::SynchronizedExistentialIterator::const_iterator> moving_sync_iterator(moving_sync_targets.size()); + for (const State moving_sync_target : moving_sync_targets) { + mata::utils::push_back(moving_sync_iterator, moving_nft.delta[moving_sync_target]); + } + while (moving_sync_iterator.advance()) { + const std::vector& same_symbol_posts{ moving_sync_iterator.get_current() }; + assert(!same_symbol_posts.empty()); + + const Symbol moving_symbol = same_symbol_posts[0]->symbol; + SymbolPost symbol_post{ moving_symbol }; + for (const auto& moving_next_targets : same_symbol_posts) { + for (const State moving_next_target : moving_next_targets->targets) { + for (const State static_sync_target : static_sync_targets) { + symbol_post.insert(create_composition_state(moving_next_target, + static_sync_target, + composition_target_level, + is_remainging_transition_in_lhs)); + } + } + } + insert_symbol_post_to_delta(composition_state, symbol_post); + } + }; + + // Helper function to perform synchronization on DONT_CARE transitions. + auto synchronization_on_dont_care = [&](const State dont_care_state, const State other_state, const bool is_dont_care_lhs) { + const Nft& dont_care_nft = is_dont_care_lhs ? lhs : rhs; + const Nft& other_nft = is_dont_care_lhs ? rhs : lhs; + + auto dont_care_sync_it = dont_care_nft.delta[dont_care_state].find(DONT_CARE); + if (dont_care_sync_it != dont_care_nft.delta[dont_care_state].end()) { + for (const SymbolPost& symbol_post : other_nft.delta[other_state]) { + if (symbol_post.symbol == EPSILON) { + // We don't want to synchronize DONT_CARE with EPSILON. + continue; + } + const Symbol symbol = reconnect ? reconnection_symbol : symbol_post.symbol; + if (is_dont_care_lhs) { + combine_targets(dont_care_sync_it->targets, symbol_post.targets, symbol); + } else { + combine_targets(symbol_post.targets, dont_care_sync_it->targets, symbol); + } + } + } + }; + + // The body of the synchronization. + mata::utils::SynchronizedUniversalIterator::const_iterator> sync_iterator(2); + mata::utils::push_back(sync_iterator, lhs.delta[lhs_state]); + mata::utils::push_back(sync_iterator, rhs.delta[rhs_state]); + while (sync_iterator.advance()) { + const std::vector& same_symbol_posts{ sync_iterator.get_current() }; + assert(same_symbol_posts.size() == 2); // One move per state in the pair. + const Symbol symbol = reconnect ? reconnection_symbol : same_symbol_posts[0]->symbol; + + if (same_symbol_posts[0]->symbol == EPSILON) { + // We don't want to synchronize EPSILON with EPSILON. + // This creates a redundant EPSILON transitions in this implementation. + // This is an optimization according to https://cs.nyu.edu/~mohri/pub/nway.pdf Figure 3. + continue; + } + combine_targets(same_symbol_posts[0]->targets, same_symbol_posts[1]->targets, symbol); + + } + + synchronization_on_dont_care(lhs_state, rhs_state, true); + synchronization_on_dont_care(rhs_state, lhs_state, false); + }; + + + /** + * @brief Copy transitions from the copy NFT to the composition NFT. + * + * @param composition_state The source state in the composition NFT from which the transitions will be connected. + * @param copy_state The state in the copy NFT from which the transitions will be copied. + * @param stationar_state The state in the other NFT (the stationary NFT) that does not move. + * @param is_copy_state_lhs If true, the copy_state is from the LHS NFT; otherwise, it is from the RHS NFT. + * @param waiting_worklist If set, the function is called from the waiting simulation, + * meaning that we are waiting in the virtual loop at the stationary state, + * and we will use the waiting_worklist to store the next state pairs. + */ + auto copy_transition = [&](const State composition_state, + const State copy_state, + const State stationar_state, + const bool is_copy_state_lhs, + std::queue>* waiting_worklist = nullptr) + { + const SynchronizationProperties& copy_sync_props = is_copy_state_lhs ? lhs_sync_props + : rhs_sync_props; + const SynchronizationProperties& stationar_sync_props = is_copy_state_lhs ? rhs_sync_props + : lhs_sync_props; + const Nft& copy_nft = copy_sync_props.nft; + const Level composition_state_level = result.levels[composition_state]; + const Level copy_state_level = copy_nft.levels[copy_state]; + const Level stationar_state_level = stationar_sync_props.nft.levels[stationar_state]; + const Level copy_sync_level = copy_sync_props.sync_level; + const std::vector& copy_sync_types = copy_sync_props.sync_types_v; + const SynchronizationType stationar_state_sync_type = stationar_sync_props.sync_types_v[stationar_state]; + + + // It may happen that + // 1) we want to project out synchronization levels, + // 2) there are no transitions after the synchronization level in both NFTs, and + // 3) targets of the copy_state are at the synchronization level. + // In this case, we are going to need to perform synchronization here and use + // the copied transitions to connect directly to the next zero-level states. + const bool handle_synchronization_in_place = project_out_sync_levels && + stationar_sync_props.num_of_levels_after_sync == 0 && + copy_sync_props.num_of_levels_after_sync == 0 && + (!is_copy_state_lhs || stationar_sync_props.num_of_levels_before_sync == 0) && + (waiting_worklist != nullptr || stationar_state_level == stationar_sync_props.sync_level); + + for (const SymbolPost& copy_symbol_post : copy_nft.delta[copy_state]) { + SymbolPost symbol_post{ copy_symbol_post.symbol }; + for (const State copy_target : copy_symbol_post.targets) { + if (copy_symbol_post.symbol == EPSILON && copy_state_level == 0 && copy_nft.levels.num_of_levels != 1 && copy_nft.levels[copy_target] == 0) { + // Skip fast EPSILON transitions. + continue; + } + + const SynchronizationType copy_target_sync_type = copy_sync_types[copy_target]; + // It makes sense to continue only if we believe that we will not get stuck + // later due to an inability to synchronize. When this function is called + // from the waiting simulation, we are interested in onyl synchronizations on EPSILON. + const bool can_synchronize_in_the_future = ( + waiting_worklist != nullptr ? exist_epsilon(copy_target_sync_type) || + copy_nft.levels[copy_target] == 0 // End of the waiting loop. + : exist_synchronization(stationar_state_sync_type, copy_target_sync_type) || + stationar_state_sync_type == SynchronizationType::UNDEFINED || + copy_target_sync_type == SynchronizationType::UNDEFINED || + copy_nft.levels[copy_target] == 0 + ); + if (!can_synchronize_in_the_future) { + // There is no way we would be able to synchronize in the future. + // We do not need to explore this path further. + continue; + } + + const Level target_level = copy_nft.levels[copy_target]; + const size_t trans_len = (target_level == 0 ? copy_nft.levels.num_of_levels : target_level) - copy_state_level; + assert(target_level == 0 || target_level > copy_state_level); + assert(trans_len > 0); + + if (handle_synchronization_in_place && target_level == copy_sync_level) { + // The target is at the synchronization level that will be projected out. + // We know that there are no transitions after the synchronization level + // in any of the NFTs. Therefore, we must perform the synchronization here + // and connect this transition directly to the next zero-level state. + if (waiting_worklist != nullptr) { + // We have been called from the waiting simulation. + // We are waiting in the stationary state. + // During this, only EPSILON synchronizations are allowed. + const auto& copy_eps_symbol_post = copy_nft.delta[copy_target].find(EPSILON); + assert(copy_eps_symbol_post != copy_nft.delta[copy_target].end()); + for (const State sync_target : copy_eps_symbol_post->targets) { + assert(copy_nft.levels[sync_target] == 0); + symbol_post.insert(create_composition_state(sync_target, + stationar_state, + 0, + is_copy_state_lhs)); + } + // We do not need to add new pairs to the waiting_worklist, + // because, if necessary, they have already been added to the main + // worklist by the create_composition_state function. + } else { + // We encountered a standard synchronization and need to synchronize the LHS and RHS. + // Call the synchronization function with the reconnection parameters set. + // This point can be reached only if there is not transition in the LHS and we are + // copying transitions from the RHS, or if the synchronization in the RHS occurs + // on the 0-level, and we are copying transitions from the LHS. + assert(!is_copy_state_lhs || rhs_sync_level == 0); + if (!is_copy_state_lhs) { + synchronize(composition_state, stationar_state, copy_target, true, copy_symbol_post.symbol); + } else { + synchronize(composition_state, copy_target, stationar_state, true, copy_symbol_post.symbol); + } + } + } else { + // We are not at a synchronization point. + // We just need to copy the transition. + const Level new_composition_state_level = static_cast((composition_state_level + trans_len) % result.levels.num_of_levels); + if (waiting_worklist != nullptr && new_composition_state_level != 0) { + // We are not connecting to the zero-level state, and we were + // called from the waiting simulation. Therefore, we need to create an auxiliary state + // that will not be tracked in the composition_storage. We cannot use composition_storage + // because, while waiting in the stationary state, we are not exactly at that state, + // but rather in virtual (nonexistent) states of the waiting loop over it. + State new_composition_state; + if (waiting_state_storage.contains(copy_target)) { + new_composition_state = waiting_state_storage[copy_target]; + } else { + new_composition_state = result.add_state_with_level(new_composition_state_level); + waiting_state_storage[copy_target] = new_composition_state; + } + symbol_post.push_back(new_composition_state); + // Sometimes, the running root state gets pushed to the worklist again. We need to handle it during the pop. + waiting_worklist->push({ new_composition_state, copy_target }); + } else { + // Just copy this transition. + symbol_post.insert(create_composition_state(copy_target, + stationar_state, + new_composition_state_level, + is_copy_state_lhs)); + } + } + } + if (!symbol_post.targets.empty()) { + insert_symbol_post_to_delta(composition_state, symbol_post); + } + } + }; + + /** + * @brief Models the "waiting" in one of the NFTs when it cannot synchronize + * with the other NFT doe to a lacking EPSILON on the synchronization level. + * + * For example, if there is an EPSILON transition at the synchronization level + * in the RHS, and the LHS cannot synchronize on it, then the LHS must "wait" + * in its root (zero-level) state that precedes the synchronization. Meanwhile, + * the RHS continues from its corresponding root state, traversing the problematic + * EPSILON synchronization to the next zero-level state. The RHS behaves as if it + * is interleaving with the LHS transitions (LHS transitions always occur before RHS + * transitions), but it will insert an EPSILON for each such transition from the LHS. + * + * A special case arises when we want to project out synchronization levels, + * but there are no transitions following them in either the LHS or RHS (i.e., + * the synchronization level is the last level in both NFTs). In this situation, + * one state before the synchronization level, we need to connect the successors + * of such states to the zero-level state that follows the synchronization level. + * + * @param composition_root_state The root state of the composition NFT. + * @param waiting_root_state The root state of the NFT that is waiting (either LHS or RHS). + * @param running_root_state The root state of the NFT that is running (either LHS or RHS). + * @param is_lhs_waiting If true, the waiting root is from the LHS; + * otherwise, it is from the RHS. + */ + auto model_waiting = [&](const State composition_root_state, + const State waiting_root_state, + const State running_root_state, + const bool is_lhs_waiting) + { + waiting_state_storage.clear(); + const SynchronizationProperties& running_sync_props = is_lhs_waiting ? rhs_sync_props + : lhs_sync_props; + const SynchronizationProperties& waiting_sync_props = is_lhs_waiting ? lhs_sync_props + : rhs_sync_props; + const Level sync_level = running_sync_props.sync_level; + const Levels& running_levels = running_sync_props.nft.levels; + const Delta& running_delta = running_sync_props.nft.delta; + const size_t running_num_of_levels = running_sync_props.nft.levels.num_of_levels; + const size_t running_trans_after_sync = running_sync_props.num_of_levels_after_sync; + const size_t waiting_trans_before_sync = waiting_sync_props.num_of_levels_before_sync; + const size_t waiting_trans_after_sync = waiting_sync_props.num_of_levels_after_sync; + // EPSILON synchronization is handled differently here than in the main loop. + // To avoid redundant transitions caused by early branching, we replace each + // EPSILON synchronization with N EPSILON transitions, where: + // - Add waiting_trans_before_sync to N if NOT waiting in LHS + // (RHS transitions go after LHS, just before the synchronization). + // - Add waiting_trans_after_sync to N if waiting in LHS, or if there are no + // running transitions after the synchronization. + // - Add 1 to N if synchronization levels are NOT being projected out. + // The first N-1 EPSILON transitions are common for all targets, + // and only the last EPSILON transition is used to connect to the appropriate targets. + + const size_t num_of_epsilons_to_replace_sync = ( + (is_lhs_waiting + ? 0 + : waiting_trans_before_sync) + + ((is_lhs_waiting || running_trans_after_sync == 0) + ? waiting_trans_after_sync + : 0) + + (project_out_sync_levels + ? 0 + : 1) + ); + + // A special case we need to handle here. + // In some cases, the running NFT has only one level. + // This can happen when applying NFA to NFT. In that case, + // we can and need to simply add EPSILON transitions to the targets + // of the EPSILON transitions from the running root state. + if (running_num_of_levels == 1) { + assert(num_of_epsilons_to_replace_sync > 0); + const auto epsilon_target_it = running_delta[running_root_state].find(EPSILON); + // There has to be some EPSILON transition. Otherwise, there would be no reason to wait. + assert(epsilon_target_it != running_delta[running_root_state].end()); + StateSet new_composition_targets; + State new_composition_state = create_epsilon_transition_with_common_path(composition_root_state, result.levels.num_of_levels - 1); + SymbolPost symbol_post{ EPSILON }; + for (const State epsilon_target : epsilon_target_it->targets) { + assert(running_levels[epsilon_target] == 0); + symbol_post.insert(create_composition_state(waiting_root_state, + epsilon_target, + 0, + is_lhs_waiting)); + } + // This function ensures that the transitions are added in the most optimal way. + // It creates one common path for all targets and then use only the last transitions of + // that path to connect to all targets. + insert_symbol_post_to_delta(new_composition_state, symbol_post); + return; + } + + // Initialization of the local worklist. + // I chose to use a queue instead of a stack to help the branch predictor + // with conditions inside the loop. With the queue, the algorithm hits the + // same branch more ofthen, because all states being explored advance "together". + std::queue> worklist; + State first_composition_state = composition_root_state; + if (is_lhs_waiting && waiting_trans_before_sync > 0) { + // Since LHS is waiting and LHS transitions have to be put before + // RHS transitions, we now add waiting_trans_before_sync EPSILON + // transitions. Doing this here simplifies the conditions in the loop below. + first_composition_state = create_epsilon_transition_with_common_path(composition_root_state, waiting_trans_before_sync); + } + worklist.push({ first_composition_state, running_root_state }); + + // The main loop of the waiting simulation. + while (!worklist.empty()) { + auto [composition_state, running_state] = worklist.front(); + worklist.pop(); + const Level running_state_level = running_levels[running_state]; + // If the synchronization level is on 0. Than we can be careful to not use it + // again when encountering next zero-level states in the running NFT. + const bool first_running_transition = (running_state == running_root_state && composition_state == first_composition_state); + const bool is_sync_level = running_state_level == sync_level && (running_state_level != 0 || first_running_transition); + if (is_sync_level) { + // We are at the synchronization level. + const bool is_last_running_transition = (running_state_level == running_sync_props.nft.levels.num_of_levels - 1); + + // It cannot happen that the synchronization level is projected out + // and there are no other transitions to add before reaching the next zero-level state. + // This is because such a scenario would already be handled by the copy_transition function. + assert(!project_out_sync_levels || !is_last_running_transition || waiting_trans_after_sync > 0 || + (!is_lhs_waiting && waiting_sync_props.num_of_levels_before_sync > 0)); + + if (num_of_epsilons_to_replace_sync > 1) { + // The synchronization will be replaced by an EPSILON transition anyway. + // To reduce the number of redundant EPSILON transitions in the resulting NFT, + // we can add N-1 EPSILON transitions now, and then use the last one to connect + // to the adequate target state, where N is num_of_epsilons_to_replace_sync. + composition_state = create_epsilon_transition_with_common_path(composition_state, num_of_epsilons_to_replace_sync - 1); + } + + // Do the EPSILON synchronization. + // We cannot use the synchronize function here, because we want to + // focus only on the EPSILON transitions. + const auto& running_epsilon_post_it = running_delta[running_state].find(EPSILON); + // There should be an EPSILON transition. It has been told by the SynchronizationType. + assert(running_epsilon_post_it != running_delta[running_state].end()); + SymbolPost epsilon_symbol_post{ EPSILON }; + for (const State running_epsilon_target : running_epsilon_post_it->targets) { + if (running_state_level == 0 && running_num_of_levels != 1 && running_levels[running_epsilon_target] == 0) { + // Skip fast EPSILON transitions. + continue; + } + assert(running_levels[running_epsilon_target] == 0 || running_levels[running_epsilon_target] > running_state_level); + if (num_of_epsilons_to_replace_sync == 0 && !is_last_running_transition) { + // This synchronization level is being projected out (it will vanish). + // There are no EPSILON transitions to add before or after the synchronization level. + // However, we are sure, that there will be a least one "running" transition after this. + worklist.push({ composition_state, running_epsilon_target }); + } else if (is_last_running_transition) { + // We are connecting to the zero-level state, therefore we have to + // create a new composition state that will be put into the main worklist + // (side effect of the create_composition_state). + assert(result.levels[composition_state] + 1 == result.levels.num_of_levels); + assert(result.levels[composition_state] + (num_of_epsilons_to_replace_sync >= 1 ? 1 : 0) == result.levels.num_of_levels); + epsilon_symbol_post.insert(create_composition_state(waiting_root_state, + running_epsilon_target, + 0, + is_lhs_waiting)); + } else { + // We are connecting to the next state in the waiting loop, + // so we simply add a transition to the next state and + // continue the waiting. + assert(result.levels[composition_state] + 1 < result.levels.num_of_levels); + State new_composition_state; + if (waiting_state_storage.contains(running_epsilon_target)) { + new_composition_state = waiting_state_storage[running_epsilon_target]; + } else { + new_composition_state = result.add_state_with_level(result.levels[composition_state] + 1); + waiting_state_storage[running_epsilon_target] = new_composition_state; + } + // const State new_composition_state = result.add_state_with_level(result.levels[composition_state] + 1); + epsilon_symbol_post.push_back(new_composition_state); + worklist.push({ new_composition_state, running_epsilon_target }); + } + } + if (!epsilon_symbol_post.targets.empty()) { + insert_symbol_post_to_delta(composition_state, epsilon_symbol_post); + } + } else if (running_state_level == 0 && !first_running_transition) { + // We are at a leaf zero-level state in the running NFT. + // We will create a connection to the zero-level state in the composition NFT + // and continue exploring that state in the main composition loop + // (i.e., we push it to the main worklist, if not already visited). + // Note: This situation can only occur if the waiting NFT is the RHS, + // because RHS transitions follow LHS transitions. Moreover, the last + // transition in the running LHS NFT should not be at the synchronization + // level; otherwise, it would be handled by the condition above. + assert(!is_lhs_waiting); + assert(sync_level != running_sync_props.nft.levels.num_of_levels - 1); + assert(waiting_trans_after_sync > 0); + assert((result.levels[composition_state] + waiting_trans_after_sync) == result.levels.num_of_levels); + create_epsilon_transition_with_target(composition_state, + create_composition_state(running_state, + waiting_root_state, + 0)); + }else { + // We are at an internal (non-sync) level in the running NFT. + // We can simply copy the transitions to the next states. + // We do not need to worry that the target state might be at the + // synchronization level with no further transitions in either + // the LHS or RHS after it, because such cases will be handled + // inside the copy_transition function. + copy_transition(composition_state, running_state, waiting_root_state, !is_lhs_waiting, &worklist); + } + } + }; + + /** + * @brief Process potential fast EPSILON transitions (transitions over EPSILON, + * between two zero-level states). + * + * @param composition_state The state in the resulting composition NFT. + * @param lhs_src The source state of a potential EPSILON transition in the LHS NFT. + * @param rhs_src The source state of a potential EPSILON transition in the RHS NFT. + */ + auto process_fast_epsilon_transitions = [&](const State composition_state, const State lhs_src, const State rhs_src) { + assert(lhs.levels[lhs_src] == 0 && rhs.levels[rhs_src] == 0); + const auto lhs_eps_post_it = lhs.delta[lhs_src].find(EPSILON); + const auto rhs_eps_post_it = rhs.delta[rhs_src].find(EPSILON); + const bool lhs_eps_exists = lhs_eps_post_it != lhs.delta[lhs_src].end(); + const bool rhs_eps_exists = rhs_eps_post_it != rhs.delta[rhs_src].end(); + + StateSet filtered_lhs_fast_eps_targets{ lhs_src }; + StateSet filtered_rhs_fast_eps_targets{ rhs_src }; + if (lhs_eps_exists && lhs.levels.num_of_levels != 1) { + std::copy_if( + lhs_eps_post_it->targets.cbegin(), + lhs_eps_post_it->targets.cend(), + std::back_inserter(filtered_lhs_fast_eps_targets), + [&](State s) { return lhs.levels[s] == 0; } + ); + } + if (rhs_eps_exists && rhs.levels.num_of_levels != 1) { + std::copy_if( + rhs_eps_post_it->targets.cbegin(), + rhs_eps_post_it->targets.cend(), + std::back_inserter(filtered_rhs_fast_eps_targets), + [&](State s) { return rhs.levels[s] == 0; } + ); + } + + if (filtered_lhs_fast_eps_targets.size() == 1 && filtered_rhs_fast_eps_targets.size() == 1) { + // There are no fast EPSILON transitions to process. + return; + } + + // Create combinations of all non-zero-level targets of lhs_src with all non-zero-level targets of rhs_src. + // Create a common path of EPSILON transitions to connect to all those combinations. + // Branch onyl at the last level of that common path. + assert(result.levels.num_of_levels > 0); + const size_t common_path_len = result_num_of_levels - 1; + State source = create_epsilon_transition_with_common_path(composition_state, common_path_len); + + SymbolPost symbol_post{ EPSILON }; + for (const State lhs_target : filtered_lhs_fast_eps_targets) { + for (const State rhs_target : filtered_rhs_fast_eps_targets) { + if (lhs_target == lhs_src && rhs_target == rhs_src) { + // This is the original state pair. + continue; + } + symbol_post.insert(create_composition_state(lhs_target, rhs_target, 0)); + } + } + insert_symbol_post_to_delta(source, symbol_post); + }; + + // Initialization of the main worklist. + for (const State lhs_root: lhs.initial) { + for (const State rhs_root: rhs.initial) { + // Get the root state in the result NFT + result.initial.insert(create_composition_state(lhs_root, rhs_root, 0)); + } + } + + // The maing loop of the composition algorithm. + while (!worklist.empty()) { + const auto [lhs_state, rhs_state] = worklist.front(); + worklist.pop(); + const State composition_state = composition_storage.get(lhs_state, rhs_state); + assert(composition_state != Limits::max_state); + const Level lhs_level = lhs.levels[lhs_state]; + const Level rhs_level = rhs.levels[rhs_state]; + const SynchronizationType lhs_sync_type = lhs_sync_props.sync_types_v[lhs_state]; + const SynchronizationType rhs_sync_type = rhs_sync_props.sync_types_v[rhs_state]; + + if (lhs_level == 0 and rhs_level == 0) { + // We are at the zero-level states before any synchronization level. + // Now is the time to decide whether to continue synchronization and/or + // to wait in the lhs_state and/or rhs_state. This is necessary when + // there is a synchronization where one of the transducers has an EPSILON + // and the other has an alphabet symbol. Note that if future synchronization + // is impossible due to the EPSILON, we will simulate waiting in the zero-level + // state of the transducer that does not have that EPSILON. + + // Process potential fast EPSILON transitions. + process_fast_epsilon_transitions(composition_state, lhs_state, rhs_state); + + // TODO: Optimize/reduce the number of similar combination of waiting simulations. + // You can see the table defining operations for pair of synchronization types + // in the documentation of the SynchronizationType enum class. + const bool perform_wait_on_lhs = exist_intersection(rhs_sync_type, SynchronizationType::ONLY_ON_EPSILON); + const bool perform_wait_on_rhs = exist_intersection(lhs_sync_type, SynchronizationType::ONLY_ON_EPSILON); + const bool can_synchronize_in_the_future = exist_synchronization(lhs_sync_type, rhs_sync_type); + if (perform_wait_on_lhs) { + // LHS is waiting (i.e., there is an EPSILON in the RHS that LHS can not synchronize on). + model_waiting(composition_state, lhs_state, rhs_state, true); + } + if (perform_wait_on_rhs) { + // RHS is waiting (i.e., there is an EPSILON in the LHS that RHS can not synchronize on). + model_waiting(composition_state, rhs_state, lhs_state, false); + } + if (!can_synchronize_in_the_future) { + // There is no way to perform the synchronization after these states. + // Therefore, it does not make sense to continue exploring this pair. + continue; + } + } + + // It makes sense to continue only if we believe that synchronization is possible, + // or if we have already passed the synchronization level (i.e., lhs_sync_type == + // SynchronizationType::UNDEFINED or rhs_sync_type == SynchronizationType::UNDEFINED). + assert(exist_synchronization(lhs_sync_type, rhs_sync_type) || + (lhs_level == 0 && rhs_level > 0 && rhs_sync_type == SynchronizationType::UNDEFINED) || + (rhs_level == 0 && lhs_level > 0 && lhs_sync_type == SynchronizationType::UNDEFINED) || + (lhs_level > lhs_sync_level && rhs_level > rhs_sync_level && lhs_sync_type == SynchronizationType::UNDEFINED && rhs_sync_type == SynchronizationType::UNDEFINED) + ); + + // Both LHS and RHS can take a step if they are not at the synchronization level. + // The LHS always moves before the RHS (i.e., lhs_level < rhs_level). + // However, there is a special case when lhs_level < rhs_level, but the LHS cannot move. + // This occurs when the LHS has already reached its last (leave) zero-level state, + // which happens if there are no transitions after the synchronization level in the LHS. + const bool do_step_in_lhs = lhs_level != lhs_sync_level && (lhs_level != 0 || rhs_level == 0); + const bool do_step_in_rhs = rhs_level != rhs_sync_level; + + if (do_step_in_lhs) { + // Always try to do the step in the LHS first. + // We don't need to worry about the case when this is the last + // transition in the LHS, the RHS is already at the synchronization level, + // and we are projecting out the synchronization levels. + // In such situation, the copy_transition function will handle it. + copy_transition(composition_state, lhs_state, rhs_state, true); + } else if (do_step_in_rhs) { + // LHS is probably at the synchronization level or at the last (leave) zero-level state. + // It's time for RHS to make a step. + // We don't need to worry about the case when this is the last + // transition in the RHS, the LHS is already at the synchronization level, + // and we are projecting out the synchronization levels. + // In such situation, the copy_transition function will handle it. + copy_transition(composition_state, rhs_state, lhs_state, false); + } else { + // Both LHS and RHS are at the synchronization level. + // Synchronization at this point is only possible if: + // 1) There is at least one transition in either the LHS or + // RHS that follows the synchronization level + // (so we can connect to their successors), or + // 2) We are not projecting out the synchronization levels. + // In this case, we use the synchronization transition to + // connect to the zero-level successors that follow. + assert(lhs_level == lhs_sync_level && rhs_level == rhs_sync_level); + assert(!project_out_sync_levels || + lhs_sync_props.num_of_levels_after_sync > 0 || + rhs_sync_props.num_of_levels_after_sync > 0); + synchronize(composition_state, lhs_state, rhs_state); + } + } + + // TODO: Make trim on demand. + if (project_out_sync_levels) { + result.trim(); + } + + return result; +} + +Nft algorithms::compose_general(const Nft& lhs, const Nft& rhs, const OrdVector& lhs_sync_levels, const OrdVector& rhs_sync_levels, bool project_out_sync_levels, const JumpMode jump_mode) { assert(!lhs_sync_levels.empty()); assert(lhs_sync_levels.size() == rhs_sync_levels.size()); @@ -115,11 +1132,4 @@ Nft compose( return result; } -Nft compose( - const Nft& lhs, const Nft& rhs, const Level lhs_sync_level, const Level rhs_sync_level, - const bool project_out_sync_levels, const JumpMode jump_mode) { - return compose( - lhs, rhs, OrdVector{ lhs_sync_level }, OrdVector{ rhs_sync_level }, project_out_sync_levels, jump_mode - ); -} } // mata::nft diff --git a/src/nft/intersection.cc b/src/nft/intersection.cc index b9a49b693..51b3a50e6 100644 --- a/src/nft/intersection.cc +++ b/src/nft/intersection.cc @@ -53,12 +53,11 @@ Nft mata::nft::algorithms::product( if (lhs_first_aux_state <= lhs_target && rhs_first_aux_state <= rhs_target) { return; } State product_target = product_storage.get(lhs_target, rhs_target); - if (product_target == Limits::max_state) { - product_target = product.add_state_with_level( - (jump_mode == JumpMode::RepeatSymbol || lhs.levels[lhs_target] == 0 || rhs.levels[rhs_target] == 0) - ? std::max(lhs.levels[lhs_target], rhs.levels[rhs_target]) - : std::min(lhs.levels[lhs_target], rhs.levels[rhs_target]) - ); + if (product_target == Limits::max_state) + { + product_target = product.add_state_with_level((jump_mode != JumpMode::AppendDontCares || lhs.levels[lhs_target] == 0 || rhs.levels[rhs_target] == 0) ? + std::max(lhs.levels[lhs_target], rhs.levels[rhs_target]) : + std::min(lhs.levels[lhs_target], rhs.levels[rhs_target])); assert(product_target < Limits::max_state); product_storage.insert(lhs_target, rhs_target, product_target); @@ -135,12 +134,22 @@ Nft mata::nft::algorithms::product( create_product_state_and_symbol_post(lhs_target, rhs_target, product_symbol_post); } } - if (product_symbol_post.empty()) { continue; } - StatePost& product_state_post{ product.delta.mutable_state_post(product_source) }; - if (const auto product_state_post_find_it = product_state_post.find(product_symbol_post.symbol); - product_state_post_find_it == product_state_post.end()) { - product_state_post.insert(product_symbol_post); - } else { product_state_post_find_it->targets.insert(product_symbol_post.targets); } + if (product_symbol_post.empty()) { + continue; + } + StatePost &product_state_post{product.delta.mutable_state_post(product_source)}; + const auto product_state_post_find_it = product_state_post.find(product_symbol_post.symbol); + if (product_state_post_find_it == product_state_post.end()) { + if (product_state_post.empty() || product_state_post.back().symbol < product_symbol_post.symbol) { + // Optimization: If the new symbol is greater than the last one, we can simply push it back. + product_state_post.push_back(std::move(product_symbol_post)); + } else { + // Otherwise, we need to insert it in the correct position to keep the order. + product_state_post.insert(std::move(product_symbol_post)); + } + } else { + product_state_post_find_it->targets.insert(product_symbol_post.targets); + } } }; @@ -170,7 +179,7 @@ Nft mata::nft::algorithms::product( const bool rhs_source_is_deeper = (lhs_source_level < rhs_source_level && lhs_source_level != 0) || ( lhs_source_level != 0 && rhs_source_level == 0); - if (sources_are_on_the_same_level || jump_mode == JumpMode::RepeatSymbol) { + if (sources_are_on_the_same_level || jump_mode != JumpMode::AppendDontCares) { // Compute classic product for current state pair. mata::utils::SynchronizedUniversalIterator::const_iterator> sync_iterator(2); diff --git a/src/nft/nft.cc b/src/nft/nft.cc index c43dfc7cb..003ec72b0 100644 --- a/src/nft/nft.cc +++ b/src/nft/nft.cc @@ -667,6 +667,76 @@ State Nft::add_transition(const State source, const std::vector& symbols return insert_word(source, symbols); } +State Nft::add_transition_with_length(const State source, const Symbol symbol, const size_t length, const JumpMode jump_mode) { + assert(source < num_of_states()); + + if (length == 0) { return source; } + + assert(levels[source] + length <= levels.num_of_levels); + const Level target_level = static_cast((levels[source] + length) % levels.num_of_levels); + const State target = add_state_with_level(target_level); + + if (length == 1 || jump_mode == JumpMode::RepeatSymbol) { + delta.add(source, symbol, target); + return target; + } + + State inner_src = source; + Level inner_level = levels[inner_src] + 1; + for (size_t i = 0; i < length - 1; ++i, ++inner_level) { + assert(inner_level < levels.num_of_levels); + const State inner_target = add_state_with_level(inner_level); + delta.add(inner_src, symbol, inner_target); + inner_src = inner_target; + } + assert(inner_level == levels[source] + length); + delta.add(inner_src, symbol, target); + + return target; +} + +void Nft::add_transition_with_same_level_targets(State source, Symbol symbol, const StateSet& targets, JumpMode jump_mode) { + assert(targets.size() > 0); + assert(source < num_of_states()); + assert(std::all_of(targets.begin(), targets.end(), [&](State target) { return target < num_of_states(); })); + + const Level target_level = levels[targets.front()]; + const size_t trans_len = (target_level == 0 ? levels.num_of_levels : target_level) - levels[source]; + assert(std::all_of(targets.begin(), targets.end(), [&](State target) { return levels[target] == target_level; })); + assert(target_level == 0 || target_level > levels[source]); + assert(trans_len > 0); + + if (trans_len == 1 || jump_mode == JumpMode::RepeatSymbol) { + StatePost& mutable_state_post = delta.mutable_state_post(source); + auto mutable_symbol_post_it = mutable_state_post.find(symbol); + if (mutable_symbol_post_it == mutable_state_post.end()) { + if (mutable_state_post.empty() || mutable_state_post.back().symbol < symbol) { + // Optimization: If the new symbol is greater than the last one, we can simply push it back. + mutable_state_post.push_back({ symbol, targets }); + } else { + // Otherwise, we need to insert it in the correct position to keep the order. + mutable_state_post.insert({ symbol, targets }); + } + } else { + mutable_symbol_post_it->targets.insert(targets); + } + return; + } + + State inner_src = source; + Level inner_level = levels[inner_src] + 1; + for (size_t i = 0; i < trans_len - 1; ++i, ++inner_level) { + assert(inner_level < levels.num_of_levels); + const State inner_target = add_state_with_level(inner_level); + delta.add(inner_src, symbol, inner_target); + inner_src = inner_target; + } + assert(inner_level == levels[source] + trans_len); + StatePost& mutable_inner_state_post = delta.mutable_state_post(inner_src); + assert(mutable_inner_state_post.find(symbol) == mutable_inner_state_post.end()); + mutable_inner_state_post.insert(std::move(SymbolPost(symbol, targets))); +} + Nft& Nft::insert_identity(const State state, const std::vector& symbols, const JumpMode jump_mode) { for (const Symbol symbol : symbols) { insert_identity(state, symbol, jump_mode); } return *this; diff --git a/src/nft/operations.cc b/src/nft/operations.cc index 686d2e88f..8498142ee 100644 --- a/src/nft/operations.cc +++ b/src/nft/operations.cc @@ -353,7 +353,7 @@ Nft mata::nft::project_out(const Nft& nft, const utils::OrdVector& levels if (is_projected_out(cls_state)) { // If there are remaining levels between cls_state and tgt_state // on a transition with a length greater than 1, then these levels must be preserved. - if (jump_mode == JumpMode::RepeatSymbol) { + if (jump_mode != JumpMode::AppendDontCares) { result.delta.add(src_state, move.symbol, tgt_state); } else { result.delta.add(src_state, DONT_CARE, tgt_state); } } else if (is_loop_on_target) { @@ -431,6 +431,7 @@ Nft mata::nft::insert_levels(const Nft& nft, const BoolVector& new_levels_mask, // Example: // Input (new_levels_mask): 0 1 1 0 1 0 1 1 0 1 1 1 // Output (JumpMode::RepeatSymbol): 1 3 3 4 5 6 8 8 9 12 12 12 + // Output (JumpMode::NoJump): 1 3 3 4 5 6 8 8 9 12 12 12 // Output (JumpMode::AppendDontCares): 3 3 3 5 5 8 8 8 12 12 12 12 const size_t mask_size = new_levels_mask.size(); std::vector next_inner_levels(mask_size); @@ -439,7 +440,9 @@ Nft mata::nft::insert_levels(const Nft& nft, const BoolVector& new_levels_mask, for (auto it = new_levels_mask.rbegin(); it != new_levels_mask.rend(); ++it, --i) { next_inner_levels[i] = next_level; if (!*it) { - if (jump_mode == JumpMode::RepeatSymbol) { next_inner_levels[i] = static_cast(i + 1); } + if (jump_mode != JumpMode::AppendDontCares) { + next_inner_levels[i] = static_cast(i+1); + } next_level = static_cast(i); } } @@ -455,10 +458,8 @@ Nft mata::nft::insert_levels(const Nft& nft, const BoolVector& new_levels_mask, // Function to create a transition between source and target states. // The transition symbol is determined based on the parameters: // it could be a specific symb, DONT_CARE, or a default symbol. - auto create_transition = [&]( - const State src, const Symbol symb, const State tgt, const bool is_inserted_level, - const bool is_old_level_processed) { - if (!is_inserted_level && (jump_mode == JumpMode::RepeatSymbol || !is_old_level_processed)) { + auto create_transition = [&](const State src, const Symbol symb, const State tgt, const bool is_inserted_level, const bool is_old_level_processed) { + if (!is_inserted_level && (jump_mode != JumpMode::AppendDontCares || !is_old_level_processed)) { result.delta.add(src, symb, tgt); } else { result.delta.add(src, DONT_CARE, tgt); } }; @@ -972,6 +973,9 @@ Nft& Nft::unite_nondet_with(const Nft& aut) { // set initial states this->initial.reserve(n + aut_states); for (const State& aut_ini : aut_initial_copy) { this->initial.insert(upd_fnc(aut_ini)); } + // combine levels + this->levels.num_of_levels = std::max(this->levels.num_of_levels, aut.levels.num_of_levels); + this->levels.append(aut.levels); return *this; } diff --git a/tests/nft/nft-composition.cc b/tests/nft/nft-composition.cc index 292302506..fefbe06be 100644 --- a/tests/nft/nft-composition.cc +++ b/tests/nft/nft-composition.cc @@ -49,43 +49,42 @@ TEST_CASE("Mata::nft::compose()") { CHECK(are_equivalent(result, expected)); } - SECTION("Epsilon perfectly matches.") { - lhs = Nft::with_levels({2, { 0, 1, 0, 1, 0, 1, 0 } }, 7, { 0 }, { 6 }); - lhs.delta.add(0, 'e', 1); - lhs.delta.add(1, 'a', 2); - lhs.delta.add(2, 'g', 3); + SECTION("Epsilon perfectly matches") { + lhs = Nft(9, { 0 }, { 8 }, Levels({ 0, 1, 2, 3, 0, 1, 2, 3, 0 })); + lhs.delta.add(0, 'i', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); lhs.delta.add(3, EPSILON, 4); - lhs.delta.add(4, EPSILON, 5); - lhs.delta.add(5, 'c', 6); + lhs.delta.add(4, 'k', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(6, 'g', 7); + lhs.delta.add(7, 'l', 8); - rhs = Nft::with_levels({2, { 0, 1, 0, 1, 0, 1, 0 } }, 7, { 0 }, { 6 }); + rhs = Nft(9, { 0 }, { 8 }, Levels({ 0, 1, 2, 3, 0, 1, 2, 3, 0 })); rhs.delta.add(0, 'a', 1); - rhs.delta.add(1, EPSILON, 2); + rhs.delta.add(1, 'i', 2); rhs.delta.add(2, EPSILON, 3); - rhs.delta.add(3, 'h', 4); - rhs.delta.add(4, 'c', 5); - rhs.delta.add(5, 'j', 6); - - expected = Nft::with_levels({2, { 0, 1, 0, 1, 0, 1, 0 } }, 7, { 0 }, { 6 }); - expected.delta.add(0, 'e', 1); - expected.delta.add(1, EPSILON, 2); - expected.delta.add(2, 'g', 3); - expected.delta.add(3, 'h', 4); - expected.delta.add(4, EPSILON, 5); - expected.delta.add(5, 'j', 6); - expected.delta.add(2, EPSILON, 7); + rhs.delta.add(3, EPSILON, 4); + rhs.delta.add(4, 'e', 5); + rhs.delta.add(5, 'k', 6); + rhs.delta.add(6, 'l', 7); + rhs.delta.add(7, 'h', 8); + + expected = Nft(9, { 0 }, { 8 }, Levels({ 0, 1, 2, 3, 0, 1, 2, 3, 0 })); + expected.delta.add(0, 'a', 1); + expected.delta.add(1, 'b', 2); + expected.delta.add(2, 'c', 3); + expected.delta.add(3, EPSILON, 4); + expected.delta.add(4, 'e', 5); + expected.delta.add(5, 'f', 6); + expected.delta.add(6, 'g', 7); expected.delta.add(7, 'h', 8); - expected.delta.add(8, 'g', 9); - expected.delta.add(9, EPSILON, 4); - expected.delta.add(2, 'g', 10); - expected.delta.add(10, EPSILON, 11); - expected.delta.add(11, EPSILON, 12); - expected.delta.add(12, 'h', 4); - result = compose(lhs, rhs, 1, 0); + result = compose(lhs, rhs, { 0, 3 }, { 1, 2 }); CHECK(are_equivalent(result, expected)); } + } SECTION("Branching") { @@ -229,8 +228,7 @@ TEST_CASE("Mata::nft::compose()") { lhs.delta.add(3, 'a', 4); lhs.delta.add(4, 'x', 5); lhs.delta.add(5, EPSILON, 6); - - rhs = Nft::with_levels({2, { 0, 1, 0, 1, 0 } }, 5, { 0 }, { 4 }); + rhs = Nft(5, { 0 }, { 4 }, Levels({ 0, 1, 0, 1, 0 })); rhs.delta.add(0, 'a', 1); rhs.delta.add(1, 'b', 2); rhs.delta.add(2, EPSILON, 3); @@ -256,12 +254,11 @@ TEST_CASE("Mata::nft::compose()") { CHECK(are_equivalent(result, expected)); } - } } - SECTION("lhs.num_of_levels != rhs.num_of_levels") { - SECTION("lhs.num_of_levels > rhs.num_of_levels") { + SECTION("lhs.levels.num_of_levels != rhs.levels.num_of_levels") { + SECTION("lhs.levels.num_of_levels > rhs.levels.num_of_levels") { lhs = Nft::with_levels({5, { 0, 1, 2, 3, 4, 0 } }, 6, { 0 }, { 5 }); lhs.delta.add(0, 'a', 1); lhs.delta.add(1, 'b', 2); @@ -285,7 +282,7 @@ TEST_CASE("Mata::nft::compose()") { CHECK(are_equivalent(result, expected)); } - SECTION("lhs.num_of_levels < rhs.num_of_levels") { + SECTION("lhs.levels.num_of_levels < rhs.levels.num_of_levels") { lhs = Nft::with_levels({3, { 0, 1, 2, 0 } }, 4, { 0 }, { 3 }); lhs.delta.add(0, 'b', 1); lhs.delta.add(1, 'd', 2); @@ -565,3 +562,2334 @@ TEST_CASE("Mata::nft::compose()") { } } } + +TEST_CASE("nft::compose(Nft&, Nft&, Level, Level, ...) - easy cases") { + SECTION("2 levels x 2 levels") { + Nft expected_full(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'e', 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, 'd', 5); + expected_full.delta.add(5, 'f', 6); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft lhs(5, { 0 }, { 4 }, Levels({ 0, 1, 0, 1, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + + Nft rhs(5, { 0 }, { 4 }, Levels({ 0, 1, 0, 1, 0 })); + rhs.delta.add(0, 'b', 1); + rhs.delta.add(1, 'e', 2); + rhs.delta.add(2, 'd', 3); + rhs.delta.add(3, 'f', 4); + + SECTION("LHS | RHS") { + Nft result_full = compose(lhs, rhs, 1, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft result_full = compose(rhs, lhs, 0, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + + } + } + SECTION("2 levels x 1 level") { + Nft expected_full(5, { 0 }, { 4 }, Levels({ 0, 1, 0, 1, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'c', 3); + expected_full.delta.add(3, 'd', 4); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft lhs(5, { 0 }, { 4 }, Levels({ 0, 1, 0, 1, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + + Nft rhs(3, { 0 }, { 2 }, Levels(std::vector({ 0, 0, 0 }))); + rhs.delta.add(0, 'b', 1); + rhs.delta.add(1, 'd', 2); + + SECTION("LHS | RHS") { + Nft result_full = compose(lhs, rhs, 1, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft result_full = compose(rhs, lhs, 0, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + SECTION("1 level x 1 level") { + Nft expected_full(4, { 0 }, { 3 }, Levels({ 0, 0, 0, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'c', 3); + + Nft lhs(4, { 0 }, { 3 }, Levels({ 0, 0, 0, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 0, 0, 0 })); + rhs.delta.add(0, 'a', 1); + rhs.delta.add(1, 'b', 2); + rhs.delta.add(2, 'c', 3); + + Nft result_full = compose(lhs, rhs, 0, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + } +} + +TEST_CASE("nft::compose(..., Level, Level, ...) - sliding without epsilon") { + SECTION("sync level 0 x sync level 0") { + Nft lhs(5, { 0 }, { 4 }, Levels({ 0, 1, 0, 1, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'd', 3); + lhs.delta.add(3, 'e', 4); + + Nft rhs(5, { 0 }, { 4 }, Levels({ 0, 1, 0, 1, 0 })); + rhs.delta.add(0, 'a', 1); + rhs.delta.add(1, 'c', 2); + rhs.delta.add(2, 'd', 3); + rhs.delta.add(3, 'f', 4); + + SECTION("LHS | RHS") { + Nft expected_full(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'c', 3); + expected_full.delta.add(3, 'd', 4); + expected_full.delta.add(4, 'e', 5); + expected_full.delta.add(5, 'f', 6); + Nft expected_proj = project_out(expected_full, { 0 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 0, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 0, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'c', 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, 'd', 4); + expected_full.delta.add(4, 'f', 5); + expected_full.delta.add(5, 'e', 6); + Nft expected_proj = project_out(expected_full, { 0 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 0, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 0 x sync level 1") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'x', 0); + lhs.delta.add(2, 'z', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'a', 2); + rhs.delta.add(2, 'h', 3); + rhs.delta.add(3, 'i', 4); + rhs.delta.add(4, 'd', 5); + rhs.delta.add(5, 'j', 6); + rhs.delta.add(2, 'w', 0); + rhs.delta.add(2, 'y', 6); + + SECTION("LHS | RHS") { + Nft expected_full(13, { 0 }, { 12 }, Levels({ 0, 1, 2, 3, 4, 4, 0, 1, 2, 3, 4, 4, 0 })); + expected_full.delta.add(0, 'g', 1); + expected_full.delta.add(1, 'a', 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, 'x', 4); + expected_full.delta.add(3, 'c', 5); + expected_full.delta.add(3, 'z', 11); + expected_full.delta.add(4, 'w', 0); + expected_full.delta.add(5, 'h', 6); + expected_full.delta.add(6, 'i', 7); + expected_full.delta.add(7, 'd', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(10, 'j', 12); + expected_full.delta.add(11, 'y', 12); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 0, 1, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 0, 1, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(15, { 0 }, { 12 }, Levels({ 0, 4, 3, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 3, 4 })); + expected_full.delta.add(0, 'g', 3); + expected_full.delta.add(3, 'a', 4); + expected_full.delta.add(4, 'w', 2); + expected_full.delta.add(2, 'b', 1); + expected_full.delta.add(1, 'x', 0); + expected_full.delta.add(4, 'h', 5); + expected_full.delta.add(5, 'b', 6); + expected_full.delta.add(6, 'c', 7); + expected_full.delta.add(7, 'i', 8); + expected_full.delta.add(8, 'd', 9); + expected_full.delta.add(9, 'j', 10); + expected_full.delta.add(10, 'e', 11); + expected_full.delta.add(11, 'f', 12); + expected_full.delta.add(4, 'y', 13); + expected_full.delta.add(13, 'b', 14); + expected_full.delta.add(14, 'z', 12); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 1, 0, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 1, 0, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 0 x sync level 2") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'x', 0); + lhs.delta.add(2, 'z', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'h', 2); + rhs.delta.add(2, 'a', 3); + rhs.delta.add(3, 'i', 4); + rhs.delta.add(4, 'j', 5); + rhs.delta.add(5, 'd', 6); + rhs.delta.add(2, 'a', 0); + rhs.delta.add(2, 'a', 6); + + Nft expected_full(15, { 0 }, { 12 }, Levels({ 0, 1, 2, 3, 4, 3, 4, 0, 1, 2, 3, 4, 0, 4, 3 })); + expected_full.delta.add(0, 'g', 1); + expected_full.delta.add(1, 'h', 2); + expected_full.delta.add(2, 'a', 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, 'x', 0); + expected_full.delta.add(2, 'a', 5); + expected_full.delta.add(5, 'b', 6); + expected_full.delta.add(6, 'c', 7); + expected_full.delta.add(7, 'i', 8); + expected_full.delta.add(8, 'j', 9); + expected_full.delta.add(9, 'd', 10); + expected_full.delta.add(10, 'e', 11); + expected_full.delta.add(11, 'f', 12); + expected_full.delta.add(2, 'a', 14); + expected_full.delta.add(14, 'b', 13); + expected_full.delta.add(13, 'z', 12); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + SECTION("LHS | RHS") { + Nft result_full = compose(lhs, rhs, 0, 2, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 0, 2, true, JumpMode::RepeatSymbol).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft result_full = compose(rhs, lhs, 2, 0, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 2, 0, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sycn level 1 x sync level 0") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'w', 0); + lhs.delta.add(2, 'z', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'b', 1); + rhs.delta.add(1, 'g', 2); + rhs.delta.add(2, 'h', 3); + rhs.delta.add(3, 'e', 4); + rhs.delta.add(4, 'i', 5); + rhs.delta.add(5, 'j', 6); + rhs.delta.add(2, 'x', 0); + rhs.delta.add(2, 'y', 6); + + SECTION("LHS | RHS") { + Nft expected_full(15, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 3, 3, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'c', 3); + expected_full.delta.add(3, 'g', 4); + expected_full.delta.add(4, 'h', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'f', 8); + expected_full.delta.add(8, 'i', 9); + expected_full.delta.add(9, 'j', 10); + expected_full.delta.add(11, 'y', 10); + expected_full.delta.add(12, 'g', 11); + expected_full.delta.add(2, 'z', 12); + expected_full.delta.add(2, 'w', 13); + expected_full.delta.add(13, 'g', 14); + expected_full.delta.add(14, 'x', 0); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 1, 0, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 0, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + + SECTION("RHS | LHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'g', 3); + expected_full.delta.add(3, 'h', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'i', 8); + expected_full.delta.add(8, 'j', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(11, 'z', 10); + expected_full.delta.add(3, 'y', 11); + expected_full.delta.add(3, 'x', 12); + expected_full.delta.add(12, 'w', 0); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 0, 1, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 1, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 1 x sync level 1") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'x', 0); + lhs.delta.add(2, 'z', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'b', 2); + rhs.delta.add(2, 'h', 3); + rhs.delta.add(3, 'i', 4); + rhs.delta.add(4, 'e', 5); + rhs.delta.add(5, 'j', 6); + rhs.delta.add(2, 'w', 0); + rhs.delta.add(2, 'y', 6); + + SECTION("LHS | RHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'g', 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, 'h', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'i', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(8, 'f', 9); + expected_full.delta.add(9, 'j', 10); + expected_full.delta.add(11, 'y', 10); + expected_full.delta.add(3, 'x', 12); + expected_full.delta.add(12, 'w', 0); + expected_full.delta.add(3, 'z', 11); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 1, 1, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 1, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 4 })); + expected_full.delta.add(0, 'g', 1); + expected_full.delta.add(1, 'a', 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, 'h', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'i', 6); + expected_full.delta.add(6, 'd', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(8, 'j', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(11, 'z', 10); + expected_full.delta.add(3, 'y', 11); + expected_full.delta.add(3, 'w', 12); + expected_full.delta.add(12, 'x', 0); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 1, 1, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 1, 1, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 1 x sync level 2") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'x', 0); + lhs.delta.add(2, 'z', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'h', 2); + rhs.delta.add(2, 'b', 3); + rhs.delta.add(3, 'i', 4); + rhs.delta.add(4, 'j', 5); + rhs.delta.add(5, 'e', 6); + rhs.delta.add(2, 'b', 0); + rhs.delta.add(2, 'b', 6); + + SECTION("LHS | RHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'g', 2); + expected_full.delta.add(2, 'h', 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'i', 7); + expected_full.delta.add(7, 'j', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(3, 'b', 12); + expected_full.delta.add(12, 'x', 0); + expected_full.delta.add(3, 'b', 11); + expected_full.delta.add(11, 'z', 10); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 1, 2, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 2, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 4 })); + expected_full.delta.add(0, 'g', 1); + expected_full.delta.add(1, 'h', 2); + expected_full.delta.add(2, 'a', 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'i', 6); + expected_full.delta.add(6, 'j', 7); + expected_full.delta.add(7, 'd', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(3, 'b', 12); + expected_full.delta.add(12, 'x', 0); + expected_full.delta.add(3, 'b', 11); + expected_full.delta.add(11, 'z', 10); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 2, 1, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 2, 1, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 2 x sync level 0") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + lhs.delta.add(2, 'c', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'c', 1); + rhs.delta.add(1, 'g', 2); + rhs.delta.add(2, 'h', 3); + rhs.delta.add(3, 'f', 4); + rhs.delta.add(4, 'i', 5); + rhs.delta.add(5, 'j', 6); + rhs.delta.add(2, 'x', 0); + rhs.delta.add(2, 'y', 6); + + Nft expected_full(15, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 3, 3, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'c', 3); + expected_full.delta.add(3, 'g', 4); + expected_full.delta.add(4, 'h', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'f', 8); + expected_full.delta.add(8, 'i', 9); + expected_full.delta.add(9, 'j', 10); + expected_full.delta.add(2, 'c', 13); + expected_full.delta.add(13, 'g', 14); + expected_full.delta.add(14, 'x', 0); + expected_full.delta.add(2, 'c', 12); + expected_full.delta.add(12, 'g', 11); + expected_full.delta.add(11, 'y', 10); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + SECTION("LHS | RHS") { + Nft result_full = compose(lhs, rhs, 2, 0, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 2, 0, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft result_full = compose(rhs, lhs, 0, 2, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 2, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 2 x sync level 1") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + lhs.delta.add(2, 'c', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'c', 2); + rhs.delta.add(2, 'h', 3); + rhs.delta.add(3, 'i', 4); + rhs.delta.add(4, 'f', 5); + rhs.delta.add(5, 'j', 6); + rhs.delta.add(2, 'x', 0); + rhs.delta.add(2, 'y', 6); + + SECTION("LHS | RHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'g', 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, 'h', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'i', 8); + expected_full.delta.add(8, 'f', 9); + expected_full.delta.add(9, 'j', 10); + expected_full.delta.add(3, 'c', 12); + expected_full.delta.add(12, 'x', 0); + expected_full.delta.add(3, 'c', 11); + expected_full.delta.add(11, 'y', 10); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 2, 1, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 2, 1, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4, 4})); + expected_full.delta.add(0, 'g', 1); + expected_full.delta.add(1, 'a', 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, 'h', 5); + expected_full.delta.add(5, 'i', 6); + expected_full.delta.add(6, 'd', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(8, 'f', 9); + expected_full.delta.add(9, 'j', 10); + expected_full.delta.add(3, 'c', 12); + expected_full.delta.add(12, 'x', 0); + expected_full.delta.add(3, 'c', 11); + expected_full.delta.add(11, 'y', 10); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 1, 2, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 1, 2, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 2 x sync level 2") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + lhs.delta.add(2, 'c', 6); + + Nft rhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'h', 2); + rhs.delta.add(2, 'c', 3); + rhs.delta.add(3, 'i', 4); + rhs.delta.add(4, 'j', 5); + rhs.delta.add(5, 'f', 6); + rhs.delta.add(2, 'c', 0); + rhs.delta.add(2, 'c', 6); + + SECTION("LHS | RHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'g', 3); + expected_full.delta.add(3, 'h', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'i', 8); + expected_full.delta.add(8, 'j', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + expected_full.delta.add(4, 'c', 10); + + Nft expected_proj(9, { 0 }, { 8 }, Levels({ 0, 1, 2, 3, 0, 1, 2, 3, 0 })); + expected_proj.delta.add(0, 'a', 1); + expected_proj.delta.add(1, 'b', 2); + expected_proj.delta.add(2, 'g', 3); + expected_proj.delta.add(3, 'h', 4); + expected_proj.delta.add(4, 'd', 5); + expected_proj.delta.add(5, 'e', 6); + expected_proj.delta.add(6, 'i', 7); + expected_proj.delta.add(7, 'j', 8); + expected_proj.delta.add(3, 'h', 8); + expected_proj.delta.add(3, 'h', 0); + + Nft result_full = compose(lhs, rhs, 2, 2, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 2, 2, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'g', 1); + expected_full.delta.add(1, 'h', 2); + expected_full.delta.add(2, 'a', 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'i', 6); + expected_full.delta.add(6, 'j', 7); + expected_full.delta.add(7, 'd', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + expected_full.delta.add(4, 'c', 10); + + Nft expected_proj(9, { 0 }, { 8 }, Levels({ 0, 1, 2, 3, 0, 1, 2, 3, 0 })); + expected_proj.delta.add(0, 'g', 1); + expected_proj.delta.add(1, 'h', 2); + expected_proj.delta.add(2, 'a', 3); + expected_proj.delta.add(3, 'b', 4); + expected_proj.delta.add(4, 'i', 5); + expected_proj.delta.add(5, 'j', 6); + expected_proj.delta.add(6, 'd', 7); + expected_proj.delta.add(7, 'e', 8); + expected_proj.delta.add(3, 'b', 8); + expected_proj.delta.add(3, 'b', 0); + + Nft result_full = compose(rhs, lhs, 2, 2, false, JumpMode::NoJump).trim(); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 2, 2, true, JumpMode::NoJump).trim(); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } +} + +TEST_CASE("nft::compose(..., Level, Level, ...) - sliding with epsilon") { + SECTION("sync level 0 x sync level 0") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, EPSILON, 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'd', 1); + rhs.delta.add(1, 'g', 2); + rhs.delta.add(2, 'h', 3); + + SECTION("LHS | RHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 3, 4 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, 'c', 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'f', 8); + expected_full.delta.add(8, 'g', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(2, 'c', 11); + expected_full.delta.add(11, EPSILON, 12); + expected_full.delta.add(12, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 0 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 0, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 0, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'g', 7); + expected_full.delta.add(7, 'h', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + Nft expected_proj = project_out(expected_full, { 0 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 0, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 0 x sync level 1") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, EPSILON, 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'd', 2); + rhs.delta.add(2, 'h', 3); + + SECTION("LHS | RHS") { + Nft expected_full(12, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'g', 6); + expected_full.delta.add(6, 'd', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(8, 'f', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(3, 'c', 11); + expected_full.delta.add(11, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 0, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 0, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'g', 6); + expected_full.delta.add(6, 'd', 7); + expected_full.delta.add(7, 'h', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 1, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 1, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 0 x sync level 2") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, EPSILON, 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'h', 2); + rhs.delta.add(2, 'd', 3); + + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'g', 6); + expected_full.delta.add(6, 'h', 7); + expected_full.delta.add(7, 'd', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + SECTION("LHS | RHS") { + Nft result_full = compose(lhs, rhs, 0, 2, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 0, 2, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft result_full = compose(rhs, lhs, 2, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 2, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 1 x sync level 0") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, EPSILON, 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'e', 1); + rhs.delta.add(1, 'g', 2); + rhs.delta.add(2, 'h', 3); + + SECTION("LHS | RHS") { + Nft expected_full(13, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 3, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, 'c', 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'f', 8); + expected_full.delta.add(8, 'g', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(2, 'c', 11); + expected_full.delta.add(11, EPSILON, 12); + expected_full.delta.add(12, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 1, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'g', 8); + expected_full.delta.add(8, 'h', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 0, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 1 x sync level 1") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, EPSILON, 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'e', 2); + rhs.delta.add(2, 'h', 3); + + SECTION("LHS | RHS") { + Nft expected_full(12, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 4 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'g', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(8, 'f', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(3, 'c', 11); + expected_full.delta.add(11, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 1, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, 'a', 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'g', 6); + expected_full.delta.add(6, 'd', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(8, 'h', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 1, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 1, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 1 x sync level 2") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, EPSILON, 2); + lhs.delta.add(2, 'c', 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, 'c', 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'h', 2); + rhs.delta.add(2, 'e', 3); + + SECTION("LHS | RHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'g', 7); + expected_full.delta.add(7, 'h', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 1, 2, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 2, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, 'a', 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'g', 6); + expected_full.delta.add(6, 'h', 7); + expected_full.delta.add(7, 'd', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, 'c', 0); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 2, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 2, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 2 x sync level 0") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, EPSILON, 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, EPSILON, 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'f', 1); + rhs.delta.add(1, 'g', 2); + rhs.delta.add(2, 'h', 3); + + SECTION("LHS | RHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'f', 8); + expected_full.delta.add(8, 'g', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(4, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 2, 0, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 2, 0, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'f', 8); + expected_full.delta.add(8, 'g', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(4, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 2 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 0, 2, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 2, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 2 x sync level 1") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, EPSILON, 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, EPSILON, 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'f', 2); + rhs.delta.add(2, 'h', 3); + + SECTION("LHS | RHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'g', 8); + expected_full.delta.add(8, 'f', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(4, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 2, 1, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 2, 1, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, 'a', 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'g', 6); + expected_full.delta.add(6, 'd', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(8, 'f', 9); + expected_full.delta.add(9, 'h', 10); + expected_full.delta.add(4, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 3 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 1, 2, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 1, 2, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("sync level 2 x sync level 2") { + Nft lhs(7, { 0 }, { 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(2, EPSILON, 3); + lhs.delta.add(3, 'd', 4); + lhs.delta.add(4, 'e', 5); + lhs.delta.add(5, 'f', 6); + lhs.delta.add(2, EPSILON, 0); + + Nft rhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'g', 1); + rhs.delta.add(1, 'h', 2); + rhs.delta.add(2, 'f', 3); + + SECTION("LHS | RHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'b', 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(6, 'e', 7); + expected_full.delta.add(7, 'g', 8); + expected_full.delta.add(8, 'h', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 4 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 2, 2, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 2, 2, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(11, { 0 }, { 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, 'a', 3); + expected_full.delta.add(3, 'b', 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'g', 6); + expected_full.delta.add(6, 'h', 7); + expected_full.delta.add(7, 'd', 8); + expected_full.delta.add(8, 'e', 9); + expected_full.delta.add(9, 'f', 10); + expected_full.delta.add(4, EPSILON, 0); + Nft expected_proj = project_out(expected_full, { 4 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 2, 2, false, JumpMode::NoJump); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 2, 2, true, JumpMode::NoJump); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } +} + +TEST_CASE("nft::composition(..., Level, Level, ...) - epsilon on both sides") { + SECTION("3 levels x 3 levels + fast EPSILON on LHS") { + Nft lhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + lhs.delta.add(0, EPSILON, 1); + lhs.delta.add(0, EPSILON, 3); + lhs.delta.add(1, 'a', 2); + lhs.delta.add(2, 'b', 3); + + Nft rhs(4, { 0 }, { 0, 3 }, Levels({ 0, 1, 2, 0 })); + rhs.delta.add(0, 'c', 1); + rhs.delta.add(1, EPSILON, 2); + rhs.delta.add(2, 'd', 3); + + SECTION("LHS | RHS") { + Nft expected_full(28, { 0 }, { 5, 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 1, 2, 3, 4, 1, 2, 3, 4 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(0, EPSILON, 6); + expected_full.delta.add(6, EPSILON, 7); + expected_full.delta.add(7, 'a', 8); + expected_full.delta.add(8, 'b', 9); + expected_full.delta.add(9, EPSILON, 5); + expected_full.delta.add(0, 'c', 11); + expected_full.delta.add(11, EPSILON, 12); + expected_full.delta.add(12, EPSILON, 13); + expected_full.delta.add(13, EPSILON, 14); + expected_full.delta.add(14, 'd', 15); + expected_full.delta.add(15, EPSILON, 16); + expected_full.delta.add(16, EPSILON, 17); + expected_full.delta.add(17, EPSILON, 18); + expected_full.delta.add(18, EPSILON, 19); + expected_full.delta.add(19, EPSILON, 10); + expected_full.delta.add(5, 'c', 20); + expected_full.delta.add(20, EPSILON, 21); + expected_full.delta.add(21, EPSILON, 22); + expected_full.delta.add(22, EPSILON, 23); + expected_full.delta.add(23, 'd', 10); + expected_full.delta.add(15, EPSILON, 24); + expected_full.delta.add(24, EPSILON, 25); + expected_full.delta.add(25, 'a', 26); + expected_full.delta.add(26, 'b', 27); + expected_full.delta.add(27, EPSILON, 10); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::RepeatSymbol); + + Nft result_full = compose(lhs, rhs, 0, 1, false, JumpMode::NoJump); + + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 0, 1, true, JumpMode::NoJump); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft expected_full(28, { 0 }, { 5, 10 }, Levels({ 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 1, 2, 3, 4, 1, 2, 3, 4 })); + expected_full.delta.add(0, EPSILON, 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, EPSILON, 3); + expected_full.delta.add(3, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(0, EPSILON, 6); + expected_full.delta.add(6, EPSILON, 7); + expected_full.delta.add(7, EPSILON, 8); + expected_full.delta.add(8, 'a', 9); + expected_full.delta.add(9, 'b', 5); + expected_full.delta.add(0, 'c', 11); + expected_full.delta.add(11, EPSILON, 12); + expected_full.delta.add(12, 'd', 13); + expected_full.delta.add(13, EPSILON, 14); + expected_full.delta.add(14, EPSILON, 15); + expected_full.delta.add(15, EPSILON, 16); + expected_full.delta.add(16, EPSILON, 17); + expected_full.delta.add(17, EPSILON, 18); + expected_full.delta.add(18, EPSILON, 19); + expected_full.delta.add(19, EPSILON, 10); + expected_full.delta.add(5, 'c', 20); + expected_full.delta.add(20, EPSILON, 21); + expected_full.delta.add(21, 'd', 22); + expected_full.delta.add(22, EPSILON, 23); + expected_full.delta.add(23, EPSILON, 10); + expected_full.delta.add(15, EPSILON, 24); + expected_full.delta.add(24, EPSILON, 25); + expected_full.delta.add(25, EPSILON, 26); + expected_full.delta.add(26, 'a', 27); + expected_full.delta.add(27, 'b', 10); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 1, 0, false, JumpMode::NoJump); + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 1, 0, true, JumpMode::NoJump); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("3 levels x 1 level") { + Nft lhs(4, { 0 }, { 3 }, Levels({ 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, EPSILON, 2); + lhs.delta.add(2, 'b', 3); + + Nft rhs(2, { 0 }, { 1 }, Levels(std::vector({ 0, 0 }))); + rhs.delta.add(0, EPSILON, 1); + + Nft expected_full(14, { 0 }, { 3 }, Levels({ 0, 1, 2, 0, 1, 2, 0, 1, 2, 1, 2, 0, 1, 2 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(0, EPSILON, 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, EPSILON, 6); + expected_full.delta.add(6, 'a', 7); + expected_full.delta.add(7, EPSILON, 8); + expected_full.delta.add(8, 'b', 3); + expected_full.delta.add(0, 'a', 9); + expected_full.delta.add(9, EPSILON, 10); + expected_full.delta.add(10, 'b', 11); + expected_full.delta.add(11, EPSILON, 12); + expected_full.delta.add(12, EPSILON, 13); + expected_full.delta.add(13, EPSILON, 3); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + SECTION("LHS | RHS") { + Nft result_full = compose(lhs, rhs, 1, 0, false, JumpMode::NoJump); + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 0, true, JumpMode::NoJump); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + SECTION("RHS | LHS") { + Nft result_full = compose(rhs, lhs, 0, 1, false, JumpMode::NoJump); + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 1, true, JumpMode::NoJump); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } + + SECTION("3 levels x 1 level (long)") { + Nft lhs(7, { 0 }, { 3, 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, EPSILON, 2); + lhs.delta.add(2, 'b', 3); + lhs.delta.add(3, 'c', 4); + lhs.delta.add(4, EPSILON, 5); + lhs.delta.add(5, 'd', 6); + + Nft rhs(2, { 0 }, { 1 }, Levels(std::vector({ 0, 0 }))); + rhs.delta.add(0, EPSILON, 1); + + Nft expected_full(24, { 0 }, { 3, 6 }, Levels({ 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, 1, 2, 0, 1, 2, 1, 2, 1, 2, 0, 1, 2 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, EPSILON, 2); + expected_full.delta.add(2, 'b', 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(0, EPSILON, 7); + expected_full.delta.add(7, EPSILON, 8); + expected_full.delta.add(8, EPSILON, 9); + expected_full.delta.add(9, 'a', 10); + expected_full.delta.add(10, EPSILON, 11); + expected_full.delta.add(11, 'b', 3); + expected_full.delta.add(3, 'c', 4); + expected_full.delta.add(4, EPSILON, 5); + expected_full.delta.add(5, 'd', 6); + expected_full.delta.add(0, 'a', 12); + expected_full.delta.add(12, EPSILON, 13); + expected_full.delta.add(13, 'b', 14); + expected_full.delta.add(14, EPSILON, 15); + expected_full.delta.add(15, EPSILON, 16); + expected_full.delta.add(16, EPSILON, 3); + expected_full.delta.add(14, 'c', 17); + expected_full.delta.add(17, EPSILON, 18); + expected_full.delta.add(18, 'd', 6); + expected_full.delta.add(14, 'c', 19); + expected_full.delta.add(19, EPSILON, 20); + expected_full.delta.add(20, 'd', 21); + expected_full.delta.add(21, EPSILON, 22); + expected_full.delta.add(22, EPSILON, 23); + expected_full.delta.add(23, EPSILON, 6); + Nft expected_proj = project_out(expected_full, { 1 }, JumpMode::NoJump); + + SECTION("LHS | RHS") { + Nft result_full = compose(lhs, rhs, 1, 0, false, JumpMode::NoJump); + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 1, 0, true, JumpMode::NoJump); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + + SECTION("RHS | LHS") { + Nft result_full = compose(rhs, lhs, 0, 1, false, JumpMode::NoJump); + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 0, 1, true, JumpMode::NoJump); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + } +} + +TEST_CASE("nft::composition(..., Level, Level, ...) - complex") { + Nft lhs(25, { 0 }, { 12, 14, 19, 24 }, Levels({ 0, 1, 2, 2, 3, 3, 3, 4, 4, 4, 4, 0, 0, 0, 0, 1, 2, 3, 4, 0, 1, 2, 3, 4, 0 })); + lhs.delta.add(0, 'a', 1); + lhs.delta.add(1, 'b', 2); + lhs.delta.add(1, 'c', 3); + lhs.delta.add(2, 'd', 4); + lhs.delta.add(2, 'e', 5); + lhs.delta.add(3, 'f', 6); + lhs.delta.add(4, EPSILON, 7); + lhs.delta.add(5, 'b', 8); + lhs.delta.add(5, EPSILON, 9); + lhs.delta.add(6, 'y', 10); + lhs.delta.add(7, 'g', 11); + lhs.delta.add(8, 'h', 12); + lhs.delta.add(9, 'i', 13); + lhs.delta.add(10, 'j', 14); + lhs.delta.add(11, 'k', 15); + lhs.delta.add(13, 'l', 20); + lhs.delta.add(15, 'm', 16); + lhs.delta.add(16, 'o', 17); + lhs.delta.add(17, 'x', 18); + lhs.delta.add(18, 'q', 19); + lhs.delta.add(20, 'n', 21); + lhs.delta.add(21, 'p', 22); + lhs.delta.add(22, 'y', 23); + lhs.delta.add(23, 'r', 24); + + Nft rhs(15, { 0 }, { 11, 12, 13, 14 }, Levels({ 0, 1, 2, 2, 3, 3, 3, 4, 4, 4, 4, 0, 0, 0, 0 })); + rhs.delta.add(0, 's', 1); + rhs.delta.add(1, 't', 2); + rhs.delta.add(1, 'u', 3); + rhs.delta.add(2, 'v', 4); + rhs.delta.add(3, 'w', 5); + rhs.delta.add(3, 'x', 6); + rhs.delta.add(4, 'a', 7); + rhs.delta.add(5, 'b', 8); + rhs.delta.add(6, 'x', 9); + rhs.delta.add(6, 'y', 10); + rhs.delta.add(7, 'y', 11); + rhs.delta.add(8, 'z', 12); + rhs.delta.add(9, 'a', 13); + rhs.delta.add(10, 'b', 14); + + SECTION("LHS | RHS") { + Nft expected_full(64, { 0 }, { 12, 22, 44, 63 }, Levels({ 0, 1, 2, 3, 4, 5, 6, 5, 6, 6, 7, 8, 0, 2, 3, 4, 5, 6, 5, 6, 7, 8, 0, 6, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 5, 6, 6, 7, 8, 0, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 5, 6, 6, 7, 8, 0 })); + expected_full.delta.add(0, 'a', 1); + expected_full.delta.add(1, 'c', 2); + expected_full.delta.add(1, 'b', 13); + expected_full.delta.add(2, 'f', 3); + expected_full.delta.add(3, 's', 4); + expected_full.delta.add(4, 't', 5); + expected_full.delta.add(5, 'v', 6); + expected_full.delta.add(4, 'u', 7); + expected_full.delta.add(7, 'w', 8); + expected_full.delta.add(7, 'x', 9); + expected_full.delta.add(9, 'y', 10); + expected_full.delta.add(10, 'j', 11); + expected_full.delta.add(11, 'b', 12); + expected_full.delta.add(13, 'e', 14); + expected_full.delta.add(14, 's', 15); + expected_full.delta.add(15, 't', 16); + expected_full.delta.add(16, 'v', 17); + expected_full.delta.add(15, 'u', 18); + expected_full.delta.add(18, 'w', 19); + expected_full.delta.add(19, 'b', 20); + expected_full.delta.add(20, 'h', 21); + expected_full.delta.add(21, 'z', 22); + expected_full.delta.add(18, 'x', 23); + expected_full.delta.add(0, 'a', 24); + expected_full.delta.add(24, 'b', 25); + expected_full.delta.add(25, 'd', 26); + expected_full.delta.add(26, EPSILON, 27); + expected_full.delta.add(27, EPSILON, 28); + expected_full.delta.add(28, EPSILON, 29); + expected_full.delta.add(29, EPSILON, 30); + expected_full.delta.add(30, 'g', 31); + expected_full.delta.add(31, EPSILON, 32); + expected_full.delta.add(32, 'k', 33); + expected_full.delta.add(33, 'm', 34); + expected_full.delta.add(34, 'o', 35); + expected_full.delta.add(35, 's', 36); + expected_full.delta.add(36, 't', 37); + expected_full.delta.add(37, 'v', 38); + expected_full.delta.add(36, 'u', 39); + expected_full.delta.add(39, 'w', 40); + expected_full.delta.add(39, 'x', 41); + expected_full.delta.add(41, 'x', 42); + expected_full.delta.add(42, 'q', 43); + expected_full.delta.add(43, 'a', 44); + expected_full.delta.add(25, 'e', 45); + expected_full.delta.add(45, EPSILON, 46); + expected_full.delta.add(46, EPSILON, 47); + expected_full.delta.add(47, EPSILON, 48); + expected_full.delta.add(48, EPSILON, 49); + expected_full.delta.add(49, 'i', 50); + expected_full.delta.add(50, EPSILON, 51); + expected_full.delta.add(51, 'l', 52); + expected_full.delta.add(52, 'n', 53); + expected_full.delta.add(53, 'p', 54); + expected_full.delta.add(54, 's', 55); + expected_full.delta.add(55, 't', 56); + expected_full.delta.add(56, 'v', 57); + expected_full.delta.add(55, 'u', 58); + expected_full.delta.add(58, 'w', 59); + expected_full.delta.add(58, 'x', 60); + expected_full.delta.add(60, 'y', 61); + expected_full.delta.add(61, 'r', 62); + expected_full.delta.add(62, 'b', 63); + Nft expected_proj = project_out(expected_full, { 6 }, JumpMode::NoJump); + + Nft result_full = compose(lhs, rhs, 3, 3, false, JumpMode::NoJump); + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(lhs, rhs, 3, 3, true, JumpMode::NoJump).trim(); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } + + SECTION("RHS | LHS") { + Nft expected_full(77, { 0 }, { 18, 27, 54, 76 }, Levels({ 0, 1, 2, 3, 4, 5, 6, 5, 6, 2, 3, 4, 5, 6, 5, 6, 7, 8, 0, 3, 4, 5, 5, 6, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 2, 3, 4, 5, 6, 3, 4, 5, 6, 7, 8, 0, 6, 7, 8, 0, 1, 2, 3, 4, 5, 6, 2, 3, 4, 5, 6, 3, 4, 5, 6, 7, 8, 0 })); + expected_full.delta.add(0, 's', 1); + expected_full.delta.add(1, 't', 2); + expected_full.delta.add(2, 'v', 3); + expected_full.delta.add(3, 'a', 4); + expected_full.delta.add(4, 'c', 5); + expected_full.delta.add(5, 'f', 6); + expected_full.delta.add(4, 'b', 7); + expected_full.delta.add(7, 'e', 8); + expected_full.delta.add(1, 'u', 9); + expected_full.delta.add(9, 'w', 10); + expected_full.delta.add(10, 'a', 11); + expected_full.delta.add(11, 'c', 12); + expected_full.delta.add(12, 'f', 13); + expected_full.delta.add(11, 'b', 14); + expected_full.delta.add(14, 'e', 15); + expected_full.delta.add(15, 'b', 16); + expected_full.delta.add(16, 'z', 17); + expected_full.delta.add(17, 'h', 18); + expected_full.delta.add(9, 'x', 19); + expected_full.delta.add(19, 'a', 20); + expected_full.delta.add(20, 'b', 21); + expected_full.delta.add(21, 'e', 23); + expected_full.delta.add(20, 'c', 22); + expected_full.delta.add(22, 'f', 24); + expected_full.delta.add(24, 'y', 25); + expected_full.delta.add(25, 'b', 26); + expected_full.delta.add(26, 'j', 27); + expected_full.delta.add(0, EPSILON, 28); + expected_full.delta.add(28, EPSILON, 29); + expected_full.delta.add(29, EPSILON, 30); + expected_full.delta.add(30, 'a', 31); + expected_full.delta.add(31, 'b', 32); + expected_full.delta.add(32, 'd', 33); + expected_full.delta.add(33, EPSILON, 34); + expected_full.delta.add(34, EPSILON, 35); + expected_full.delta.add(35, 'g', 36); + expected_full.delta.add(36, 's', 37); + expected_full.delta.add(37, 't', 38); + expected_full.delta.add(38, 'v', 39); + expected_full.delta.add(39, 'k', 40); + expected_full.delta.add(40, 'm', 41); + expected_full.delta.add(41, 'o', 42); + expected_full.delta.add(37, 'u', 43); + expected_full.delta.add(43, 'w', 44); + expected_full.delta.add(44, 'k', 45); + expected_full.delta.add(45, 'm', 46); + expected_full.delta.add(46, 'o', 47); + expected_full.delta.add(43, 'x', 48); + expected_full.delta.add(48, 'k', 49); + expected_full.delta.add(49, 'm', 50); + expected_full.delta.add(50, 'o', 51); + expected_full.delta.add(51, 'x', 52); + expected_full.delta.add(52, 'a', 53); + expected_full.delta.add(53, 'q', 54); + expected_full.delta.add(32, 'e', 55); + expected_full.delta.add(55, EPSILON, 56); + expected_full.delta.add(56, EPSILON, 57); + expected_full.delta.add(57, 'i', 58); + expected_full.delta.add(58, 's', 59); + expected_full.delta.add(59, 't', 60); + expected_full.delta.add(60, 'v', 61); + expected_full.delta.add(61, 'l', 62); + expected_full.delta.add(62, 'n', 63); + expected_full.delta.add(63, 'p', 64); + expected_full.delta.add(59, 'u', 65); + expected_full.delta.add(65, 'w', 66); + expected_full.delta.add(66, 'l', 67); + expected_full.delta.add(67, 'n', 68); + expected_full.delta.add(68, 'p', 69); + expected_full.delta.add(65, 'x', 70); + expected_full.delta.add(70, 'l', 71); + expected_full.delta.add(71, 'n', 72); + expected_full.delta.add(72, 'p', 73); + expected_full.delta.add(73, 'y', 74); + expected_full.delta.add(74, 'b', 75); + expected_full.delta.add(75, 'r', 76); + Nft expected_proj = project_out(expected_full, { 6 }, JumpMode::NoJump); + + Nft result_full = compose(rhs, lhs, 3, 3, false, JumpMode::NoJump); + CHECK(result_full.final.size() == expected_full.final.size()); + CHECK(result_full.num_of_states() <= expected_full.num_of_states()); + CHECK(result_full.levels.num_of_levels == expected_full.levels.num_of_levels); + CHECK(result_full.delta.num_of_transitions() <= expected_full.delta.num_of_transitions()); + result_full.trim(); + result_full.remove_epsilon(); + expected_full.trim(); + expected_full.remove_epsilon(); + CHECK(are_equivalent(result_full, expected_full)); + + Nft result_proj = compose(rhs, lhs, 3, 3, true, JumpMode::NoJump).trim(); + CHECK(result_proj.final.size() == expected_proj.final.size()); + CHECK(result_proj.num_of_states() <= expected_proj.num_of_states()); + CHECK(result_proj.levels.num_of_levels == expected_proj.levels.num_of_levels); + CHECK(result_proj.delta.num_of_transitions() <= expected_proj.delta.num_of_transitions()); + result_proj.trim(); + result_proj.remove_epsilon(); + expected_proj.trim(); + expected_proj.remove_epsilon(); + CHECK(are_equivalent(result_proj, expected_proj)); + } +} diff --git a/tests/nft/nft.cc b/tests/nft/nft.cc index 027b3cacf..3f2fe8eee 100644 --- a/tests/nft/nft.cc +++ b/tests/nft/nft.cc @@ -5505,7 +5505,7 @@ TEST_CASE("mata::nft::Nft::apply()") { Nfa nfa = nfa::builder::create_from_regex("da+b+ce"); mata::EnumAlphabet alphabet{ 'a', 'b', 'c', 'd', 'e', 'f' }; Nft nft{ mata::applications::strings::replace::replace_reluctant_regex("a+b+c", { 'f' }, &alphabet) }; - Nft nft_applied_nfa{ nft.apply(nfa, 0) }; + Nft nft_applied_nfa{ nft.apply(nfa, 0, true, mata::nft::JumpMode::NoJump) }; Nfa result{ nft_applied_nfa.to_nfa_move() }; result.remove_epsilon(); result.trim(); @@ -5521,10 +5521,8 @@ TEST_CASE("mata::nft::Nft::apply()") { SECTION("replace reluctant literal NFT") { Nfa nfa = nfa::builder::create_from_regex("dabce"); mata::EnumAlphabet alphabet{ 'a', 'b', 'c', 'd', 'e', 'f' }; - Nft nft{ - mata::applications::strings::replace::replace_reluctant_literal({ 'a', 'b', 'c' }, { 'f' }, &alphabet) - }; - Nft nft_applied_nfa{ nft.apply(nfa, 0) }; + Nft nft{ mata::applications::strings::replace::replace_reluctant_literal({'a', 'b', 'c' }, { 'f' }, &alphabet) }; + Nft nft_applied_nfa{ nft.apply(nfa, 0, true, JumpMode::NoJump) }; Nfa result{ nft_applied_nfa.to_nfa_move() }; result.remove_epsilon(); result.trim(); @@ -5541,8 +5539,8 @@ TEST_CASE("mata::nft::Nft::apply()") { Nfa nfa = nfa::builder::create_from_regex("(a|b)*"); Nft nft{ Nft::with_levels({ 5, { 0, 0 } }, 1, { 0 }, { 0 }) }; nft.insert_identity(0, 'a'); - CHECK(nft.apply(nfa).levels.num_of_levels == 4); - CHECK(nft.apply(nfa, 3, false).levels.num_of_levels == 5); + CHECK(nft.apply(nfa, 0, true, JumpMode::NoJump).levels.num_of_levels == 4); + CHECK(nft.apply(nfa, 3, false, JumpMode::NoJump).levels.num_of_levels == 5); } }