Fix a bug when the automaton contain trivial acceptance conditions

hoa/parsers.py

@@ -207,12 +207,19 @@ def acceptance(self, args):
         actual_nb_accepting_sets = nb_accepting_sets(acceptance_condition)
         accepting_sets_ = accepting_sets(acceptance_condition)
         # this checks whether the number of acc. sets in the acceptance condition is correct.
-        assert_(
-            max(accepting_sets_)
-            == len(accepting_sets_) - 1
-            == expected_nb_accepting_sets - 1
-            == actual_nb_accepting_sets - 1
-        )
+        if expected_nb_accepting_sets > 0:
+            assert_(
+                max(accepting_sets_)
+                ==  len(accepting_sets_) - 1
+                == expected_nb_accepting_sets - 1
+                == actual_nb_accepting_sets - 1,
+            )
+        else:
+            assert_(
+                len(accepting_sets_)
+                == expected_nb_accepting_sets
+                == actual_nb_accepting_sets,
+            )
         return HeaderItemType.ACCEPTANCE, acceptance_condition
 
     def acc_name(self, args):

tests/examples/aut12.hoa

@@ -0,0 +1,18 @@
+HOA: v1
+name: "(Fa & G(b&Xc)) | c"
+States: 4
+Start: 0&2
+Start: 3
+Acceptance: 0 t
+AP: 3 "a" "b" "c"
+--BODY--
+State: 0 "Fa"
+[t] 0
+[0] 1
+State: 1 "true"
+[t] 1
+State: 2 "G(b&Xc)"
+[1] 2&3
+State: 3 "c"
+[2] 1
+--END--

tests/test_parsing.py

@@ -23,7 +23,7 @@
 import pytest
 
 from hoa.ast.acceptance import Fin, Inf, nb_accepting_sets
-from hoa.ast.boolean_expression import TRUE
+from hoa.ast.boolean_expression import TRUE, TrueFormula
 from hoa.ast.label import LabelAlias, LabelAtom
 from hoa.core import Acceptance, Edge, HOA, HOABody, HOAHeader, State
 from hoa.dumpers import dump
@@ -584,3 +584,43 @@ def test_hoa(self):
 
         hoa_obj = HOA(hoa_header, hoa_body)
         assert self.hoa_obj == hoa_obj
+
+
+class TestParsingAut12:
+    """Test parsing for tests/examples/aut11."""
+
+    @classmethod
+    def setup_class(cls):
+        """Set the test up."""
+        parser = HOAParser()
+        cls.hoa_obj: HOA = parser(
+            Path(TEST_ROOT_DIR, "examples", "aut12.hoa").read_text()
+        )
+        cls.hoa_header = cls.hoa_obj.header
+        cls.hoa_body = cls.hoa_obj.body
+
+    def test_hoa(self):
+        """Test that the HOA automaton is correct."""
+        hoa_header = HOAHeader(
+            identifier("v1"),
+            Acceptance(TrueFormula(), None),
+            nb_states=4,
+            start_states={frozenset([0, 2]), frozenset([3])},
+            propositions=(string("a"), string("b"), string("c")),
+            name=string("(Fa & G(b&Xc)) | c"),
+        )
+
+        state_edges_dict = OrderedDict({})
+        state_edges_dict[State(0, name=string("Fa"))] = [
+            Edge([0], label=TRUE),
+            Edge([1], label=LabelAtom(0)),
+        ]
+        state_edges_dict[State(1, name=string("true"))] = [Edge([1], label=TRUE)]
+        state_edges_dict[State(2, name=string("G(b&Xc)"))] = [
+            Edge([2, 3], label=LabelAtom(1))
+        ]
+        state_edges_dict[State(3, name=string("c"))] = [Edge([1], label=LabelAtom(2))]
+        hoa_body = HOABody(state_edges_dict)
+
+        hoa_obj = HOA(hoa_header, hoa_body)
+        assert self.hoa_obj == hoa_obj