From 52090e48752121b8da21c9c60de82df0c80e212d Mon Sep 17 00:00:00 2001 From: Felix Abecassis Date: Sat, 20 Mar 2010 15:23:19 +0100 Subject: [PATCH] Small fixes. * src/tgbatest/minimize.cc: Delete useless includes. * src/tgbaalgos/minimize.cc: Delete useless includes, fixed acceptance conditions. * src/tgbatest/ltl2tgba.cc: Add -Rm option for minimization. * src/tgba/tgbaexplicit.cc: Fixed typo. --- ChangeLog | 10 ++++++ src/tgba/tgbaexplicit.cc | 2 +- src/tgbaalgos/minimize.cc | 64 +++++++++++++++++++++++++-------------- src/tgbatest/ltl2tgba.cc | 11 +++++++ src/tgbatest/minimize.cc | 22 +++++++------- 5 files changed, 74 insertions(+), 35 deletions(-) diff --git a/ChangeLog b/ChangeLog index 787c79129..9f02e272c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2010-03-20 Felix Abecassis + + Small fixes. + + * src/tgbatest/minimize.cc: Delete useless includes. + * src/tgbaalgos/minimize.cc: Delete useless includes, + fixed acceptance conditions. + * src/tgbatest/ltl2tgba.cc: Add -Rm option for minimization. + * src/tgba/tgbaexplicit.cc: Fixed typo. + 2010-03-20 Felix Abecassis Test program for the minimization algorithm. diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index 1cbcc628c..88917cbae 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -358,7 +358,7 @@ namespace spot tgba_explicit::state::iterator i2; for (i2 = i->second->begin(); i2 != i->second->end(); ++i2) delete *i2; - // Advance the iterator before deleting the formula. + // Advance the iterator before deleting the state. delete i->second; ++i; } diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index 236b2f57f..cd81f11e4 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -18,10 +18,6 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include -#include -#include -#include #include #include "minimize.hh" #include "ltlast/allnodes.hh" @@ -44,14 +40,14 @@ namespace spot hash_map& state_set_map) { hash_set seen; - std::queue tovisit; + std::queue tovisit; // Perform breadth-first traversal. - state* init = a->get_init_state(); + const state* init = a->get_init_state(); tovisit.push(init); seen.insert(init); while (!tovisit.empty()) { - state* src = tovisit.front(); + const state* src = tovisit.front(); tovisit.pop(); // Is the state final ? if (final.find(src) == final.end()) @@ -65,7 +61,7 @@ namespace spot tgba_succ_iterator* sit = a->succ_iter(src); for (sit->first(); !sit->done(); sit->next()) { - state* dst = sit->current_state(); + const state* dst = sit->current_state(); // Is it a new state ? if (seen.find(dst) == seen.end()) { @@ -76,6 +72,7 @@ namespace spot else delete dst; } + delete sit; } } @@ -113,21 +110,24 @@ namespace spot const state* src = *hit; unsigned src_num = state_num[src]; tgba_succ_iterator* succit = a->succ_iter(src); - bool accepting = final->find(src) == final->end(); + bool accepting = (final->find(src) != final->end()); for (succit->first(); !succit->done(); succit->next()) { - state* dst = succit->current_state(); + const state* dst = succit->current_state(); unsigned dst_num = state_num[dst]; + delete dst; trs* t = res->create_transition(src_num, dst_num); res->add_conditions(t, succit->current_condition()); if (accepting) res->add_acceptance_condition(t, ltl::constant::true_instance()); } + delete succit; } } res->merge_transitions(); const state* init_state = a->get_init_state(); unsigned init_num = state_num[init_state]; + delete init_state; res->set_init_state(init_num); return res; } @@ -137,23 +137,25 @@ namespace spot // The list of accepting states of a. std::list acc_list; std::queue todo; + // The list of equivalent states. std::list done; tgba_explicit* det_a = tgba_powerset(a, &acc_list); - hash_set final; - hash_set non_final; + hash_set* final = new hash_set; + hash_set* non_final = new hash_set; hash_map state_set_map; std::list::iterator li; for (li = acc_list.begin(); li != acc_list.end(); ++li) - final.insert(*li); - init_sets(det_a, final, non_final, state_set_map); - if (final.size() > 1) - todo.push(&final); - else if (final.size() != 0) - done.push_back(&final); - if (non_final.size() > 1) - todo.push(&non_final); - else if (non_final.size() != 0) - done.push_back(&non_final); + final->insert(*li); + init_sets(det_a, *final, *non_final, state_set_map); + hash_set* final_copy = new hash_set(*final); + if (final->size() > 1) + todo.push(final); + else if (!final->empty()) + done.push_back(final); + if (non_final->size() > 1) + todo.push(non_final); + else if (!non_final->empty()) + done.push_back(non_final); unsigned set_num = 1; // A bdd_states_map is a list of formulae (in a BDD form) associated with a // destination set of states. @@ -175,8 +177,10 @@ namespace spot { const state* dst = si->current_state(); unsigned dst_set = state_set_map[dst]; + delete dst; f |= (bdd_ithvar(dst_set) & si->current_condition()); } + delete si; bdd_states_map::iterator bsi; // Have we already seen this formula ? for (bsi = bdd_map.begin(); bsi != bdd_map.end() && bsi->first != f; @@ -217,8 +221,22 @@ namespace spot todo.push(set); } } + delete cur; } - tgba_explicit_number* res = build_result(det_a, done, &final); + + // Build the result. + tgba_explicit_number* res = build_result(det_a, done, final_copy); + + // Free all the allocated memory. + delete final_copy; + hash_map::iterator hit; + for (hit = state_set_map.begin(); hit != state_set_map.end(); ++hit) + delete hit->first; + std::list::iterator it; + for (it = done.begin(); it != done.end(); ++it) + delete *it; + delete det_a; + return res; } } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index a352145a4..9eaa05204 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -47,6 +47,7 @@ #include "tgbaparse/public.hh" #include "neverparse/public.hh" #include "tgbaalgos/dupexp.hh" +#include "tgbaalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/reductgba_sim.hh" #include "tgbaalgos/replayrun.hh" @@ -207,6 +208,7 @@ syntax(char* prog) << std::endl << " -Rd display the simulation relation" << std::endl << " -RD display the parity game (dot format)" << std::endl + << " -Rm attempt to minimize the automata" << std::endl << std::endl << "Options for performing emptiness checks:" << std::endl @@ -309,6 +311,7 @@ main(int argc, char** argv) bool graph_run_opt = false; bool graph_run_tgba_opt = false; bool opt_reduce = false; + bool opt_minimize = false; bool containment = false; bool show_fc = false; bool spin_comments = false; @@ -617,6 +620,10 @@ main(int argc, char** argv) { display_parity_game = true; } + else if (!strcmp(argv[formula_index], "-Rm")) + { + opt_minimize = true; + } else if (!strcmp(argv[formula_index], "-s")) { dupexp = DFS; @@ -891,6 +898,10 @@ main(int argc, char** argv) a = state_labeled = new spot::tgba_sgba_proxy(a); } + spot::tgba_explicit* minimized = 0; + if (opt_minimize) + a = minimized = minimize(a); + spot::tgba_reduc* aut_red = 0; if (reduc_aut != spot::Reduce_None) { diff --git a/src/tgbatest/minimize.cc b/src/tgbatest/minimize.cc index 954f4fd80..5f193de42 100644 --- a/src/tgbatest/minimize.cc +++ b/src/tgbatest/minimize.cc @@ -19,20 +19,14 @@ // 02111-1307, USA. #include -#include -#include +#include #include "ltlast/unop.hh" #include "tgbaalgos/dotty.hh" -#include "tgbaalgos/prettydotdec.hh" -#include "tgbaalgos/rundotdec.hh" #include "tgbaalgos/minimize.hh" #include "tgbaalgos/powerset.hh" -#include "tgbaalgos/scc.hh" #include "ltlparse/public.hh" -#include "ltlvisit/tostring.hh" #include "tgba/tgbaexplicit.hh" #include "ltlparse/ltlfile.hh" -#include "tgbaparse/public.hh" #include "tgbaalgos/ltl2tgba_fm.hh" namespace spot @@ -115,12 +109,14 @@ int main(int argc, char* argv[]) spot::ltl::parse_error_list pel; spot::ltl::formula* f = spot::ltl::parse(argv[2], pel); spot::tgba_explicit* a = ltl_to_tgba_fm(f, dict, true); - spot::tgba_explicit* det = spot::tgba_powerset(a); +// spot::tgba_explicit* det = spot::tgba_powerset(a); spot::tgba_explicit* res = minimize(a); compare_automata(a, res); - spot::dotty_reachable(out_dot, det); + spot::dotty_reachable(out_dot, res); +// delete det; delete a; delete res; + f->destroy(); } else { @@ -129,13 +125,17 @@ int main(int argc, char* argv[]) spot::ltl::formula* f; while ((f = formulae.next())) { - spot::ltl::formula* f_neg = spot::ltl::unop::instance(spot::ltl::unop::Not, - f->clone()); + spot::ltl::formula* f_neg = + spot::ltl::unop::instance(spot::ltl::unop::Not, + f->clone()); spot::tgba_explicit* a = ltl_to_tgba_fm(f_neg, dict, true); spot::tgba_explicit* res = minimize(a); compare_automata(a, res); delete a; delete res; + f->destroy(); + f_neg->destroy(); } } + delete dict; }