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

Downcase a couple of misnamed class names.

Browse source 
* src/misc/acccompl.hh, src/misc/acccompl.cc (AccCompl): Rename to
acc_compl.
* src/tgbaalgos/simulation.cc (AccComplAutomaton, Simulation): Rename
to acc_compl_automaton and direct_simulation.  At the same time,
reindent the whole file.
* src/sanity/style.test: Detect capitalized class names.
* src/kripke/kripkeexplicit.hh (KripkePrint): Remove useless
predeclaration.
* src/tgbaalgos/simulation.hh: Typo in comment.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-02 17:57:38 +02:00
parent dadfbdad9d
commit db4693b303
6 changed files with 329 additions and 326 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/kripke/kripkeexplicit.hh
View file

@ -1,4 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE) // de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -29,10 +30,7 @@
namespace spot namespace spot
{ {
// Define in kripkeprint.hh /// \brief Concrete class for kripke states.
class KripkeVisitor;
/// \brief Concrete class for kripke states.
class state_kripke : public state class state_kripke : public state
{ {
friend class kripke_explicit; friend class kripke_explicit;

4
src/misc/acccompl.cc
View file

@ -34,7 +34,7 @@ namespace spot
// we need to know wich one is go to one when true. So we are looping // we need to know wich one is go to one when true. So we are looping
// through the conditions until bdd_high is true. // through the conditions until bdd_high is true.
// Once found, we keep only it. // Once found, we keep only it.
bdd AccCompl::complement(const bdd acc) bdd acc_compl::complement(const bdd acc)
{ {
bdd_cache_t::const_iterator it = cache_.find(acc); bdd_cache_t::const_iterator it = cache_.find(acc);
if (it != cache_.end()) if (it != cache_.end())
@ -70,7 +70,7 @@ namespace spot
} }
bdd AccCompl::reverse_complement(const bdd acc) bdd acc_compl::reverse_complement(const bdd acc)
{ {
// We are sure that if we have no acceptance condition // We are sure that if we have no acceptance condition
// the result is all_. // the result is all_.

12
src/misc/acccompl.hh
View file

@ -30,14 +30,14 @@
namespace spot namespace spot
{ {
/// \brief Help class to convert a bdd of an automaton into /// \brief Helper class to convert acceptance conditions into promises
/// its complement. ///
/// This is used when you need to complement all the acceptance /// A set of acceptance conditions represented by the sum "à la Spot",
/// conditions in an automaton. For example in the simulation. /// is converted into a product of promises.
class AccCompl class acc_compl
{ {
public: public:
AccCompl(bdd all, bdd neg) acc_compl(bdd all, bdd neg)
: all_(all), : all_(all),
neg_(neg) neg_(neg)
{ {

3
src/sanity/style.test
View file

@ -67,6 +67,9 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
case $file in case $file in
*.test);; *.test);;
*) *)
grep -E '[^<]class[ \t]+[A-Z]' $tmp &&
diag 'Use lower case class names.'
grep '[ ]if(' $tmp && grep '[ ]if(' $tmp &&
diag 'Missing space after "if"' diag 'Missing space after "if"'

626
src/tgbaalgos/simulation.cc
View file

@ -60,7 +60,7 @@
// state. This function is `update_sig'. // state. This function is `update_sig'.
// - Enter in a double loop to adapt the partial order, and set // - Enter in a double loop to adapt the partial order, and set
// 'relation_' accordingly. This function is `update_po'. // 'relation_' accordingly. This function is `update_po'.
// 3. Rename the class (to actualize the name in the previous_it_class and // 3. Rename the class (to actualize the name in the previous_class and
// in relation_). // in relation_).
// 4. Building an automaton with the result, with the condition: // 4. Building an automaton with the result, with the condition:
// "a transition in the original automaton appears in the simulated one // "a transition in the original automaton appears in the simulated one
@ -99,20 +99,20 @@ namespace spot
bdd_less_than> map_bdd_lstate; bdd_less_than> map_bdd_lstate;
// This class takes an automaton and creates a copy with all // This class takes an automaton and creates a copy with all
// acceptance conditions complemented. // acceptance conditions complemented.
class AccComplAutomaton: class acc_compl_automaton:
public tgba_reachable_iterator_depth_first public tgba_reachable_iterator_depth_first
{ {
public: public:
AccComplAutomaton(const tgba* a) acc_compl_automaton(const tgba* a)
: tgba_reachable_iterator_depth_first(a), : tgba_reachable_iterator_depth_first(a),
size(0), size(0),
out_(new tgba_explicit_number(a->get_dict())), out_(new tgba_explicit_number(a->get_dict())),
ea_(a), ea_(a),
ac_(ea_->all_acceptance_conditions(), ac_(ea_->all_acceptance_conditions(),
ea_->neg_acceptance_conditions()), ea_->neg_acceptance_conditions()),
current_max(0) current_max(0)
{ {
init_ = ea_->get_init_state(); init_ = ea_->get_init_state();
out_->set_init_state(get_state(init_)); out_->set_init_state(get_state(init_));
@ -122,10 +122,10 @@ namespace spot
get_state(const state* s) get_state(const state* s)
{ {
if (state2int.find(s) == state2int.end()) if (state2int.find(s) == state2int.end())
{ {
state2int[s] = ++current_max; state2int[s] = ++current_max;
previous_it_class_[out_->add_state(current_max)] = bddfalse; previous_class_[out_->add_state(current_max)] = bddfalse;
} }
return state2int[s]; return state2int[s];
} }
@ -155,7 +155,7 @@ namespace spot
++size; ++size;
} }
~AccComplAutomaton() ~acc_compl_automaton()
{ {
init_->destroy(); init_->destroy();
} }
@ -163,128 +163,128 @@ namespace spot
public: public:
size_t size; size_t size;
tgba_explicit_number* out_; tgba_explicit_number* out_;
map_state_bdd previous_it_class_; map_state_bdd previous_class_;
private: private:
const tgba* ea_; const tgba* ea_;
AccCompl ac_; acc_compl ac_;
map_state_unsigned state2int; map_state_unsigned state2int;
unsigned current_max; unsigned current_max;
state* init_; state* init_;
}; };
class Simulation class direct_simulation
{ {
// Shortcut used in update_po and go_to_next_it. // Shortcut used in update_po and go_to_next_it.
typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd; typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd;
public: public:
Simulation(const tgba* t) direct_simulation(const tgba* t)
: a_(0), : a_(0),
po_size_(0), po_size_(0),
all_class_var_(bddtrue) all_class_var_(bddtrue)
{ {
AccComplAutomaton acc_compl_automaton
acc_compl(t); acc_compl(t);
// We'll start our work by replacing all the acceptance // We'll start our work by replacing all the acceptance
// conditions by their complement. // conditions by their complement.
acc_compl.run(); acc_compl.run();
a_ = acc_compl.out_; a_ = acc_compl.out_;
// We use the previous run to know the size of the // We use the previous run to know the size of the
// automaton, and to class all the reachable states in the // automaton, and to class all the reachable states in the
// map previous_it_class_. // map previous_class_.
size_a_ = acc_compl.size; size_a_ = acc_compl.size;
// Now, we have to get the bdd which will represent the // Now, we have to get the bdd which will represent the
// class. We register one bdd by state, because in the worst // class. We register one bdd by state, because in the worst
// case, |Class| == |State|. // case, |Class| == |State|.
unsigned set_num = a_->get_dict() unsigned set_num = a_->get_dict()
->register_anonymous_variables(size_a_, a_); ->register_anonymous_variables(size_a_, a_);
bdd init = bdd_ithvar(set_num); bdd init = bdd_ithvar(set_num);
// Because we have already take the first element which is init. // Because we have already take the first element which is init.
++set_num; ++set_num;
used_var_.push_back(init); used_var_.push_back(init);
all_class_var_ = init; all_class_var_ = init;
// We fetch the result the run of AccComplAutomaton which // We fetch the result the run of acc_compl_automaton which
// has recorded all the state in a hash table, and we set all // has recorded all the state in a hash table, and we set all
// to init. // to init.
for (map_state_bdd::iterator it for (map_state_bdd::iterator it
= acc_compl.previous_it_class_.begin(); = acc_compl.previous_class_.begin();
it != acc_compl.previous_it_class_.end(); it != acc_compl.previous_class_.end();
++it) ++it)
{ {
previous_it_class_[it->first] = init; previous_class_[it->first] = init;
} }
// Put all the anonymous variable in a queue, and record all // Put all the anonymous variable in a queue, and record all
// of these in a variable all_class_var_ which will be used // of these in a variable all_class_var_ which will be used
// to understand the destination part in the signature when // to understand the destination part in the signature when
// building the resulting automaton. // building the resulting automaton.
for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i) for (unsigned i = set_num; i < set_num + size_a_ - 1; ++i)
{ {
free_var_.push(i); free_var_.push(i);
all_class_var_ &= bdd_ithvar(i); all_class_var_ &= bdd_ithvar(i);
} }
relation_[init] = init; relation_[init] = init;
} }
// Reverse all the acceptance condition at the destruction of // Reverse all the acceptance condition at the destruction of
// this object, because it occurs after the return of the // this object, because it occurs after the return of the
// function simulation. // function simulation.
~Simulation() ~direct_simulation()
{ {
delete a_; delete a_;
} }
// We update the name of the class. // We update the name of the class.
void update_previous_it_class() void update_previous_class()
{ {
std::list<bdd>::iterator it_bdd = used_var_.begin(); std::list<bdd>::iterator it_bdd = used_var_.begin();
// We run through the map bdd/list<state>, and we update // We run through the map bdd/list<state>, and we update
// the previous_it_class_ with the new data. // the previous_class_ with the new data.
it_bdd = used_var_.begin(); it_bdd = used_var_.begin();
for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end(); it != bdd_lstate_.end();
++it) ++it)
{ {
for (std::list<const state*>::iterator it_s = it->second.begin(); for (std::list<const state*>::iterator it_s = it->second.begin();
it_s != it->second.end(); it_s != it->second.end();
++it_s) ++it_s)
{ {
// If the signature of a state is bddfalse (which is // If the signature of a state is bddfalse (which is
// roughly equivalent to no transition) the class of // roughly equivalent to no transition) the class of
// this state is bddfalse instead of an anonymous // this state is bddfalse instead of an anonymous
// variable. It allows simplifications in the signature // variable. It allows simplifications in the signature
// by removing a transition which has as a destination a // by removing a transition which has as a destination a
// state with no outgoing transition. // state with no outgoing transition.
if (it->first == bddfalse) if (it->first == bddfalse)
previous_it_class_[*it_s] = bddfalse; previous_class_[*it_s] = bddfalse;
else else
previous_it_class_[*it_s] = *it_bdd; previous_class_[*it_s] = *it_bdd;
} }
++it_bdd; ++it_bdd;
} }
} }
// The core loop of the algorithm. // The core loop of the algorithm.
tgba* run() tgba* run()
{ {
unsigned int nb_partition_before = 0; unsigned int nb_partition_before = 0;
unsigned int nb_po_before = po_size_ - 1; unsigned int nb_po_before = po_size_ - 1;
while (nb_partition_before != bdd_lstate_.size() while (nb_partition_before != bdd_lstate_.size()
|| nb_po_before != po_size_) || nb_po_before != po_size_)
{ {
update_previous_it_class(); update_previous_class();
nb_partition_before = bdd_lstate_.size(); nb_partition_before = bdd_lstate_.size();
bdd_lstate_.clear(); bdd_lstate_.clear();
nb_po_before = po_size_; nb_po_before = po_size_;
@ -293,17 +293,17 @@ namespace spot
go_to_next_it(); go_to_next_it();
} }
update_previous_it_class(); update_previous_class();
return build_result(); return build_result();
} }
// Take a state and compute its signature. // Take a state and compute its signature.
bdd compute_sig(const state* src) bdd compute_sig(const state* src)
{ {
tgba_succ_iterator* sit = a_->succ_iter(src); tgba_succ_iterator* sit = a_->succ_iter(src);
bdd res = bddfalse; bdd res = bddfalse;
for (sit->first(); !sit->done(); sit->next()) for (sit->first(); !sit->done(); sit->next())
{ {
const state* dst = sit->current_state(); const state* dst = sit->current_state();
bdd acc = sit->current_acceptance_conditions(); bdd acc = sit->current_acceptance_conditions();
@ -312,65 +312,65 @@ namespace spot
// the label of the transition and the class of the // the label of the transition and the class of the
// destination and all the class it implies. // destination and all the class it implies.
bdd to_add = acc & sit->current_condition() bdd to_add = acc & sit->current_condition()
& relation_[previous_it_class_[dst]]; & relation_[previous_class_[dst]];
res |= to_add; res |= to_add;
dst->destroy(); dst->destroy();
} }
delete sit; delete sit;
return res; return res;
} }
void update_sig() void update_sig()
{ {
// At this time, current_class_ must be empty. It implies // At this time, current_class_ must be empty. It implies
// that the "previous_it_class_ = current_class_" must be // that the "previous_class_ = current_class_" must be
// done before. // done before.
assert(current_class_.empty()); assert(current_class_.empty());
// Here we suppose that previous_it_class_ always contains // Here we suppose that previous_class_ always contains
// all the reachable states of this automaton. We do not // all the reachable states of this automaton. We do not
// have to make (again) a traversal. We just have to run // have to make (again) a traversal. We just have to run
// through this map. // through this map.
for (map_state_bdd::iterator it = previous_it_class_.begin(); for (map_state_bdd::iterator it = previous_class_.begin();
it != previous_it_class_.end(); it != previous_class_.end();
++it) ++it)
{ {
const state* src = it->first; const state* src = it->first;
bdd_lstate_[compute_sig(src)].push_back(src); bdd_lstate_[compute_sig(src)].push_back(src);
} }
} }
// This method rename the color set, update the partial order. // This method rename the color set, update the partial order.
void go_to_next_it() void go_to_next_it()
{ {
int nb_new_color = bdd_lstate_.size() - used_var_.size(); int nb_new_color = bdd_lstate_.size() - used_var_.size();
for (int i = 0; i < nb_new_color; ++i) for (int i = 0; i < nb_new_color; ++i)
{ {
assert(!free_var_.empty()); assert(!free_var_.empty());
used_var_.push_back(bdd_ithvar(free_var_.front())); used_var_.push_back(bdd_ithvar(free_var_.front()));
free_var_.pop(); free_var_.pop();
} }
assert(bdd_lstate_.size() == used_var_.size()); assert(bdd_lstate_.size() == used_var_.size());
// Now we make a temporary hash_table which links the tuple // Now we make a temporary hash_table which links the tuple
// "C^(i-1), N^(i-1)" to the new class coloring. If we // "C^(i-1), N^(i-1)" to the new class coloring. If we
// rename the class before updating the partial order, we // rename the class before updating the partial order, we
// loose the information, and if we make it after, I can't // loose the information, and if we make it after, I can't
// figure out how to apply this renaming on rel_. // figure out how to apply this renaming on rel_.
// It adds a data structure but it solves our problem. // It adds a data structure but it solves our problem.
map_bdd_bdd now_to_next; map_bdd_bdd now_to_next;
std::list<bdd>::iterator it_bdd = used_var_.begin(); std::list<bdd>::iterator it_bdd = used_var_.begin();
for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end(); it != bdd_lstate_.end();
++it) ++it)
{ {
// If the signature of a state is bddfalse (which is // If the signature of a state is bddfalse (which is
// roughly equivalent to no transition) the class of // roughly equivalent to no transition) the class of
@ -385,85 +385,85 @@ namespace spot
++it_bdd; ++it_bdd;
} }
update_po(now_to_next); update_po(now_to_next);
} }
// This function computes the new po with previous_it_class_ // This function computes the new po with previous_class_
// and the argument. `now_to_next' contains the relation // and the argument. `now_to_next' contains the relation
// between the signature and the future name of the class. // between the signature and the future name of the class.
void update_po(const map_bdd_bdd& now_to_next) void update_po(const map_bdd_bdd& now_to_next)
{ {
// This loop follows the pattern given by the paper. // This loop follows the pattern given by the paper.
// foreach class do // foreach class do
// | foreach class do // | foreach class do
// | | update po if needed // | | update po if needed
// | od // | od
// od // od
for (map_bdd_bdd::const_iterator it1 = now_to_next.begin(); for (map_bdd_bdd::const_iterator it1 = now_to_next.begin();
it1 != now_to_next.end(); it1 != now_to_next.end();
++it1) ++it1)
{ {
bdd accu = it1->second; bdd accu = it1->second;
for (map_bdd_bdd::const_iterator it2 = now_to_next.begin(); for (map_bdd_bdd::const_iterator it2 = now_to_next.begin();
it2 != now_to_next.end(); it2 != now_to_next.end();
++it2) ++it2)
{ {
// Skip the case managed by the initialization of accu. // Skip the case managed by the initialization of accu.
if (it1 == it2) if (it1 == it2)
continue; continue;
// We detect that "a&b -> a" by testing "a&b = a". // We detect that "a&b -> a" by testing "a&b = a".
if ((it1->first & it2->first) == (it1->first)) if ((it1->first & it2->first) == (it1->first))
{ {
accu &= it2->second; accu &= it2->second;
++po_size_; ++po_size_;
} }
} }
relation_[it1->second] = accu; relation_[it1->second] = accu;
} }
} }
// Build the minimal resulting automaton. // Build the minimal resulting automaton.
tgba* build_result() tgba* build_result()
{ {
// Now we need to create a state per partition. But the // Now we need to create a state per partition. But the
// problem is that we don't know exactly the class. We know // problem is that we don't know exactly the class. We know
// that it is a combination of the acceptance condition // that it is a combination of the acceptance condition
// contained in all_class_var_. So we need to make a little // contained in all_class_var_. So we need to make a little
// workaround. We will create a map which will associate bdd // workaround. We will create a map which will associate bdd
// and unsigned. // and unsigned.
std::map<bdd, unsigned, bdd_less_than> bdd2state; std::map<bdd, unsigned, bdd_less_than> bdd2state;
unsigned int current_max = 0; unsigned int current_max = 0;
bdd all_acceptance_conditions bdd all_acceptance_conditions
= a_->all_acceptance_conditions(); = a_->all_acceptance_conditions();
// We have all the a_'s acceptances conditions // We have all the a_'s acceptances conditions
// complemented. So we need to complement it when adding a // complemented. So we need to complement it when adding a
// transition. We *must* keep the complemented because it // transition. We *must* keep the complemented because it
// is easy to know if an acceptance condition is maximal or // is easy to know if an acceptance condition is maximal or
// not. // not.
AccCompl reverser(all_acceptance_conditions, acc_compl reverser(all_acceptance_conditions,
a_->neg_acceptance_conditions()); a_->neg_acceptance_conditions());
typedef tgba_explicit_number::transition trs; typedef tgba_explicit_number::transition trs;
tgba_explicit_number* res tgba_explicit_number* res
= new tgba_explicit_number(a_->get_dict()); = new tgba_explicit_number(a_->get_dict());
res->set_acceptance_conditions res->set_acceptance_conditions
(all_acceptance_conditions); (all_acceptance_conditions);
bdd sup_all_acc = bdd_support(all_acceptance_conditions); bdd sup_all_acc = bdd_support(all_acceptance_conditions);
// Non atomic propositions variables (= acc and class) // Non atomic propositions variables (= acc and class)
bdd nonapvars = sup_all_acc & bdd_support(all_class_var_); bdd nonapvars = sup_all_acc & bdd_support(all_class_var_);
// Create one state per partition. // Create one state per partition.
for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end(); ++it) it != bdd_lstate_.end(); ++it)
{ {
res->add_state(++current_max); res->add_state(++current_max);
bdd part = previous_it_class_[*it->second.begin()]; bdd part = previous_class_[*it->second.begin()];
// The difference between the two next lines is: // The difference between the two next lines is:
// the first says "if you see A", the second "if you // the first says "if you see A", the second "if you
@ -472,11 +472,11 @@ namespace spot
bdd2state[relation_[part]] = current_max; bdd2state[relation_[part]] = current_max;
} }
// For each partition, we will create // For each partition, we will create
// all the transitions between the states. // all the transitions between the states.
for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end(); it != bdd_lstate_.end();
++it) ++it)
{ {
// Get the signature. // Get the signature.
bdd sig = compute_sig(*(it->second.begin())); bdd sig = compute_sig(*(it->second.begin()));
@ -494,80 +494,82 @@ namespace spot
// First loop over all possible valuations atomic properties. // First loop over all possible valuations atomic properties.
while (all_atomic_prop != bddfalse) while (all_atomic_prop != bddfalse)
{ {
bdd one = bdd_satoneset(all_atomic_prop, bdd one = bdd_satoneset(all_atomic_prop,
sup_all_atomic_prop, sup_all_atomic_prop,
bddtrue); bddtrue);
all_atomic_prop -= one; all_atomic_prop -= one;
// For each possible valuation, iterator over all possible // For each possible valuation, iterator over all possible
// destination classes. We use minato_isop here, because // destination classes. We use minato_isop here, because
// if the same valuation of atomic properties can go // if the same valuation of atomic properties can go
// to two different classes C1 and C2, iterating on // to two different classes C1 and C2, iterating on
// C1 + C2 with the above bdd_satoneset loop will see // C1 + C2 with the above bdd_satoneset loop will see
// C1 then (!C1)C2, instead of C1 then C2. // C1 then (!C1)C2, instead of C1 then C2.
// With minatop_isop, we ensure that the no negative // With minatop_isop, we ensure that the no negative
// class variable will be seen (likewise for promises). // class variable will be seen (likewise for promises).
minato_isop isop(sig & one); minato_isop isop(sig & one);
bdd cond_acc_dest; bdd cond_acc_dest;
while ((cond_acc_dest = isop.next()) != bddfalse) while ((cond_acc_dest = isop.next()) != bddfalse)
{ {
// Take the transition, and keep only the variable which // Take the transition, and keep only the variable which
// are used to represent the class. // are used to represent the class.
bdd dest = bdd_existcomp(cond_acc_dest, bdd dest = bdd_existcomp(cond_acc_dest,
all_class_var_); all_class_var_);
// Keep only ones who are acceptance condition. // Keep only ones who are acceptance condition.
bdd acc = bdd_existcomp(cond_acc_dest, sup_all_acc); bdd acc = bdd_existcomp(cond_acc_dest, sup_all_acc);
// Keep the other ! // Keep the other !
bdd cond = bdd_existcomp(cond_acc_dest, sup_all_atomic_prop); bdd cond = bdd_existcomp(cond_acc_dest,
sup_all_atomic_prop);
// Because we have complemented all the acceptance condition // Because we have complemented all the acceptance
// on the input automaton, we must re invert them to create // condition on the input automaton, we must re
// a new transition. // invert them to create a new transition.
acc = reverser.reverse_complement(acc); acc = reverser.reverse_complement(acc);
// Take the id of the source and destination. // Take the id of the source and destination. To
// To know the source, we must take a random state in the // know the source, we must take a random state in
// list which is in the class we currently work on. // the list which is in the class we currently
int src = bdd2state[previous_it_class_[*it->second.begin()]]; // work on.
int dst = bdd2state[dest]; int src = bdd2state[previous_class_[*it->second.begin()]];
int dst = bdd2state[dest];
// src or dst == 0 means "dest" or "prev..." isn't in the map. // src or dst == 0 means "dest" or "prev..." isn't
// so it is a bug. // in the map. so it is a bug.
assert(src != 0); assert(src != 0);
assert(dst != 0); assert(dst != 0);
// Create the transition, add the condition and the // Create the transition, add the condition and the
// acceptance condition. // acceptance condition.
tgba_explicit_number::transition* t tgba_explicit_number::transition* t
= res->create_transition(src , dst); = res->create_transition(src , dst);
res->add_conditions(t, cond); res->add_conditions(t, cond);
res->add_acceptance_conditions(t, acc); res->add_acceptance_conditions(t, acc);
} }
} }
} }
res->set_init_state(bdd2state[previous_it_class_ res->set_init_state(bdd2state[previous_class_
[a_->get_init_state()]]); [a_->get_init_state()]]);
res->merge_transitions(); res->merge_transitions();
return res; return res;
} }
// Debug: // Debug:
// In a first time, print the signature, and the print a list // In a first time, print the signature, and the print a list
// of each state in this partition. // of each state in this partition.
// In a second time, print foreach state, who is where, // In a second time, print foreach state, who is where,
// where is the new class name. // where is the new class name.
void print_partition() void print_partition()
{ {
for (map_bdd_lstate::iterator it = bdd_lstate_.begin(); for (map_bdd_lstate::iterator it = bdd_lstate_.begin();
it != bdd_lstate_.end(); it != bdd_lstate_.end();
++it) ++it)
{ {
std::cerr << "partition: " std::cerr << "partition: "
<< bdd_format_set(a_->get_dict(), it->first) << std::endl; << bdd_format_set(a_->get_dict(), it->first) << std::endl;
@ -575,70 +577,70 @@ namespace spot
for (std::list<const state*>::iterator it_s = it->second.begin(); for (std::list<const state*>::iterator it_s = it->second.begin();
it_s != it->second.end(); it_s != it->second.end();
++it_s) ++it_s)
{ {
std::cerr << " - " std::cerr << " - "
<< a_->format_state(*it_s) << std::endl; << a_->format_state(*it_s) << std::endl;
} }
} }
std::cerr << "\nPrevious iteration\n" << std::endl; std::cerr << "\nPrevious iteration\n" << std::endl;
for (map_state_bdd::const_iterator it = previous_it_class_.begin(); for (map_state_bdd::const_iterator it = previous_class_.begin();
it != previous_it_class_.end(); it != previous_class_.end();
++it) ++it)
{ {
std::cerr << a_->format_state(it->first) std::cerr << a_->format_state(it->first)
<< " was in " << " was in "
<< bdd_format_set(a_->get_dict(), it->second) << bdd_format_set(a_->get_dict(), it->second)
<< std::endl; << std::endl;
} }
} }
private: private:
// The automaton which is simulated. // The automaton which is simulated.
tgba_explicit_number* a_; tgba_explicit_number* a_;
// Relation is aimed to represent the same thing than // Relation is aimed to represent the same thing than
// rel_. The difference is in the way it does. // rel_. The difference is in the way it does.
// If A => A /\ A => B, rel will be (!A U B), but relation_ // If A => A /\ A => B, rel will be (!A U B), but relation_
// will have A /\ B at the key A. This trick is due to a problem // will have A /\ B at the key A. This trick is due to a problem
// with the computation of the resulting automaton with the signature. // with the computation of the resulting automaton with the signature.
// rel_ will pollute the meaning of the signature. // rel_ will pollute the meaning of the signature.
map_bdd_bdd relation_; map_bdd_bdd relation_;
// Represent the class of each state at the previous iteration. // Represent the class of each state at the previous iteration.
map_state_bdd previous_it_class_; map_state_bdd previous_class_;
// The class at the current iteration. // The class at the current iteration.
map_state_bdd current_class_; map_state_bdd current_class_;
// The list of state for each class at the current_iteration. // The list of state for each class at the current_iteration.
// Computed in `update_sig'. // Computed in `update_sig'.
map_bdd_lstate bdd_lstate_; map_bdd_lstate bdd_lstate_;
// The queue of free bdd. They will be used as the identifier // The queue of free bdd. They will be used as the identifier
// for the class. // for the class.
std::queue<int> free_var_; std::queue<int> free_var_;
// The list of used bdd. They are in used as identifier for class. // The list of used bdd. They are in used as identifier for class.
std::list<bdd> used_var_; std::list<bdd> used_var_;
// Size of the automaton. // Size of the automaton.
unsigned int size_a_; unsigned int size_a_;
// Used to know when there is no evolution in the po. Updated // Used to know when there is no evolution in the po. Updated
// in the `update_po' method. // in the `update_po' method.
unsigned int po_size_; unsigned int po_size_;
// All the class variable: // All the class variable:
bdd all_class_var_; bdd all_class_var_;
}; };
} // End namespace anonymous. } // End namespace anonymous.
tgba* tgba*
simulation(const tgba* t) simulation(const tgba* t)
{ {
Simulation simul(t); direct_simulation simul(t);
return simul.run(); return simul.run();
} }

2
src/tgbaalgos/simulation.hh
View file

@ -35,7 +35,7 @@ namespace spot
/// When the language recognized by one state is included in the /// When the language recognized by one state is included in the
/// language recognized by an another one, the first one is merged /// language recognized by an another one, the first one is merged
/// with the second. The algorithm is based on the following /// with the second. The algorithm is based on the following
/// paper, but generalized to handled TGBA directly. /// paper, but generalized to handle TGBA directly.
/// ///
/// \verbatim /// \verbatim
/// @InProceedings{ etessami.00.concur, /// @InProceedings{ etessami.00.concur,