From 1c5468a93a89f7dcc27fd060bcf204be8e9db52b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 22 Jul 2020 16:23:34 +0200
Subject: [PATCH] simplify: fix handling of keep_top_xor

Under that option, !(a ^ b) was converted
to (!a <=> !b) instead of simply (a <=> b).

* spot/tl/simplify.cc (equiv_or_xor): Improve
rewriting.
* tests/core/ltl2tgba2.test, tests/python/simstate.py: Adjust test
cases.
---
 NEWS                      |  9 +++++++--
 spot/tl/simplify.cc       | 16 ++++++++--------
 tests/core/ltl2tgba2.test |  4 ++--
 tests/python/simstate.py  |  6 +++---
 4 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/NEWS b/NEWS
index c6cdb07ed..65a99887b 100644
--- a/NEWS
+++ b/NEWS
@@ -45,18 +45,23 @@ New in spot 2.9.3.dev  (not yet released)
     file. With this refactoring, we can retrieve both a kripke or a
     kripkecube from a PINS file.
 
+  Bugs fixed:
+
+  - Handle xor and <-> in a more natural way when translating
+    LTL formulas to generic acceptancee conditions.
+
 New in spot 2.9.3 (2020-07-22)
 
   Bug fixed:
 
-  - Completely fix the ltlcross issue mentionned in previous release.
+  - Completely fix the ltlcross issue mentioned in previous release.
 
 New in spot 2.9.2 (2020-07-21)
 
   Bugs fixed:
 
   - ltlcross --csv=... --product=N with N>0 could output spurious
-    diagnosics claiming that words were rejected when evaluating
+    diagnostics claiming that words were rejected when evaluating
     the automaton on state-space.
 
   - spot::scc_info::determine_unknown_acceptance() now also update the
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 24f94d5eb..2848c3e9e 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -431,12 +431,12 @@ namespace spot
       if (equiv)
         {
           // Rewrite a<=>b as (a&b)|(!a&!b)
-          auto recurse_f1_true = rec(f1, true);
-          auto recurse_f2_true = rec(f2, true);
-          if (!deep && c->options.keep_top_xor)
-            return formula::Equiv(recurse_f1_true, recurse_f2_true);
           auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_false = rec(f2, false);
+          if (!deep && c->options.keep_top_xor)
+            return formula::Equiv(recurse_f1_false, recurse_f2_false);
+          auto recurse_f1_true = rec(f1, true);
+          auto recurse_f2_true = rec(f2, true);
           auto left = formula::And({recurse_f1_false, recurse_f2_false});
           auto right = formula::And({recurse_f1_true, recurse_f2_true});
           return formula::Or({left, right});
@@ -444,12 +444,12 @@ namespace spot
       else
         {
           // Rewrite a^b as (a&!b)|(!a&b)
-          auto recurse_f1_true = rec(f1, true);
-          auto recurse_f2_true = rec(f2, true);
-          if (!deep && c->options.keep_top_xor)
-            return formula::Xor(recurse_f1_true, recurse_f2_true);
           auto recurse_f1_false = rec(f1, false);
           auto recurse_f2_false = rec(f2, false);
+          if (!deep && c->options.keep_top_xor)
+            return formula::Xor(recurse_f1_false, recurse_f2_false);
+          auto recurse_f1_true = rec(f1, true);
+          auto recurse_f2_true = rec(f2, true);
           auto left = formula::And({recurse_f1_false, recurse_f2_true});
           auto right = formula::And({recurse_f1_true, recurse_f2_false});
           return formula::Or({left, right});
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index 22c7c215c..1878e3efd 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -453,9 +453,9 @@ test 1,3,2 = `ltl2tgba -G -D "(GFp0 | FGp1)" --stats=%s,%e,%a`
 
 # Handling of Xor and <-> by ltl-split and -D -G.
 res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) <-> GFe)' --stats='%s %g'`
-test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
-res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
 test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))"
+res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
+test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
 ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe'
 
 f='G(p1 | G!p0) M Xp1'
diff --git a/tests/python/simstate.py b/tests/python/simstate.py
index 1be3d9a94..8e5e1c712 100644
--- a/tests/python/simstate.py
+++ b/tests/python/simstate.py
@@ -178,13 +178,13 @@ b.copy_state_names_from(a)
 assert b.to_str() == """HOA: v1
 States: 1
 Start: 0
-AP: 2 "p1" "p0"
+AP: 2 "p0" "p1"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0 "[1,7]"
-[!0] 0 {0}
-[0] 0
+[!1] 0 {0}
+[1] 0
 --END--"""