From 284fca678b3bdd856a585116d7cdae4fccea5fc3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20Chocholat=C3=BD?= Date: Wed, 1 Jul 2026 11:38:42 +0200 Subject: [PATCH] nft/composition(fix): Skip recomputing synchronization types for precomputed states Skip recomputing synchronization types of targets of transitions from states already computed. --- src/nft/composition.cc | 19 ++++++++++-- tests/nft/nft-composition.cc | 59 +++++++++++++++++++++++++++++++++++- 2 files changed, 74 insertions(+), 4 deletions(-) diff --git a/src/nft/composition.cc b/src/nft/composition.cc index cf39ffc59..75dd942ae 100644 --- a/src/nft/composition.cc +++ b/src/nft/composition.cc @@ -2,11 +2,13 @@ * @brief Composition of two NFTs. */ -#include #include #include -#include "mata/nft/nft.hh" +#include + #include "mata/nft/algorithms.hh" +#include "mata/nft/nft.hh" +#include "mata/utils/assert.hh" #include "mata/utils/two-dimensional-map.hh" @@ -118,7 +120,18 @@ namespace { 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 (current_sync_type != SynchronizationType::UNDEFINED + && current_sync_type != SynchronizationType::UNDER_COMPUTATION) { + // We already computed the synchronization type for this state, so we can skip it. + // It can happen that when a transducer has a state that has multiple transitions to the same + // target, the target can be, in some cases, added to the stack multiple times before the first + // occurrence of the target can be processed. + // See https://github.com/VeriFIT/mata/pull/673. + continue; + } + MATA_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) { diff --git a/tests/nft/nft-composition.cc b/tests/nft/nft-composition.cc index fefbe06be..342db4953 100644 --- a/tests/nft/nft-composition.cc +++ b/tests/nft/nft-composition.cc @@ -4,6 +4,8 @@ #include #include +#include "mata/nft/algorithms.hh" +#include "mata/nft/builder.hh" #include "mata/nft/nft.hh" #include "mata/utils/ord-vector.hh" @@ -13,7 +15,6 @@ using namespace mata::utils; TEST_CASE("Mata::nft::compose()") { - Nft lhs, rhs, expected, result; SECTION("levels_cnt == 2") { @@ -2893,3 +2894,59 @@ TEST_CASE("nft::composition(..., Level, Level, ...) - complex") { CHECK(are_equivalent(result_proj, expected_proj)); } } + +TEST_CASE("mata::nft::compose_fast_no_jump()") { + SECTION("Issue #670") { + const Nft lhs{ mata::nft::builder::parse_from_mata( + std::string{ "@NFT-explicit\n" + "%Alphabet-auto\n" + "%Initial q0\n" + "%Final q1\n" + "%Levels q0:0 q1:0\n" + "%LevelsNum 1\n" + "q0 35 q1\n" } + ) }; + const Nft rhs{ mata::nft::builder::parse_from_mata( + std::string{ "@NFT-explicit\n" + "%Alphabet-auto\n" + "%Initial q0\n" + "%Final q0 q1 q9\n" + "%Levels q0:0 q1:0 q2:0 q3:1 q4:1 q5:1 q6:0 q7:0 q8:1 q9:0 q10:1 q11:0 q12:1 q13:1 q14:1 " + "q15:1\n" + "%LevelsNum 2\n" + "q0 35 q3\n" + "q0 48 q5\n" + "q0 49 q5\n" + "q0 196608 q4\n" + "q1 35 q3\n" + "q1 196608 q4\n" + "q2 48 q5\n" + "q2 49 q5\n" + "q3 35 q1\n" + "q3 35 q2\n" + "q4 196608 q1\n" + "q4 196608 q2\n" + "q5 4294967295 q6\n" + "q5 4294967295 q7\n" + "q6 4294967295 q8\n" + "q7 4294967295 q10\n" + "q8 35 q9\n" + "q9 35 q12\n" + "q9 196608 q13\n" + "q10 35 q11\n" + "q11 48 q14\n" + "q11 49 q15\n" + "q12 35 q9\n" + "q12 35 q11\n" + "q13 196608 q9\n" + "q13 196608 q11\n" + "q14 48 q9\n" + "q14 48 q11\n" + "q15 49 q9\n" + "q15 49 q11\n" } + ) }; + const Nft composed_normal{ compose(lhs, rhs, 0, 1) }; + const Nft composed_fast_no_jump{ algorithms::compose_fast_no_jump(lhs, rhs, 0, 1) }; + CHECK(are_equivalent(composed_normal, composed_fast_no_jump)); + } +}