diff --git a/hoa/parsers.py b/hoa/parsers.py index c1e4dda..b87c8b6 100644 --- a/hoa/parsers.py +++ b/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): diff --git a/tests/examples/aut12.hoa b/tests/examples/aut12.hoa new file mode 100644 index 0000000..9d28a64 --- /dev/null +++ b/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-- diff --git a/tests/test_parsing.py b/tests/test_parsing.py index f91cbef..11d939f 100644 --- a/tests/test_parsing.py +++ b/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