From fac30eb08ee4015e89b0eb4235bb75f6651eec92 Mon Sep 17 00:00:00 2001 From: Felix Abecassis Date: Sat, 20 Mar 2010 14:51:02 +0100 Subject: [PATCH] Test program for the minimization algorithm. * src/tgbatest/minimize.cc: New file. Minimize an automaton from a LTL formula and compare the size of the initial automaton to the size of the minimized automaton. --- ChangeLog | 10 ++- src/tgbatest/Makefile.am | 2 + src/tgbatest/minimize.cc | 141 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 151 insertions(+), 2 deletions(-) create mode 100644 src/tgbatest/minimize.cc diff --git a/ChangeLog b/ChangeLog index 304b3033a..787c79129 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,9 +1,15 @@ 2010-03-20 Felix Abecassis - Algorithm to minimize an automaton. + Test program for the minimization algorithm. + + * src/tgbatest/minimize.cc: New file. Minimize an automaton + from a LTL formula and compare the size of the initial automaton + to the size of the minimized automaton. + +2010-03-20 Felix Abecassis * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh: - New files. Minimize an automaton using first the powerset + New files. Algorithm to minimize an automaton using first the powerset construction to determinize the input automaton, the automaton is then minimized using the standard algorithm, using BDDs to check if states are equivalent. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index cbac6e62b..f3867f054 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -38,6 +38,7 @@ check_PROGRAMS = \ expldot \ explprod \ ltlprod \ + minimize \ mixprod \ powerset \ reductgba \ @@ -56,6 +57,7 @@ expldot_CXXFLAGS = -DDOTTY explprod_SOURCES = explprod.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc +minimize_SOURCES = minimize.cc mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc diff --git a/src/tgbatest/minimize.cc b/src/tgbatest/minimize.cc new file mode 100644 index 000000000..954f4fd80 --- /dev/null +++ b/src/tgbatest/minimize.cc @@ -0,0 +1,141 @@ +// Copyright (C) 2010 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#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 +{ + unsigned tgba_size(const tgba* a) + { + typedef Sgi::hash_set hash_type; + hash_type seen; + std::queue tovisit; + // Perform breadth-first search. + state* init = a->get_init_state(); + tovisit.push(init); + seen.insert(init); + unsigned count = 0; + // While there are still states to visit. + while (!tovisit.empty()) + { + ++count; + state* cur = tovisit.front(); + tovisit.pop(); + tgba_succ_iterator* sit = a->succ_iter(cur); + for (sit->first(); !sit->done(); sit->next()) + { + state* dst = sit->current_state(); + // Is it a new state ? + if (seen.find(dst) == seen.end()) + { + // Yes, register the successor for later processing. + tovisit.push(dst); + seen.insert(dst); + } + else + // No, free dst. + delete dst; + } + delete sit; + } + hash_type::iterator it2; + // Free visited states. + for (it2 = seen.begin(); it2 != seen.end(); it2++) + delete *it2; + return count; + } +} + +// Compare the sizes of the initial and the minimal automata. +void compare_automata(const spot::tgba* a, + const spot::tgba* min_a) +{ + unsigned init_size = spot::tgba_size(a); + unsigned min_size = spot::tgba_size(min_a); + unsigned diff_size = init_size - min_size; + std::cout << init_size << " " << min_size << " " << diff_size << std::endl; +} + +void usage(const char* prog) +{ + std::cout << "Usage: " << prog << " ltl_file" << std::endl + << " " << prog << " -f formula" << std::endl; +} + +int main(int argc, char* argv[]) +{ + if (argc == 1) + { + usage(argv[0]); + return 1; + } + spot::bdd_dict* dict = new spot::bdd_dict(); + // Use the formula in argv[2] + if (!strcmp(argv[1], "-f")) + { + if (argc != 3) + { + usage(argv[0]); + return 1; + } + std::ofstream out_dot ("auto.dot"); + 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* res = minimize(a); + compare_automata(a, res); + spot::dotty_reachable(out_dot, det); + delete a; + delete res; + } + else + { + // Read a serie of formulae in a file. + spot::ltl::ltl_file formulae(argv[1]); + spot::ltl::formula* f; + while ((f = formulae.next())) + { + 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; + } + } +}