diff --git a/tests/core/safra.test b/tests/core/safra.test index 2257450b7..a758b7631 100755 --- a/tests/core/safra.test +++ b/tests/core/safra.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -171,9 +171,14 @@ Fa W Gb Ga | GFb a M G(F!b | X!a) G!a R XFb +F(G((a) | (F(b)))) +FG(!p1 | (p1 M XX!p1)) EOF run 0 ../safra --hoa double_b.hoa -H > out.hoa -ltl2tgba=ltl2tgba ltlcross -F formulae \ "../safra -f %f -H > %O" \ - "$ltl2tgba -f %f -H > %O" + "../safra --scc_opt -f %f -H > %O" \ + "../safra --bisim_opt -f %f -H > %O" \ + "../safra --stutter -f %f -H > %O" \ + "../safra --scc_opt --bisim_opt --stutter -f %f -H > %O" \ + "ltl2tgba"