whitemech · marcofavorito · Mar 22, 2020 · Feb 28, 2020 · Feb 28, 2020 · Feb 28, 2020
diff --git a/pythomata/impl/symbolic.py b/pythomata/impl/symbolic.py
@@ -305,16 +305,27 @@ def greatest_fixpoint_condition(el: Tuple[int, int], current_set: Set):
             class2newstate[state2class[final_state]]
             for final_state in dfa.accepting_states
         }
-        transitions = set()
 
+        # normalize transitions
+        from_edge_to_guard = {}  # type: Dict[Tuple[int, int], BooleanFunction]
         for old_source in dfa._transition_function:
             for old_dest, guard in dfa._transition_function[old_source].items():
                 new_source = class2newstate[state2class[old_source]]
                 new_dest = class2newstate[state2class[old_dest]]
-                transitions.add((new_source, guard, new_dest))
+
+                edge = (new_source, new_dest)
+                if edge in from_edge_to_guard:
+                    old_guard = from_edge_to_guard[edge]
+                    new_guard = (guard | old_guard).simplify()
+                else:
+                    new_guard = guard
+                from_edge_to_guard[(new_source, new_dest)] = new_guard
 
         return SymbolicAutomaton._from_transitions(
-            new_states, initial_state, final_states, transitions
+            new_states,
+            initial_state,
+            final_states,
+            {(u, guard, v) for ((u, v), guard) in from_edge_to_guard.items()},
         )
 
     @classmethod

diff --git a/tests/test_symbolic_automaton.py b/tests/test_symbolic_automaton.py
@@ -9,6 +9,7 @@
 from sympy.logic.boolalg import BooleanTrue
 
 from pythomata import SymbolicAutomaton
+from pythomata.impl.symbolic import SymbolicDFA
 from pythomata.simulator import AutomatonSimulator
 from .strategies import propositional_words
 
@@ -416,6 +417,42 @@ def test_minimized_is_complete(self):
         assert self.minimized.is_complete()
 
 
+class TestMinimizeWhenNoAcceptingState:
+    @classmethod
+    def setup_class(cls):
+        """Set the tests up."""
+        cls.automaton = SymbolicDFA()
+        automaton = cls.automaton
+        q0 = automaton.create_state()
+        q1 = automaton.create_state()
+        q2 = automaton.create_state()
+        q3 = automaton.create_state()
+        q4 = automaton.create_state()
+
+        automaton.set_initial_state(q0)
+        automaton.add_transition((q0, "a", q1))
+        automaton.add_transition((q0, "b", q2))
+        automaton.add_transition((q1, "c", q3))
+        automaton.add_transition((q2, "c", q3))
+        automaton.add_transition((q3, "c", q4))
+        automaton.add_transition((q4, "c", q4))
+
+        cls.minimized = automaton.minimize()
+
+    def test_states(self):
+        # the renaming of the states is non deterministic, so we need to compare every substructure.
+        assert self.minimized.size == 1
+
+    @given(propositional_words(list("abc"), min_size=0, max_size=5))
+    def test_accepts(self, word):
+        """Test equivalence of acceptance between the two automata."""
+        assert self.automaton.accepts(word) == self.minimized.accepts(word)
+
+    def test_minimized_is_complete(self):
+        """Test that every minimized DFA is complete."""
+        assert self.minimized.is_complete()
+
+
 def test_to_graphviz():
     """Test 'to_graphviz' method."""