Commit 4df4b4ef authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Adjust some uses of bddtrue/bddfalse.

* src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03opt.cc: Fix
cases where bddtrue and bddfalse where used in a ternary operator.
* src/sanity/style.test: Allow bdd_true()/bdd_false() to be
used in ternary operators.
parent af6cb049
......@@ -246,7 +246,8 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
grep '[^a-zA-Z0-9_](\*[a-zA-Z0-9_]*)\.' $tmp &&
diag 'Use "x->y", not "(*x).y"'
egrep 'bdd_(false|true)[ ]*\(' $tmp &&
# we allow these functions only in ?...:...
egrep 'bdd_(false|true)[ ]*\(' $tmp | grep -v '[?:]' &&
diag 'Use bddfalse and bddtrue instead of bdd_false() and bdd_true()'
res=`perl -ne '$/ = undef;
......
......@@ -768,8 +768,9 @@ namespace spot
bdd f2 = p.acc_cand |
d.all_cand_acc[f];
bdd f2p = is_weak ? bddfalse
: p.acc_ref | curacc;
bdd f2p = bddfalse;
if (!is_weak)
f2p = p.acc_ref | curacc;
path p2(p.src_cand, p.src_ref,
q3, dp, f2, f2p);
......
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2012, 2013 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -195,7 +195,10 @@ namespace spot
// Update finish_ with finish(node).
// FIXME: when node is loop, it does not make sense; hence the bddtrue.
finish_[node] = !node->get_nfa()->is_loop() ? bddtrue : finish;
if (!node->get_nfa()->is_loop())
finish_[node] = bddtrue;
else
finish_[node] = finish;
bdd tmp = bddtrue;
for (nmap::iterator it = m.begin(); it != m.end(); ++it)
......
......@@ -470,8 +470,10 @@ namespace spot
// simplifications in the signature by removing a
// transition which has as a destination a state with
// no outgoing transition.
now_to_next[p.first] =
(p.first == bddfalse) ? bddfalse : *it_bdd;
bdd acc = bddfalse;
if (p.first != bddfalse)
acc = *it_bdd;
now_to_next[p.first] = acc;
++it_bdd;
}
......@@ -650,15 +652,17 @@ namespace spot
if (Cosimulation)
{
gb->new_transition(dst.id(), src.id(),
cond, Sba ? bddfalse : acc);
if (Sba)
// acc should be attached to src, or rather,
// in our transition-based representation)
// to all transitions leaving src. As we
// can't do this here, store this in a table
// so we can fix it later.
accst[gb->get_state(src.id())] = acc;
{
// acc should be attached to src, or rather,
// in our transition-based representation)
// to all transitions leaving src. As we
// can't do this here, store this in a table
// so we can fix it later.
accst[gb->get_state(src.id())] = acc;
acc = bddfalse;
}
gb->new_transition(dst.id(), src.id(), cond, acc);
}
else
{
......
......@@ -347,7 +347,7 @@ namespace spot
else if (c_prime.get_color() == CYAN &&
(all_acc == ((use_red_weights ?
(current_weight - c_prime.get_weight())
: bddfalse)
: bdd_false())
| c_prime.get_acc()
| acc
| acu)))
......
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