alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

forq: remove the "same AP set" restriction

Browse source 
* spot/twaalgos/forq_contains.cc: Remove the check.
* tests/python/forq_contains.py: Add two test cases for this.
This commit is contained in:
Alexandre Duret-Lutz 2023-09-13 17:46:48 +02:00
parent 6eff384fca
commit 6ac2416e5d
2 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
spot/twaalgos/forq_contains.cc
View file

@ -628,9 +628,6 @@ namespace spot
if (lhs->get_dict() != rhs->get_dict()) if (lhs->get_dict() != rhs->get_dict())
throw std::runtime_error throw std::runtime_error
("The two input automata must use the same twa_dict."); ("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); forq::forq_setup setup = forq::create_forq_setup(lhs, rhs);

12
tests/python/forq_contains.py
View file

@ -349,3 +349,15 @@ else:
tc.assertEqual(str(one.exclusive_word(both)), "!a & !b; cycle{a}") tc.assertEqual(str(one.exclusive_word(both)), "!a & !b; cycle{a}")
spot.containment_select_version("default") spot.containment_select_version("default")
tc.assertEqual(str(one.exclusive_word(both)), "cycle{a}") 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)