alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgba/tgbatba.cc: Register the variables of the source automaton.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2013-05-22 17:48:12 +02:00
parent 84dabae374
commit 260ab53cb5
1 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/tgba/tgbatba.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Développement de // Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// l'Epita. // Développement de l'Epita.
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -399,7 +399,11 @@ namespace spot
{ {
// We will use one acceptance condition for this automata. // We will use one acceptance condition for this automata.
// Let's call it Acc[True]. // Let's call it Acc[True].
int v = get_dict() bdd_dict* d = get_dict();
d->register_all_variables_of(a, this);
d->unregister_all_typed_variables(bdd_dict::acc, this);
int v = d
->register_acceptance_variable(ltl::constant::true_instance(), this); ->register_acceptance_variable(ltl::constant::true_instance(), this);
the_acceptance_cond_ = bdd_ithvar(v); the_acceptance_cond_ = bdd_ithvar(v);