twa_graph: do not order BDDs by IDs in merge_edges()

Fixes #282.

* spot/misc/bddlt.hh (bdd_less_than_stable): New function.
* spot/twa/twagraph.cc (merge_edges): Use it.
* tests/core/genltl.test: Adjust, and add an extra test
for the behavior of #282.
* tests/core/complement.test, tests/core/degenid.test,
tests/core/ltldo.test, tests/core/prodor.test,
tests/core/readsave.test, tests/core/sbacc.test,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/dualize.py,
tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
tests/python/product.ipynb, tests/python/simstate.py,
tests/python/tra2tba.py: Adjust all expected outputs.
* NEWS: Mention the bug.

tests/core/complement.test

@@ -62,10 +62,10 @@ properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0
-[0&1] 0 {0 1}
 [!0&!1] 0
 [!0&1] 0 {1}
 [0&!1] 0 {0}
+[0&1] 0 {0 1}
 --END--
 HOA: v1
 States: 4

tests/core/degenid.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2011, 2013, 2014, 2015, 2017 Laboratoire de Recherche
+# et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -242,15 +242,15 @@ State: 0
 [0] 1
 State: 1 {0}
 [1&2] 1
-[!1&2] 2
-[!2] 3
+[!2] 2
+[!1&2] 3
 State: 2
-[1] 1
-[!1] 2
-State: 3
 [1&2] 1
-[!1&2] 2
-[!2] 3
+[!2] 2
+[!1&2] 3
+State: 3
+[1] 1
+[!1] 3
 --END--
 EOF
 diff out expected

tests/core/genltl.test

@@ -136,7 +136,7 @@ test $(genltl --kr-nlogn=4 | ltl2tgba --low --stats=%s) -ge 16
 test $(genltl --kr-n=4 | ltl2tgba --low --stats=%s) -ge 16
 
 genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
-       --format=%F=%L,%f |
+       --gf-equiv=0..5 --format=%F=%L,%f |
     ltl2tgba -G -D -F-/2 --stats='%<,%s' > out
 cat >exp<<EOF
 ms-example=0,1
@@ -146,21 +146,15 @@ ms-example=3,7
 ms-example=4,12
 ms-phi-r=0,2
 ms-phi-r=1,16
-ms-phi-r=2,25
+ms-phi-r=2,29
 ms-phi-s=0,5
-ms-phi-s=1,7
-ms-phi-s=2,1322
+ms-phi-s=1,8
+ms-phi-s=2,497
 ms-phi-h=0,2
 ms-phi-h=1,4
 ms-phi-h=2,21
 ms-phi-h=3,170
 ms-phi-h=4,1816
-EOF
-diff out exp
-
-genltl --gf-equiv=0..5 --format=%F=%L,%f |
-  ltl2tgba -G -D -F-/2 --stats='%<,%s' > out
-cat >exp<<EOF
 gf-equiv=0,1
 gf-equiv=1,4
 gf-equiv=2,8
@@ -169,3 +163,9 @@ gf-equiv=4,81
 gf-equiv=5,431
 EOF
 diff out exp
+
+# Running ltl2tgba on one formula at a time should give the same results
+genltl --ms-example=0..4 --ms-phi-r=0..2 --ms-phi-s=0..2 --ms-phi-h=0..4 \
+       --gf-equiv=0..5 --format=%F=%L,%f |
+    ltldo -F-/2 'ltl2tgba -G -D' --stats='%<,%s' > out
+diff out exp

tests/core/ltldo.test

@@ -82,8 +82,8 @@ properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0
-[0] 0 {0}
 [!0] 0
+[0] 0 {0}
 --END--
 EOF
 diff output expected
@@ -103,8 +103,8 @@ properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic stutter-invariant
 --BODY--
 State: 0
-[0] 0 {0}
 [!0] 0
+[0] 0 {0}
 --END--
 EOF
 diff output expected
@@ -124,8 +124,8 @@ properties: trans-labels explicit-labels trans-acc complete
 properties: deterministic
 --BODY--
 State: 0
-[0] 0 {0}
 [!0] 0
+[0] 0 {0}
 --END--
 EOF
 diff output expected

tests/core/prodor.test

@@ -65,18 +65,18 @@ properties: trans-labels explicit-labels trans-acc complete
 properties: stutter-invariant
 --BODY--
 State: 0
-[0] 0 {1}
 [!0] 0
-[0&1] 1 {1}
+[0] 0 {1}
 [!0&1] 1
+[0&1] 1 {1}
 State: 1
-[0&1] 1 {0 1}
 [!0&1] 1 {0}
-[0&!1] 2 {0 1}
+[0&1] 1 {0 1}
 [!0&!1] 2 {0}
+[0&!1] 2 {0 1}
 State: 2
-[0] 2 {1}
 [!0] 2
+[0] 2 {1}
 --END--
 EOF
 diff por.hoa exp
@@ -96,13 +96,13 @@ Acceptance: 2 Inf(0)&Inf(1)
 properties: trans-labels explicit-labels trans-acc stutter-invariant
 --BODY--
 State: 0
-[0] 0 {1}
 [!0] 0
-[0&1] 1 {1}
+[0] 0 {1}
 [!0&1] 1
+[0&1] 1 {1}
 State: 1
-[0&1] 1 {0 1}
 [!0&1] 1 {0}
+[0&1] 1 {0 1}
 --END--
 EOF
 diff pand.hoa exp

tests/core/readsave.test

@@ -363,10 +363,10 @@ digraph G {
   I [label="", style=invis, width=0]
   I -> 0
   0 [label="0"]
-  0 -> 0 [label="a & b\n{0,1}"]
   0 -> 0 [label="!a & !b"]
   0 -> 0 [label="!a & b\n{1}"]
   0 -> 0 [label="a & !b\n{0}"]
+  0 -> 0 [label="a & b\n{0,1}"]
 }
 EOF
 diff output expected
@@ -382,10 +382,10 @@ digraph G {
   I [label="", style=invis, width=0]
   I -> 0
   0 [label="0"]
-  0 -> 0 [label="a & b\n⓿❶"]
   0 -> 0 [label="!a & !b"]
   0 -> 0 [label="!a & b\n❶"]
   0 -> 0 [label="a & !b\n⓿"]
+  0 -> 0 [label="a & b\n⓿❶"]
 }
 EOF
 diff output expected
@@ -407,10 +407,10 @@ digraph G {
   I [label="", style=invis, width=0]
   I -> 0
   0 [label=<0>]
-  0 -> 0 [label=<a &amp; b<br/>$zero$one>]
   0 -> 0 [label=<!a &amp; !b>]
   0 -> 0 [label=<!a &amp; b<br/>$one>]
   0 -> 0 [label=<a &amp; !b<br/>$zero>]
+  0 -> 0 [label=<a &amp; b<br/>$zero$one>]
 }
 EOF
 diff output expected

tests/core/sbacc.test

@@ -37,26 +37,26 @@ Acceptance: 2 Inf(0)&Inf(1)
 properties: trans-labels explicit-labels state-acc complete
 properties: deterministic stutter-invariant
 --BODY--
-State: 0 {0}
-[0&!1] 0
-[0&1] 1
-[!0&!1] 2
-[!0&1] 3
-State: 1 {0 1}
-[0&!1] 0
-[0&1] 1
-[!0&!1] 2
-[!0&1] 3
-State: 2
-[0&!1] 0
-[0&1] 1
-[!0&!1] 2
-[!0&1] 3
-State: 3 {1}
-[0&!1] 0
-[0&1] 1
-[!0&!1] 2
-[!0&1] 3
+State: 0 {0 1}
+[0&1] 0
+[!0&!1] 1
+[!0&1] 2
+[0&!1] 3
+State: 1
+[0&1] 0
+[!0&!1] 1
+[!0&1] 2
+[0&!1] 3
+State: 2 {1}
+[0&1] 0
+[!0&!1] 1
+[!0&1] 2
+[0&!1] 3
+State: 3 {0}
+[0&1] 0
+[!0&!1] 1
+[!0&1] 2
+[0&!1] 3
 --END--
 EOF