rename tgba files as twa
Automatic mass renaming. * src/graphtest/tgbagraph.cc, src/tgba/acc.cc, src/tgba/acc.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh, src/tgba/fwd.hh, src/tgba/Makefile.am, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgba.hh, src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh, src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh, src/tgba/.cvsignore: Rename as... * src/graphtest/twagraph.cc, src/twa/acc.cc, src/twa/acc.hh, src/twa/bdddict.cc, src/twa/bdddict.hh, src/twa/bddprint.cc, src/twa/bddprint.hh, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh, src/twa/fwd.hh, src/twa/Makefile.am, src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twa.cc, src/twa/twagraph.cc, src/twa/twagraph.hh, src/twa/twa.hh, src/twa/twamask.cc, src/twa/twamask.hh, src/twa/twaproduct.cc, src/twa/twaproduct.hh, src/twa/twaproxy.cc, src/twa/twaproxy.hh, src/twa/twasafracomplement.cc, src/twa/twasafracomplement.hh, src/twa/.cvsignore: ... these. * README, bench/stutter/stutter_invariance_randomgraph.cc, configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am, src/bin/common_aoutput.cc, src/bin/common_conv.hh, src/bin/common_trans.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgta.cc, src/bin/randaut.cc, src/dstarparse/dra2ba.cc, src/dstarparse/public.hh, src/graphtest/Makefile.am, src/graphtest/ngraph.cc, src/hoaparse/hoaparse.yy, src/hoaparse/public.hh, src/kripke/fairkripke.hh, src/kripke/kripkeexplicit.cc, src/kripke/kripkeprint.cc, src/kripkeparse/kripkeparse.yy, src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh, src/ltlvisit/exclusive.hh, src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh, src/priv/accmap.hh, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc, src/taalgos/emptinessta.cc, src/taalgos/minimize.cc, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh, src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh, src/tgbaalgos/bfssteps.cc, src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.hh, src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.hh, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.cc, src/tgbaalgos/hoa.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/mask.hh, src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh, src/tgbaalgos/product.cc, src/tgbaalgos/product.hh, src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.hh, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh, src/tgbaalgos/relabel.hh, src/tgbaalgos/remfin.hh, src/tgbaalgos/remprop.hh, src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh, src/tgbaalgos/sbacc.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.hh, src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh, src/tgbaalgos/weight.hh, src/tgbaalgos/word.cc, src/tgbatest/acc.cc, src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/taatgba.cc, wrap/python/spot_impl.i: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
8839f50a0f
commit
703fbd0e99
154 changed files with 232 additions and 231 deletions
6
src/twa/.cvsignore
Normal file
6
src/twa/.cvsignore
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
.deps
|
||||
.libs
|
||||
*.lo
|
||||
*.la
|
||||
Makefile
|
||||
Makefile.in
|
||||
6
src/twa/.gitignore
vendored
Normal file
6
src/twa/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
.deps
|
||||
.libs
|
||||
*.lo
|
||||
*.la
|
||||
Makefile
|
||||
Makefile.in
|
||||
54
src/twa/Makefile.am
Normal file
54
src/twa/Makefile.am
Normal file
|
|
@ -0,0 +1,54 @@
|
|||
## -*- coding: utf-8 -*-
|
||||
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
|
||||
## de Recherche et Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
## et Marie Curie.
|
||||
##
|
||||
## 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/>.
|
||||
|
||||
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
|
||||
twadir = $(pkgincludedir)/twa
|
||||
|
||||
twa_HEADERS = \
|
||||
acc.hh \
|
||||
bdddict.hh \
|
||||
bddprint.hh \
|
||||
formula2bdd.hh \
|
||||
fwd.hh \
|
||||
taatgba.hh \
|
||||
twa.hh \
|
||||
twagraph.hh \
|
||||
twamask.hh \
|
||||
twaproxy.hh \
|
||||
twaproduct.hh \
|
||||
twasafracomplement.hh
|
||||
|
||||
noinst_LTLIBRARIES = libtwa.la
|
||||
libtwa_la_SOURCES = \
|
||||
acc.cc \
|
||||
bdddict.cc \
|
||||
bddprint.cc \
|
||||
formula2bdd.cc \
|
||||
taatgba.cc \
|
||||
twa.cc \
|
||||
twagraph.cc \
|
||||
twaproduct.cc \
|
||||
twamask.cc \
|
||||
twaproxy.cc \
|
||||
twasafracomplement.cc
|
||||
1015
src/twa/acc.cc
Normal file
1015
src/twa/acc.cc
Normal file
File diff suppressed because it is too large
Load diff
1003
src/twa/acc.hh
Normal file
1003
src/twa/acc.hh
Normal file
File diff suppressed because it is too large
Load diff
465
src/twa/bdddict.cc
Normal file
465
src/twa/bdddict.cc
Normal file
|
|
@ -0,0 +1,465 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2012, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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 <ostream>
|
||||
#include <sstream>
|
||||
#include <cassert>
|
||||
#include <ltlvisit/tostring.hh>
|
||||
#include <ltlvisit/tostring.hh>
|
||||
#include <ltlast/atomic_prop.hh>
|
||||
#include <ltlenv/defaultenv.hh>
|
||||
#include "priv/bddalloc.hh"
|
||||
#include "bdddict.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
// Empty anonymous namespace so that the style checker does no
|
||||
// complain about bdd_dict_priv (which should not be in an anonymous
|
||||
// namespace).
|
||||
namespace
|
||||
{
|
||||
}
|
||||
|
||||
class bdd_dict_priv: public bdd_allocator
|
||||
{
|
||||
public:
|
||||
|
||||
class anon_free_list : public spot::free_list
|
||||
{
|
||||
public:
|
||||
// WARNING: We need a default constructor so this can be used in
|
||||
// a hash; but we should ensure that no object in the hash is
|
||||
// constructed with p==0.
|
||||
anon_free_list(bdd_dict_priv* p = 0)
|
||||
: priv_(p)
|
||||
{
|
||||
}
|
||||
|
||||
virtual int
|
||||
extend(int n)
|
||||
{
|
||||
assert(priv_);
|
||||
int b = priv_->allocate_variables(n);
|
||||
free_anonymous_list_of_type::iterator i;
|
||||
for (i = priv_->free_anonymous_list_of.begin();
|
||||
i != priv_->free_anonymous_list_of.end(); ++i)
|
||||
if (&i->second != this)
|
||||
i->second.insert(b, n);
|
||||
return b;
|
||||
}
|
||||
|
||||
private:
|
||||
bdd_dict_priv* priv_;
|
||||
};
|
||||
|
||||
bdd_dict_priv()
|
||||
{
|
||||
free_anonymous_list_of[0] = anon_free_list(this);
|
||||
}
|
||||
|
||||
/// List of unused anonymous variable number for each automaton.
|
||||
typedef std::map<const void*, anon_free_list> free_anonymous_list_of_type;
|
||||
free_anonymous_list_of_type free_anonymous_list_of;
|
||||
};
|
||||
|
||||
bdd_dict::bdd_dict()
|
||||
// Initialize priv_ first, because it also initializes BuDDy
|
||||
: priv_(new bdd_dict_priv()),
|
||||
bdd_map(bdd_varnum())
|
||||
{
|
||||
}
|
||||
|
||||
bdd_dict::~bdd_dict()
|
||||
{
|
||||
assert_emptiness();
|
||||
delete priv_;
|
||||
}
|
||||
|
||||
int
|
||||
bdd_dict::register_proposition(const ltl::formula* f, const void* for_me)
|
||||
{
|
||||
int num;
|
||||
// Do not build a variable that already exists.
|
||||
fv_map::iterator sii = var_map.find(f);
|
||||
if (sii != var_map.end())
|
||||
{
|
||||
num = sii->second;
|
||||
}
|
||||
else
|
||||
{
|
||||
f = f->clone();
|
||||
num = priv_->allocate_variables(1);
|
||||
var_map[f] = num;
|
||||
bdd_map.resize(bdd_varnum());
|
||||
bdd_map[num].type = var;
|
||||
bdd_map[num].f = f;
|
||||
}
|
||||
bdd_map[num].refs.insert(for_me);
|
||||
return num;
|
||||
}
|
||||
|
||||
int
|
||||
bdd_dict::has_registered_proposition(const ltl::formula* f,
|
||||
const void* me)
|
||||
{
|
||||
auto ssi = var_map.find(f);
|
||||
if (ssi == var_map.end())
|
||||
return -1;
|
||||
int num = ssi->second;
|
||||
auto& r = bdd_map[num].refs;
|
||||
if (r.find(me) == r.end())
|
||||
return -1;
|
||||
return num;
|
||||
}
|
||||
|
||||
void
|
||||
bdd_dict::register_propositions(bdd f, const void* for_me)
|
||||
{
|
||||
if (f == bddtrue || f == bddfalse)
|
||||
return;
|
||||
|
||||
int v = bdd_var(f);
|
||||
assert(unsigned(v) < bdd_map.size());
|
||||
bdd_info& i = bdd_map[v];
|
||||
assert(i.type == var);
|
||||
i.refs.insert(for_me);
|
||||
|
||||
register_propositions(bdd_high(f), for_me);
|
||||
register_propositions(bdd_low(f), for_me);
|
||||
}
|
||||
|
||||
int
|
||||
bdd_dict::register_acceptance_variable(const ltl::formula* f,
|
||||
const void* for_me)
|
||||
{
|
||||
int num;
|
||||
// Do not build an acceptance variable that already exists.
|
||||
fv_map::iterator sii = acc_map.find(f);
|
||||
if (sii != acc_map.end())
|
||||
{
|
||||
num = sii->second;
|
||||
}
|
||||
else
|
||||
{
|
||||
f = f->clone();
|
||||
num = priv_->allocate_variables(1);
|
||||
acc_map[f] = num;
|
||||
bdd_map.resize(bdd_varnum());
|
||||
bdd_info& i = bdd_map[num];
|
||||
i.type = acc;
|
||||
i.f = f;
|
||||
i.clone_counts = 0;
|
||||
}
|
||||
bdd_map[num].refs.insert(for_me);
|
||||
return num;
|
||||
}
|
||||
|
||||
void
|
||||
bdd_dict::register_acceptance_variables(bdd f, const void* for_me)
|
||||
{
|
||||
if (f == bddtrue || f == bddfalse)
|
||||
return;
|
||||
|
||||
int v = bdd_var(f);
|
||||
assert(unsigned(v) < bdd_map.size());
|
||||
bdd_info& i = bdd_map[v];
|
||||
assert(i.type == acc);
|
||||
i.refs.insert(for_me);
|
||||
|
||||
register_acceptance_variables(bdd_high(f), for_me);
|
||||
register_acceptance_variables(bdd_low(f), for_me);
|
||||
}
|
||||
|
||||
int
|
||||
bdd_dict::register_clone_acc(int v, const void* for_me)
|
||||
{
|
||||
assert(unsigned(v) < bdd_map.size());
|
||||
bdd_info& i = bdd_map[v];
|
||||
assert(i.type == acc);
|
||||
|
||||
std::ostringstream s;
|
||||
// FIXME: We could be smarter and reuse unused "$n" numbers.
|
||||
s << ltl::to_string(i.f) << '$' << ++i.clone_counts;
|
||||
const ltl::formula* f =
|
||||
ltl::atomic_prop::instance(s.str(),
|
||||
ltl::default_environment::instance());
|
||||
int res = register_acceptance_variable(f, for_me);
|
||||
f->destroy();
|
||||
return res;
|
||||
}
|
||||
|
||||
const ltl::formula*
|
||||
bdd_dict::oneacc_to_formula(int var) const
|
||||
{
|
||||
assert(unsigned(var) < bdd_map.size());
|
||||
const bdd_info& i = bdd_map[var];
|
||||
assert(i.type == acc);
|
||||
return i.f;
|
||||
}
|
||||
|
||||
const ltl::formula*
|
||||
bdd_dict::oneacc_to_formula(bdd oneacc) const
|
||||
{
|
||||
assert(oneacc != bddfalse);
|
||||
while (bdd_high(oneacc) == bddfalse)
|
||||
{
|
||||
oneacc = bdd_low(oneacc);
|
||||
assert(oneacc != bddfalse);
|
||||
}
|
||||
return oneacc_to_formula(bdd_var(oneacc));
|
||||
}
|
||||
|
||||
int
|
||||
bdd_dict::register_anonymous_variables(int n, const void* for_me)
|
||||
{
|
||||
typedef bdd_dict_priv::free_anonymous_list_of_type fal;
|
||||
fal::iterator i = priv_->free_anonymous_list_of.find(for_me);
|
||||
|
||||
if (i == priv_->free_anonymous_list_of.end())
|
||||
{
|
||||
i = (priv_->free_anonymous_list_of.insert
|
||||
(fal::value_type(for_me,
|
||||
priv_->free_anonymous_list_of[0]))).first;
|
||||
}
|
||||
int res = i->second.register_n(n);
|
||||
|
||||
bdd_map.resize(bdd_varnum());
|
||||
|
||||
while (n--)
|
||||
{
|
||||
bdd_map[res + n].type = anon;
|
||||
bdd_map[res + n].refs.insert(for_me);
|
||||
}
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
bdd_dict::register_all_variables_of(const void* from_other,
|
||||
const void* for_me)
|
||||
{
|
||||
auto j = priv_->free_anonymous_list_of.find(from_other);
|
||||
if (j != priv_->free_anonymous_list_of.end())
|
||||
priv_->free_anonymous_list_of[for_me] = j->second;
|
||||
|
||||
for (auto& i: bdd_map)
|
||||
{
|
||||
ref_set& s = i.refs;
|
||||
if (s.find(from_other) != s.end())
|
||||
s.insert(for_me);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void
|
||||
bdd_dict::register_all_propositions_of(const void* from_other,
|
||||
const void* for_me)
|
||||
{
|
||||
for (auto& i: bdd_map)
|
||||
{
|
||||
if (i.type != var_type::var)
|
||||
continue;
|
||||
ref_set& s = i.refs;
|
||||
if (s.find(from_other) != s.end())
|
||||
s.insert(for_me);
|
||||
}
|
||||
}
|
||||
|
||||
void
|
||||
bdd_dict::unregister_variable(int v, const void* me)
|
||||
{
|
||||
assert(unsigned(v) < bdd_map.size());
|
||||
|
||||
ref_set& s = bdd_map[v].refs;
|
||||
// If the variable is not owned by me, ignore it.
|
||||
ref_set::iterator si = s.find(me);
|
||||
if (si == s.end())
|
||||
return;
|
||||
|
||||
s.erase(si);
|
||||
|
||||
// If var is anonymous, we should reinsert it into the free list
|
||||
// of ME's anonymous variables.
|
||||
if (bdd_map[v].type == anon)
|
||||
priv_->free_anonymous_list_of[me].release_n(v, 1);
|
||||
|
||||
if (!s.empty())
|
||||
return;
|
||||
|
||||
// ME was the last user of this variable.
|
||||
// Let's free it. First, we need to find
|
||||
// if this is a Var or an Acc variable.
|
||||
int n = 1;
|
||||
const ltl::formula* f = 0;
|
||||
switch (bdd_map[v].type)
|
||||
{
|
||||
case var:
|
||||
f = bdd_map[v].f;
|
||||
var_map.erase(f);
|
||||
break;
|
||||
case acc:
|
||||
f = bdd_map[v].f;
|
||||
acc_map.erase(f);
|
||||
break;
|
||||
case anon:
|
||||
{
|
||||
bdd_dict_priv::free_anonymous_list_of_type::iterator i;
|
||||
// Nobody use this variable as an anonymous variable
|
||||
// anymore, so remove it entirely from the anonymous
|
||||
// free list so it can be used for something else.
|
||||
for (i = priv_->free_anonymous_list_of.begin();
|
||||
i != priv_->free_anonymous_list_of.end(); ++i)
|
||||
i->second.remove(v, n);
|
||||
break;
|
||||
}
|
||||
}
|
||||
// Actually release the associated BDD variables, and the
|
||||
// formula itself.
|
||||
priv_->release_variables(v, n);
|
||||
if (f)
|
||||
f->destroy();
|
||||
while (n--)
|
||||
bdd_map[v + n].type = anon;
|
||||
}
|
||||
|
||||
void
|
||||
bdd_dict::unregister_all_my_variables(const void* me)
|
||||
{
|
||||
unsigned s = bdd_map.size();
|
||||
for (unsigned i = 0; i < s; ++i)
|
||||
unregister_variable(i, me);
|
||||
priv_->free_anonymous_list_of.erase(me);
|
||||
}
|
||||
|
||||
void
|
||||
bdd_dict::unregister_all_typed_variables(var_type type, const void* me)
|
||||
{
|
||||
unsigned s = bdd_map.size();
|
||||
for (unsigned i = 0; i < s; ++i)
|
||||
if (bdd_map[i].type == type)
|
||||
unregister_variable(i, me);
|
||||
if (type == anon)
|
||||
priv_->free_anonymous_list_of.erase(me);
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_dict::dump(std::ostream& os) const
|
||||
{
|
||||
os << "Variable Map:\n";
|
||||
unsigned s = bdd_map.size();
|
||||
for (unsigned i = 0; i < s; ++i)
|
||||
{
|
||||
os << ' ' << i << ' ';
|
||||
const bdd_info& r = bdd_map[i];
|
||||
switch (r.type)
|
||||
{
|
||||
case anon:
|
||||
os << (r.refs.empty() ? "Free" : "Anon");
|
||||
break;
|
||||
case acc:
|
||||
os << "Acc[" << to_string(r.f) << ']';
|
||||
break;
|
||||
case var:
|
||||
os << "Var[" << to_string(r.f) << ']';
|
||||
break;
|
||||
}
|
||||
if (!r.refs.empty())
|
||||
{
|
||||
os << " x" << r.refs.size() << " {";
|
||||
for (ref_set::const_iterator si = r.refs.begin();
|
||||
si != r.refs.end(); ++si)
|
||||
os << ' ' << *si;
|
||||
os << " }";
|
||||
}
|
||||
os << '\n';
|
||||
}
|
||||
os << "Anonymous lists:\n";
|
||||
bdd_dict_priv::free_anonymous_list_of_type::const_iterator ai;
|
||||
for (ai = priv_->free_anonymous_list_of.begin();
|
||||
ai != priv_->free_anonymous_list_of.end(); ++ai)
|
||||
{
|
||||
os << " [" << ai->first << "] ";
|
||||
ai->second.dump_free_list(os) << std::endl;
|
||||
}
|
||||
os << "Free list:\n";
|
||||
priv_->dump_free_list(os);
|
||||
os << '\n';
|
||||
return os;
|
||||
}
|
||||
|
||||
void
|
||||
bdd_dict::assert_emptiness() const
|
||||
{
|
||||
bool fail = false;
|
||||
|
||||
bool var_seen = false;
|
||||
bool acc_seen = false;
|
||||
bool refs_seen = false;
|
||||
unsigned s = bdd_map.size();
|
||||
for (unsigned i = 0; i < s; ++i)
|
||||
{
|
||||
switch (bdd_map[i].type)
|
||||
{
|
||||
case var:
|
||||
var_seen = true;
|
||||
break;
|
||||
case acc:
|
||||
acc_seen = true;
|
||||
break;
|
||||
case anon:
|
||||
break;
|
||||
}
|
||||
refs_seen |= !bdd_map[i].refs.empty();
|
||||
}
|
||||
if (var_map.empty() && acc_map.empty())
|
||||
{
|
||||
if (var_seen)
|
||||
{
|
||||
std::cerr << "var_map is empty but Var in map" << std::endl;
|
||||
fail = true;
|
||||
}
|
||||
if (acc_seen)
|
||||
{
|
||||
std::cerr << "acc_map is empty but Acc in map" << std::endl;
|
||||
fail = true;
|
||||
}
|
||||
if (refs_seen)
|
||||
{
|
||||
std::cerr << "maps are empty but var_refs is not" << std::endl;
|
||||
fail = true;
|
||||
}
|
||||
if (!fail)
|
||||
return;
|
||||
}
|
||||
else
|
||||
{
|
||||
std::cerr << "some maps are not empty" << std::endl;
|
||||
}
|
||||
dump(std::cerr);
|
||||
abort();
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
357
src/twa/bdddict.hh
Normal file
357
src/twa/bdddict.hh
Normal file
|
|
@ -0,0 +1,357 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
|
||||
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <list>
|
||||
#include <set>
|
||||
#include <map>
|
||||
#include <iosfwd>
|
||||
#include <bddx.h>
|
||||
#include <vector>
|
||||
#include <memory>
|
||||
#include "ltlast/formula.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Private data for bdd_dict.
|
||||
class bdd_dict_priv;
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief Map BDD variables to formulae.
|
||||
///
|
||||
/// The BDD library uses integers to designate Boolean variables in
|
||||
/// its decision diagrams. This class is used to map such integers
|
||||
/// to objects actually used in Spot. These objects are usually
|
||||
/// atomic propositions, but they can also be acceptance conditions.
|
||||
///
|
||||
/// When a BDD variable is registered using a bdd_dict, it is always
|
||||
/// associated to a "user" (or "owner") object. This is done by
|
||||
/// supplying the bdd_dict with a pointer to the intended user of
|
||||
/// the variable. When the user object dies, it should release the
|
||||
/// BDD variables it was using by calling (for instance)
|
||||
/// unregister_all_my_variables(), giving the same pointer.
|
||||
/// Variables can also by unregistered one by one using
|
||||
/// unregister_variable().
|
||||
class SPOT_API bdd_dict
|
||||
{
|
||||
bdd_dict_priv* priv_;
|
||||
public:
|
||||
|
||||
bdd_dict();
|
||||
|
||||
/// \brief Destroy the BDD dict.
|
||||
///
|
||||
/// This always calls assert_emptiness() to diagnose cases where
|
||||
/// variables have not been unregistered.
|
||||
~bdd_dict();
|
||||
|
||||
/// Formula-to-BDD-variable maps.
|
||||
typedef std::map<const ltl::formula*, int> fv_map;
|
||||
/// BDD-variable-to-formula maps.
|
||||
typedef std::map<int, const ltl::formula*> vf_map;
|
||||
|
||||
fv_map var_map; ///< Maps atomic propositions to BDD variables
|
||||
fv_map acc_map; ///< Maps acceptance conditions to BDD variables
|
||||
|
||||
/// BDD-variable reference counts.
|
||||
typedef std::set<const void*> ref_set;
|
||||
|
||||
enum var_type { anon = 0, var, acc };
|
||||
struct bdd_info {
|
||||
bdd_info() : type(anon) {}
|
||||
var_type type;
|
||||
const ltl::formula* f; // Used unless t==anon.
|
||||
ref_set refs;
|
||||
int clone_counts;
|
||||
};
|
||||
typedef std::vector<bdd_info> bdd_info_map;
|
||||
// Map BDD variables to their meaning.
|
||||
bdd_info_map bdd_map;
|
||||
|
||||
/// \brief Register an atomic proposition.
|
||||
///
|
||||
/// Return (and maybe allocate) a BDD variable designating formula
|
||||
/// \a f. The \a for_me argument should point to the object using
|
||||
/// this BDD variable, this is used for reference counting. It is
|
||||
/// perfectly safe to call this function several time with the same
|
||||
/// arguments.
|
||||
///
|
||||
/// \return The variable number. Use bdd_ithvar() or bdd_nithvar()
|
||||
/// to convert this to a BDD.
|
||||
/// @{
|
||||
int register_proposition(const ltl::formula* f, const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
int register_proposition(const ltl::formula* f,
|
||||
std::shared_ptr<T> for_me)
|
||||
{
|
||||
return register_proposition(f, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Register BDD variables as atomic propositions.
|
||||
///
|
||||
/// Register all variables occurring in \a f as atomic propositions
|
||||
/// used by \a for_me. This assumes that these atomic propositions
|
||||
/// are already known from the dictionary (i.e., they have already
|
||||
/// been registered by register_proposition() for another
|
||||
/// automaton).
|
||||
/// @{
|
||||
void register_propositions(bdd f, const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
void register_propositions(bdd f, std::shared_ptr<T> for_me)
|
||||
{
|
||||
register_propositions(f, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief whether a proposition has already been registered
|
||||
///
|
||||
/// If \a f has been registered for \a me, this returns
|
||||
/// a non-negative value that is the BDD variable number.
|
||||
/// Otherwise this returns -1.
|
||||
/// @{
|
||||
int has_registered_proposition(const ltl::formula* f,
|
||||
const void* me);
|
||||
template <typename T>
|
||||
int has_registered_proposition(const ltl::formula* f,
|
||||
std::shared_ptr<T> for_me)
|
||||
{
|
||||
return has_registered_proposition(f, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Register an acceptance variable.
|
||||
///
|
||||
/// Return (and maybe allocate) a BDD variable designating an
|
||||
/// acceptance set associated to formula \a f. The \a for_me
|
||||
/// argument should point to the object using this BDD variable,
|
||||
/// this is used for reference counting. It is perfectly safe to
|
||||
/// call this function several time with the same arguments.
|
||||
///
|
||||
/// \return The variable number. Use bdd_ithvar() or bdd_nithvar()
|
||||
/// to convert this to a BDD.
|
||||
/// @{
|
||||
int register_acceptance_variable(const ltl::formula* f, const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
int register_acceptance_variable(const ltl::formula* f,
|
||||
std::shared_ptr<T> for_me)
|
||||
{
|
||||
return register_acceptance_variable(f, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Clone an acceptance variable VAR for FOR_ME.
|
||||
///
|
||||
/// This is used in products TGBAs when both operands share the
|
||||
/// same acceptance variables but they need to be distinguished in
|
||||
/// the result.
|
||||
/// @{
|
||||
int register_clone_acc(int var, const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
int register_clone_acc(int var, std::shared_ptr<T> for_me)
|
||||
{
|
||||
return register_clone_acc(var, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Register BDD variables as acceptance variables.
|
||||
///
|
||||
/// Register all variables occurring in \a f as acceptance variables
|
||||
/// used by \a for_me. This assumes that these acceptance variables
|
||||
/// are already known from the dictionary (i.e., they have already
|
||||
/// been registered by register_acceptance_variable() for another
|
||||
/// automaton).
|
||||
/// @{
|
||||
void register_acceptance_variables(bdd f, const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
void register_acceptance_variables(bdd f, std::shared_ptr<T> for_me)
|
||||
{
|
||||
register_acceptance_variables(f, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Convert one acceptance condition into the associated
|
||||
/// formula.
|
||||
///
|
||||
/// This version accepts a conjunction of Acc variables, in which
|
||||
/// only one must be positive. This positive variable will be
|
||||
/// converted back into the associated formula.
|
||||
///
|
||||
/// The returned formula is not cloned, and is valid until the BDD
|
||||
/// variable used in \a oneacc are unregistered.
|
||||
const ltl::formula* oneacc_to_formula(bdd oneacc) const;
|
||||
|
||||
/// \brief Convert one acceptance condition into the associated
|
||||
/// formula.
|
||||
///
|
||||
/// This version takes the number of a BDD variable that must has
|
||||
/// been returned by a call to register_acceptance_variable().
|
||||
///
|
||||
/// The returned formula is not cloned, and is valid until the BDD
|
||||
/// variable \a var is unregistered.
|
||||
const ltl::formula* oneacc_to_formula(int var) const;
|
||||
|
||||
/// \brief Register anonymous BDD variables.
|
||||
///
|
||||
/// Return (and maybe allocate) \a n consecutive BDD variables which
|
||||
/// will be used only by \a for_me.
|
||||
///
|
||||
/// \return The variable number. Use bdd_ithvar() or bdd_nithvar()
|
||||
/// to convert this to a BDD.
|
||||
/// @{
|
||||
int register_anonymous_variables(int n, const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
int register_anonymous_variables(int n, std::shared_ptr<T> for_me)
|
||||
{
|
||||
return register_anonymous_variables(n, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Duplicate the variable usage of another object.
|
||||
///
|
||||
/// This tells this dictionary that the \a for_me object will be
|
||||
/// using the same BDD variables as the \a from_other objects.
|
||||
/// This ensures that the variables won't be freed when \a
|
||||
/// from_other is deleted if \a from_other is still alive.
|
||||
/// @{
|
||||
void register_all_variables_of(const void* from_other, const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
void register_all_variables_of(const void* from_other,
|
||||
std::shared_ptr<T> for_me)
|
||||
{
|
||||
register_all_variables_of(from_other, for_me.get());
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
void register_all_variables_of(std::shared_ptr<T> from_other,
|
||||
const void* for_me)
|
||||
{
|
||||
register_all_variables_of(from_other.get(), for_me);
|
||||
}
|
||||
|
||||
template <typename T, typename U>
|
||||
void register_all_variables_of(std::shared_ptr<T> from_other,
|
||||
std::shared_ptr<U> for_me)
|
||||
{
|
||||
register_all_variables_of(from_other.get(), for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Register the same propositions as another object.
|
||||
///
|
||||
/// This tells this dictionary that the \a for_me object will be
|
||||
/// using the same BDD variable used for atomic propositions by
|
||||
/// the \a from_other object. This ensures that the variables
|
||||
/// won't be freed when \a from_other is deleted if \a from_other
|
||||
/// is still alive.
|
||||
/// @{
|
||||
void register_all_propositions_of(const void* from_other,
|
||||
const void* for_me);
|
||||
|
||||
template <typename T>
|
||||
void register_all_propositions_of(const void* from_other,
|
||||
std::shared_ptr<T> for_me)
|
||||
{
|
||||
register_all_propositions_of(from_other, for_me.get());
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
void register_all_propositions_of(std::shared_ptr<T> from_other,
|
||||
const void* for_me)
|
||||
{
|
||||
register_all_propositions_of(from_other.get(), for_me);
|
||||
}
|
||||
|
||||
template <typename T, typename U>
|
||||
void register_all_propositions_of(std::shared_ptr<T> from_other,
|
||||
std::shared_ptr<U> for_me)
|
||||
{
|
||||
register_all_propositions_of(from_other.get(), for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Release all variables used by an object.
|
||||
///
|
||||
/// Usually called in the destructor if \a me.
|
||||
void unregister_all_my_variables(const void* me);
|
||||
|
||||
/// \brief Release all variables of a given type, used by an
|
||||
/// object.
|
||||
/// @{
|
||||
void unregister_all_typed_variables(var_type type, const void* me);
|
||||
|
||||
template <typename T>
|
||||
void unregister_all_typed_variables(var_type type, std::shared_ptr<T> me)
|
||||
{
|
||||
unregister_all_typed_variables(type, me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Release a variable used by \a me.
|
||||
/// @{
|
||||
void unregister_variable(int var, const void* me);
|
||||
|
||||
template <typename T>
|
||||
void unregister_variable(int var, std::shared_ptr<T> me)
|
||||
{
|
||||
unregister_variable(var, me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Dump all variables for debugging.
|
||||
/// \param os The output stream.
|
||||
std::ostream& dump(std::ostream& os) const;
|
||||
|
||||
/// \brief Make sure the dictionary is empty.
|
||||
///
|
||||
/// This will print diagnostics if the dictionary is not empty.
|
||||
/// Use for debugging. This is called automatically by the
|
||||
/// destructor. When Spot is compiled in development mode (i.e.,
|
||||
/// with <code>./configure --enable-devel</code>), this function
|
||||
/// will abort if the dictionary is not empty.
|
||||
///
|
||||
/// The errors detected by this function usually indicate missing
|
||||
/// calls to unregister_variable() or
|
||||
/// unregister_all_my_variables().
|
||||
void assert_emptiness() const;
|
||||
|
||||
private:
|
||||
// Disallow copy.
|
||||
bdd_dict(const bdd_dict& other) SPOT_DELETED;
|
||||
bdd_dict& operator=(const bdd_dict& other) SPOT_DELETED;
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
|
||||
|
||||
inline bdd_dict_ptr make_bdd_dict()
|
||||
{
|
||||
return std::make_shared<bdd_dict>();
|
||||
}
|
||||
}
|
||||
261
src/twa/bddprint.cc
Normal file
261
src/twa/bddprint.cc
Normal file
|
|
@ -0,0 +1,261 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2012, 2014 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
|
||||
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
|
||||
// Pierre et Marie Curie.
|
||||
//
|
||||
// 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 <sstream>
|
||||
#include <cassert>
|
||||
#include <ostream>
|
||||
#include "bddprint.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
#include "formula2bdd.hh"
|
||||
#include "misc/minato.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// Global dictionary used by print_handler() to lookup variables.
|
||||
static bdd_dict_ptr dict;
|
||||
|
||||
/// Global flag to enable Acc[x] output (instead of `x').
|
||||
static bool want_acc;
|
||||
|
||||
/// Global flag to enable UTF-8 output.
|
||||
static bool utf8;
|
||||
|
||||
static
|
||||
std::ostream& print_ltl(const ltl::formula* f, std::ostream& o)
|
||||
{
|
||||
if (utf8)
|
||||
ltl::to_utf8_string(f, o);
|
||||
else
|
||||
ltl::to_string(f, o);
|
||||
return o;
|
||||
}
|
||||
|
||||
/// Stream handler used by Buddy to display BDD variables.
|
||||
static void
|
||||
print_handler(std::ostream& o, int v)
|
||||
{
|
||||
assert(unsigned(v) < dict->bdd_map.size());
|
||||
const bdd_dict::bdd_info& ref = dict->bdd_map[v];
|
||||
switch (ref.type)
|
||||
{
|
||||
case bdd_dict::var:
|
||||
to_string(ref.f, o);
|
||||
break;
|
||||
case bdd_dict::acc:
|
||||
if (want_acc)
|
||||
{
|
||||
o << "Acc[";
|
||||
print_ltl(ref.f, o) << ']';
|
||||
}
|
||||
else
|
||||
{
|
||||
o << '"';
|
||||
print_ltl(ref.f, o) << '"';
|
||||
}
|
||||
break;
|
||||
case bdd_dict::anon:
|
||||
o << '?' << v;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
static std::ostream* where;
|
||||
static void
|
||||
print_sat_handler(char* varset, int size)
|
||||
{
|
||||
bool not_first = false;
|
||||
for (int v = 0; v < size; ++v)
|
||||
{
|
||||
if (varset[v] < 0)
|
||||
continue;
|
||||
if (not_first)
|
||||
*where << ' ';
|
||||
else
|
||||
not_first = true;
|
||||
if (varset[v] == 0)
|
||||
*where << "! ";
|
||||
print_handler(*where, v);
|
||||
}
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_sat(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
dict = d;
|
||||
where = &os;
|
||||
want_acc = false;
|
||||
assert(bdd_satone(b) == b);
|
||||
bdd_allsat(b, print_sat_handler);
|
||||
return os;
|
||||
}
|
||||
|
||||
static void
|
||||
print_acc_handler(char* varset, int size)
|
||||
{
|
||||
for (int v = 0; v < size; ++v)
|
||||
if (varset[v] > 0)
|
||||
{
|
||||
*where << ' ';
|
||||
print_handler(*where, v);
|
||||
}
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_acc(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
dict = d;
|
||||
where = &os;
|
||||
want_acc = false;
|
||||
bdd_allsat(b, print_acc_handler);
|
||||
return os;
|
||||
}
|
||||
|
||||
static bool first_done = false;
|
||||
static void
|
||||
print_accset_handler(char* varset, int size)
|
||||
{
|
||||
for (int v = 0; v < size; ++v)
|
||||
if (varset[v] > 0)
|
||||
{
|
||||
*where << (first_done ? ", " : "{");
|
||||
print_handler(*where, v);
|
||||
first_done = true;
|
||||
}
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_accset(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
dict = d;
|
||||
where = &os;
|
||||
want_acc = true;
|
||||
first_done = false;
|
||||
bdd_allsat(b, print_accset_handler);
|
||||
if (first_done)
|
||||
*where << '}';
|
||||
return os;
|
||||
}
|
||||
|
||||
std::string
|
||||
bdd_format_accset(const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
std::ostringstream os;
|
||||
bdd_print_accset(os, d, b);
|
||||
return os.str();
|
||||
}
|
||||
|
||||
std::string
|
||||
bdd_format_sat(const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
std::ostringstream os;
|
||||
bdd_print_sat(os, d, b);
|
||||
return os.str();
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_set(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
dict = d;
|
||||
want_acc = true;
|
||||
bdd_strm_hook(print_handler);
|
||||
os << bddset << b;
|
||||
bdd_strm_hook(0);
|
||||
return os;
|
||||
}
|
||||
|
||||
std::string
|
||||
bdd_format_set(const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
std::ostringstream os;
|
||||
bdd_print_set(os, d, b);
|
||||
return os.str();
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_formula(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
const ltl::formula* f = bdd_to_formula(b, d);
|
||||
print_ltl(f, os);
|
||||
f->destroy();
|
||||
return os;
|
||||
}
|
||||
|
||||
std::string
|
||||
bdd_format_formula(const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
std::ostringstream os;
|
||||
bdd_print_formula(os, d, b);
|
||||
return os.str();
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_dot(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
dict = d;
|
||||
want_acc = true;
|
||||
bdd_strm_hook(print_handler);
|
||||
os << bdddot << b;
|
||||
bdd_strm_hook(0);
|
||||
return os;
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_table(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
dict = d;
|
||||
want_acc = true;
|
||||
bdd_strm_hook(print_handler);
|
||||
os << bddtable << b;
|
||||
bdd_strm_hook(0);
|
||||
return os;
|
||||
}
|
||||
|
||||
void
|
||||
enable_utf8()
|
||||
{
|
||||
utf8 = true;
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
bdd_print_isop(std::ostream& os, const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
dict = d;
|
||||
want_acc = true;
|
||||
minato_isop isop(b);
|
||||
|
||||
bdd p;
|
||||
while ((p = isop.next()) != bddfalse)
|
||||
{
|
||||
os << bdd_format_set(d, p);
|
||||
}
|
||||
|
||||
return os;
|
||||
}
|
||||
|
||||
std::string
|
||||
bdd_format_isop(const bdd_dict_ptr& d, bdd b)
|
||||
{
|
||||
std::ostringstream os;
|
||||
bdd_print_isop(os, d, b);
|
||||
return os.str();
|
||||
}
|
||||
}
|
||||
140
src/twa/bddprint.hh
Normal file
140
src/twa/bddprint.hh
Normal file
|
|
@ -0,0 +1,140 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <string>
|
||||
#include <iosfwd>
|
||||
#include "bdddict.hh"
|
||||
#include <bddx.h>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
/// \brief Print a BDD as a list of literals.
|
||||
///
|
||||
/// This assumes that \a b is a conjunction of literals.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_sat(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Format a BDD as a list of literals.
|
||||
///
|
||||
/// This assumes that \a b is a conjunction of literals.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
/// \return The BDD formated as a string.
|
||||
SPOT_API std::string
|
||||
bdd_format_sat(const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Print a BDD as a list of acceptance conditions.
|
||||
///
|
||||
/// This is used when saving a TGBA.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
/// \return The BDD formated as a string.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_acc(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Print a BDD as a set of acceptance conditions.
|
||||
///
|
||||
/// This is used when saving a TGBA.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
/// \return The BDD formated as a string.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_accset(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Format a BDD as a set of acceptance conditions.
|
||||
///
|
||||
/// This is used when saving a TGBA.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
/// \return The BDD formated as a string.
|
||||
SPOT_API std::string
|
||||
bdd_format_accset(const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Print a BDD as a set.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_set(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Format a BDD as a set.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
/// \return The BDD formated as a string.
|
||||
SPOT_API std::string
|
||||
bdd_format_set(const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Print a BDD as a formula.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_formula(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Format a BDD as a formula.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
/// \return The BDD formated as a string.
|
||||
SPOT_API std::string
|
||||
bdd_format_formula(const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Print a BDD as a diagram in dotty format.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_dot(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Print a BDD as a table.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_table(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
/// \brief Enable UTF-8 output for bdd printers.
|
||||
SPOT_API void enable_utf8();
|
||||
|
||||
|
||||
/// \brief Format a BDD as an irredundant sum of product.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
/// \return The BDD formated as a string.
|
||||
SPOT_API std::string
|
||||
bdd_format_isop(const bdd_dict_ptr& dict, bdd b);
|
||||
|
||||
|
||||
/// \brief Print a BDD as an irredundant sum of product.
|
||||
/// \param os The output stream.
|
||||
/// \param dict The dictionary to use, to lookup variables.
|
||||
/// \param b The BDD to print.
|
||||
SPOT_API std::ostream&
|
||||
bdd_print_isop(std::ostream& os, const bdd_dict_ptr& dict, bdd b);
|
||||
}
|
||||
231
src/twa/formula2bdd.cc
Normal file
231
src/twa/formula2bdd.cc
Normal file
|
|
@ -0,0 +1,231 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
|
||||
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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 "formula2bdd.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlast/visitor.hh"
|
||||
#include "misc/minato.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
using namespace ltl;
|
||||
|
||||
namespace
|
||||
{
|
||||
class formula_to_bdd_visitor: public ltl::visitor
|
||||
{
|
||||
public:
|
||||
formula_to_bdd_visitor(const bdd_dict_ptr& d, void* owner)
|
||||
: d_(d), owner_(owner)
|
||||
{
|
||||
}
|
||||
|
||||
virtual
|
||||
~formula_to_bdd_visitor()
|
||||
{
|
||||
}
|
||||
|
||||
virtual void
|
||||
visit(const atomic_prop* node)
|
||||
{
|
||||
res_ = bdd_ithvar(d_->register_proposition(node, owner_));
|
||||
}
|
||||
|
||||
virtual void
|
||||
visit(const constant* node)
|
||||
{
|
||||
switch (node->val())
|
||||
{
|
||||
case constant::True:
|
||||
res_ = bddtrue;
|
||||
return;
|
||||
case constant::False:
|
||||
res_ = bddfalse;
|
||||
return;
|
||||
case constant::EmptyWord:
|
||||
SPOT_UNIMPLEMENTED();
|
||||
}
|
||||
SPOT_UNREACHABLE();
|
||||
}
|
||||
|
||||
virtual void
|
||||
visit(const bunop*)
|
||||
{
|
||||
SPOT_UNIMPLEMENTED();
|
||||
}
|
||||
|
||||
virtual void
|
||||
visit(const unop* node)
|
||||
{
|
||||
switch (node->op())
|
||||
{
|
||||
case unop::F:
|
||||
case unop::G:
|
||||
case unop::X:
|
||||
case unop::Closure:
|
||||
case unop::NegClosure:
|
||||
case unop::NegClosureMarked:
|
||||
SPOT_UNIMPLEMENTED();
|
||||
case unop::Not:
|
||||
{
|
||||
res_ = bdd_not(recurse(node->child()));
|
||||
return;
|
||||
}
|
||||
}
|
||||
SPOT_UNREACHABLE();
|
||||
}
|
||||
|
||||
virtual void
|
||||
visit(const binop* node)
|
||||
{
|
||||
bdd f1 = recurse(node->first());
|
||||
bdd f2 = recurse(node->second());
|
||||
|
||||
switch (node->op())
|
||||
{
|
||||
case binop::Xor:
|
||||
res_ = bdd_apply(f1, f2, bddop_xor);
|
||||
return;
|
||||
case binop::Implies:
|
||||
res_ = bdd_apply(f1, f2, bddop_imp);
|
||||
return;
|
||||
case binop::Equiv:
|
||||
res_ = bdd_apply(f1, f2, bddop_biimp);
|
||||
return;
|
||||
case binop::U:
|
||||
case binop::R:
|
||||
case binop::W:
|
||||
case binop::M:
|
||||
case binop::UConcat:
|
||||
case binop::EConcat:
|
||||
case binop::EConcatMarked:
|
||||
SPOT_UNIMPLEMENTED();
|
||||
}
|
||||
SPOT_UNREACHABLE();
|
||||
}
|
||||
|
||||
virtual void
|
||||
visit(const multop* node)
|
||||
{
|
||||
int op = -1;
|
||||
switch (node->op())
|
||||
{
|
||||
case multop::And:
|
||||
op = bddop_and;
|
||||
res_ = bddtrue;
|
||||
break;
|
||||
case multop::Or:
|
||||
op = bddop_or;
|
||||
res_ = bddfalse;
|
||||
break;
|
||||
case multop::Concat:
|
||||
case multop::Fusion:
|
||||
case multop::AndNLM:
|
||||
case multop::OrRat:
|
||||
case multop::AndRat:
|
||||
SPOT_UNIMPLEMENTED();
|
||||
}
|
||||
assert(op != -1);
|
||||
unsigned s = node->size();
|
||||
for (unsigned n = 0; n < s; ++n)
|
||||
{
|
||||
res_ = bdd_apply(res_, recurse(node->nth(n)), op);
|
||||
}
|
||||
}
|
||||
|
||||
bdd
|
||||
result() const
|
||||
{
|
||||
return res_;
|
||||
}
|
||||
|
||||
bdd
|
||||
recurse(const formula* f) const
|
||||
{
|
||||
return formula_to_bdd(f, d_, owner_);
|
||||
}
|
||||
|
||||
private:
|
||||
bdd_dict_ptr d_;
|
||||
void* owner_;
|
||||
bdd res_;
|
||||
};
|
||||
|
||||
// Convert a BDD which is known to be a conjonction into a formula.
|
||||
static const ltl::formula*
|
||||
conj_to_formula(bdd b, const bdd_dict_ptr d)
|
||||
{
|
||||
if (b == bddfalse)
|
||||
return constant::false_instance();
|
||||
multop::vec* v = new multop::vec;
|
||||
while (b != bddtrue)
|
||||
{
|
||||
int var = bdd_var(b);
|
||||
const bdd_dict::bdd_info& i = d->bdd_map[var];
|
||||
assert(i.type == bdd_dict::var);
|
||||
const formula* res = i.f->clone();
|
||||
|
||||
bdd high = bdd_high(b);
|
||||
if (high == bddfalse)
|
||||
{
|
||||
res = unop::instance(unop::Not, res);
|
||||
b = bdd_low(b);
|
||||
}
|
||||
else
|
||||
{
|
||||
// If bdd_low is not false, then b was not a conjunction.
|
||||
assert(bdd_low(b) == bddfalse);
|
||||
b = high;
|
||||
}
|
||||
assert(b != bddfalse);
|
||||
v->push_back(res);
|
||||
}
|
||||
return multop::instance(multop::And, v);
|
||||
}
|
||||
|
||||
} // anonymous
|
||||
|
||||
bdd
|
||||
formula_to_bdd(const formula* f, const bdd_dict_ptr& d, void* for_me)
|
||||
{
|
||||
formula_to_bdd_visitor v(d, for_me);
|
||||
f->accept(v);
|
||||
return v.result();
|
||||
}
|
||||
|
||||
const formula*
|
||||
bdd_to_formula(bdd f, const bdd_dict_ptr d)
|
||||
{
|
||||
if (f == bddfalse)
|
||||
return constant::false_instance();
|
||||
|
||||
multop::vec* v = new multop::vec;
|
||||
|
||||
minato_isop isop(f);
|
||||
bdd cube;
|
||||
while ((cube = isop.next()) != bddfalse)
|
||||
v->push_back(conj_to_formula(cube, d));
|
||||
|
||||
return multop::instance(multop::Or, v);
|
||||
}
|
||||
}
|
||||
63
src/twa/formula2bdd.hh
Normal file
63
src/twa/formula2bdd.hh
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita (LRDE).
|
||||
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "bdddict.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Convert a Boolean formula into a BDD.
|
||||
///
|
||||
/// Convert the Boolean formula \a f into a BDD, using existing
|
||||
/// variables from \a d, and registering new ones as necessary. \a
|
||||
/// for_me, the address of the user of these BDD variables will be
|
||||
/// passed to \a d when registering the variables.
|
||||
///
|
||||
/// If you only use the BDD representation temporarily, for instance
|
||||
/// passing it right away to bdd_to_formula(), you should not forget
|
||||
/// to unregister the variables that have been registered for \a
|
||||
/// for_me. See bdd_dict::unregister_all_my_variables().
|
||||
/// @{
|
||||
SPOT_API bdd
|
||||
formula_to_bdd(const ltl::formula* f, const bdd_dict_ptr& d, void* for_me);
|
||||
|
||||
template<typename T>
|
||||
SPOT_API bdd
|
||||
formula_to_bdd(const ltl::formula* f, const bdd_dict_ptr& d,
|
||||
const std::shared_ptr<T>& for_me)
|
||||
{
|
||||
return formula_to_bdd(f, d, for_me.get());
|
||||
}
|
||||
/// @}
|
||||
|
||||
/// \brief Convert a BDD into a formula.
|
||||
///
|
||||
/// Format the BDD as an irredundant sum of product (see the
|
||||
/// minato_isop class for details) and map the BDD variables back
|
||||
/// into their atomic propositions. This works only for Boolean
|
||||
/// formulas, and all the BDD variables used in \a f should have
|
||||
/// been registered in \a d. Although the result has type
|
||||
/// ltl::formula*, it obviously does not use any temporal operator.
|
||||
SPOT_API const
|
||||
ltl::formula* bdd_to_formula(bdd f, const bdd_dict_ptr d);
|
||||
}
|
||||
37
src/twa/fwd.hh
Normal file
37
src/twa/fwd.hh
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014, 2015 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <memory>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class twa;
|
||||
typedef std::shared_ptr<twa> twa_ptr;
|
||||
typedef std::shared_ptr<const twa> const_twa_ptr;
|
||||
|
||||
class twa_graph;
|
||||
typedef std::shared_ptr<const twa_graph> const_twa_graph_ptr;
|
||||
typedef std::shared_ptr<twa_graph> twa_graph_ptr;
|
||||
|
||||
class twa_product;
|
||||
typedef std::shared_ptr<const twa_product> const_twa_product_ptr;
|
||||
typedef std::shared_ptr<twa_product> twa_product_ptr;
|
||||
}
|
||||
371
src/twa/taatgba.cc
Normal file
371
src/twa/taatgba.cc
Normal file
|
|
@ -0,0 +1,371 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 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 <map>
|
||||
#include <algorithm>
|
||||
#include <iterator>
|
||||
#include <iostream>
|
||||
#include "twa/formula2bdd.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
#include "ltlvisit/clone.hh"
|
||||
#include "taatgba.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/*--------.
|
||||
| taa_tgba |
|
||||
`--------*/
|
||||
|
||||
taa_tgba::taa_tgba(const bdd_dict_ptr& dict)
|
||||
: twa(dict),
|
||||
init_(0), state_set_vec_()
|
||||
{
|
||||
}
|
||||
|
||||
taa_tgba::~taa_tgba()
|
||||
{
|
||||
ss_vec::iterator j;
|
||||
for (j = state_set_vec_.begin(); j != state_set_vec_.end(); ++j)
|
||||
delete *j;
|
||||
get_dict()->unregister_all_my_variables(this);
|
||||
}
|
||||
|
||||
void
|
||||
taa_tgba::add_condition(transition* t, const ltl::formula* f)
|
||||
{
|
||||
t->condition &= formula_to_bdd(f, get_dict(), this);
|
||||
f->destroy();
|
||||
}
|
||||
|
||||
state*
|
||||
taa_tgba::get_init_state() const
|
||||
{
|
||||
assert(init_);
|
||||
return new spot::set_state(init_);
|
||||
}
|
||||
|
||||
twa_succ_iterator*
|
||||
taa_tgba::succ_iter(const spot::state* state) const
|
||||
{
|
||||
const spot::set_state* s = down_cast<const spot::set_state*>(state);
|
||||
assert(s);
|
||||
return new taa_succ_iterator(s->get_state(), acc_);
|
||||
}
|
||||
|
||||
bdd
|
||||
taa_tgba::compute_support_conditions(const spot::state* s) const
|
||||
{
|
||||
const spot::set_state* se = down_cast<const spot::set_state*>(s);
|
||||
assert(se);
|
||||
const state_set* ss = se->get_state();
|
||||
|
||||
bdd res = bddtrue;
|
||||
taa_tgba::state_set::const_iterator i;
|
||||
taa_tgba::state::const_iterator j;
|
||||
for (i = ss->begin(); i != ss->end(); ++i)
|
||||
for (j = (*i)->begin(); j != (*i)->end(); ++j)
|
||||
res |= (*j)->condition;
|
||||
return res;
|
||||
}
|
||||
|
||||
/*----------.
|
||||
| state_set |
|
||||
`----------*/
|
||||
|
||||
const taa_tgba::state_set*
|
||||
set_state::get_state() const
|
||||
{
|
||||
return s_;
|
||||
}
|
||||
|
||||
int
|
||||
set_state::compare(const spot::state* other) const
|
||||
{
|
||||
const set_state* o = down_cast<const set_state*>(other);
|
||||
assert(o);
|
||||
|
||||
const taa_tgba::state_set* s1 = get_state();
|
||||
const taa_tgba::state_set* s2 = o->get_state();
|
||||
|
||||
if (s1->size() != s2->size())
|
||||
return s1->size() - s2->size();
|
||||
|
||||
taa_tgba::state_set::const_iterator it1 = s1->begin();
|
||||
taa_tgba::state_set::const_iterator it2 = s2->begin();
|
||||
while (it2 != s2->end())
|
||||
{
|
||||
int i = *it1++ - *it2++;
|
||||
if (i != 0)
|
||||
return i;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
size_t
|
||||
set_state::hash() const
|
||||
{
|
||||
size_t res = 0;
|
||||
taa_tgba::state_set::const_iterator it = s_->begin();
|
||||
while (it != s_->end())
|
||||
{
|
||||
res ^= reinterpret_cast<const char*>(*it++) - static_cast<char*>(0);
|
||||
res = wang32_hash(res);
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
set_state*
|
||||
set_state::clone() const
|
||||
{
|
||||
if (delete_me_ && s_)
|
||||
return new spot::set_state(new taa_tgba::state_set(*s_), true);
|
||||
else
|
||||
return new spot::set_state(s_, false);
|
||||
}
|
||||
|
||||
/*--------------.
|
||||
| taa_succ_iter |
|
||||
`--------------*/
|
||||
|
||||
taa_succ_iterator::taa_succ_iterator(const taa_tgba::state_set* s,
|
||||
const acc_cond& acc)
|
||||
: seen_(), acc_(acc)
|
||||
{
|
||||
if (s->empty())
|
||||
{
|
||||
taa_tgba::transition* t = new taa_tgba::transition;
|
||||
t->condition = bddtrue;
|
||||
t->acceptance_conditions = 0U;
|
||||
t->dst = new taa_tgba::state_set;
|
||||
succ_.push_back(t);
|
||||
return;
|
||||
}
|
||||
|
||||
bounds_t bounds;
|
||||
for (auto& i: *s)
|
||||
bounds.emplace_back(i->begin(), i->end());
|
||||
|
||||
/// Sorting might make the cartesian product faster by not
|
||||
/// exploring all possibilities.
|
||||
std::sort(bounds.begin(), bounds.end(), distance_sort());
|
||||
|
||||
std::vector<iterator> pos;
|
||||
pos.reserve(bounds.size());
|
||||
for (auto i: bounds)
|
||||
pos.push_back(i.first);
|
||||
|
||||
while (pos[0] != bounds[0].second)
|
||||
{
|
||||
taa_tgba::transition* t = new taa_tgba::transition;
|
||||
t->condition = bddtrue;
|
||||
t->acceptance_conditions = 0U;
|
||||
taa_tgba::state_set* ss = new taa_tgba::state_set;
|
||||
|
||||
unsigned p;
|
||||
for (p = 0; p < pos.size() && t->condition != bddfalse; ++p)
|
||||
{
|
||||
taa_tgba::state_set::const_iterator j;
|
||||
for (j = (*pos[p])->dst->begin(); j != (*pos[p])->dst->end(); ++j)
|
||||
if ((*j)->size() > 0) // Remove sink states.
|
||||
ss->insert(*j);
|
||||
|
||||
// Fill the new transition.
|
||||
t->condition &= (*pos[p])->condition;
|
||||
t->acceptance_conditions |= (*pos[p])->acceptance_conditions;
|
||||
} // If p != pos.size() we have found a contradiction
|
||||
assert(p > 0);
|
||||
t->dst = ss;
|
||||
// Boxing to be able to insert ss in the map directly.
|
||||
spot::set_state* b = new spot::set_state(ss);
|
||||
|
||||
// If no contradiction, then look for another transition to
|
||||
// merge with the new one.
|
||||
seen_map::iterator i = seen_.end(); // Initialize to silent a g++ warning.
|
||||
std::vector<taa_tgba::transition*>::iterator j;
|
||||
if (t->condition != bddfalse)
|
||||
{
|
||||
i = seen_.find(b);
|
||||
if (i != seen_.end())
|
||||
for (j = i->second.begin(); j != i->second.end(); ++j)
|
||||
{
|
||||
taa_tgba::transition* current = *j;
|
||||
if (*current->dst == *t->dst
|
||||
&& current->condition == t->condition)
|
||||
{
|
||||
current->acceptance_conditions &= t->acceptance_conditions;
|
||||
break;
|
||||
}
|
||||
if (*current->dst == *t->dst
|
||||
&& current->acceptance_conditions == t->acceptance_conditions)
|
||||
{
|
||||
current->condition |= t->condition;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
// Mark the new transition as seen and keep it if we have not
|
||||
// found any contradiction and no other transition to merge
|
||||
// with, or delete it otherwise.
|
||||
if (t->condition != bddfalse
|
||||
&& (i == seen_.end() || j == i->second.end()))
|
||||
{
|
||||
seen_[b].push_back(t);
|
||||
if (i != seen_.end())
|
||||
delete b;
|
||||
succ_.push_back(t);
|
||||
}
|
||||
else
|
||||
{
|
||||
delete t->dst;
|
||||
delete t;
|
||||
delete b;
|
||||
}
|
||||
|
||||
for (int i = pos.size() - 1; i >= 0; --i)
|
||||
{
|
||||
if ((i < int(p))
|
||||
&& (std::distance(pos[i], bounds[i].second) > 1
|
||||
|| (i == 0 && std::distance(pos[i], bounds[i].second) == 1)))
|
||||
{
|
||||
++pos[i];
|
||||
break;
|
||||
}
|
||||
else
|
||||
pos[i] = bounds[i].first;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
taa_succ_iterator::~taa_succ_iterator()
|
||||
{
|
||||
for (seen_map::iterator i = seen_.begin(); i != seen_.end();)
|
||||
{
|
||||
// Advance the iterator before deleting the state set.
|
||||
const spot::set_state* s = i->first;
|
||||
++i;
|
||||
delete s;
|
||||
}
|
||||
for (unsigned i = 0; i < succ_.size(); ++i)
|
||||
{
|
||||
delete succ_[i]->dst;
|
||||
delete succ_[i];
|
||||
}
|
||||
}
|
||||
|
||||
bool
|
||||
taa_succ_iterator::first()
|
||||
{
|
||||
i_ = succ_.begin();
|
||||
return i_ != succ_.end();
|
||||
}
|
||||
|
||||
bool
|
||||
taa_succ_iterator::next()
|
||||
{
|
||||
++i_;
|
||||
return i_ != succ_.end();
|
||||
}
|
||||
|
||||
bool
|
||||
taa_succ_iterator::done() const
|
||||
{
|
||||
return i_ == succ_.end();
|
||||
}
|
||||
|
||||
spot::set_state*
|
||||
taa_succ_iterator::current_state() const
|
||||
{
|
||||
assert(!done());
|
||||
return new spot::set_state(new taa_tgba::state_set(*(*i_)->dst), true);
|
||||
}
|
||||
|
||||
bdd
|
||||
taa_succ_iterator::current_condition() const
|
||||
{
|
||||
assert(!done());
|
||||
return (*i_)->condition;
|
||||
}
|
||||
|
||||
acc_cond::mark_t
|
||||
taa_succ_iterator::current_acceptance_conditions() const
|
||||
{
|
||||
assert(!done());
|
||||
return acc_.comp((*i_)->acceptance_conditions);
|
||||
}
|
||||
|
||||
/*----------------.
|
||||
| taa_tgba_string |
|
||||
`----------------*/
|
||||
|
||||
taa_tgba_string::~taa_tgba_string()
|
||||
{
|
||||
ns_map::iterator i;
|
||||
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
|
||||
{
|
||||
taa_tgba::state::iterator i2;
|
||||
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
|
||||
delete *i2;
|
||||
delete i->second;
|
||||
}
|
||||
}
|
||||
|
||||
std::string
|
||||
taa_tgba_string::label_to_string(const label_t& label) const
|
||||
{
|
||||
return label;
|
||||
}
|
||||
|
||||
std::string
|
||||
taa_tgba_string::clone_if(const label_t& label) const
|
||||
{
|
||||
return label;
|
||||
}
|
||||
|
||||
/*-----------------.
|
||||
| taa_tgba_formula |
|
||||
`-----------------*/
|
||||
|
||||
taa_tgba_formula::~taa_tgba_formula()
|
||||
{
|
||||
ns_map::iterator i;
|
||||
for (i = name_state_map_.begin(); i != name_state_map_.end();)
|
||||
{
|
||||
taa_tgba::state::iterator i2;
|
||||
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
|
||||
delete *i2;
|
||||
// Advance the iterator before destroying the formula.
|
||||
const ltl::formula* s = i->first;
|
||||
delete i->second;
|
||||
++i;
|
||||
s->destroy();
|
||||
}
|
||||
}
|
||||
|
||||
std::string
|
||||
taa_tgba_formula::label_to_string(const label_t& label) const
|
||||
{
|
||||
return ltl::to_string(label);
|
||||
}
|
||||
|
||||
const ltl::formula*
|
||||
taa_tgba_formula::clone_if(const label_t& label) const
|
||||
{
|
||||
return label->clone();
|
||||
}
|
||||
}
|
||||
356
src/twa/taatgba.hh
Normal file
356
src/twa/taatgba.hh
Normal file
|
|
@ -0,0 +1,356 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <set>
|
||||
#include <iosfwd>
|
||||
#include <vector>
|
||||
#include <string>
|
||||
#include "misc/hash.hh"
|
||||
#include "ltlast/formula.hh"
|
||||
#include "bdddict.hh"
|
||||
#include "twa.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief A self-loop Transition-based Alternating Automaton (TAA)
|
||||
/// which is seen as a TGBA (abstract class, see below).
|
||||
class SPOT_API taa_tgba: public twa
|
||||
{
|
||||
public:
|
||||
taa_tgba(const bdd_dict_ptr& dict);
|
||||
|
||||
struct transition;
|
||||
typedef std::list<transition*> state;
|
||||
typedef std::set<state*> state_set;
|
||||
|
||||
/// Explicit transitions.
|
||||
struct transition
|
||||
{
|
||||
bdd condition;
|
||||
acc_cond::mark_t acceptance_conditions;
|
||||
const state_set* dst;
|
||||
};
|
||||
|
||||
void add_condition(transition* t, const ltl::formula* f);
|
||||
|
||||
/// TGBA interface.
|
||||
virtual ~taa_tgba();
|
||||
virtual spot::state* get_init_state() const final;
|
||||
virtual twa_succ_iterator* succ_iter(const spot::state* state) const final;
|
||||
virtual std::string format_state(const spot::state* state) const = 0;
|
||||
|
||||
protected:
|
||||
virtual bdd compute_support_conditions(const spot::state* state)
|
||||
const final;
|
||||
|
||||
typedef std::vector<taa_tgba::state_set*> ss_vec;
|
||||
|
||||
taa_tgba::state_set* init_;
|
||||
ss_vec state_set_vec_;
|
||||
|
||||
std::map<const ltl::formula*, acc_cond::mark_t,
|
||||
ltl::formula_ptr_less_than> acc_map_;
|
||||
|
||||
private:
|
||||
// Disallow copy.
|
||||
taa_tgba(const taa_tgba& other) SPOT_DELETED;
|
||||
taa_tgba& operator=(const taa_tgba& other) SPOT_DELETED;
|
||||
};
|
||||
|
||||
/// Set of states deriving from spot::state.
|
||||
class SPOT_API set_state final: public spot::state
|
||||
{
|
||||
public:
|
||||
set_state(const taa_tgba::state_set* s, bool delete_me = false)
|
||||
: s_(s), delete_me_(delete_me)
|
||||
{
|
||||
}
|
||||
|
||||
virtual int compare(const spot::state*) const;
|
||||
virtual size_t hash() const;
|
||||
virtual set_state* clone() const;
|
||||
|
||||
virtual ~set_state()
|
||||
{
|
||||
if (delete_me_)
|
||||
delete s_;
|
||||
}
|
||||
|
||||
const taa_tgba::state_set* get_state() const;
|
||||
private:
|
||||
const taa_tgba::state_set* s_;
|
||||
bool delete_me_;
|
||||
};
|
||||
|
||||
class SPOT_API taa_succ_iterator final: public twa_succ_iterator
|
||||
{
|
||||
public:
|
||||
taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc);
|
||||
virtual ~taa_succ_iterator();
|
||||
|
||||
virtual bool first();
|
||||
virtual bool next();
|
||||
virtual bool done() const;
|
||||
|
||||
virtual set_state* current_state() const;
|
||||
virtual bdd current_condition() const;
|
||||
virtual acc_cond::mark_t current_acceptance_conditions() const;
|
||||
|
||||
private:
|
||||
/// Those typedefs are used to generate all possible successors in
|
||||
/// the constructor using a cartesian product.
|
||||
typedef taa_tgba::state::const_iterator iterator;
|
||||
typedef std::pair<iterator, iterator> iterator_pair;
|
||||
typedef std::vector<iterator_pair> bounds_t;
|
||||
typedef std::unordered_map<const spot::set_state*,
|
||||
std::vector<taa_tgba::transition*>,
|
||||
state_ptr_hash, state_ptr_equal> seen_map;
|
||||
|
||||
struct distance_sort :
|
||||
public std::binary_function<const iterator_pair&,
|
||||
const iterator_pair&, bool>
|
||||
{
|
||||
bool
|
||||
operator()(const iterator_pair& lhs, const iterator_pair& rhs) const
|
||||
{
|
||||
return std::distance(lhs.first, lhs.second) <
|
||||
std::distance(rhs.first, rhs.second);
|
||||
}
|
||||
};
|
||||
|
||||
std::vector<taa_tgba::transition*>::const_iterator i_;
|
||||
std::vector<taa_tgba::transition*> succ_;
|
||||
seen_map seen_;
|
||||
const acc_cond& acc_;
|
||||
};
|
||||
|
||||
/// A taa_tgba instance with states labeled by a given type.
|
||||
/// Still an abstract class, see below.
|
||||
template<typename label>
|
||||
class SPOT_API taa_tgba_labelled: public taa_tgba
|
||||
{
|
||||
public:
|
||||
taa_tgba_labelled(const bdd_dict_ptr& dict) : taa_tgba(dict) {};
|
||||
|
||||
~taa_tgba_labelled()
|
||||
{
|
||||
auto i = acc_map_.begin();
|
||||
while (i != acc_map_.end())
|
||||
(i++)->first->destroy();
|
||||
}
|
||||
|
||||
void set_init_state(const label& s)
|
||||
{
|
||||
std::vector<label> v(1);
|
||||
v[0] = s;
|
||||
set_init_state(v);
|
||||
}
|
||||
void set_init_state(const std::vector<label>& s)
|
||||
{
|
||||
init_ = add_state_set(s);
|
||||
}
|
||||
|
||||
transition*
|
||||
create_transition(const label& s,
|
||||
const std::vector<label>& d)
|
||||
{
|
||||
state* src = add_state(s);
|
||||
state_set* dst = add_state_set(d);
|
||||
transition* t = new transition;
|
||||
t->dst = dst;
|
||||
t->condition = bddtrue;
|
||||
t->acceptance_conditions = 0U;
|
||||
src->push_back(t);
|
||||
return t;
|
||||
}
|
||||
|
||||
transition*
|
||||
create_transition(const label& s, const label& d)
|
||||
{
|
||||
std::vector<std::string> vec;
|
||||
vec.push_back(d);
|
||||
return create_transition(s, vec);
|
||||
}
|
||||
|
||||
void add_acceptance_condition(transition* t, const ltl::formula* f)
|
||||
{
|
||||
auto p = acc_map_.emplace(f, 0);
|
||||
if (p.second)
|
||||
p.first->second = acc_.marks({acc_.add_set()});
|
||||
else
|
||||
f->destroy();
|
||||
t->acceptance_conditions |= p.first->second;
|
||||
}
|
||||
|
||||
/// \brief Format the state as a string for printing.
|
||||
///
|
||||
/// If state is a spot::set_state of only one element, then the
|
||||
/// string corresponding to state->get_state() is returned.
|
||||
///
|
||||
/// Otherwise a string composed of each string corresponding to
|
||||
/// each state->get_state() in the spot::set_state is returned,
|
||||
/// e.g. like {string_1,...,string_n}.
|
||||
virtual std::string format_state(const spot::state* s) const
|
||||
{
|
||||
const spot::set_state* se = down_cast<const spot::set_state*>(s);
|
||||
assert(se);
|
||||
const state_set* ss = se->get_state();
|
||||
return format_state_set(ss);
|
||||
}
|
||||
|
||||
/// \brief Output a TAA in a stream.
|
||||
void output(std::ostream& os) const
|
||||
{
|
||||
typename ns_map::const_iterator i;
|
||||
for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
|
||||
{
|
||||
taa_tgba::state::const_iterator i2;
|
||||
os << "State: " << label_to_string(i->first) << std::endl;
|
||||
for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
|
||||
{
|
||||
os << ' ' << format_state_set((*i2)->dst)
|
||||
<< ", C:" << (*i2)->condition
|
||||
<< ", A:" << (*i2)->acceptance_conditions << std::endl;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
protected:
|
||||
typedef label label_t;
|
||||
|
||||
typedef std::unordered_map<label, taa_tgba::state*> ns_map;
|
||||
typedef std::unordered_map<const taa_tgba::state*, label,
|
||||
ptr_hash<taa_tgba::state> > sn_map;
|
||||
|
||||
ns_map name_state_map_;
|
||||
sn_map state_name_map_;
|
||||
|
||||
/// \brief Return a label as a string.
|
||||
virtual std::string label_to_string(const label_t& lbl) const = 0;
|
||||
|
||||
/// \brief Clone the label if necessary to assure it is owned by
|
||||
/// this, avoiding memory issues when label is a pointer.
|
||||
virtual label_t clone_if(const label_t& lbl) const = 0;
|
||||
|
||||
private:
|
||||
/// \brief Return the taa_tgba::state for \a name, creating it
|
||||
/// when it does not exist already.
|
||||
taa_tgba::state* add_state(const label& name)
|
||||
{
|
||||
typename ns_map::iterator i = name_state_map_.find(name);
|
||||
if (i == name_state_map_.end())
|
||||
{
|
||||
const label& name_ = clone_if(name);
|
||||
taa_tgba::state* s = new taa_tgba::state;
|
||||
name_state_map_[name_] = s;
|
||||
state_name_map_[s] = name_;
|
||||
return s;
|
||||
}
|
||||
return i->second;
|
||||
}
|
||||
|
||||
/// \brief Return the taa::state_set for \a names.
|
||||
taa_tgba::state_set* add_state_set(const std::vector<label>& names)
|
||||
{
|
||||
state_set* ss = new state_set;
|
||||
for (unsigned i = 0; i < names.size(); ++i)
|
||||
ss->insert(add_state(names[i]));
|
||||
state_set_vec_.push_back(ss);
|
||||
return ss;
|
||||
}
|
||||
|
||||
std::string format_state_set(const taa_tgba::state_set* ss) const
|
||||
{
|
||||
state_set::const_iterator i1 = ss->begin();
|
||||
typename sn_map::const_iterator i2;
|
||||
if (ss->empty())
|
||||
return std::string("{}");
|
||||
if (ss->size() == 1)
|
||||
{
|
||||
i2 = state_name_map_.find(*i1);
|
||||
assert(i2 != state_name_map_.end());
|
||||
return "{" + label_to_string(i2->second) + "}";
|
||||
}
|
||||
else
|
||||
{
|
||||
std::string res("{");
|
||||
while (i1 != ss->end())
|
||||
{
|
||||
i2 = state_name_map_.find(*i1++);
|
||||
assert(i2 != state_name_map_.end());
|
||||
res += label_to_string(i2->second);
|
||||
res += ",";
|
||||
}
|
||||
res[res.size() - 1] = '}';
|
||||
return res;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
class SPOT_API taa_tgba_string final:
|
||||
#ifndef SWIG
|
||||
public taa_tgba_labelled<std::string>
|
||||
#else
|
||||
public taa_tgba
|
||||
#endif
|
||||
{
|
||||
public:
|
||||
taa_tgba_string(const bdd_dict_ptr& dict) :
|
||||
taa_tgba_labelled<std::string>(dict) {};
|
||||
~taa_tgba_string();
|
||||
protected:
|
||||
virtual std::string label_to_string(const std::string& label) const;
|
||||
virtual std::string clone_if(const std::string& label) const;
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
|
||||
typedef std::shared_ptr<const taa_tgba_string> const_taa_tgba_string_ptr;
|
||||
|
||||
inline taa_tgba_string_ptr make_taa_tgba_string(const bdd_dict_ptr& dict)
|
||||
{
|
||||
return std::make_shared<taa_tgba_string>(dict);
|
||||
}
|
||||
|
||||
class SPOT_API taa_tgba_formula final:
|
||||
#ifndef SWIG
|
||||
public taa_tgba_labelled<const ltl::formula*>
|
||||
#else
|
||||
public taa_tgba
|
||||
#endif
|
||||
{
|
||||
public:
|
||||
taa_tgba_formula(const bdd_dict_ptr& dict) :
|
||||
taa_tgba_labelled<const ltl::formula*>(dict) {};
|
||||
~taa_tgba_formula();
|
||||
protected:
|
||||
virtual std::string label_to_string(const label_t& label) const;
|
||||
virtual const ltl::formula* clone_if(const label_t& label) const;
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
|
||||
typedef std::shared_ptr<const taa_tgba_formula> const_taa_tgba_formula_ptr;
|
||||
|
||||
inline taa_tgba_formula_ptr make_taa_tgba_formula(const bdd_dict_ptr& dict)
|
||||
{
|
||||
return std::make_shared<taa_tgba_formula>(dict);
|
||||
}
|
||||
}
|
||||
119
src/twa/twa.cc
Normal file
119
src/twa/twa.cc
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2014, 2015 Laboratoire de Recherche et Developpement de
|
||||
// l'EPITA (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 "twa.hh"
|
||||
#include "twagraph.hh"
|
||||
#include "tgbaalgos/gtec/gtec.hh"
|
||||
#include "tgbaalgos/remfin.hh"
|
||||
#include <utility>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
twa::twa(const bdd_dict_ptr& d)
|
||||
: iter_cache_(nullptr),
|
||||
dict_(d),
|
||||
last_support_conditions_input_(0)
|
||||
{
|
||||
props = 0U;
|
||||
}
|
||||
|
||||
twa::~twa()
|
||||
{
|
||||
if (last_support_conditions_input_)
|
||||
last_support_conditions_input_->destroy();
|
||||
delete iter_cache_;
|
||||
release_named_properties();
|
||||
}
|
||||
|
||||
bdd
|
||||
twa::support_conditions(const state* state) const
|
||||
{
|
||||
if (!last_support_conditions_input_
|
||||
|| last_support_conditions_input_->compare(state) != 0)
|
||||
{
|
||||
last_support_conditions_output_ = compute_support_conditions(state);
|
||||
if (last_support_conditions_input_)
|
||||
last_support_conditions_input_->destroy();
|
||||
last_support_conditions_input_ = state->clone();
|
||||
}
|
||||
return last_support_conditions_output_;
|
||||
}
|
||||
|
||||
state*
|
||||
twa::project_state(const state* s,
|
||||
const const_twa_ptr& t) const
|
||||
{
|
||||
if (t.get() == this)
|
||||
return s->clone();
|
||||
return 0;
|
||||
}
|
||||
|
||||
std::string
|
||||
twa::transition_annotation(const twa_succ_iterator*) const
|
||||
{
|
||||
return "";
|
||||
}
|
||||
|
||||
bool
|
||||
twa::is_empty() const
|
||||
{
|
||||
// FIXME: This should be improved based on properties of the
|
||||
// automaton. For instance we do not need couvreur99 is we know
|
||||
// the automaton is weak.
|
||||
auto a = shared_from_this();
|
||||
if (a->acc().uses_fin_acceptance())
|
||||
{
|
||||
auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
|
||||
if (!aa)
|
||||
aa = make_twa_graph(a, prop_set::all());
|
||||
a = remove_fin(aa);
|
||||
}
|
||||
return !couvreur99(a)->check();
|
||||
}
|
||||
|
||||
void
|
||||
twa::set_named_prop(std::string s,
|
||||
void* val, std::function<void(void*)> destructor)
|
||||
{
|
||||
auto p = named_prop_.emplace(std::piecewise_construct,
|
||||
std::forward_as_tuple(s),
|
||||
std::forward_as_tuple(val, destructor));
|
||||
if (!p.second)
|
||||
{
|
||||
p.first->second.second(p.first->second.first);
|
||||
p.first->second = std::make_pair(val, destructor);
|
||||
}
|
||||
}
|
||||
|
||||
void*
|
||||
twa::get_named_prop_(std::string s) const
|
||||
{
|
||||
auto i = named_prop_.find(s);
|
||||
if (i == named_prop_.end())
|
||||
return nullptr;
|
||||
return i->second.first;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
}
|
||||
871
src/twa/twa.hh
Normal file
871
src/twa/twa.hh
Normal file
|
|
@ -0,0 +1,871 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2011, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "fwd.hh"
|
||||
#include "acc.hh"
|
||||
#include "bdddict.hh"
|
||||
#include <cassert>
|
||||
#include <memory>
|
||||
#include <unordered_map>
|
||||
#include <functional>
|
||||
#include <array>
|
||||
#include "misc/casts.hh"
|
||||
#include "misc/hash.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief Abstract class for states.
|
||||
class SPOT_API state
|
||||
{
|
||||
public:
|
||||
/// \brief Compares two states (that come from the same automaton).
|
||||
///
|
||||
/// This method returns an integer less than, equal to, or greater
|
||||
/// than zero if \a this is found, respectively, to be less than, equal
|
||||
/// to, or greater than \a other according to some implicit total order.
|
||||
///
|
||||
/// This method should not be called to compare states from
|
||||
/// different automata.
|
||||
///
|
||||
/// \sa spot::state_ptr_less_than
|
||||
virtual int compare(const state* other) const = 0;
|
||||
|
||||
/// \brief Hash a state.
|
||||
///
|
||||
/// This method returns an integer that can be used as a
|
||||
/// hash value for this state.
|
||||
///
|
||||
/// Note that the hash value is guaranteed to be unique for all
|
||||
/// equal states (in compare()'s sense) for only has long has one
|
||||
/// of these states exists. So it's OK to use a spot::state as a
|
||||
/// key in a \c hash_map because the mere use of the state as a
|
||||
/// key in the hash will ensure the state continues to exist.
|
||||
///
|
||||
/// However if you create the state, get its hash key, delete the
|
||||
/// state, recreate the same state, and get its hash key, you may
|
||||
/// obtain two different hash keys if the same state were not
|
||||
/// already used elsewhere. In practice this weird situation can
|
||||
/// occur only when the state is BDD-encoded, because BDD numbers
|
||||
/// (used to build the hash value) can be reused for other
|
||||
/// formulas. That probably doesn't matter, since the hash value
|
||||
/// is meant to be used in a \c hash_map, but it had to be noted.
|
||||
virtual size_t hash() const = 0;
|
||||
|
||||
/// Duplicate a state.
|
||||
virtual state* clone() const = 0;
|
||||
|
||||
/// \brief Release a state.
|
||||
///
|
||||
/// Methods from the tgba or twa_succ_iterator always return a
|
||||
/// new state that you should deallocate with this function.
|
||||
/// Before Spot 0.7, you had to "delete" your state directly.
|
||||
/// Starting with Spot 0.7, you should update your code to use
|
||||
/// this function instead. destroy() usually call delete, except
|
||||
/// in subclasses that destroy() to allow better memory management
|
||||
/// (e.g., no memory allocation for explicit automata).
|
||||
virtual void destroy() const
|
||||
{
|
||||
delete this;
|
||||
}
|
||||
|
||||
protected:
|
||||
/// \brief Destructor.
|
||||
///
|
||||
/// Note that client code should call
|
||||
/// <code>s->destroy();</code> instead of <code>delete s;</code>.
|
||||
virtual ~state()
|
||||
{
|
||||
}
|
||||
};
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief Strict Weak Ordering for \c state*.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type \c state*.
|
||||
///
|
||||
/// For instance here is how one could declare
|
||||
/// a map of \c state*.
|
||||
/// \code
|
||||
/// // Remember how many times each state has been visited.
|
||||
/// std::map<spot::state*, int, spot::state_ptr_less_than> seen;
|
||||
/// \endcode
|
||||
struct state_ptr_less_than
|
||||
{
|
||||
bool
|
||||
operator()(const state* left, const state* right) const
|
||||
{
|
||||
assert(left);
|
||||
return left->compare(right) < 0;
|
||||
}
|
||||
};
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief An Equivalence Relation for \c state*.
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// an \c unordered_map whose key are of type \c state*.
|
||||
///
|
||||
/// For instance here is how one could declare
|
||||
/// a map of \c state*.
|
||||
/// \code
|
||||
/// // Remember how many times each state has been visited.
|
||||
/// std::unordered_map<spot::state*, int, spot::state_ptr_hash,
|
||||
/// spot::state_ptr_equal> seen;
|
||||
/// \endcode
|
||||
struct state_ptr_equal
|
||||
{
|
||||
bool
|
||||
operator()(const state* left, const state* right) const
|
||||
{
|
||||
assert(left);
|
||||
return 0 == left->compare(right);
|
||||
}
|
||||
};
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief Hash Function for \c state*.
|
||||
///
|
||||
/// This is meant to be used as a hash functor for
|
||||
/// an \c unordered_map whose key are of type \c state*.
|
||||
///
|
||||
/// For instance here is how one could declare
|
||||
/// a map of \c state*.
|
||||
/// \code
|
||||
/// // Remember how many times each state has been visited.
|
||||
/// std::unordered_map<spot::state*, int, spot::state_ptr_hash,
|
||||
/// spot::state_ptr_equal> seen;
|
||||
/// \endcode
|
||||
struct state_ptr_hash
|
||||
{
|
||||
size_t
|
||||
operator()(const state* that) const
|
||||
{
|
||||
assert(that);
|
||||
return that->hash();
|
||||
}
|
||||
};
|
||||
|
||||
typedef std::unordered_set<const state*,
|
||||
state_ptr_hash, state_ptr_equal> state_set;
|
||||
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief Render state pointers unique via a hash table.
|
||||
class SPOT_API state_unicity_table
|
||||
{
|
||||
state_set m;
|
||||
public:
|
||||
|
||||
/// \brief Canonicalize state pointer.
|
||||
///
|
||||
/// If this is the first time a state is seen, this return the
|
||||
/// state pointer as-is, otherwise it frees the state and returns
|
||||
/// a point to the previously seen copy.
|
||||
///
|
||||
/// States are owned by the table and will be freed on
|
||||
/// destruction.
|
||||
const state* operator()(const state* s)
|
||||
{
|
||||
auto p = m.insert(s);
|
||||
if (!p.second)
|
||||
s->destroy();
|
||||
return *p.first;
|
||||
}
|
||||
|
||||
/// \brief Canonicalize state pointer.
|
||||
///
|
||||
/// Same as operator(), except that a nullptr
|
||||
/// is returned if the state is not new.
|
||||
const state* is_new(const state* s)
|
||||
{
|
||||
auto p = m.insert(s);
|
||||
if (!p.second)
|
||||
{
|
||||
s->destroy();
|
||||
return nullptr;
|
||||
}
|
||||
return *p.first;
|
||||
}
|
||||
|
||||
~state_unicity_table()
|
||||
{
|
||||
for (state_set::iterator i = m.begin(); i != m.end();)
|
||||
{
|
||||
// Advance the iterator before destroying its key. This
|
||||
// avoid issues with old g++ implementations.
|
||||
state_set::iterator old = i++;
|
||||
(*old)->destroy();
|
||||
}
|
||||
}
|
||||
|
||||
size_t
|
||||
size()
|
||||
{
|
||||
return m.size();
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
||||
// Functions related to shared_ptr.
|
||||
//////////////////////////////////////////////////
|
||||
|
||||
typedef std::shared_ptr<const state> shared_state;
|
||||
|
||||
inline void shared_state_deleter(state* s) { s->destroy(); }
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief Strict Weak Ordering for \c shared_state
|
||||
/// (shared_ptr<const state*>).
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// STL \c map whose key are of type \c shared_state.
|
||||
///
|
||||
/// For instance here is how one could declare
|
||||
/// a map of \c shared_state.
|
||||
/// \code
|
||||
/// // Remember how many times each state has been visited.
|
||||
/// std::map<shared_state, int, spot::state_shared_ptr_less_than> seen;
|
||||
/// \endcode
|
||||
struct state_shared_ptr_less_than
|
||||
{
|
||||
bool
|
||||
operator()(shared_state left,
|
||||
shared_state right) const
|
||||
{
|
||||
assert(left);
|
||||
return left->compare(right.get()) < 0;
|
||||
}
|
||||
};
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief An Equivalence Relation for \c shared_state
|
||||
/// (shared_ptr<const state*>).
|
||||
///
|
||||
/// This is meant to be used as a comparison functor for
|
||||
/// un \c unordered_map whose key are of type \c shared_state.
|
||||
///
|
||||
/// For instance here is how one could declare
|
||||
/// a map of \c shared_state
|
||||
/// \code
|
||||
/// // Remember how many times each state has been visited.
|
||||
/// std::unordered_map<shared_state, int,
|
||||
/// state_shared_ptr_hash,
|
||||
/// state_shared_ptr_equal> seen;
|
||||
/// \endcode
|
||||
struct state_shared_ptr_equal
|
||||
{
|
||||
bool
|
||||
operator()(shared_state left,
|
||||
shared_state right) const
|
||||
{
|
||||
assert(left);
|
||||
return 0 == left->compare(right.get());
|
||||
}
|
||||
};
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \ingroup hash_funcs
|
||||
/// \brief Hash Function for \c shared_state (shared_ptr<const state*>).
|
||||
///
|
||||
/// This is meant to be used as a hash functor for
|
||||
/// an \c unordered_map whose key are of type
|
||||
/// \c shared_state.
|
||||
///
|
||||
/// For instance here is how one could declare
|
||||
/// a map of \c shared_state.
|
||||
/// \code
|
||||
/// // Remember how many times each state has been visited.
|
||||
/// std::unordered_map<shared_state, int,
|
||||
/// state_shared_ptr_hash,
|
||||
/// state_shared_ptr_equal> seen;
|
||||
/// \endcode
|
||||
struct state_shared_ptr_hash
|
||||
{
|
||||
size_t
|
||||
operator()(shared_state that) const
|
||||
{
|
||||
assert(that);
|
||||
return that->hash();
|
||||
}
|
||||
};
|
||||
|
||||
typedef std::unordered_set<shared_state,
|
||||
state_shared_ptr_hash,
|
||||
state_shared_ptr_equal> shared_state_set;
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief Iterate over the successors of a state.
|
||||
///
|
||||
/// This class provides the basic functionalities required to
|
||||
/// iterate over the successors of a state, as well as querying
|
||||
/// transition labels. Because transitions are never explicitely
|
||||
/// encoded, labels (conditions and acceptance conditions) can only
|
||||
/// be queried while iterating over the successors.
|
||||
class SPOT_API twa_succ_iterator
|
||||
{
|
||||
public:
|
||||
virtual
|
||||
~twa_succ_iterator()
|
||||
{
|
||||
}
|
||||
|
||||
/// \name Iteration
|
||||
//@{
|
||||
|
||||
/// \brief Position the iterator on the first successor (if any).
|
||||
///
|
||||
/// This method can be called several times to make multiple
|
||||
/// passes over successors.
|
||||
///
|
||||
/// \warning One should always call \c done() (or better: check
|
||||
/// the return value of first()) to ensure there is a successor,
|
||||
/// even after \c first(). A common trap is to assume that there
|
||||
/// is at least one successor: this is wrong.
|
||||
///
|
||||
/// \return whether there is actually a successor
|
||||
virtual bool first() = 0;
|
||||
|
||||
/// \brief Jump to the next successor (if any).
|
||||
///
|
||||
/// \warning Again, one should always call \c done() (or better:
|
||||
/// check the return value of next()) ensure there is a successor.
|
||||
///
|
||||
/// \return whether there is actually a successor
|
||||
virtual bool next() = 0;
|
||||
|
||||
/// \brief Check whether the iteration is finished.
|
||||
///
|
||||
/// This function should be called after any call to \c first()
|
||||
/// or \c next() and before any enquiry about the current state.
|
||||
///
|
||||
/// The usual way to do this is with a \c for loop.
|
||||
///
|
||||
/// for (s->first(); !s->done(); s->next())
|
||||
/// ...
|
||||
virtual bool done() const = 0;
|
||||
|
||||
//@}
|
||||
|
||||
/// \name Inspection
|
||||
//@{
|
||||
|
||||
/// \brief Get the state of the current successor.
|
||||
///
|
||||
/// Note that the same state may occur at different points
|
||||
/// in the iteration. These actually correspond to the same
|
||||
/// destination. It just means there were several transitions,
|
||||
/// with different conditions, leading to the same state.
|
||||
///
|
||||
/// The returned state should be destroyed (see state::destroy)
|
||||
/// by the caller after it is no longer used.
|
||||
virtual state* current_state() const = 0;
|
||||
/// \brief Get the condition on the transition leading to this successor.
|
||||
///
|
||||
/// This is a boolean function of atomic propositions.
|
||||
virtual bdd current_condition() const = 0;
|
||||
/// \brief Get the acceptance conditions on the transition leading
|
||||
/// to this successor.
|
||||
virtual acc_cond::mark_t current_acceptance_conditions() const = 0;
|
||||
|
||||
//@}
|
||||
};
|
||||
|
||||
namespace internal
|
||||
{
|
||||
struct SPOT_API succ_iterator
|
||||
{
|
||||
protected:
|
||||
twa_succ_iterator* it_;
|
||||
public:
|
||||
|
||||
succ_iterator(twa_succ_iterator* it):
|
||||
it_(it)
|
||||
{
|
||||
}
|
||||
|
||||
bool operator==(succ_iterator o) const
|
||||
{
|
||||
return it_ == o.it_;
|
||||
}
|
||||
|
||||
bool operator!=(succ_iterator o) const
|
||||
{
|
||||
return it_ != o.it_;
|
||||
}
|
||||
|
||||
const twa_succ_iterator* operator*() const
|
||||
{
|
||||
return it_;
|
||||
}
|
||||
|
||||
void operator++()
|
||||
{
|
||||
if (!it_->next())
|
||||
it_ = nullptr;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
/// \defgroup twa TωA (Transition-based ω-Automata)
|
||||
///
|
||||
/// Spot is centered around the spot::twa type. This type and its
|
||||
/// cousins are listed \ref tgba_essentials "here". This is an
|
||||
/// abstract interface. Its implementations are either \ref
|
||||
/// tgba_representation "concrete representations", or \ref
|
||||
/// tgba_on_the_fly_algorithms "on-the-fly algorithms". Other
|
||||
/// algorithms that work on spot::twa are \ref tgba_algorithms
|
||||
/// "listed separately".
|
||||
|
||||
/// \addtogroup twa_essentials Essential TωA types
|
||||
/// \ingroup twa
|
||||
|
||||
/// \ingroup twa_essentials
|
||||
/// \brief A Transition-based ω-Automaton.
|
||||
///
|
||||
/// The acronym TωA stands for Transition-based ω-automaton.
|
||||
/// We may write it as TwA or twa, but never as TWA as the
|
||||
/// w is just a non-utf8 replacement for ω that should not be
|
||||
/// capitalized.
|
||||
///
|
||||
/// TωAs are transition-based automata, meanings that not-only
|
||||
/// do they have labels on arcs, they also have an acceptance
|
||||
/// condition defined in term of sets of transitions.
|
||||
/// The acceptance condition can be anything supported by
|
||||
/// the HOA format (http://adl.github.io/hoaf/). The only
|
||||
/// restriction w.r.t. the format is that this class does
|
||||
/// not support alternating automata
|
||||
///
|
||||
/// Previous version of Spot supported a type of automata called
|
||||
/// TGBA, which are TωA in which the acceptance condition is a set
|
||||
/// of sets of transitions that must be intersected infinitely
|
||||
/// often.
|
||||
///
|
||||
/// In this version, TGBAs are now represented by TωAs for which
|
||||
/// <code>aut->acc().is_generalized_buchi())</code> returns true.
|
||||
///
|
||||
/// Browsing such automaton can be achieved using two functions:
|
||||
/// \c get_init_state, and \c succ. The former returns
|
||||
/// the initial state while the latter lists the
|
||||
/// successor states of any state.
|
||||
///
|
||||
/// Note that although this is a transition-based automata, we never
|
||||
/// represent transitions in the API! Transition data are
|
||||
/// obtained by querying the iterator over the successors of a
|
||||
/// state.
|
||||
class SPOT_API twa: public std::enable_shared_from_this<twa>
|
||||
{
|
||||
protected:
|
||||
twa(const bdd_dict_ptr& d);
|
||||
// Any iterator returned via release_iter.
|
||||
mutable twa_succ_iterator* iter_cache_;
|
||||
bdd_dict_ptr dict_;
|
||||
public:
|
||||
|
||||
#ifndef SWIG
|
||||
class succ_iterable
|
||||
{
|
||||
protected:
|
||||
const twa* aut_;
|
||||
twa_succ_iterator* it_;
|
||||
public:
|
||||
succ_iterable(const twa* aut, twa_succ_iterator* it)
|
||||
: aut_(aut), it_(it)
|
||||
{
|
||||
}
|
||||
|
||||
succ_iterable(succ_iterable&& other)
|
||||
: aut_(other.aut_), it_(other.it_)
|
||||
{
|
||||
other.it_ = nullptr;
|
||||
}
|
||||
|
||||
~succ_iterable()
|
||||
{
|
||||
if (it_)
|
||||
aut_->release_iter(it_);
|
||||
}
|
||||
|
||||
internal::succ_iterator begin()
|
||||
{
|
||||
return it_->first() ? it_ : nullptr;
|
||||
}
|
||||
|
||||
internal::succ_iterator end()
|
||||
{
|
||||
return nullptr;
|
||||
}
|
||||
};
|
||||
#endif
|
||||
|
||||
virtual ~twa();
|
||||
|
||||
/// \brief Get the initial state of the automaton.
|
||||
///
|
||||
/// The state has been allocated with \c new. It is the
|
||||
/// responsability of the caller to \c destroy it when no
|
||||
/// longer needed.
|
||||
virtual state* get_init_state() const = 0;
|
||||
|
||||
/// \brief Get an iterator over the successors of \a local_state.
|
||||
///
|
||||
/// The iterator has been allocated with \c new. It is the
|
||||
/// responsability of the caller to \c delete it when no
|
||||
/// longer needed.
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* local_state) const = 0;
|
||||
|
||||
#ifndef SWIG
|
||||
/// \brief Build an iterable over the successors of \a s.
|
||||
///
|
||||
/// This is meant to be used as
|
||||
/// <code>for (auto i: aut->succ(s)) { /* i->current_state() */ }</code>.
|
||||
succ_iterable
|
||||
succ(const state* s) const
|
||||
{
|
||||
return {this, succ_iter(s)};
|
||||
}
|
||||
#endif
|
||||
|
||||
/// \brief Release an iterator after usage.
|
||||
///
|
||||
/// This iterator can then be reused by succ_iter() to avoid
|
||||
/// memory allocation.
|
||||
void release_iter(twa_succ_iterator* i) const
|
||||
{
|
||||
if (iter_cache_)
|
||||
delete i;
|
||||
else
|
||||
iter_cache_ = i;
|
||||
}
|
||||
|
||||
/// \brief Get a formula that must hold whatever successor is taken.
|
||||
///
|
||||
/// \return A formula which must be verified for all successors
|
||||
/// of \a state.
|
||||
///
|
||||
/// This can be as simple as \c bddtrue, or more completely
|
||||
/// the disjunction of the condition of all successors. This
|
||||
/// is used as an hint by \c succ_iter() to reduce the number
|
||||
/// of successor to compute in a product.
|
||||
///
|
||||
/// Sub classes should implement compute_support_conditions(),
|
||||
/// this function is just a wrapper that will cache the
|
||||
/// last return value for efficiency.
|
||||
bdd support_conditions(const state* state) const;
|
||||
|
||||
/// \brief Get the dictionary associated to the automaton.
|
||||
///
|
||||
/// Atomic propositions and acceptance conditions are represented
|
||||
/// as BDDs. The dictionary allows to map BDD variables back to
|
||||
/// formulae, and vice versa. This is useful when dealing with
|
||||
/// several automata (which may use the same BDD variable for
|
||||
/// different formula), or simply when printing.
|
||||
bdd_dict_ptr get_dict() const
|
||||
{
|
||||
return dict_;
|
||||
}
|
||||
|
||||
/// \brief Format the state as a string for printing.
|
||||
///
|
||||
/// This formating is the responsability of the automata
|
||||
/// that owns the state.
|
||||
virtual std::string format_state(const state* state) const = 0;
|
||||
|
||||
/// \brief Return a possible annotation for the transition
|
||||
/// pointed to by the iterator.
|
||||
///
|
||||
/// You may decide to use annotations when building a tgba class
|
||||
/// that represents the state space of a model, for instance to
|
||||
/// indicate how the tgba transitions relate to the original model
|
||||
/// (e.g. the annotation could be the name of a PetriNet
|
||||
/// transition, or the line number of some textual formalism).
|
||||
///
|
||||
/// Implementing this method is optional; the default annotation
|
||||
/// is the empty string.
|
||||
///
|
||||
/// This method is used for instance in dotty_reachable(),
|
||||
/// and replay_tgba_run().
|
||||
///
|
||||
/// \param t a non-done twa_succ_iterator for this automaton
|
||||
virtual std::string
|
||||
transition_annotation(const twa_succ_iterator* t) const;
|
||||
|
||||
/// \brief Project a state on an automaton.
|
||||
///
|
||||
/// This converts \a s, into that corresponding spot::state for \a
|
||||
/// t. This is useful when you have the state of a product, and
|
||||
/// want restrict this state to a specific automata occuring in
|
||||
/// the product.
|
||||
///
|
||||
/// It goes without saying that \a s and \a t should be compatible
|
||||
/// (i.e., \a s is a state of \a t).
|
||||
///
|
||||
/// \return 0 if the projection fails (\a s is unrelated to \a t),
|
||||
/// or a new \c state* (the projected state) that must be
|
||||
/// destroyed by the caller.
|
||||
virtual state* project_state(const state* s,
|
||||
const const_twa_ptr& t) const;
|
||||
|
||||
|
||||
const acc_cond& acc() const
|
||||
{
|
||||
return acc_;
|
||||
}
|
||||
|
||||
acc_cond& acc()
|
||||
{
|
||||
return acc_;
|
||||
}
|
||||
|
||||
virtual bool is_empty() const;
|
||||
|
||||
protected:
|
||||
acc_cond acc_;
|
||||
|
||||
void set_num_sets_(unsigned num)
|
||||
{
|
||||
if (num < acc_.num_sets())
|
||||
{
|
||||
acc_.~acc_cond();
|
||||
new (&acc_) acc_cond;
|
||||
}
|
||||
acc_.add_sets(num - acc_.num_sets());
|
||||
}
|
||||
|
||||
public:
|
||||
const acc_cond::acc_code& get_acceptance() const
|
||||
{
|
||||
return acc_.get_acceptance();
|
||||
}
|
||||
|
||||
void set_acceptance(unsigned num, const acc_cond::acc_code& c)
|
||||
{
|
||||
set_num_sets_(num);
|
||||
acc_.set_acceptance(c);
|
||||
if (num == 0)
|
||||
prop_state_based_acc();
|
||||
}
|
||||
|
||||
/// \brief Copy the acceptance condition of another tgba.
|
||||
void copy_acceptance_of(const const_twa_ptr& a)
|
||||
{
|
||||
acc_ = a->acc();
|
||||
unsigned num = acc_.num_sets();
|
||||
if (num == 0)
|
||||
prop_state_based_acc();
|
||||
}
|
||||
|
||||
void copy_ap_of(const const_twa_ptr& a)
|
||||
{
|
||||
get_dict()->register_all_propositions_of(a, this);
|
||||
}
|
||||
|
||||
void set_generalized_buchi(unsigned num)
|
||||
{
|
||||
set_num_sets_(num);
|
||||
acc_.set_generalized_buchi();
|
||||
if (num == 0)
|
||||
prop_state_based_acc();
|
||||
}
|
||||
|
||||
acc_cond::mark_t set_buchi()
|
||||
{
|
||||
set_generalized_buchi(1);
|
||||
return acc_.mark(0);
|
||||
}
|
||||
|
||||
protected:
|
||||
/// Do the actual computation of tgba::support_conditions().
|
||||
virtual bdd compute_support_conditions(const state* state) const = 0;
|
||||
mutable const state* last_support_conditions_input_;
|
||||
private:
|
||||
mutable bdd last_support_conditions_output_;
|
||||
|
||||
protected:
|
||||
|
||||
// Boolean properties. Beware: true means that the property
|
||||
// holds, but false means the property is unknown.
|
||||
struct bprop
|
||||
{
|
||||
bool state_based_acc:1; // State-based acceptance.
|
||||
bool inherently_weak:1; // Weak automaton.
|
||||
bool deterministic:1; // Deterministic automaton.
|
||||
bool stutter_inv:1; // Stutter invariant
|
||||
};
|
||||
union
|
||||
{
|
||||
unsigned props;
|
||||
bprop is;
|
||||
};
|
||||
|
||||
#ifndef SWIG
|
||||
// Dynamic properties, are given with a name and a destructor function.
|
||||
std::unordered_map<std::string,
|
||||
std::pair<void*,
|
||||
std::function<void(void*)>>> named_prop_;
|
||||
#endif
|
||||
void* get_named_prop_(std::string s) const;
|
||||
|
||||
public:
|
||||
|
||||
#ifndef SWIG
|
||||
void set_named_prop(std::string s,
|
||||
void* val, std::function<void(void*)> destructor);
|
||||
|
||||
template<typename T>
|
||||
void set_named_prop(std::string s, T* val)
|
||||
{
|
||||
set_named_prop(s, val, [](void *p) { delete static_cast<T*>(p); });
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
T* get_named_prop(std::string s) const
|
||||
{
|
||||
void* p = get_named_prop_(s);
|
||||
if (!p)
|
||||
return nullptr;
|
||||
return static_cast<T*>(p);
|
||||
}
|
||||
#endif
|
||||
|
||||
void release_named_properties()
|
||||
{
|
||||
// Destroy all named properties.
|
||||
for (auto& np: named_prop_)
|
||||
np.second.second(np.second.first);
|
||||
named_prop_.clear();
|
||||
}
|
||||
|
||||
bool has_state_based_acc() const
|
||||
{
|
||||
return is.state_based_acc;
|
||||
}
|
||||
|
||||
void prop_state_based_acc(bool val = true)
|
||||
{
|
||||
is.state_based_acc = val;
|
||||
}
|
||||
|
||||
bool is_sba() const
|
||||
{
|
||||
return has_state_based_acc() && acc().is_buchi();
|
||||
}
|
||||
|
||||
bool is_inherently_weak() const
|
||||
{
|
||||
return is.inherently_weak;
|
||||
}
|
||||
|
||||
void prop_inherently_weak(bool val = true)
|
||||
{
|
||||
is.inherently_weak = val;
|
||||
}
|
||||
|
||||
bool is_deterministic() const
|
||||
{
|
||||
return is.deterministic;
|
||||
}
|
||||
|
||||
void prop_deterministic(bool val = true)
|
||||
{
|
||||
is.deterministic = val;
|
||||
}
|
||||
|
||||
bool is_stutter_invariant() const
|
||||
{
|
||||
return is.stutter_inv;
|
||||
}
|
||||
|
||||
void prop_stutter_invariant(bool val = true)
|
||||
{
|
||||
is.stutter_inv = val;
|
||||
}
|
||||
|
||||
struct prop_set
|
||||
{
|
||||
bool state_based;
|
||||
bool inherently_weak;
|
||||
bool deterministic;
|
||||
bool stutter_inv;
|
||||
|
||||
static prop_set all()
|
||||
{
|
||||
return { true, true, true, true };
|
||||
}
|
||||
};
|
||||
|
||||
// There is no default value here on purpose. This way any time we
|
||||
// add a new property we have to update every call to prop_copy().
|
||||
void prop_copy(const const_twa_ptr& other, prop_set p)
|
||||
{
|
||||
if (p.state_based)
|
||||
prop_state_based_acc(other->has_state_based_acc());
|
||||
if (p.inherently_weak)
|
||||
prop_inherently_weak(other->is_inherently_weak());
|
||||
if (p.deterministic)
|
||||
prop_deterministic(other->is_deterministic());
|
||||
if (p.stutter_inv)
|
||||
prop_stutter_invariant(other->is_stutter_invariant());
|
||||
}
|
||||
|
||||
void prop_keep(prop_set p)
|
||||
{
|
||||
if (!p.state_based)
|
||||
prop_state_based_acc(false);
|
||||
if (!p.inherently_weak)
|
||||
prop_inherently_weak(false);
|
||||
if (!p.deterministic)
|
||||
prop_deterministic(false);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
/// \addtogroup twa_representation TGBA representations
|
||||
/// \ingroup twa
|
||||
|
||||
/// \addtogroup twa_algorithms TGBA algorithms
|
||||
/// \ingroup twa
|
||||
|
||||
/// \addtogroup twa_on_the_fly_algorithms TGBA on-the-fly algorithms
|
||||
/// \ingroup twa_algorithms
|
||||
|
||||
/// \addtogroup twa_io Input/Output of TGBA
|
||||
/// \ingroup twa_algorithms
|
||||
|
||||
/// \addtogroup twa_ltl Translating LTL formulae into TGBA
|
||||
/// \ingroup twa_algorithms
|
||||
|
||||
/// \addtogroup twa_generic Algorithm patterns
|
||||
/// \ingroup twa_algorithms
|
||||
|
||||
/// \addtogroup twa_reduction TGBA simplifications
|
||||
/// \ingroup twa_algorithms
|
||||
|
||||
/// \addtogroup twa_misc Miscellaneous algorithms on TGBA
|
||||
/// \ingroup twa_algorithms
|
||||
}
|
||||
251
src/twa/twagraph.cc
Normal file
251
src/twa/twagraph.cc
Normal file
|
|
@ -0,0 +1,251 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
//
|
||||
// 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 "twagraph.hh"
|
||||
#include "ltlast/constant.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
void twa_graph::merge_transitions()
|
||||
{
|
||||
g_.remove_dead_transitions_();
|
||||
|
||||
typedef graph_t::trans_storage_t tr_t;
|
||||
g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
|
||||
{
|
||||
if (lhs.src < rhs.src)
|
||||
return true;
|
||||
if (lhs.src > rhs.src)
|
||||
return false;
|
||||
if (lhs.dst < rhs.dst)
|
||||
return true;
|
||||
if (lhs.dst > rhs.dst)
|
||||
return false;
|
||||
return lhs.acc < rhs.acc;
|
||||
// Do not sort on conditions, we'll merge
|
||||
// them.
|
||||
});
|
||||
|
||||
auto& trans = this->transition_vector();
|
||||
unsigned tend = trans.size();
|
||||
unsigned out = 0;
|
||||
unsigned in = 1;
|
||||
// Skip any leading false transition.
|
||||
while (in < tend && trans[in].cond == bddfalse)
|
||||
++in;
|
||||
if (in < tend)
|
||||
{
|
||||
++out;
|
||||
if (out != in)
|
||||
trans[out] = trans[in];
|
||||
for (++in; in < tend; ++in)
|
||||
{
|
||||
if (trans[in].cond == bddfalse) // Unusable transition
|
||||
continue;
|
||||
// Merge transitions with the same source, destination, and
|
||||
// acceptance. (We test the source last, because this is the
|
||||
// most likely test to be true as transitions are ordered by
|
||||
// sources and then destinations.)
|
||||
if (trans[out].dst == trans[in].dst
|
||||
&& trans[out].acc == trans[in].acc
|
||||
&& trans[out].src == trans[in].src)
|
||||
{
|
||||
trans[out].cond |= trans[in].cond;
|
||||
}
|
||||
else
|
||||
{
|
||||
++out;
|
||||
if (in != out)
|
||||
trans[out] = trans[in];
|
||||
}
|
||||
}
|
||||
}
|
||||
if (++out != tend)
|
||||
trans.resize(out);
|
||||
|
||||
tend = out;
|
||||
out = in = 2;
|
||||
|
||||
// FIXME: We could should also merge transitions when using
|
||||
// fin_acceptance, but the rule for Fin sets are different than
|
||||
// those for Inf sets, (and we need to be careful if a set is used
|
||||
// both as Inf and Fin)
|
||||
if ((in < tend) && !acc().uses_fin_acceptance())
|
||||
{
|
||||
typedef graph_t::trans_storage_t tr_t;
|
||||
g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
|
||||
{
|
||||
if (lhs.src < rhs.src)
|
||||
return true;
|
||||
if (lhs.src > rhs.src)
|
||||
return false;
|
||||
if (lhs.dst < rhs.dst)
|
||||
return true;
|
||||
if (lhs.dst > rhs.dst)
|
||||
return false;
|
||||
return lhs.cond.id() < rhs.cond.id();
|
||||
// Do not sort on acceptance, we'll merge
|
||||
// them.
|
||||
});
|
||||
|
||||
for (; in < tend; ++in)
|
||||
{
|
||||
// Merge transitions with the same source, destination,
|
||||
// and conditions. (We test the source last, for the
|
||||
// same reason as above.)
|
||||
if (trans[out].dst == trans[in].dst
|
||||
&& trans[out].cond.id() == trans[in].cond.id()
|
||||
&& trans[out].src == trans[in].src)
|
||||
{
|
||||
trans[out].acc |= trans[in].acc;
|
||||
}
|
||||
else
|
||||
{
|
||||
++out;
|
||||
if (in != out)
|
||||
trans[out] = trans[in];
|
||||
}
|
||||
}
|
||||
if (++out != tend)
|
||||
trans.resize(out);
|
||||
}
|
||||
|
||||
g_.chain_transitions_();
|
||||
}
|
||||
|
||||
void twa_graph::purge_unreachable_states()
|
||||
{
|
||||
unsigned num_states = g_.num_states();
|
||||
if (SPOT_UNLIKELY(num_states == 0))
|
||||
return;
|
||||
// The TODO vector serves two purposes:
|
||||
// - it is a stack of state to process,
|
||||
// - it is a set of processed states.
|
||||
// The lower 31 bits of each entry is a state on the stack. (The
|
||||
// next usable entry on the stack is indicated by todo_pos.) The
|
||||
// 32th bit (i.e., the sign bit) of todo[x] indicates whether
|
||||
// states number x has been seen.
|
||||
std::vector<unsigned> todo(num_states, 0);
|
||||
const unsigned seen = 1 << (sizeof(unsigned)*8-1);
|
||||
const unsigned mask = seen - 1;
|
||||
todo[0] = init_number_;
|
||||
todo[init_number_] |= seen;
|
||||
unsigned todo_pos = 1;
|
||||
do
|
||||
{
|
||||
unsigned cur = todo[--todo_pos] & mask;
|
||||
todo[todo_pos] ^= cur; // Zero the state
|
||||
for (auto& t: g_.out(cur))
|
||||
if (!(todo[t.dst] & seen))
|
||||
{
|
||||
todo[t.dst] |= seen;
|
||||
todo[todo_pos++] |= t.dst;
|
||||
}
|
||||
}
|
||||
while (todo_pos > 0);
|
||||
// Now renumber each used state.
|
||||
unsigned current = 0;
|
||||
for (auto& v: todo)
|
||||
if (!(v & seen))
|
||||
v = -1U;
|
||||
else
|
||||
v = current++;
|
||||
if (current == todo.size())
|
||||
return; // No unreachable state.
|
||||
init_number_ = todo[init_number_];
|
||||
g_.defrag_states(std::move(todo), current);
|
||||
}
|
||||
|
||||
void twa_graph::purge_dead_states()
|
||||
{
|
||||
unsigned num_states = g_.num_states();
|
||||
if (num_states == 0)
|
||||
return;
|
||||
|
||||
std::vector<unsigned> useful(num_states, 0);
|
||||
|
||||
// Make a DFS to compute a topological order.
|
||||
std::vector<unsigned> order;
|
||||
order.reserve(num_states);
|
||||
std::vector<std::pair<unsigned, unsigned>> todo; // state, trans
|
||||
useful[init_number_] = 1;
|
||||
todo.emplace_back(init_number_, g_.state_storage(init_number_).succ);
|
||||
do
|
||||
{
|
||||
unsigned src;
|
||||
unsigned tid;
|
||||
std::tie(src, tid) = todo.back();
|
||||
if (tid == 0U)
|
||||
{
|
||||
todo.pop_back();
|
||||
order.push_back(src);
|
||||
continue;
|
||||
}
|
||||
auto& t = g_.trans_storage(tid);
|
||||
todo.back().second = t.next_succ;
|
||||
unsigned dst = t.dst;
|
||||
if (useful[dst] != 1)
|
||||
{
|
||||
todo.emplace_back(dst, g_.state_storage(dst).succ);
|
||||
useful[dst] = 1;
|
||||
}
|
||||
}
|
||||
while (!todo.empty());
|
||||
|
||||
// Process states in topological order
|
||||
for (auto s: order)
|
||||
{
|
||||
auto t = g_.out_iteraser(s);
|
||||
bool useless = true;
|
||||
while (t)
|
||||
{
|
||||
// Erase any transition to a useless state.
|
||||
if (!useful[t->dst])
|
||||
{
|
||||
t.erase();
|
||||
continue;
|
||||
}
|
||||
// if we have a transition to a useful state, then the
|
||||
// state is useful.
|
||||
useless = false;
|
||||
++t;
|
||||
}
|
||||
if (useless)
|
||||
useful[s] = 0;
|
||||
}
|
||||
|
||||
// Make sure the initial state is useful (even if it has been
|
||||
// marked as useless by the previous loop because it has no
|
||||
// successor).
|
||||
useful[init_number_] = 1;
|
||||
|
||||
// Now renumber each used state.
|
||||
unsigned current = 0;
|
||||
for (unsigned s = 0; s < num_states; ++s)
|
||||
if (useful[s])
|
||||
useful[s] = current++;
|
||||
else
|
||||
useful[s] = -1U;
|
||||
if (current == num_states)
|
||||
return; // No useless state.
|
||||
init_number_ = useful[init_number_];
|
||||
g_.defrag_states(std::move(useful), current);
|
||||
}
|
||||
}
|
||||
482
src/twa/twagraph.hh
Normal file
482
src/twa/twagraph.hh
Normal file
|
|
@ -0,0 +1,482 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||
// de l'Epita.
|
||||
//
|
||||
// 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "fwd.hh"
|
||||
#include "graph/graph.hh"
|
||||
#include "graph/ngraph.hh"
|
||||
#include "twa/bdddict.hh"
|
||||
#include "twa/twa.hh"
|
||||
#include "tgbaalgos/dupexp.hh"
|
||||
#include <sstream>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
struct SPOT_API twa_graph_state: public spot::state
|
||||
{
|
||||
public:
|
||||
twa_graph_state():
|
||||
spot::state()
|
||||
{
|
||||
}
|
||||
|
||||
virtual ~twa_graph_state() noexcept
|
||||
{
|
||||
}
|
||||
|
||||
virtual int compare(const spot::state* other) const
|
||||
{
|
||||
auto o = down_cast<const twa_graph_state*>(other);
|
||||
assert(o);
|
||||
|
||||
// Do not simply return "other - this", it might not fit in an int.
|
||||
if (o < this)
|
||||
return -1;
|
||||
if (o > this)
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
|
||||
virtual size_t hash() const
|
||||
{
|
||||
return
|
||||
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
|
||||
}
|
||||
|
||||
virtual twa_graph_state*
|
||||
clone() const
|
||||
{
|
||||
return const_cast<twa_graph_state*>(this);
|
||||
}
|
||||
|
||||
virtual void destroy() const
|
||||
{
|
||||
}
|
||||
};
|
||||
|
||||
struct SPOT_API twa_graph_trans_data
|
||||
{
|
||||
bdd cond;
|
||||
acc_cond::mark_t acc;
|
||||
|
||||
explicit twa_graph_trans_data()
|
||||
: cond(bddfalse), acc(0)
|
||||
{
|
||||
}
|
||||
|
||||
twa_graph_trans_data(bdd cond, acc_cond::mark_t acc = 0U)
|
||||
: cond(cond), acc(acc)
|
||||
{
|
||||
}
|
||||
|
||||
bool operator<(const twa_graph_trans_data& other) const
|
||||
{
|
||||
if (cond.id() < other.cond.id())
|
||||
return true;
|
||||
if (cond.id() > other.cond.id())
|
||||
return false;
|
||||
return acc < other.acc;
|
||||
}
|
||||
|
||||
bool operator==(const twa_graph_trans_data& other) const
|
||||
{
|
||||
return cond.id() == other.cond.id() &&
|
||||
acc == other.acc;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
template<class Graph>
|
||||
class SPOT_API twa_graph_succ_iterator final:
|
||||
public twa_succ_iterator
|
||||
{
|
||||
private:
|
||||
typedef typename Graph::transition transition;
|
||||
typedef typename Graph::state_data_t state;
|
||||
const Graph* g_;
|
||||
transition t_;
|
||||
transition p_;
|
||||
|
||||
public:
|
||||
twa_graph_succ_iterator(const Graph* g, transition t)
|
||||
: g_(g), t_(t)
|
||||
{
|
||||
}
|
||||
|
||||
virtual void recycle(transition t)
|
||||
{
|
||||
t_ = t;
|
||||
}
|
||||
|
||||
virtual bool first()
|
||||
{
|
||||
p_ = t_;
|
||||
return p_;
|
||||
}
|
||||
|
||||
virtual bool next()
|
||||
{
|
||||
p_ = g_->trans_storage(p_).next_succ;
|
||||
return p_;
|
||||
}
|
||||
|
||||
virtual bool done() const
|
||||
{
|
||||
return !p_;
|
||||
}
|
||||
|
||||
virtual twa_graph_state* current_state() const
|
||||
{
|
||||
assert(!done());
|
||||
return const_cast<twa_graph_state*>
|
||||
(&g_->state_data(g_->trans_storage(p_).dst));
|
||||
}
|
||||
|
||||
virtual bdd current_condition() const
|
||||
{
|
||||
assert(!done());
|
||||
return g_->trans_data(p_).cond;
|
||||
}
|
||||
|
||||
virtual acc_cond::mark_t current_acceptance_conditions() const
|
||||
{
|
||||
assert(!done());
|
||||
return g_->trans_data(p_).acc;
|
||||
}
|
||||
|
||||
transition pos() const
|
||||
{
|
||||
return p_;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
class SPOT_API twa_graph final: public twa
|
||||
{
|
||||
public:
|
||||
typedef digraph<twa_graph_state, twa_graph_trans_data> graph_t;
|
||||
typedef graph_t::trans_storage_t trans_storage_t;
|
||||
|
||||
protected:
|
||||
graph_t g_;
|
||||
mutable unsigned init_number_;
|
||||
|
||||
public:
|
||||
twa_graph(const bdd_dict_ptr& dict)
|
||||
: twa(dict),
|
||||
init_number_(0)
|
||||
{
|
||||
}
|
||||
|
||||
explicit twa_graph(const const_twa_graph_ptr& other, prop_set p)
|
||||
: twa(other->get_dict()),
|
||||
g_(other->g_), init_number_(other->init_number_)
|
||||
{
|
||||
copy_acceptance_of(other);
|
||||
copy_ap_of(other);
|
||||
prop_copy(other, p);
|
||||
}
|
||||
|
||||
virtual ~twa_graph()
|
||||
{
|
||||
get_dict()->unregister_all_my_variables(this);
|
||||
// Prevent this state from being destroyed by ~twa(),
|
||||
// as the state will be destroyed when g_ is destroyed.
|
||||
last_support_conditions_input_ = 0;
|
||||
}
|
||||
|
||||
// FIXME: Once we ditch GCC 4.6, we can using a template aliases
|
||||
// (supported from GCC 4.7 onward) instead of this.
|
||||
template <typename State_Name,
|
||||
typename Name_Hash = std::hash<State_Name>,
|
||||
typename Name_Equal = std::equal_to<State_Name>>
|
||||
struct namer
|
||||
{
|
||||
typedef named_graph<graph_t, State_Name, Name_Hash, Name_Equal> type;
|
||||
};
|
||||
|
||||
template <typename State_Name,
|
||||
typename Name_Hash = std::hash<State_Name>,
|
||||
typename Name_Equal = std::equal_to<State_Name>>
|
||||
typename namer<State_Name, Name_Hash, Name_Equal>::type*
|
||||
create_namer()
|
||||
{
|
||||
return new named_graph<graph_t, State_Name, Name_Hash, Name_Equal>(g_);
|
||||
}
|
||||
|
||||
graph_t& get_graph()
|
||||
{
|
||||
return g_;
|
||||
}
|
||||
|
||||
const graph_t& get_graph() const
|
||||
{
|
||||
return g_;
|
||||
}
|
||||
|
||||
unsigned num_states() const
|
||||
{
|
||||
return g_.num_states();
|
||||
}
|
||||
|
||||
unsigned num_transitions() const
|
||||
{
|
||||
return g_.num_transitions();
|
||||
}
|
||||
|
||||
void set_init_state(graph_t::state s)
|
||||
{
|
||||
assert(s < num_states());
|
||||
init_number_ = s;
|
||||
}
|
||||
|
||||
void set_init_state(const state* s)
|
||||
{
|
||||
set_init_state(state_number(s));
|
||||
}
|
||||
|
||||
graph_t::state get_init_state_number() const
|
||||
{
|
||||
if (num_states() == 0)
|
||||
const_cast<graph_t&>(g_).new_state();
|
||||
return init_number_;
|
||||
}
|
||||
|
||||
// FIXME: The return type ought to be const.
|
||||
virtual twa_graph_state* get_init_state() const
|
||||
{
|
||||
if (num_states() == 0)
|
||||
const_cast<graph_t&>(g_).new_state();
|
||||
return const_cast<twa_graph_state*>(state_from_number(init_number_));
|
||||
}
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* st) const
|
||||
{
|
||||
auto s = down_cast<const typename graph_t::state_storage_t*>(st);
|
||||
assert(s);
|
||||
assert(!s->succ || g_.valid_trans(s->succ));
|
||||
|
||||
if (this->iter_cache_)
|
||||
{
|
||||
auto it =
|
||||
down_cast<twa_graph_succ_iterator<graph_t>*>(this->iter_cache_);
|
||||
it->recycle(s->succ);
|
||||
this->iter_cache_ = nullptr;
|
||||
return it;
|
||||
}
|
||||
return new twa_graph_succ_iterator<graph_t>(&g_, s->succ);
|
||||
}
|
||||
|
||||
graph_t::state
|
||||
state_number(const state* st) const
|
||||
{
|
||||
auto s = down_cast<const typename graph_t::state_storage_t*>(st);
|
||||
assert(s);
|
||||
return s - &g_.state_storage(0);
|
||||
}
|
||||
|
||||
const twa_graph_state*
|
||||
state_from_number(graph_t::state n) const
|
||||
{
|
||||
return &g_.state_data(n);
|
||||
}
|
||||
|
||||
std::string format_state(unsigned n) const
|
||||
{
|
||||
std::stringstream ss;
|
||||
ss << n;
|
||||
return ss.str();
|
||||
}
|
||||
|
||||
virtual std::string format_state(const state* st) const
|
||||
{
|
||||
return format_state(state_number(st));
|
||||
}
|
||||
|
||||
twa_graph_trans_data& trans_data(const twa_succ_iterator* it)
|
||||
{
|
||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||
return g_.trans_data(i->pos());
|
||||
}
|
||||
|
||||
twa_graph_trans_data& trans_data(unsigned t)
|
||||
{
|
||||
return g_.trans_data(t);
|
||||
}
|
||||
|
||||
const twa_graph_trans_data& trans_data(const twa_succ_iterator* it) const
|
||||
{
|
||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||
return g_.trans_data(i->pos());
|
||||
}
|
||||
|
||||
const twa_graph_trans_data& trans_data(unsigned t) const
|
||||
{
|
||||
return g_.trans_data(t);
|
||||
}
|
||||
|
||||
trans_storage_t& trans_storage(const twa_succ_iterator* it)
|
||||
{
|
||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||
return g_.trans_storage(i->pos());
|
||||
}
|
||||
|
||||
trans_storage_t& trans_storage(unsigned t)
|
||||
{
|
||||
return g_.trans_storage(t);
|
||||
}
|
||||
|
||||
const trans_storage_t
|
||||
trans_storage(const twa_succ_iterator* it) const
|
||||
{
|
||||
auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
|
||||
return g_.trans_storage(i->pos());
|
||||
}
|
||||
|
||||
const trans_storage_t trans_storage(unsigned t) const
|
||||
{
|
||||
return g_.trans_storage(t);
|
||||
}
|
||||
|
||||
unsigned new_state()
|
||||
{
|
||||
return g_.new_state();
|
||||
}
|
||||
|
||||
unsigned new_states(unsigned n)
|
||||
{
|
||||
return g_.new_states(n);
|
||||
}
|
||||
|
||||
unsigned new_transition(unsigned src, unsigned dst,
|
||||
bdd cond, acc_cond::mark_t acc = 0U)
|
||||
{
|
||||
return g_.new_transition(src, dst, cond, acc);
|
||||
}
|
||||
|
||||
unsigned new_acc_transition(unsigned src, unsigned dst,
|
||||
bdd cond, bool acc = true)
|
||||
{
|
||||
if (acc)
|
||||
return g_.new_transition(src, dst, cond, acc_.all_sets());
|
||||
else
|
||||
return g_.new_transition(src, dst, cond);
|
||||
}
|
||||
|
||||
#ifndef SWIG
|
||||
auto out(unsigned src) const
|
||||
SPOT_RETURN(g_.out(src));
|
||||
auto out(unsigned src)
|
||||
SPOT_RETURN(g_.out(src));
|
||||
|
||||
auto states() const
|
||||
SPOT_RETURN(g_.states());
|
||||
auto states()
|
||||
SPOT_RETURN(g_.states());
|
||||
|
||||
auto transitions() const
|
||||
SPOT_RETURN(g_.transitions());
|
||||
auto transitions()
|
||||
SPOT_RETURN(g_.transitions());
|
||||
|
||||
auto transition_vector() const
|
||||
SPOT_RETURN(g_.transition_vector());
|
||||
auto transition_vector()
|
||||
SPOT_RETURN(g_.transition_vector());
|
||||
|
||||
auto is_dead_transition(const graph_t::trans_storage_t& t) const
|
||||
SPOT_RETURN(g_.is_dead_transition(t));
|
||||
#endif
|
||||
|
||||
virtual bdd compute_support_conditions(const state* s) const
|
||||
{
|
||||
bdd sum = bddfalse;
|
||||
for (auto& t: out(state_number(s)))
|
||||
sum |= t.cond;
|
||||
return sum;
|
||||
}
|
||||
|
||||
/// Iterate over all transitions, and merge those with compatible
|
||||
/// extremities and acceptance.
|
||||
void merge_transitions();
|
||||
|
||||
/// Remove all states without successors.
|
||||
void purge_dead_states();
|
||||
|
||||
/// Remove all unreachable states.
|
||||
void purge_unreachable_states();
|
||||
|
||||
bool state_is_accepting(unsigned s) const
|
||||
{
|
||||
assert(has_state_based_acc() || acc_.num_sets() == 0);
|
||||
for (auto& t: g_.out(s))
|
||||
// Stop at the first transition, since the remaining should be
|
||||
// labeled identically.
|
||||
return acc_.accepting(t.acc);
|
||||
return false;
|
||||
}
|
||||
|
||||
bool state_is_accepting(const state* s) const
|
||||
{
|
||||
return state_is_accepting(state_number(s));
|
||||
}
|
||||
|
||||
bool operator==(const twa_graph& aut) const
|
||||
{
|
||||
if (num_states() != aut.num_states() ||
|
||||
num_transitions() != aut.num_transitions() ||
|
||||
acc().num_sets() != aut.acc().num_sets())
|
||||
return false;
|
||||
auto& trans1 = transition_vector();
|
||||
auto& trans2 = aut.transition_vector();
|
||||
return std::equal(trans1.begin() + 1, trans1.end(),
|
||||
trans2.begin() + 1);
|
||||
}
|
||||
};
|
||||
|
||||
inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict)
|
||||
{
|
||||
return std::make_shared<twa_graph>(dict);
|
||||
}
|
||||
|
||||
inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut,
|
||||
twa::prop_set p)
|
||||
{
|
||||
return std::make_shared<twa_graph>(aut, p);
|
||||
}
|
||||
|
||||
inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut,
|
||||
twa::prop_set p)
|
||||
{
|
||||
return std::make_shared<twa_graph>(aut, p);
|
||||
}
|
||||
|
||||
inline twa_graph_ptr make_twa_graph(const const_twa_ptr& aut,
|
||||
twa::prop_set p)
|
||||
{
|
||||
auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
|
||||
if (a)
|
||||
return std::make_shared<twa_graph>(a, p);
|
||||
else
|
||||
return tgba_dupexp_dfs(aut, p);
|
||||
}
|
||||
}
|
||||
231
src/twa/twamask.cc
Normal file
231
src/twa/twamask.cc
Normal file
|
|
@ -0,0 +1,231 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 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/>.
|
||||
|
||||
#include "twamask.hh"
|
||||
#include <vector>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
struct transition
|
||||
{
|
||||
const state* dest;
|
||||
bdd cond;
|
||||
acc_cond::mark_t acc;
|
||||
};
|
||||
typedef std::vector<transition> transitions;
|
||||
|
||||
struct succ_iter_filtered: public twa_succ_iterator
|
||||
{
|
||||
~succ_iter_filtered()
|
||||
{
|
||||
for (auto& t: trans_)
|
||||
t.dest->destroy();
|
||||
}
|
||||
|
||||
bool first()
|
||||
{
|
||||
it_ = trans_.begin();
|
||||
return it_ != trans_.end();
|
||||
}
|
||||
|
||||
bool next()
|
||||
{
|
||||
++it_;
|
||||
return it_ != trans_.end();
|
||||
}
|
||||
|
||||
bool done() const
|
||||
{
|
||||
return it_ == trans_.end();
|
||||
}
|
||||
|
||||
state* current_state() const
|
||||
{
|
||||
return it_->dest->clone();
|
||||
}
|
||||
|
||||
bdd current_condition() const
|
||||
{
|
||||
return it_->cond;
|
||||
}
|
||||
|
||||
acc_cond::mark_t current_acceptance_conditions() const
|
||||
{
|
||||
return it_->acc;
|
||||
}
|
||||
|
||||
transitions trans_;
|
||||
transitions::const_iterator it_;
|
||||
};
|
||||
|
||||
/// \ingroup twa_on_the_fly_algorithms
|
||||
/// \brief A masked TGBA (abstract).
|
||||
///
|
||||
/// Ignores some states from a TGBA. What state are preserved or
|
||||
/// ignored is controlled by the wanted() method.
|
||||
///
|
||||
/// This is an abstract class. You should inherit from it and
|
||||
/// supply a wanted() method to specify which states to keep.
|
||||
class twa_mask: public twa_proxy
|
||||
{
|
||||
protected:
|
||||
/// \brief Constructor.
|
||||
/// \param masked The automaton to mask
|
||||
/// \param init Any state to use as initial state. This state will be
|
||||
/// destroyed by the destructor.
|
||||
twa_mask(const const_twa_ptr& masked, const state* init = 0):
|
||||
twa_proxy(masked),
|
||||
init_(init)
|
||||
{
|
||||
if (!init)
|
||||
init_ = masked->get_init_state();
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
virtual ~twa_mask()
|
||||
{
|
||||
init_->destroy();
|
||||
}
|
||||
|
||||
virtual state* get_init_state() const
|
||||
{
|
||||
return init_->clone();
|
||||
}
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* local_state) const
|
||||
{
|
||||
succ_iter_filtered* res;
|
||||
if (iter_cache_)
|
||||
{
|
||||
res = down_cast<succ_iter_filtered*>(iter_cache_);
|
||||
res->trans_.clear();
|
||||
iter_cache_ = nullptr;
|
||||
}
|
||||
else
|
||||
{
|
||||
res = new succ_iter_filtered;
|
||||
}
|
||||
for (auto it: original_->succ(local_state))
|
||||
{
|
||||
const spot::state* s = it->current_state();
|
||||
auto acc = it->current_acceptance_conditions();
|
||||
if (!wanted(s, acc))
|
||||
{
|
||||
s->destroy();
|
||||
continue;
|
||||
}
|
||||
res->trans_.emplace_back
|
||||
(transition {s, it->current_condition(), acc});
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
virtual bool wanted(const state* s, acc_cond::mark_t acc) const = 0;
|
||||
|
||||
protected:
|
||||
const state* init_;
|
||||
};
|
||||
|
||||
class twa_mask_keep: public twa_mask
|
||||
{
|
||||
const state_set& mask_;
|
||||
public:
|
||||
twa_mask_keep(const const_twa_ptr& masked,
|
||||
const state_set& mask,
|
||||
const state* init)
|
||||
: twa_mask(masked, init),
|
||||
mask_(mask)
|
||||
{
|
||||
}
|
||||
|
||||
bool wanted(const state* s, const acc_cond::mark_t) const
|
||||
{
|
||||
state_set::const_iterator i = mask_.find(s);
|
||||
return i != mask_.end();
|
||||
}
|
||||
};
|
||||
|
||||
class twa_mask_ignore: public twa_mask
|
||||
{
|
||||
const state_set& mask_;
|
||||
public:
|
||||
twa_mask_ignore(const const_twa_ptr& masked,
|
||||
const state_set& mask,
|
||||
const state* init)
|
||||
: twa_mask(masked, init),
|
||||
mask_(mask)
|
||||
{
|
||||
}
|
||||
|
||||
bool wanted(const state* s, const acc_cond::mark_t) const
|
||||
{
|
||||
state_set::const_iterator i = mask_.find(s);
|
||||
return i == mask_.end();
|
||||
}
|
||||
};
|
||||
|
||||
class twa_mask_acc_ignore: public twa_mask
|
||||
{
|
||||
unsigned mask_;
|
||||
public:
|
||||
twa_mask_acc_ignore(const const_twa_ptr& masked,
|
||||
unsigned mask,
|
||||
const state* init)
|
||||
: twa_mask(masked, init),
|
||||
mask_(mask)
|
||||
{
|
||||
}
|
||||
|
||||
bool wanted(const state*, const acc_cond::mark_t acc) const
|
||||
{
|
||||
return !acc.has(mask_);
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
const_twa_ptr
|
||||
build_twa_mask_keep(const const_twa_ptr& to_mask,
|
||||
const state_set& to_keep,
|
||||
const state* init)
|
||||
{
|
||||
return std::make_shared<twa_mask_keep>(to_mask, to_keep, init);
|
||||
}
|
||||
|
||||
const_twa_ptr
|
||||
build_twa_mask_ignore(const const_twa_ptr& to_mask,
|
||||
const state_set& to_ignore,
|
||||
const state* init)
|
||||
{
|
||||
return std::make_shared<twa_mask_ignore>(to_mask, to_ignore, init);
|
||||
}
|
||||
|
||||
const_twa_ptr
|
||||
build_twa_mask_acc_ignore(const const_twa_ptr& to_mask,
|
||||
unsigned to_ignore,
|
||||
const state* init)
|
||||
{
|
||||
return std::make_shared<twa_mask_acc_ignore>(to_mask, to_ignore, init);
|
||||
}
|
||||
|
||||
}
|
||||
66
src/twa/twamask.hh
Normal file
66
src/twa/twamask.hh
Normal file
|
|
@ -0,0 +1,66 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <bddx.h>
|
||||
#include "twaproxy.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
/// \ingroup twa_on_the_fly_algorithms
|
||||
/// \brief Mask a TGBA, keeping a given set of states.
|
||||
///
|
||||
/// Mask the TGBA \a to_mask, keeping only the
|
||||
/// states from \a to_keep. The initial state
|
||||
/// can optionally be reset to \a init.
|
||||
SPOT_API const_twa_ptr
|
||||
build_twa_mask_keep(const const_twa_ptr& to_mask,
|
||||
const state_set& to_keep,
|
||||
const state* init = 0);
|
||||
|
||||
/// \ingroup twa_on_the_fly_algorithms
|
||||
/// \brief Mask a TGBA, rejecting a given set of states.
|
||||
///
|
||||
/// Mask the TGBA \a to_mask, keeping only the states that are not
|
||||
/// in \a to_ignore. The initial state can optionally be reset to
|
||||
/// \a init.
|
||||
SPOT_API const_twa_ptr
|
||||
build_twa_mask_ignore(const const_twa_ptr& to_mask,
|
||||
const state_set& to_ignore,
|
||||
const state* init = 0);
|
||||
|
||||
|
||||
/// \ingroup twa_on_the_fly_algorithms
|
||||
/// \brief Mask a TGBA, rejecting some acceptance set of transitions.
|
||||
///
|
||||
/// This will ignore all transitions that have the TO_IGNORE
|
||||
/// acceptance mark. The initial state can optionally be reset to
|
||||
/// \a init.
|
||||
///
|
||||
/// Note that the acceptance condition of the automaton (i.e. the
|
||||
/// set of all acceptance set) is not changed, because so far this
|
||||
/// function is only needed in graph algorithms that do not call
|
||||
/// all_acceptance_conditions().
|
||||
SPOT_API const_twa_ptr
|
||||
build_twa_mask_acc_ignore(const const_twa_ptr& to_mask,
|
||||
unsigned to_ignore,
|
||||
const state* init = 0);
|
||||
}
|
||||
445
src/twa/twaproduct.cc
Normal file
445
src/twa/twaproduct.cc
Normal file
|
|
@ -0,0 +1,445 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2011, 2012, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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 "twaproduct.hh"
|
||||
#include <string>
|
||||
#include <cassert>
|
||||
#include "misc/hashfunc.hh"
|
||||
#include "kripke/kripke.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
////////////////////////////////////////////////////////////
|
||||
// state_product
|
||||
|
||||
state_product::~state_product()
|
||||
{
|
||||
left_->destroy();
|
||||
right_->destroy();
|
||||
}
|
||||
|
||||
void
|
||||
state_product::destroy() const
|
||||
{
|
||||
if (--count_)
|
||||
return;
|
||||
fixed_size_pool* p = pool_;
|
||||
this->~state_product();
|
||||
p->deallocate(this);
|
||||
}
|
||||
|
||||
int
|
||||
state_product::compare(const state* other) const
|
||||
{
|
||||
const state_product* o = down_cast<const state_product*>(other);
|
||||
assert(o);
|
||||
int res = left_->compare(o->left());
|
||||
if (res != 0)
|
||||
return res;
|
||||
return right_->compare(o->right());
|
||||
}
|
||||
|
||||
size_t
|
||||
state_product::hash() const
|
||||
{
|
||||
// We assume that size_t is 32-bit wide.
|
||||
return wang32_hash(left_->hash()) ^ wang32_hash(right_->hash());
|
||||
}
|
||||
|
||||
state_product*
|
||||
state_product::clone() const
|
||||
{
|
||||
++count_;
|
||||
return const_cast<state_product*>(this);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////
|
||||
// twa_succ_iterator_product
|
||||
|
||||
namespace
|
||||
{
|
||||
|
||||
class twa_succ_iterator_product_common: public twa_succ_iterator
|
||||
{
|
||||
public:
|
||||
twa_succ_iterator_product_common(twa_succ_iterator* left,
|
||||
twa_succ_iterator* right,
|
||||
const twa_product* prod,
|
||||
fixed_size_pool* pool)
|
||||
: left_(left), right_(right), prod_(prod), pool_(pool)
|
||||
{
|
||||
}
|
||||
|
||||
void recycle(const const_twa_ptr& l, twa_succ_iterator* left,
|
||||
const_twa_ptr r, twa_succ_iterator* right)
|
||||
{
|
||||
l->release_iter(left_);
|
||||
left_ = left;
|
||||
r->release_iter(right_);
|
||||
right_ = right;
|
||||
}
|
||||
|
||||
virtual ~twa_succ_iterator_product_common()
|
||||
{
|
||||
delete left_;
|
||||
delete right_;
|
||||
}
|
||||
|
||||
virtual bool next_non_false_() = 0;
|
||||
|
||||
bool first()
|
||||
{
|
||||
if (!right_)
|
||||
return false;
|
||||
|
||||
// If one of the two successor sets is empty initially, we
|
||||
// reset right_, so that done() can detect this situation
|
||||
// easily. (We choose to reset right_ because this variable
|
||||
// is already used by done().)
|
||||
if (!(left_->first() && right_->first()))
|
||||
{
|
||||
delete right_;
|
||||
right_ = 0;
|
||||
return false;
|
||||
}
|
||||
return next_non_false_();
|
||||
}
|
||||
|
||||
bool done() const
|
||||
{
|
||||
return !right_ || right_->done();
|
||||
}
|
||||
|
||||
state_product* current_state() const
|
||||
{
|
||||
return new(pool_->allocate()) state_product(left_->current_state(),
|
||||
right_->current_state(),
|
||||
pool_);
|
||||
}
|
||||
|
||||
protected:
|
||||
twa_succ_iterator* left_;
|
||||
twa_succ_iterator* right_;
|
||||
const twa_product* prod_;
|
||||
fixed_size_pool* pool_;
|
||||
friend class spot::twa_product;
|
||||
};
|
||||
|
||||
|
||||
/// \brief Iterate over the successors of a product computed on the fly.
|
||||
class twa_succ_iterator_product: public twa_succ_iterator_product_common
|
||||
{
|
||||
public:
|
||||
twa_succ_iterator_product(twa_succ_iterator* left,
|
||||
twa_succ_iterator* right,
|
||||
const twa_product* prod,
|
||||
fixed_size_pool* pool)
|
||||
: twa_succ_iterator_product_common(left, right, prod, pool)
|
||||
{
|
||||
}
|
||||
|
||||
virtual ~twa_succ_iterator_product()
|
||||
{
|
||||
}
|
||||
|
||||
bool step_()
|
||||
{
|
||||
if (left_->next())
|
||||
return true;
|
||||
left_->first();
|
||||
return right_->next();
|
||||
}
|
||||
|
||||
bool next_non_false_()
|
||||
{
|
||||
assert(!done());
|
||||
do
|
||||
{
|
||||
bdd l = left_->current_condition();
|
||||
bdd r = right_->current_condition();
|
||||
bdd current_cond = l & r;
|
||||
|
||||
if (current_cond != bddfalse)
|
||||
{
|
||||
current_cond_ = current_cond;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
while (step_());
|
||||
return false;
|
||||
}
|
||||
|
||||
bool next()
|
||||
{
|
||||
if (step_())
|
||||
return next_non_false_();
|
||||
return false;
|
||||
}
|
||||
|
||||
bdd current_condition() const
|
||||
{
|
||||
return current_cond_;
|
||||
}
|
||||
|
||||
acc_cond::mark_t current_acceptance_conditions() const
|
||||
{
|
||||
return
|
||||
prod_->acc().join(prod_->left_acc(),
|
||||
left_->current_acceptance_conditions(),
|
||||
prod_->right_acc(),
|
||||
right_->current_acceptance_conditions());
|
||||
}
|
||||
|
||||
protected:
|
||||
bdd current_cond_;
|
||||
};
|
||||
|
||||
/// Iterate over the successors of a product computed on the fly.
|
||||
/// This one assumes that LEFT is an iterator over a Kripke structure
|
||||
class twa_succ_iterator_product_kripke:
|
||||
public twa_succ_iterator_product_common
|
||||
{
|
||||
public:
|
||||
twa_succ_iterator_product_kripke(twa_succ_iterator* left,
|
||||
twa_succ_iterator* right,
|
||||
const twa_product* prod,
|
||||
fixed_size_pool* pool)
|
||||
: twa_succ_iterator_product_common(left, right, prod, pool)
|
||||
{
|
||||
}
|
||||
|
||||
virtual ~twa_succ_iterator_product_kripke()
|
||||
{
|
||||
}
|
||||
|
||||
bool next_non_false_()
|
||||
{
|
||||
// All the transitions of left_ iterator have the
|
||||
// same label, because it is a Kripke structure.
|
||||
bdd l = left_->current_condition();
|
||||
assert(!right_->done());
|
||||
do
|
||||
{
|
||||
bdd r = right_->current_condition();
|
||||
bdd current_cond = l & r;
|
||||
|
||||
if (current_cond != bddfalse)
|
||||
{
|
||||
current_cond_ = current_cond;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
while (right_->next());
|
||||
return false;
|
||||
}
|
||||
|
||||
bool next()
|
||||
{
|
||||
if (left_->next())
|
||||
return true;
|
||||
left_->first();
|
||||
if (right_->next())
|
||||
return next_non_false_();
|
||||
return false;
|
||||
}
|
||||
|
||||
bdd current_condition() const
|
||||
{
|
||||
return current_cond_;
|
||||
}
|
||||
|
||||
acc_cond::mark_t current_acceptance_conditions() const
|
||||
{
|
||||
return right_->current_acceptance_conditions();
|
||||
}
|
||||
|
||||
protected:
|
||||
bdd current_cond_;
|
||||
};
|
||||
|
||||
} // anonymous
|
||||
|
||||
////////////////////////////////////////////////////////////
|
||||
// twa_product
|
||||
|
||||
twa_product::twa_product(const const_twa_ptr& left,
|
||||
const const_twa_ptr& right)
|
||||
: twa(left->get_dict()), left_(left), right_(right),
|
||||
pool_(sizeof(state_product))
|
||||
{
|
||||
assert(get_dict() == right_->get_dict());
|
||||
|
||||
// If one of the side is a Kripke structure, it is easier to deal
|
||||
// with (we don't have to fix the acceptance conditions, and
|
||||
// computing the successors can be improved a bit).
|
||||
if (dynamic_cast<const kripke*>(left_.get()))
|
||||
{
|
||||
left_kripke_ = true;
|
||||
}
|
||||
else if (dynamic_cast<const kripke*>(right_.get()))
|
||||
{
|
||||
std::swap(left_, right_);
|
||||
left_kripke_ = true;
|
||||
}
|
||||
else
|
||||
{
|
||||
left_kripke_ = false;
|
||||
}
|
||||
|
||||
auto d = get_dict();
|
||||
d->register_all_propositions_of(&left_, this);
|
||||
d->register_all_propositions_of(&right_, this);
|
||||
|
||||
assert(acc_.num_sets() == 0);
|
||||
auto left_num = left->acc().num_sets();
|
||||
auto right_acc = right->get_acceptance();
|
||||
right_acc.shift_left(left_num);
|
||||
right_acc.append_and(left->get_acceptance());
|
||||
set_acceptance(left_num + right->acc().num_sets(), right_acc);
|
||||
}
|
||||
|
||||
twa_product::~twa_product()
|
||||
{
|
||||
get_dict()->unregister_all_my_variables(this);
|
||||
// Prevent these states from being destroyed by ~tgba(): they
|
||||
// will be destroyed before when the pool is destructed.
|
||||
if (last_support_conditions_input_)
|
||||
{
|
||||
last_support_conditions_input_->destroy();
|
||||
last_support_conditions_input_ = 0;
|
||||
}
|
||||
}
|
||||
|
||||
state*
|
||||
twa_product::get_init_state() const
|
||||
{
|
||||
fixed_size_pool* p = const_cast<fixed_size_pool*>(&pool_);
|
||||
return new(p->allocate()) state_product(left_->get_init_state(),
|
||||
right_->get_init_state(), p);
|
||||
}
|
||||
|
||||
twa_succ_iterator*
|
||||
twa_product::succ_iter(const state* state) const
|
||||
{
|
||||
const state_product* s = down_cast<const state_product*>(state);
|
||||
assert(s);
|
||||
twa_succ_iterator* li = left_->succ_iter(s->left());
|
||||
twa_succ_iterator* ri = right_->succ_iter(s->right());
|
||||
|
||||
if (iter_cache_)
|
||||
{
|
||||
twa_succ_iterator_product_common* it =
|
||||
down_cast<twa_succ_iterator_product_common*>(iter_cache_);
|
||||
it->recycle(left_, li, right_, ri);
|
||||
iter_cache_ = nullptr;
|
||||
return it;
|
||||
}
|
||||
|
||||
fixed_size_pool* p = const_cast<fixed_size_pool*>(&pool_);
|
||||
if (left_kripke_)
|
||||
return new twa_succ_iterator_product_kripke(li, ri, this, p);
|
||||
else
|
||||
return new twa_succ_iterator_product(li, ri, this, p);
|
||||
}
|
||||
|
||||
bdd
|
||||
twa_product::compute_support_conditions(const state* in) const
|
||||
{
|
||||
const state_product* s = down_cast<const state_product*>(in);
|
||||
assert(s);
|
||||
bdd lsc = left_->support_conditions(s->left());
|
||||
bdd rsc = right_->support_conditions(s->right());
|
||||
return lsc & rsc;
|
||||
}
|
||||
|
||||
const acc_cond& twa_product::left_acc() const
|
||||
{
|
||||
return left_->acc();
|
||||
}
|
||||
|
||||
const acc_cond& twa_product::right_acc() const
|
||||
{
|
||||
return right_->acc();
|
||||
}
|
||||
|
||||
std::string
|
||||
twa_product::format_state(const state* state) const
|
||||
{
|
||||
const state_product* s = down_cast<const state_product*>(state);
|
||||
assert(s);
|
||||
return (left_->format_state(s->left())
|
||||
+ " * "
|
||||
+ right_->format_state(s->right()));
|
||||
}
|
||||
|
||||
state*
|
||||
twa_product::project_state(const state* s, const const_twa_ptr& t) const
|
||||
{
|
||||
const state_product* s2 = down_cast<const state_product*>(s);
|
||||
assert(s2);
|
||||
if (t.get() == this)
|
||||
return s2->clone();
|
||||
state* res = left_->project_state(s2->left(), t);
|
||||
if (res)
|
||||
return res;
|
||||
return right_->project_state(s2->right(), t);
|
||||
}
|
||||
|
||||
std::string
|
||||
twa_product::transition_annotation(const twa_succ_iterator* t) const
|
||||
{
|
||||
const twa_succ_iterator_product_common* i =
|
||||
down_cast<const twa_succ_iterator_product_common*>(t);
|
||||
assert(i);
|
||||
std::string left = left_->transition_annotation(i->left_);
|
||||
std::string right = right_->transition_annotation(i->right_);
|
||||
if (left == "")
|
||||
return right;
|
||||
if (right == "")
|
||||
return left;
|
||||
return "<" + left + ", " + right + ">";
|
||||
}
|
||||
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
// twa_product_init
|
||||
|
||||
twa_product_init::twa_product_init(const const_twa_ptr& left,
|
||||
const const_twa_ptr& right,
|
||||
const state* left_init,
|
||||
const state* right_init)
|
||||
: twa_product(left, right),
|
||||
left_init_(left_init), right_init_(right_init)
|
||||
{
|
||||
if (left_ != left)
|
||||
std::swap(left_init_, right_init_);
|
||||
}
|
||||
|
||||
state*
|
||||
twa_product_init::get_init_state() const
|
||||
{
|
||||
fixed_size_pool* p = const_cast<fixed_size_pool*>(&pool_);
|
||||
return new(p->allocate()) state_product(left_init_->clone(),
|
||||
right_init_->clone(), p);
|
||||
}
|
||||
|
||||
}
|
||||
149
src/twa/twaproduct.hh
Normal file
149
src/twa/twaproduct.hh
Normal file
|
|
@ -0,0 +1,149 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
|
||||
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "twa.hh"
|
||||
#include "misc/fixpool.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
/// \ingroup twa_on_the_fly_algorithms
|
||||
/// \brief A state for spot::twa_product.
|
||||
///
|
||||
/// This state is in fact a pair of state: the state from the left
|
||||
/// automaton and that of the right.
|
||||
class SPOT_API state_product final: public state
|
||||
{
|
||||
public:
|
||||
/// \brief Constructor
|
||||
/// \param left The state from the left automaton.
|
||||
/// \param right The state from the right automaton.
|
||||
/// \param pool The pool from which the state was allocated.
|
||||
/// These states are acquired by spot::state_product, and will
|
||||
/// be destroyed on destruction.
|
||||
state_product(state* left, state* right, fixed_size_pool* pool)
|
||||
: left_(left), right_(right), count_(1), pool_(pool)
|
||||
{
|
||||
}
|
||||
|
||||
virtual void destroy() const;
|
||||
|
||||
state*
|
||||
left() const
|
||||
{
|
||||
return left_;
|
||||
}
|
||||
|
||||
state*
|
||||
right() const
|
||||
{
|
||||
return right_;
|
||||
}
|
||||
|
||||
virtual int compare(const state* other) const;
|
||||
virtual size_t hash() const;
|
||||
virtual state_product* clone() const;
|
||||
|
||||
private:
|
||||
state* left_; ///< State from the left automaton.
|
||||
state* right_; ///< State from the right automaton.
|
||||
mutable unsigned count_;
|
||||
fixed_size_pool* pool_;
|
||||
|
||||
virtual ~state_product();
|
||||
state_product(const state_product& o); // No implementation.
|
||||
};
|
||||
|
||||
|
||||
/// \brief A lazy product. (States are computed on the fly.)
|
||||
class SPOT_API twa_product: public twa
|
||||
{
|
||||
public:
|
||||
/// \brief Constructor.
|
||||
/// \param left The left automata in the product.
|
||||
/// \param right The right automata in the product.
|
||||
/// Do not be fooled by these arguments: a product is commutative.
|
||||
twa_product(const const_twa_ptr& left, const const_twa_ptr& right);
|
||||
|
||||
virtual ~twa_product();
|
||||
|
||||
virtual state* get_init_state() const;
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* state) const;
|
||||
|
||||
virtual std::string format_state(const state* state) const;
|
||||
|
||||
virtual std::string
|
||||
transition_annotation(const twa_succ_iterator* t) const;
|
||||
|
||||
virtual state* project_state(const state* s, const const_twa_ptr& t) const;
|
||||
|
||||
const acc_cond& left_acc() const;
|
||||
const acc_cond& right_acc() const;
|
||||
|
||||
protected:
|
||||
virtual bdd compute_support_conditions(const state* state) const;
|
||||
|
||||
protected:
|
||||
const_twa_ptr left_;
|
||||
const_twa_ptr right_;
|
||||
bool left_kripke_;
|
||||
fixed_size_pool pool_;
|
||||
|
||||
private:
|
||||
// Disallow copy.
|
||||
twa_product(const twa_product&) SPOT_DELETED;
|
||||
twa_product& operator=(const twa_product&) SPOT_DELETED;
|
||||
};
|
||||
|
||||
/// \brief A lazy product with different initial states.
|
||||
class SPOT_API twa_product_init final: public twa_product
|
||||
{
|
||||
public:
|
||||
twa_product_init(const const_twa_ptr& left, const const_twa_ptr& right,
|
||||
const state* left_init, const state* right_init);
|
||||
virtual state* get_init_state() const;
|
||||
protected:
|
||||
const state* left_init_;
|
||||
const state* right_init_;
|
||||
};
|
||||
|
||||
/// \brief on-the-fly TGBA product
|
||||
inline twa_product_ptr otf_product(const const_twa_ptr& left,
|
||||
const const_twa_ptr& right)
|
||||
{
|
||||
return std::make_shared<twa_product>(left, right);
|
||||
}
|
||||
|
||||
/// \brief on-the-fly TGBA product with forced initial states
|
||||
inline twa_product_ptr otf_product_at(const const_twa_ptr& left,
|
||||
const const_twa_ptr& right,
|
||||
const state* left_init,
|
||||
const state* right_init)
|
||||
{
|
||||
return std::make_shared<twa_product_init>(left, right,
|
||||
left_init, right_init);
|
||||
}
|
||||
}
|
||||
75
src/twa/twaproxy.cc
Normal file
75
src/twa/twaproxy.cc
Normal file
|
|
@ -0,0 +1,75 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014, 2015 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 "twaproxy.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
twa_proxy::twa_proxy(const const_twa_ptr& original)
|
||||
: twa(original->get_dict()), original_(original)
|
||||
{
|
||||
get_dict()->register_all_variables_of(original, this);
|
||||
acc_.add_sets(original->acc().num_sets());
|
||||
}
|
||||
|
||||
twa_proxy::~twa_proxy()
|
||||
{
|
||||
get_dict()->unregister_all_my_variables(this);
|
||||
}
|
||||
|
||||
state* twa_proxy::get_init_state() const
|
||||
{
|
||||
return original_->get_init_state();
|
||||
}
|
||||
|
||||
twa_succ_iterator*
|
||||
twa_proxy::succ_iter(const state* state) const
|
||||
{
|
||||
if (iter_cache_)
|
||||
{
|
||||
original_->release_iter(iter_cache_);
|
||||
iter_cache_ = nullptr;
|
||||
}
|
||||
return original_->succ_iter(state);
|
||||
}
|
||||
|
||||
std::string
|
||||
twa_proxy::format_state(const state* state) const
|
||||
{
|
||||
return original_->format_state(state);
|
||||
}
|
||||
|
||||
std::string
|
||||
twa_proxy::transition_annotation(const twa_succ_iterator* t) const
|
||||
{
|
||||
return original_->transition_annotation(t);
|
||||
}
|
||||
|
||||
state*
|
||||
twa_proxy::project_state(const state* s, const const_twa_ptr& t) const
|
||||
{
|
||||
return original_->project_state(s, t);
|
||||
}
|
||||
|
||||
bdd
|
||||
twa_proxy::compute_support_conditions(const state* state) const
|
||||
{
|
||||
return original_->support_conditions(state);
|
||||
}
|
||||
}
|
||||
59
src/twa/twaproxy.hh
Normal file
59
src/twa/twaproxy.hh
Normal file
|
|
@ -0,0 +1,59 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014, 2015 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "twa.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \ingroup twa_on_the_fly_algorithms
|
||||
/// \brief A TGBA proxy.
|
||||
///
|
||||
/// This implements a simple proxy to an existing
|
||||
/// TGBA, forwarding all methods to the original.
|
||||
/// By itself this class is pointless: better use the
|
||||
/// original automaton right away. However it is useful
|
||||
/// to inherit from this class and override some of its
|
||||
/// methods to implement some on-the-fly algorithm.
|
||||
class SPOT_API twa_proxy: public twa
|
||||
{
|
||||
protected:
|
||||
twa_proxy(const const_twa_ptr& original);
|
||||
|
||||
public:
|
||||
virtual ~twa_proxy();
|
||||
|
||||
virtual state* get_init_state() const;
|
||||
|
||||
virtual twa_succ_iterator*
|
||||
succ_iter(const state* state) const;
|
||||
|
||||
virtual std::string format_state(const state* state) const;
|
||||
|
||||
virtual std::string
|
||||
transition_annotation(const twa_succ_iterator* t) const;
|
||||
|
||||
virtual state* project_state(const state* s, const const_twa_ptr& t) const;
|
||||
|
||||
protected:
|
||||
virtual bdd compute_support_conditions(const state* state) const;
|
||||
const_twa_ptr original_;
|
||||
};
|
||||
}
|
||||
1267
src/twa/twasafracomplement.cc
Normal file
1267
src/twa/twasafracomplement.cc
Normal file
File diff suppressed because it is too large
Load diff
95
src/twa/twasafracomplement.hh
Normal file
95
src/twa/twasafracomplement.hh
Normal file
|
|
@ -0,0 +1,95 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2010, 2011, 2013, 2014, 2015 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <vector>
|
||||
#include "twa.hh"
|
||||
|
||||
#ifndef TRANSFORM_TO_TBA
|
||||
# define TRANSFORM_TO_TBA 0
|
||||
#endif
|
||||
#define TRANSFORM_TO_TGBA (!TRANSFORM_TO_TBA)
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \ingroup twa_on_the_fly_algorithms
|
||||
/// \brief Build a complemented automaton.
|
||||
///
|
||||
/// It creates an automaton that recognizes the
|
||||
/// negated language of \a aut.
|
||||
///
|
||||
/// 1. First Safra construction algorithm produces a
|
||||
/// deterministic Rabin automaton.
|
||||
/// 2. Interpreting this deterministic Rabin automaton as a
|
||||
/// deterministic Streett will produce a complemented automaton.
|
||||
/// 3. Then we use a transformation from deterministic Streett
|
||||
/// automaton to nondeterministic Büchi automaton.
|
||||
///
|
||||
/// Safra construction is done in \a tgba_complement, the transformation
|
||||
/// is done on-the-fly when successors are called.
|
||||
///
|
||||
/// \sa safra_determinisation, tgba_safra_complement::succ_iter.
|
||||
class SPOT_API tgba_safra_complement : public twa
|
||||
{
|
||||
public:
|
||||
tgba_safra_complement(const const_twa_graph_ptr& a);
|
||||
virtual ~tgba_safra_complement();
|
||||
|
||||
// tgba interface.
|
||||
virtual state* get_init_state() const;
|
||||
virtual twa_succ_iterator* succ_iter(const state* state) const;
|
||||
|
||||
virtual std::string format_state(const state* state) const;
|
||||
|
||||
void* get_safra() const
|
||||
{
|
||||
return safra_;
|
||||
}
|
||||
|
||||
protected:
|
||||
virtual bdd compute_support_conditions(const state* state) const;
|
||||
private:
|
||||
const_twa_graph_ptr automaton_;
|
||||
void* safra_;
|
||||
#if TRANSFORM_TO_TBA
|
||||
acc_cond::mark_t the_acceptance_cond_;
|
||||
#endif
|
||||
#if TRANSFORM_TO_TGBA
|
||||
// Map to i the i-th acceptance condition of the final automaton.
|
||||
std::vector<acc_cond::mark_t> acceptance_cond_vec_;
|
||||
#endif
|
||||
};
|
||||
|
||||
typedef std::shared_ptr<tgba_safra_complement> tgba_safra_complement_ptr;
|
||||
typedef std::shared_ptr<const tgba_safra_complement>
|
||||
const_tgba_safra_complement_ptr;
|
||||
inline tgba_safra_complement_ptr
|
||||
make_safra_complement(const const_twa_graph_ptr& a)
|
||||
{
|
||||
return std::make_shared<tgba_safra_complement>(a);
|
||||
}
|
||||
|
||||
/// \brief Produce a dot output of the Safra automaton associated
|
||||
/// to \a a.
|
||||
///
|
||||
/// \param a The \c tgba_safra_complement with an intermediate Safra
|
||||
/// automaton to display
|
||||
void SPOT_API display_safra(const const_tgba_safra_complement_ptr& a);
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue