Commit 884493bd authored by Etienne Renault's avatar Etienne Renault

twacube: fix erroneous translation

* spot/twacube_algos/convert.cc,
tests/core/twacube.test: Here.
parent f6644511
......@@ -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());
......
#!/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"]
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment