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

mealy: make output_assignment the default for reduce_mealy

Browse source 
* spot/twaalgos/mealy_machine.hh: Here. Also cite the FORTE paper.
* doc/spot.bib (renkin.22.forte): New entry.
This commit is contained in:
Alexandre Duret-Lutz 2022-08-06 14:06:52 +02:00
parent b0165cf39c
commit de9041bb31
2 changed files with 38 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

30
doc/spot.bib
View file

@ -214,13 +214,13 @@
doi = {10.1109/DepCoS-RELCOMEX.2009.31}
}
@InProceedings{ cimatti.06.fmcad,
author = {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone and
Tonetta, Stefano},
title = {From {PSL} to {NBA}: a Modular Symbolic Encoding},
booktitle = {Proceedings of the 6th conference on Formal Methods in Computer
Aided Design (FMCAD'06)},
pages = {125--133},
@InProceedings{ cimatti.06.fmcad,
author = {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone
and Tonetta, Stefano},
title = {From {PSL} to {NBA}: a Modular Symbolic Encoding},
booktitle = {Proceedings of the 6th conference on Formal Methods in
Computer Aided Design (FMCAD'06)},
pages = {125--133},
year = {2006},
publisher = {IEEE Computer Society},
doi = {10.1109/FMCAD.2006.19}
@ -858,6 +858,22 @@
doi = {10.1007/978-3-030-59152-6_7}
}
@InProceedings{ renkin.22.forte,
author = {Florian Renkin and Philipp Schlehuber-Caissier and
Alexandre Duret-Lutz and Adrien Pommellet},
title = {Effective Reductions of {M}ealy Machines},
year = 2022,
booktitle = {Proceedings of the 42nd International Conference on Formal
Techniques for Distributed Objects, Components, and Systems
(FORTE'22)},
series = {Lecture Notes in Computer Science},
volume = 13273,
pages = {170--187},
month = jun,
publisher = {Springer},
doi = {10.1007/978-3-031-08679-3_8}
}
@InProceedings{ rozier.07.spin,
author = {Kristin Y. Rozier and Moshe Y. Vardi},
title = {LTL Satisfiability Checking},

26
spot/twaalgos/mealy_machine.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2021 Laboratoire de Recherche et Développement
// Copyright (C) 2021-2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -87,28 +87,30 @@ namespace spot
unsplit_mealy(const const_twa_graph_ptr& m);
/// \brief reduce an (in)completely specified mealy machine
/// Based on signature inclusion or equality. This is not guaranteed
/// to find the minimal number of states but is usually faster.
/// This also comes at another drawback:
/// All applicable sequences have to be infinite. Finite
/// traces are disregarded
/// \param mm The mealy machine to be minimized, has to be unsplit
///
/// This is a bisimulation based reduction, that optionally use
/// inclusion between signatures to force some output when there is
/// a choice in order to favor more reductions. Only infinite
/// traces are considered. See \cite renkin.22.forte for details.
///
/// \param mm The mealy machine to be minimized, has to be unsplit.
/// \param output_assignment Whether or not to use output assignment
/// \return A specialization of \c mm. Note that if mm is separated,
/// the returned machine is separated as well.
/// \note See todo TACAS22 Effective reductions of mealy machines
/// @{
/// @{
SPOT_API twa_graph_ptr
reduce_mealy(const const_twa_graph_ptr& mm,
bool output_assignment = false);
bool output_assignment = true);
SPOT_API void
reduce_mealy_here(twa_graph_ptr& mm,
bool output_assignment = false);
bool output_assignment = true);
/// @}
/// \brief Minimizes an (in)completely specified mealy machine
/// The approach is described in \todo TACAS
///
/// The approach is described in \cite renkin.22.forte.
///
/// \param premin Use reduce_mealy before applying the
/// main algorithm if demanded AND
/// the original machine has no finite trace.