accconv, acccompl: remove unused files
* src/priv/acccompl.cc, src/priv/acccompl.hh, src/priv/accconv.cc, src/priv/accconv.hh: Delete. * src/priv/Makefile.am: Adjust. * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/sccinfo.cc, src/tgbaalgos/simulation.cc: Remove unused includes.
This commit is contained in:
Alexandre Duret-Lutz
parent
12401fe91a
commit
202b960994
9 changed files with 1 additions and 286 deletions
|
|
@ -21,8 +21,6 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
|
||||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||||
|
|
||||||
noinst_HEADERS = \
|
noinst_HEADERS = \
|
||||||
acccompl.hh \
|
|
||||||
accconv.hh \
|
|
||||||
accmap.hh \
|
accmap.hh \
|
||||||
bddalloc.hh \
|
bddalloc.hh \
|
||||||
countstates.hh \
|
countstates.hh \
|
||||||
|
|
@ -30,10 +28,6 @@ noinst_HEADERS = \
|
||||||
|
|
||||||
noinst_LTLIBRARIES = libpriv.la
|
noinst_LTLIBRARIES = libpriv.la
|
||||||
libpriv_la_SOURCES = \
|
libpriv_la_SOURCES = \
|
||||||
acccompl.cc \
|
|
||||||
accconv.cc \
|
|
||||||
bddalloc.cc \
|
bddalloc.cc \
|
||||||
countstates.cc \
|
countstates.cc \
|
||||||
freelist.cc
|
freelist.cc
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,88 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement
|
|
||||||
// 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 "acccompl.hh"
|
|
||||||
#include <cassert>
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
// If ALL = a!b!c + !ab!c + !a!bc", the negation of ACC = a!b!c is
|
|
||||||
// RES = bc. We do that by computing ALL-ACC and enumerating
|
|
||||||
// all positive variables in the remaining products.
|
|
||||||
bdd acc_compl::complement(const bdd& acc)
|
|
||||||
{
|
|
||||||
bdd_cache_t::const_iterator it = cache_.find(acc);
|
|
||||||
if (it != cache_.end())
|
|
||||||
return it->second;
|
|
||||||
|
|
||||||
bdd res = bddtrue;
|
|
||||||
bdd n = all_ - acc;
|
|
||||||
|
|
||||||
while (n != bddfalse)
|
|
||||||
{
|
|
||||||
bdd cond = bdd_satone(n);
|
|
||||||
bdd oldcond = cond;
|
|
||||||
n -= cond;
|
|
||||||
|
|
||||||
while (bdd_high(cond) == bddfalse)
|
|
||||||
cond = bdd_low(cond);
|
|
||||||
|
|
||||||
// Here we want to keep only the current one.
|
|
||||||
// tmp is only useful to keep the value and cache it.
|
|
||||||
bdd tmp = bdd_ithvar(bdd_var(cond));
|
|
||||||
res &= tmp;
|
|
||||||
}
|
|
||||||
|
|
||||||
cache_[acc] = res;
|
|
||||||
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd acc_compl::reverse_complement(const bdd& acc)
|
|
||||||
{
|
|
||||||
// We are sure that if we have no acceptance condition the result
|
|
||||||
// is all_.
|
|
||||||
if (acc == bddtrue)
|
|
||||||
return all_;
|
|
||||||
|
|
||||||
assert(acc != bddfalse);
|
|
||||||
|
|
||||||
// Since we never cache a unique positive bdd, we can reuse the
|
|
||||||
// same cache. In fact the only kind of acc we will receive in
|
|
||||||
// this method, are a conjunction of positive acceptance
|
|
||||||
// conditions. (i.e., "ab" and not "a!b + !ab")
|
|
||||||
bdd_cache_t::const_iterator it = cache_.find(acc);
|
|
||||||
if (it != cache_.end())
|
|
||||||
return it->second;
|
|
||||||
|
|
||||||
bdd res = all_;
|
|
||||||
bdd cond = acc;
|
|
||||||
bdd neg = bddtrue;
|
|
||||||
while (cond != bddtrue)
|
|
||||||
{
|
|
||||||
neg &= bdd_nithvar(bdd_var(cond));
|
|
||||||
cond = bdd_high(cond);
|
|
||||||
}
|
|
||||||
res &= neg;
|
|
||||||
cache_[acc] = res;
|
|
||||||
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
} // End namespace spot.
|
|
||||||
|
|
@ -1,56 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
|
|
||||||
// Developpement 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_PRIV_ACCCOMPL_HH
|
|
||||||
# define SPOT_PRIV_ACCCOMPL_HH
|
|
||||||
|
|
||||||
#include <map>
|
|
||||||
#include <bddx.h>
|
|
||||||
#include "misc/hash.hh"
|
|
||||||
#include "misc/bddlt.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
/// \brief Helper class to convert acceptance conditions into promises
|
|
||||||
///
|
|
||||||
/// A set of acceptance conditions represented by the sum "à la Spot",
|
|
||||||
/// is converted into a product of promises.
|
|
||||||
class acc_compl
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
acc_compl(const bdd& all, const bdd& neg)
|
|
||||||
: all_(all),
|
|
||||||
neg_(neg)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
bdd complement(const bdd& acc);
|
|
||||||
bdd reverse_complement(const bdd& acc);
|
|
||||||
|
|
||||||
protected:
|
|
||||||
const bdd all_;
|
|
||||||
const bdd neg_;
|
|
||||||
typedef std::unordered_map<bdd, bdd, bdd_hash> bdd_cache_t;
|
|
||||||
bdd_cache_t cache_;
|
|
||||||
};
|
|
||||||
} // End namespace Spot
|
|
||||||
|
|
||||||
#endif // SPOT_PRIV_ACCCOMPL_HH
|
|
||||||
|
|
@ -1,80 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2011, 2012 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 <cassert>
|
|
||||||
#include "accconv.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
bdd acceptance_convertor::as_positive_product(bdd acc)
|
|
||||||
{
|
|
||||||
// Cache lookup.
|
|
||||||
bdd_cache_t::const_iterator it = pos_prod_cache_.find(acc);
|
|
||||||
if (it != pos_prod_cache_.end())
|
|
||||||
return it->second;
|
|
||||||
|
|
||||||
// This would be one way to construct the positive product,
|
|
||||||
// if we did not want to populate a cache.
|
|
||||||
//
|
|
||||||
// bdd res = bddtrue;
|
|
||||||
// BDD a = acc.id();
|
|
||||||
// while (a)
|
|
||||||
// {
|
|
||||||
// if (bdd_high(a))
|
|
||||||
// res &= bdd_ithvar(bdd_var(a));
|
|
||||||
// a = bdd_low(a);
|
|
||||||
// }
|
|
||||||
|
|
||||||
// Skip all negative variables.
|
|
||||||
bdd a = acc;
|
|
||||||
while (a != bddfalse && bdd_high(a) == bddfalse)
|
|
||||||
a = bdd_low(a);
|
|
||||||
|
|
||||||
bdd res = bddtrue;
|
|
||||||
if (a != bddfalse)
|
|
||||||
{
|
|
||||||
// Make a recursive call right below each positive variable,
|
|
||||||
// in order to populate the cache.
|
|
||||||
res = bdd_ithvar(bdd_var(a));
|
|
||||||
bdd low = bdd_low(a);
|
|
||||||
if (low != bddfalse)
|
|
||||||
res &= as_positive_product(low);
|
|
||||||
}
|
|
||||||
|
|
||||||
// Cache final result.
|
|
||||||
pos_prod_cache_[acc] = res;
|
|
||||||
return res;
|
|
||||||
};
|
|
||||||
|
|
||||||
bdd acceptance_convertor::as_full_product(bdd acc)
|
|
||||||
{
|
|
||||||
// Lookup in cache.
|
|
||||||
bdd_cache_t::const_iterator it = full_prod_cache_.find(acc);
|
|
||||||
if (it != full_prod_cache_.end())
|
|
||||||
return it->second;
|
|
||||||
|
|
||||||
bdd pos = as_positive_product(acc);
|
|
||||||
bdd res = bdd_exist(allneg_, pos) & pos;
|
|
||||||
|
|
||||||
// Cache final result.
|
|
||||||
full_prod_cache_[acc] = res;
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -1,52 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
|
|
||||||
// Developpement 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_PRIV_ACCCONV_HH
|
|
||||||
# define SPOT_PRIV_ACCCONV_HH
|
|
||||||
|
|
||||||
#include <bddx.h>
|
|
||||||
#include "misc/hash.hh"
|
|
||||||
#include "misc/bddlt.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
/// \brief Help class to convert between acceptance conditions to
|
|
||||||
/// other BDD formats.
|
|
||||||
class acceptance_convertor
|
|
||||||
{
|
|
||||||
public:
|
|
||||||
acceptance_convertor(bdd allneg)
|
|
||||||
: allneg_(allneg)
|
|
||||||
{
|
|
||||||
}
|
|
||||||
|
|
||||||
bdd as_positive_product(bdd acc);
|
|
||||||
|
|
||||||
bdd as_full_product(bdd acc);
|
|
||||||
|
|
||||||
protected:
|
|
||||||
bdd allneg_;
|
|
||||||
typedef std::unordered_map<bdd, bdd, bdd_hash> bdd_cache_t;
|
|
||||||
bdd_cache_t pos_prod_cache_;
|
|
||||||
bdd_cache_t full_prod_cache_;
|
|
||||||
};
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif // SPOT_PRIV_ACCCONV_HH
|
|
||||||
|
|
@ -39,7 +39,6 @@
|
||||||
#include "tgba/bddprint.hh"
|
#include "tgba/bddprint.hh"
|
||||||
#include "tgbaalgos/sccinfo.hh"
|
#include "tgbaalgos/sccinfo.hh"
|
||||||
//#include "tgbaalgos/dotty.hh"
|
//#include "tgbaalgos/dotty.hh"
|
||||||
#include "priv/acccompl.hh"
|
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -24,7 +24,6 @@
|
||||||
#include "scc.hh"
|
#include "scc.hh"
|
||||||
#include "tgba/bddprint.hh"
|
#include "tgba/bddprint.hh"
|
||||||
#include "misc/escape.hh"
|
#include "misc/escape.hh"
|
||||||
#include "priv/accconv.hh"
|
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -23,7 +23,6 @@
|
||||||
#include <queue>
|
#include <queue>
|
||||||
#include "tgba/bddprint.hh"
|
#include "tgba/bddprint.hh"
|
||||||
#include "misc/escape.hh"
|
#include "misc/escape.hh"
|
||||||
#include "priv/accconv.hh"
|
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -23,13 +23,13 @@
|
||||||
#include <cmath>
|
#include <cmath>
|
||||||
#include <limits>
|
#include <limits>
|
||||||
#include "simulation.hh"
|
#include "simulation.hh"
|
||||||
#include "priv/acccompl.hh"
|
|
||||||
#include "misc/minato.hh"
|
#include "misc/minato.hh"
|
||||||
#include "tgba/bddprint.hh"
|
#include "tgba/bddprint.hh"
|
||||||
#include "tgbaalgos/reachiter.hh"
|
#include "tgbaalgos/reachiter.hh"
|
||||||
#include "tgbaalgos/sccfilter.hh"
|
#include "tgbaalgos/sccfilter.hh"
|
||||||
#include "tgbaalgos/sccinfo.hh"
|
#include "tgbaalgos/sccinfo.hh"
|
||||||
#include "tgbaalgos/dupexp.hh"
|
#include "tgbaalgos/dupexp.hh"
|
||||||
|
#include "misc/bddlt.hh"
|
||||||
|
|
||||||
// The way we developed this algorithm is the following: We take an
|
// The way we developed this algorithm is the following: We take an
|
||||||
// automaton, and reverse all these acceptance conditions. We reverse
|
// automaton, and reverse all these acceptance conditions. We reverse
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue