f120dd3206
* NEWS: Mention the change. * src/: Rename as ... * spot/: ... this, adjust all headers to include <spot/...> instead of "...", and adjust all Makefile.am to search headers from the top-level directory. * HACKING: Add conventions about #include. * spot/sanity/style.test: Add a few more grep to catch cases that do not follow these conventions. * .gitignore, Makefile.am, README, bench/stutter/Makefile.am, bench/stutter/stutter_invariance_formulas.cc, bench/stutter/stutter_invariance_randomgraph.cc, configure.ac, debian/rules, doc/Doxyfile.in, doc/Makefile.am, doc/org/.dir-locals.el.in, doc/org/g++wrap.in, doc/org/init.el.in, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut30.org, iface/ltsmin/Makefile.am, iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc, wrap/python/Makefile.am, wrap/python/ajax/spotcgi.in, wrap/python/spot_impl.i, wrap/python/tests/ltl2tgba.py, wrap/python/tests/randgen.py, wrap/python/tests/run.in: Adjust.
76 lines
2.7 KiB
C++
76 lines
2.7 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
#pragma once
|
|
|
|
#include <spot/ta/ta.hh>
|
|
#include <spot/ta/tgta.hh>
|
|
#include <spot/ta/tgtaexplicit.hh>
|
|
|
|
namespace spot
|
|
{
|
|
/// \addtogroup ta_reduction
|
|
/// @{
|
|
|
|
|
|
/// \brief Construct a simplified TA by merging bisimilar states.
|
|
///
|
|
/// A TA automaton can be simplified by merging bisimilar states:
|
|
/// Two states are bisimilar if the automaton can accept the
|
|
/// same executions starting for either of these states. This can be
|
|
/// achieved using any algorithm based on partition refinement
|
|
///
|
|
/// For more detail about this type of algorithm, see the following paper:
|
|
/** \verbatim
|
|
@InProceedings{valmari.09.icatpn,
|
|
author = {Antti Valmari},
|
|
title = {Bisimilarity Minimization in in O(m logn) Time},
|
|
booktitle = {Proceedings of the 30th International Conference on
|
|
the Applications and Theory of Petri Nets
|
|
(ICATPN'09)},
|
|
series = {Lecture Notes in Computer Science},
|
|
publisher = {Springer},
|
|
isbn = {978-3-642-02423-8},
|
|
pages = {123--142},
|
|
volume = 5606,
|
|
url = {http://dx.doi.org/10.1007/978-3-642-02424-5_9},
|
|
year = {2009}
|
|
}
|
|
\endverbatim */
|
|
///
|
|
/// \param ta_ the TA automaton to convert into a simplified TA
|
|
SPOT_API ta_explicit_ptr
|
|
minimize_ta(const const_ta_ptr& ta_);
|
|
|
|
|
|
|
|
/// \brief Construct a simplified TGTA by merging bisimilar states.
|
|
///
|
|
/// A TGTA automaton can be simplified by merging bisimilar states:
|
|
/// Two states are bisimilar if the automaton can accept the
|
|
/// same executions starting for either of these states. This can be
|
|
/// achieved using same algorithm used to simplify a TA taking into account
|
|
/// the acceptance conditions of the outgoing transitions.
|
|
///
|
|
/// \param tgta_ the TGTA automaton to convert into a simplified TGTA
|
|
SPOT_API tgta_explicit_ptr
|
|
minimize_tgta(const const_tgta_explicit_ptr& tgta_);
|
|
|
|
/// @}
|
|
}
|