From 420fcd62e4d261e2c6da2ae6642d67e073e6ab1b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Sep 2012 18:05:34 +0200 Subject: [PATCH] Add a is_weak_scc() function based on cycle enumeration. * src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltl2tgba.cc: Add a -KW option. * src/tgbatest/cycles.test: Test it on a small example. --- src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/isweakscc.cc | 83 ++++++++++++++++++++++++++++++++++++++ src/tgbaalgos/isweakscc.hh | 47 +++++++++++++++++++++ src/tgbatest/cycles.test | 6 +++ src/tgbatest/ltl2tgba.cc | 20 +++++++++ 5 files changed, 158 insertions(+) create mode 100644 src/tgbaalgos/isweakscc.cc create mode 100644 src/tgbaalgos/isweakscc.hh diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 3f8e964d8..51d4e67bb 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -42,6 +42,7 @@ tgbaalgos_HEADERS = \ emptiness_stats.hh \ gv04.hh \ isdet.hh \ + isweakscc.hh \ lbtt.hh \ ltl2taa.hh \ ltl2tgba_fm.hh \ @@ -82,6 +83,7 @@ libtgbaalgos_la_SOURCES = \ emptiness.cc \ gv04.cc \ isdet.cc \ + isweakscc.cc \ lbtt.cc \ ltl2taa.cc \ ltl2tgba_fm.cc \ diff --git a/src/tgbaalgos/isweakscc.cc b/src/tgbaalgos/isweakscc.cc new file mode 100644 index 000000000..5409fdd17 --- /dev/null +++ b/src/tgbaalgos/isweakscc.cc @@ -0,0 +1,83 @@ +// Copyright (C) 2012 Laboratoire de Recherche et Developpement 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. + +#ifndef SPOT_TGBAALGOS_ISWEAKSCC_CC +# define SPOT_TGBAALGOS_ISWEAKSCC_CC + +#include "cycles.hh" + +namespace spot +{ + namespace + { + class weak_checker: public enumerate_cycles + { + public: + bool result; + + weak_checker(const tgba* aut, const scc_map& map) + : enumerate_cycles(aut, map), result(true) + { + } + + virtual bool + cycle_found(const state* start) + { + dfs_stack::const_iterator i = dfs.begin(); + bdd acc = bddfalse; + while (i->ts->first != start) + ++i; + do + { + acc |= i->succ->current_acceptance_conditions(); + ++i; + } + while (i != dfs.end()); + if (acc != aut_->all_acceptance_conditions()) + { + // We have found an non-accepting cycle, so the SCC is not + // weak. + result = false; + return false; + } + return true; + } + + }; + + } + + bool + is_weak_scc(const tgba* aut, scc_map& map, unsigned scc) + { + // If no cycle is accepting, the SCC is weak. + if (!map.accepting(scc)) + return true; + // If the SCC is accepting, but one cycle is not, the SCC is not + // weak. + weak_checker w(aut, map); + w.run(scc); + return w.result; + } + + +} + +#endif // SPOT_TGBAALGOS_ISWEAKSCC_CC diff --git a/src/tgbaalgos/isweakscc.hh b/src/tgbaalgos/isweakscc.hh new file mode 100644 index 000000000..b52f06c57 --- /dev/null +++ b/src/tgbaalgos/isweakscc.hh @@ -0,0 +1,47 @@ +// Copyright (C) 2012 Laboratoire de Recherche et Developpement 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. + +#ifndef SPOT_TGBAALGOS_ISWEAKSCC_HH +# define SPOT_TGBAALGOS_ISWEAKSCC_HH + +#include "scc.hh" + +namespace spot +{ + /// \addtogroup tgba_misc + /// @{ + + /// \brief Whether the SCC number \a scc in \a aut is weak. + /// + /// An SCC is weak if its cycles are all accepting, or the are all + /// non-accepting. + /// + /// The scc_map \a map should have been built already. The absence + /// of accepting cycle is easy to check (the scc_map can tell + /// whether the SCC is non-accepting already). For the accepting + /// SCC, this function works by enumerating all cycles in the given + /// SCC (it stops if it find a non-accepting cycle). + bool is_weak_scc(const tgba* aut, scc_map& map, unsigned scc); + + /// @} +} + + +#endif // SPOT_TGBAALGOS_ISWEAKSCC_HH diff --git a/src/tgbatest/cycles.test b/src/tgbatest/cycles.test index 4500c3390..0f8ba05ac 100755 --- a/src/tgbatest/cycles.test +++ b/src/tgbatest/cycles.test @@ -60,3 +60,9 @@ echo "s$x,s$w,,;" run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out test `wc -l < out` -eq 10 + + + +run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out +test `grep 'is weak' out | wc -l` -eq 4 +test `grep 'is not weak' out | wc -l` -eq 1 diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 3561a6369..5a0eeb322 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -65,6 +65,7 @@ #include "tgbaalgos/scc.hh" #include "tgbaalgos/isdet.hh" #include "tgbaalgos/cycles.hh" +#include "tgbaalgos/isweakscc.hh" #include "kripkeparse/public.hh" #include "tgbaalgos/simulation.hh" @@ -283,6 +284,7 @@ syntax(char* prog) << " -KV verbosely dump the graph of SCCs in dot format" << std::endl << " -KC list cycles in automaton" << std::endl + << " -KW list weak SCCs" << std::endl << " -N output the never clain for Spin (implies -DS)" << std::endl << " -NN output the never clain for Spin, with commented states" @@ -528,6 +530,10 @@ main(int argc, char** argv) { output = 15; } + else if (!strcmp(argv[formula_index], "-KW")) + { + output = 16; + } else if (!strcmp(argv[formula_index], "-l")) { translation = TransLaCIM; @@ -1428,6 +1434,20 @@ main(int argc, char** argv) } break; } + case 16: + { + spot::scc_map m(a); + m.build_map(); + unsigned max = m.scc_count(); + for (unsigned n = 0; n < max; ++n) + { + bool w = spot::is_weak_scc(a, m, n); + std::cout << "SCC #" << n + << (w ? " is weak" : " is not weak") + << std::endl; + } + break; + } default: assert(!"unknown output option");