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

bib: more references

Browse source 
* doc/spot.bib (blahoudek.16.atva, degiacomo.13.ijcai): New entries.
* spot/tl/ltlf.hh, spot/twaalgos/complement.hh: Use them.
This commit is contained in:
Alexandre Duret-Lutz 2022-01-14 15:49:23 +01:00
parent fc92c88cdb
commit b2b37ba3e9
3 changed files with 48 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/tl/ltlf.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2016 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -27,7 +27,7 @@ namespace spot
/// \brief Convert an LTLf into an LTL formula.
///
/// This is based on De Giacomo & Vardi (IJCAI'13) reduction from
/// LTLf (finite-LTL) to LTL.
/// LTLf (finite-LTL) to LTL. \cite degiacomo.13.ijcai
///
/// In this reduction, finite words are extended into infinite words
/// in which a new atomic proposition <code>alive</code> marks the

6
spot/twaalgos/complement.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013-2015, 2017, 2019 Laboratoire de Recherche et
// Copyright (C) 2013-2015, 2017, 2019, 2022 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -49,8 +49,8 @@ namespace spot
///
/// The automaton \a aut should be semideterministic.
///
/// Uses the NCSB algorithm described by F. Blahoudek, M. Heizmann,
/// S. Schewe, J. Strejček, and MH. Tsai (TACAS'16).
/// Uses the NCSB algorithm described by F. Blahoudek, et al.
/// \cite blahoudek.16.atva
SPOT_API twa_graph_ptr
complement_semidet(const const_twa_graph_ptr& aut, bool show_names = false);