From 85ff53c45eb344dbb720d465b5822223f2704119 Mon Sep 17 00:00:00 2001
From: Etienne Renault <renault@lrde.epita.fr>
Date: Thu, 7 May 2020 14:07:27 +0200
Subject: [PATCH] twacube: fix erroneous translation

* spot/twacube_algos/convert.cc,
tests/core/twacube.test: Here.
---
 spot/twacube_algos/convert.cc | 24 +++++++++---------------
 tests/core/twacube.test       |  4 +---
 2 files changed, 10 insertions(+), 18 deletions(-)

diff --git a/spot/twacube_algos/convert.cc b/spot/twacube_algos/convert.cc
index 5f0d4ccc2..0f9ff5f18 100644
--- a/spot/twacube_algos/convert.cc
+++ b/spot/twacube_algos/convert.cc
@@ -98,23 +98,17 @@ namespace spot
 
           // Special case for bddfalse
           if (cond == bddfalse)
+            continue;
+
+          // Split the bdd into multiple transitions
+          while (cond != bddfalse)
             {
-              spot::cube cube = tg->get_cubeset().alloc();
-              for (unsigned int i = 0; i < cs.size(); ++i)
-                cs.set_false_var(cube, i); // FIXME ! use fill!
-              tg->create_transition(st_binder[n], cube,
-                                    t.acc, st_binder[t.dst]);
+              bdd one = bdd_satone(cond);
+              cond -= one;
+              spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
+              tg->create_transition(st_binder[n], cube, t.acc,
+                                    st_binder[t.dst]);
             }
-          else
-            // Split the bdd into multiple transitions
-            while (cond != bddfalse)
-              {
-                bdd one = bdd_satone(cond);
-                cond -= one;
-                spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
-                tg->create_transition(st_binder[n], cube, t.acc,
-                                      st_binder[t.dst]);
-              }
         }
     // Must be contiguous to support swarming.
     assert(tg->succ_contiguous());
diff --git a/tests/core/twacube.test b/tests/core/twacube.test
index d02897f24..3d906afd2 100755
--- a/tests/core/twacube.test
+++ b/tests/core/twacube.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2015, 2016, 2018 Laboratoire de Recherche et
+# Copyright (C) 2014, 2015, 2016, 2018, 2020 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -51,7 +51,6 @@ digraph "" {
 }
 -----------
 init : 0
-0->0 : !p1&!p2 {}
 0->1 : p1 {}
 0->2 : p2 {1}
 1->2 : p1&p2 {0}
@@ -72,7 +71,6 @@ digraph "" {
   I [label="", style=invis, width=0]
   I -> 0
   0 [label="0"]
-  0 -> 0 [label="!p1 & !p2"]
   0 -> 1 [label="p1"]
   0 -> 2 [label="p2\n{1}"]
   1 [label="1"]