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

cleanacc: cleanup documentation and API

Browse source 
* spot/twaalgos/cleanacc.hh: Fix Doxygen comments, and
add a strip argument to cleanup_acceptance().
* spot/twaalgos/cleanacc.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2019-04-26 11:34:50 +02:00
parent 7300488a24
commit 653ffcebe1
2 changed files with 20 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

7
spot/twaalgos/cleanacc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -68,9 +68,10 @@ namespace spot
return cleanup_acceptance_here(aut, strip);
}
twa_graph_ptr cleanup_acceptance(const_twa_graph_ptr aut)
twa_graph_ptr cleanup_acceptance(const_twa_graph_ptr aut, bool strip)
{
return cleanup_acceptance_here(make_twa_graph(aut, twa::prop_set::all()));
return cleanup_acceptance_here(make_twa_graph(aut, twa::prop_set::all()),
strip);
}
namespace

33
spot/twaalgos/cleanacc.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et
// Copyright (C) 2015, 2017-2019 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -23,37 +23,33 @@
namespace spot
{
/// @{
/// \ingroup twa_acc_transform
/// \brief Remove useless acceptance sets
///
/// This removes from the automaton the acceptance marks that are
/// not used in the acceptance condition. This also removes from
/// the acceptance conditions the terms that corresponds to empty
/// or full sets.
/// Removes from \a aut the acceptance marks that are not used
/// in its acceptance condition. Also removes from the acceptance
/// conditions the terms that corresponds to empty or full sets.
///
/// If \a strip is true (the default), the remaining acceptance set
/// numbers will be shifted down to reduce maximal number of
/// numbers will be shifted down to reduce the maximal number of
/// acceptance sets used.
///
/// cleanup_acceptance_here() works in place, cleanup_acceptance()
/// returns a new automaton that has been simplified.
SPOT_API twa_graph_ptr
cleanup_acceptance_here(twa_graph_ptr aut, bool strip = true);
/// \ingroup twa_acc_transform
/// \brief Remove useless acceptance sets
///
/// This removes from the automaton the acceptance marks that are
/// not used in the acceptance condition. This also removes from
/// the acceptance conditions the terms that corresponds to empty
/// or full sets.
///
SPOT_API twa_graph_ptr
cleanup_acceptance(const_twa_graph_ptr aut);
cleanup_acceptance(const_twa_graph_ptr aut, bool strip = true);
/// @}
/// @{
/// \ingroup twa_acc_transform
/// \brief Simplify an acceptance condition
///
/// Does evereything cleanup_acceptance() does, but additionally:
/// merge identical sets, detect whether to sets i and j are
/// Does everything cleanup_acceptance() does, but additionally:
/// merge identical sets, detect whether two sets i and j are
/// complementary to apply the following reductions:
/// - `Fin(i) & Inf(j) = Fin(i)`
/// - `Fin(i) & Fin(j) = f`
@ -61,6 +57,9 @@ namespace spot
/// - `Fin(i) | Inf(j) = Inf(j)`
/// - `Inf(i) | Inf(j) = t`
/// - `Fin(i) | Inf(i) = t`
///
/// simplify_acceptance_here() works in place, simplify_acceptance()
/// returns a new automaton that has been simplified.
SPOT_API twa_graph_ptr
simplify_acceptance_here(twa_graph_ptr aut);