From 9a617d0c7b186b9094720949d6e2583002622e66 Mon Sep 17 00:00:00 2001 From: Ondra Lengal Date: Tue, 27 Oct 2026 12:06:44 +0100 Subject: [PATCH] Fix inclusion into an automaton with no root states (#40) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The inclusion searches build one source vertex per root state of A from the root states of B. With no root states in B that vertex is empty and *(vertex.begin()) is undefined behaviour: a segfault for a <= b and in ver, unbounded memory growth on the symbolic path. - bottom_up_reduce() could merge a root state into an equivalent state that is not a root and then drop it, so b || zero_amplitude(n) lost the zero vector's root. Merged root states are now mapped to their representative. - inclusion_bfs_holds and inclusion_index_compare return early when B has no root states: A ⊆ ∅ holds iff A is empty. A unit test checks <=, <<= (concrete and symbolic) and the union with the zero vector on an automaton whose root state has no transitions. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013gtFQRPe1eSSpmA7EJ2KNY --- include/autoq/inclusion_bfs.hh | 3 +++ src/inclusion/inclusion_index.cc | 8 +++++++ src/reduce.cc | 16 +++++++++++++ unit_tests/explicit_tree_aut_test.cc | 23 +++++++++++++++++++ unit_tests/testcase/EmptyAutomaton/empty.lsta | 6 +++++ unit_tests/testcase/EmptyAutomaton/zero.lsta | 8 +++++++ .../testcase/EmptyAutomaton/zero_sym.lsta | 8 +++++++ 7 files changed, 72 insertions(+) create mode 100644 unit_tests/testcase/EmptyAutomaton/empty.lsta create mode 100644 unit_tests/testcase/EmptyAutomaton/zero.lsta create mode 100644 unit_tests/testcase/EmptyAutomaton/zero_sym.lsta diff --git a/include/autoq/inclusion_bfs.hh b/include/autoq/inclusion_bfs.hh index d3e1b977c..b9ce934ee 100644 --- a/include/autoq/inclusion_bfs.hh +++ b/include/autoq/inclusion_bfs.hh @@ -34,6 +34,9 @@ bool inclusion_bfs_holds( LeafPolicy& policy) { using Aut = AUTOQ::Automata; + // With no root states B accepts nothing, so A ⊆ B iff A is empty (#40). + if (autB.finalStates.empty()) + return autA.empty(); // Main Routine: Graph Traversal typedef std::map Cell; typedef std::set Vertex; diff --git a/src/inclusion/inclusion_index.cc b/src/inclusion/inclusion_index.cc index 25042fd93..4d125cdc8 100644 --- a/src/inclusion/inclusion_index.cc +++ b/src/inclusion/inclusion_index.cc @@ -17,6 +17,14 @@ bool inclusion_index_compare(const IndexAutomata &autA, const IndexAutomata &aut std::vector>> transB; build_inclusion_trans(autA, autB, transA, transB); + // With no root states B accepts nothing, so A ⊆ B iff A is empty (#40). + if (autB.finalStates.empty()) { + bool holds = autA.empty(); + auto stop_include = std::chrono::steady_clock::now(); + autA.stats_->include_status = AUTOQ::Util::Convert::ToString(stop_include - start_include) + (holds ? "" : " X"); + autA.stats_->total_include_time += stop_include - start_include; + return holds; + } // Main Routine: Graph Traversal typedef std::map Cell; typedef std::set Vertex; diff --git a/src/reduce.cc b/src/reduce.cc index 038fa57bf..a0d6a1805 100644 --- a/src/reduce.cc +++ b/src/reduce.cc @@ -317,6 +317,7 @@ void AUTOQ::Automata::bottom_up_reduce(int starts_from_depth) { // std::map>, State> repr; // 9.9 sec in make test std::unordered_map>, State, HASH> repr; // 9.6 sec in make test std::map rewrite; + std::map merged_into; // every merged-away state -> its representative bool may_be_merged_furthermore = true; /* Convert leaf transitions into the new data structure. */ @@ -344,6 +345,7 @@ void AUTOQ::Automata::bottom_up_reduce(int starts_from_depth) { auto it = repr.find(top_.second); if (it != repr.end()) { rewrite[top] = it->second; + merged_into[top] = it->second; may_be_merged_furthermore = true; } else { // create a new class rewrite[top] = top; @@ -394,6 +396,7 @@ void AUTOQ::Automata::bottom_up_reduce(int starts_from_depth) { auto it = repr.find(top_.second); if (it != repr.end()) { rewrite[top] = it->second; + merged_into[top] = it->second; may_be_merged_furthermore = true; } else { // create a new class rewrite[top] = top; @@ -417,6 +420,19 @@ void AUTOQ::Automata::bottom_up_reduce(int starts_from_depth) { } } transitions = transitions2; + /* A root state can be merged into an equivalent state; that state then + becomes the root instead, or the root would be lost (#40). */ + if (!merged_into.empty()) { + StateVector finalStates2; + for (auto s : finalStates) { + auto m = merged_into.find(s); + if (m != merged_into.end()) + s = m->second; + if (std::find(finalStates2.begin(), finalStates2.end(), s) == finalStates2.end()) + finalStates2.push_back(s); + } + finalStates = finalStates2; + } state_renumbering(); } diff --git a/unit_tests/explicit_tree_aut_test.cc b/unit_tests/explicit_tree_aut_test.cc index 50124d9d0..fc6e87dd4 100644 --- a/unit_tests/explicit_tree_aut_test.cc +++ b/unit_tests/explicit_tree_aut_test.cc @@ -654,3 +654,26 @@ BOOST_AUTO_TEST_CASE(qubit_reordering) } } + +// An automaton whose root state is the target of no transition accepts +// nothing. Inclusion into it must be false, not crash (#40). +BOOST_AUTO_TEST_CASE(inclusion_into_empty_automaton){ + std::string folder = test_dir_from_file(__FILE__, "testcase/EmptyAutomaton/"); + auto zero = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "zero.lsta"); + auto empty = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "empty.lsta"); + BOOST_REQUIRE(empty.finalStates.empty()); + BOOST_CHECK(!(zero <= empty)); + BOOST_CHECK(empty <= zero); + BOOST_CHECK(empty <= empty); + BOOST_CHECK(!(zero <<= empty)); + + // reduce() must not drop the root state of the zero vector when it is + // merged into an equivalent state that is not a root. + auto with_zero = empty || AUTOQ::ConcreteAutomata::zero_amplitude(1); + BOOST_CHECK(!with_zero.finalStates.empty()); + BOOST_CHECK(AUTOQ::ConcreteAutomata::zero_amplitude(1) <= with_zero); + + auto zero_sym = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "zero_sym.lsta"); + auto empty_sym = AUTOQ::Parsing::TimbukParser::ReadAutomaton(folder + "empty.lsta"); + BOOST_CHECK(!(zero_sym <<= empty_sym)); +} diff --git a/unit_tests/testcase/EmptyAutomaton/empty.lsta b/unit_tests/testcase/EmptyAutomaton/empty.lsta new file mode 100644 index 000000000..dba4c7865 --- /dev/null +++ b/unit_tests/testcase/EmptyAutomaton/empty.lsta @@ -0,0 +1,6 @@ +Constants +c0 := 0 +Root States r +Transitions +[1,1](q0, q0) -> s +[c0,1] -> q0 diff --git a/unit_tests/testcase/EmptyAutomaton/zero.lsta b/unit_tests/testcase/EmptyAutomaton/zero.lsta new file mode 100644 index 000000000..d20544bd1 --- /dev/null +++ b/unit_tests/testcase/EmptyAutomaton/zero.lsta @@ -0,0 +1,8 @@ +Constants +c0 := 0 +c1 := 1 +Root States r +Transitions +[1,1](q1, q0) -> r +[c1,1] -> q1 +[c0,1] -> q0 diff --git a/unit_tests/testcase/EmptyAutomaton/zero_sym.lsta b/unit_tests/testcase/EmptyAutomaton/zero_sym.lsta new file mode 100644 index 000000000..4ea64dc44 --- /dev/null +++ b/unit_tests/testcase/EmptyAutomaton/zero_sym.lsta @@ -0,0 +1,8 @@ +Constants +c0 := 0 +c1 := 1 +Root States r +Transitions +[1,1](q1, q0) -> r +[a,1] -> q1 +[c0,1] -> q0