diff --git a/spot/twaalgos/forq_contains.cc b/spot/twaalgos/forq_contains.cc index 94bad76a6..6292dbe76 100644 --- a/spot/twaalgos/forq_contains.cc +++ b/spot/twaalgos/forq_contains.cc @@ -628,9 +628,6 @@ namespace spot if (lhs->get_dict() != rhs->get_dict()) throw std::runtime_error ("The two input automata must use the same twa_dict."); - if (lhs->ap() != rhs->ap()) - throw std::runtime_error("The two input graphs must use the same set " - "of APs"); forq::forq_setup setup = forq::create_forq_setup(lhs, rhs); diff --git a/tests/python/forq_contains.py b/tests/python/forq_contains.py index 8525f3f92..5c94c3946 100644 --- a/tests/python/forq_contains.py +++ b/tests/python/forq_contains.py @@ -349,3 +349,15 @@ else: tc.assertEqual(str(one.exclusive_word(both)), "!a & !b; cycle{a}") spot.containment_select_version("default") tc.assertEqual(str(one.exclusive_word(both)), "cycle{a}") + +tba2 = spot.translate('GFa & GFb', "buchi") +spot.containment_select_version("default") +tc.assertTrue(spot.contains(tba, tba2)) +tc.assertFalse(spot.contains(tba2, tba)) +spot.containment_select_version("forq") +tc.assertTrue(spot.contains(tba, tba2)) +tc.assertFalse(spot.contains(tba2, tba)) + +a = spot.translate("(p0 & p2) -> G!p1", "buchi") +b = spot.translate("p0 -> G!p1", "buchi") +do_symmetric_test(b, a)