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

bddop: remove unused file

* src/misc/bddop.cc, src/misc/bddop.hh: Delete.
* src/misc/Makefile.am, src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc,
src/taalgos/tgba2ta.cc, src/tgba/taatgba.cc, src/tgba/tgbagraph.hh:
Adjust.
parent 202b9609
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et ## Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
## Développement de l'Epita (LRDE). ## Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
...@@ -32,7 +32,6 @@ DISTCLEANFILES = _config.h ...@@ -32,7 +32,6 @@ DISTCLEANFILES = _config.h
misc_HEADERS = \ misc_HEADERS = \
bareword.hh \ bareword.hh \
bddlt.hh \ bddlt.hh \
bddop.hh \
bitvect.hh \ bitvect.hh \
casts.hh \ casts.hh \
common.hh \ common.hh \
...@@ -59,7 +58,6 @@ misc_HEADERS = \ ...@@ -59,7 +58,6 @@ misc_HEADERS = \
noinst_LTLIBRARIES = libmisc.la noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \ libmisc_la_SOURCES = \
bareword.cc \ bareword.cc \
bddop.cc \
bitvect.cc \ bitvect.cc \
escape.cc \ escape.cc \
formater.cc \ formater.cc \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "config.h"
#include <cassert>
#include "bddop.hh"
namespace spot
{
bdd
compute_all_acceptance_conditions(bdd neg_acceptance_conditions)
{
bdd all = bddfalse;
// Build all_acceptance_conditions_ from neg_acceptance_conditions_
// I.e., transform !A & !B & !C into
// A & !B & !C
// + !A & B & !C
// + !A & !B & C
bdd cur = neg_acceptance_conditions;
while (cur != bddtrue)
{
assert(cur != bddfalse);
bdd v = bdd_ithvar(bdd_var(cur));
all |= v & bdd_exist(neg_acceptance_conditions, v);
assert(bdd_high(cur) != bddtrue);
cur = bdd_low(cur);
}
return all;
}
bdd
compute_neg_acceptance_conditions(bdd all_acceptance_conditions)
{
bdd cur = bdd_support(all_acceptance_conditions);
bdd neg = bddtrue;
while (cur != bddtrue)
{
neg &= bdd_nithvar(bdd_var(cur));
assert(bdd_low(cur) != bddtrue);
cur = bdd_high(cur);
}
return neg;
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#ifndef SPOT_MISC_BDDOP_HH
# define SPOT_MISC_BDDOP_HH
#include "common.hh"
#include <bddx.h>
namespace spot
{
/// \brief Compute all acceptance conditions from all neg acceptance
/// conditions.
SPOT_API bdd
compute_all_acceptance_conditions(bdd neg_acceptance_conditions);
/// \brief Compute neg acceptance conditions from all acceptance
/// conditions.
SPOT_API bdd
compute_neg_acceptance_conditions(bdd all_acceptance_conditions);
}
#endif // SPOT_MISC_BDDOP_HH
...@@ -30,7 +30,6 @@ ...@@ -30,7 +30,6 @@
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "taexplicit.hh" #include "taexplicit.hh"
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "misc/bddop.hh"
#include <cassert> #include <cassert>
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
......
...@@ -21,7 +21,6 @@ ...@@ -21,7 +21,6 @@
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "tgtaexplicit.hh" #include "tgtaexplicit.hh"
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "misc/bddop.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
......
...@@ -29,7 +29,6 @@ ...@@ -29,7 +29,6 @@
#include "ltlast/atomic_prop.hh" #include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "misc/bddop.hh"
#include <cassert> #include <cassert>
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include <iostream> #include <iostream>
......
...@@ -24,7 +24,6 @@ ...@@ -24,7 +24,6 @@
#include "tgba/formula2bdd.hh" #include "tgba/formula2bdd.hh"
#include "ltlvisit/tostring.hh" #include "ltlvisit/tostring.hh"
#include "ltlvisit/clone.hh" #include "ltlvisit/clone.hh"
#include "misc/bddop.hh"
#include "taatgba.hh" #include "taatgba.hh"
namespace spot namespace spot
......
...@@ -26,7 +26,6 @@ ...@@ -26,7 +26,6 @@
#include "tgba/bdddict.hh" #include "tgba/bdddict.hh"
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "tgbaalgos/dupexp.hh" #include "tgbaalgos/dupexp.hh"
#include "misc/bddop.hh"
#include <sstream> #include <sstream>
namespace spot namespace spot
......
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