Commit 420fcd62 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 374a489e
......@@ -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 \
......
// 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
// 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
......@@ -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
......@@ -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");
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment