From 9a8becb8d89014718fb94afaf1c1f8df3b55c7c4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 31 Aug 2014 18:12:28 +0200
Subject: [PATCH] ltlcross: fix missing check for complement of negative
 automata

* src/bin/ltlcross.cc: Fix it.
* src/tgbatest/ltl2dstar.test: Test it.
* NEWS: Mention it.
---
 NEWS                        |  9 +++++++++
 src/bin/ltlcross.cc         |  2 +-
 src/tgbatest/ltl2dstar.test | 16 +++++++++++++++-
 3 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index 398ab6366..12456d143 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,15 @@ New in spot 1.2.5a (not yet released)
 
     - ltlcross --verbose is a new option to see what is being done
 
+  * Bug fixes:
+
+    - When the automaton resulting from the translation of a positive
+      formula is deterministic, ltlcross will compute its complement
+      to perform additional checks against other translations of the
+      positive formula.  The same procedure should be performed with
+      automata obtained from negated formulas, but because of a typo
+      this was not the case.
+
 New in spot 1.2.5 (2014-08-21)
 
   * New features:
diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index a79f276dd..8fb70d3e5 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -1473,7 +1473,7 @@ namespace
 		      problems +=
 			check_empty_prod(pos[i], comp_pos[j],
 					 i, j, false, true);
-		    if (i != j && comp_neg[i] && !comp_neg[i])
+		    if (i != j && comp_neg[i] && !comp_pos[i])
 		      problems +=
 			check_empty_prod(comp_neg[i], neg[j],
 					 i, j, true, false);
diff --git a/src/tgbatest/ltl2dstar.test b/src/tgbatest/ltl2dstar.test
index 190bc149b..640c3fd23 100755
--- a/src/tgbatest/ltl2dstar.test
+++ b/src/tgbatest/ltl2dstar.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -61,3 +61,17 @@ grep '"in_type"' out.csv
 grep '"DSA"' out.csv
 grep '"DRA"' out.csv
 grep ',,,,' out.csv
+
+
+# A bug in ltlcross <=1.2.5 caused it to not use the complement of the
+# negative automaton.  So running ltlcross with GFa would check one
+# complement (the positive one), but running with FGa would ignore
+# the negative complement.
+$ltlcross -f 'GFa' --verbose \
+"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
+"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
+test `grep -c 'info: check_empty.*Comp' err` = 1
+$ltlcross -f 'FGa' --verbose \
+"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
+"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
+test `grep -c 'info: check_empty.*Comp' err` = 1