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

Properly free memory and print logs

Browse source 
* src/tgbatest/ltl2tgba.cc: Properly free memory
* src/taalgos/tgba2ta.cc, src/taalgos/emptinessta.cc: print logs
This commit is contained in:
Ala-Eddine Ben-Salem 2011-08-31 18:32:25 +02:00 • committed by Alexandre Duret-Lutz
parent 83e7f0fa18
commit 422bb842bf
3 changed files with 34 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/taalgos/emptinessta.cc
View file

@ -276,6 +276,9 @@ namespace spot
std::list<state*> rem;
bool acc = false;
trace
<< "***PASS 1: CYCLE***" << std::endl;
while (threshold < scc.top().index)
{
assert(!scc.empty());
@ -306,15 +309,23 @@ namespace spot
if (is_accepting_sscc)
{
clear(h, todo, init_set);
trace
<< "PASS 1: SUCCESS" << std::endl;
<< "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " << a_->is_livelock_accepting_state(curr) << std::endl;
trace
<< "PASS 1: scc.top().condition : " << bdd_format_accset(a_->get_dict(),
scc.top().condition) << std::endl;
trace
<< "PASS 1: a_->all_acceptance_conditions() : " << bdd_format_accset(a_->get_dict(),
a_->all_acceptance_conditions()) << std::endl;
<< "PASS 1: a_->all_acceptance_conditions() : " << (scc.top().condition == a_->all_acceptance_conditions()) << std::endl;
trace
<< "PASS 1: bddtrue : " << (a_->all_acceptance_conditions()==
bddtrue) << std::endl;
trace
<< "PASS 1: bddfalse : " << (a_->all_acceptance_conditions()==
bddfalse) << std::endl;
clear(h, todo, init_set);
return true;
}

16
src/taalgos/tgba2ta.cc
View file

@ -18,6 +18,17 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#define TRACE
#include <iostream>
#ifdef TRACE
#define trace std::clog
#else
#define trace while (0) std::clog
#endif
#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "tgba/formula2bdd.hh"
@ -441,6 +452,9 @@ namespace spot
if (*spi.second == -1)
continue;
trace
<< "***compute_livelock_acceptance_states: CYCLE***" << std::endl;
if (!curr->compare(dest))
{
state_ta_explicit * self_loop_state =
@ -449,6 +463,8 @@ namespace spot
if (testing_automata->is_accepting_state(self_loop_state))
self_loop_state->set_livelock_accepting_state(true);
trace
<< "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" << std::endl;
}

4
src/tgbatest/ltl2tgba.cc
View file

@ -1136,7 +1136,9 @@ main(int argc, char** argv)
}
delete testing_automata_nm;
delete testing_automata;
//delete testing_automata;
a = 0;
degeneralized = 0;
output = -1;
}