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

Remove is_syntactic_weak_scc and is_syntactic_terminal_scc

Browse source 
Those cannot work now that automata are not labeled by formulas
anymore.

* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh
(is_syntactic_weak_scc, is_syntactic_terminal_scc): Remove.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-10 18:03:59 +02:00
parent ead04cb1ac
commit 57e7bbb3b1
2 changed files with 2 additions and 62 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/tgbaalgos/isweakscc.cc
View file

@ -89,44 +89,6 @@ namespace spot
== bdd_support(map.get_aut()->neg_acceptance_conditions()));
}
bool
is_syntactic_weak_scc(scc_map& map, unsigned scc)
{
const tgba_explicit_formula* aut =
dynamic_cast<const tgba_explicit_formula*>(map.get_aut());
if (!aut)
return false;
for (auto ss: map.states_of(scc))
{
const state_explicit_formula* s =
down_cast<const state_explicit_formula*>(ss);
assert(s);
if (aut->get_label(s)->is_syntactic_persistence())
return true;
}
return false;
}
bool
is_syntactic_terminal_scc(scc_map& map, unsigned scc)
{
const tgba_explicit_formula* aut =
dynamic_cast<const tgba_explicit_formula*>(map.get_aut());
if (!aut)
return false;
for (auto ss: map.states_of(scc))
{
const state_explicit_formula* s =
down_cast<const state_explicit_formula*>(ss);
assert(s);
if (aut->get_label(s)->is_syntactic_guarantee())
return true;
}
return false;
}
bool
is_complete_scc(scc_map& map, unsigned scc)
{

26
src/tgbaalgos/isweakscc.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -66,28 +66,6 @@ namespace spot
SPOT_API bool
is_complete_scc(scc_map& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is syntactically
/// weak.
///
/// This works only on tgba whose labels are formulas. An SCC is
/// syntactically weak if one of its states is labeled by a
/// syntactic-persistence formula.
///
/// The scc_map \a map should have been built already.
SPOT_API bool
is_syntactic_weak_scc(scc_map& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is syntactically
/// terminal.
///
/// This works only on tgba whose labels are formulas. An SCC is
/// syntactically terminal if one of its states is labeled by a
/// syntactic-guarantee formula.
///
/// The scc_map \a map should have been built already.
SPOT_API bool
is_syntactic_terminal_scc(scc_map& map, unsigned scc);
/// \brief Whether the SCC number \a scc in \a map is terminal.
///
/// An SCC is terminal if it is weak, complete, and accepting.