Fix inclusion into an automaton with no root states (#40)

include/autoq/inclusion_bfs.hh

@@ -34,6 +34,9 @@ bool inclusion_bfs_holds(
     LeafPolicy& policy)
 {
     using Aut = AUTOQ::Automata<Symbol>;
+    // 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<typename Aut::State, typename Aut::StateSet> Cell;
     typedef std::set<Cell> Vertex;

src/inclusion/inclusion_index.cc

@@ -17,6 +17,14 @@ bool inclusion_index_compare(const IndexAutomata &autA, const IndexAutomata &aut
     std::vector<std::map<IndexAutomata::Symbol, std::map<IndexAutomata::Tag, IndexAutomata::StateVector>>> 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<IndexAutomata::State, IndexAutomata::StateSet> Cell;
     typedef std::set<Cell> Vertex;

src/reduce.cc

@@ -317,6 +317,7 @@ void AUTOQ::Automata<Symbol>::bottom_up_reduce(int starts_from_depth) {
     // std::map<std::map<Symbol, std::map<StateVector, Tag>>, State> repr; // 9.9 sec in make test
     std::unordered_map<std::map<Symbol, std::map<StateVector, Tag>>, State, HASH<Symbol>> repr; // 9.6 sec in make test
     std::map<State, State> rewrite;
+    std::map<State, State> 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<Symbol>::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<Symbol>::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<Symbol>::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();
 }
 

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<AUTOQ::Symbol::Concrete>::ReadAutomaton(folder + "zero.lsta");
+    auto empty = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Concrete>::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<AUTOQ::Symbol::Symbolic>::ReadAutomaton(folder + "zero_sym.lsta");
+    auto empty_sym = AUTOQ::Parsing::TimbukParser<AUTOQ::Symbol::Symbolic>::ReadAutomaton(folder + "empty.lsta");
+    BOOST_CHECK(!(zero_sym <<= empty_sym));
+}

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

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

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