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

@@ -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

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});

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'

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}
+[!1] 0 {0}
-[0] 0
+[1] 0
 --END--"""