From 0288aaa3043b733a7661c032c1a3309e6c28272a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 10 Feb 2016 09:51:10 +0100
Subject: [PATCH] determinize: add tests for the bug Alexandre L fixed

* tests/core/safra.test: More tests.
---
 tests/core/safra.test | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

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"
-- 
GitLab