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

use a bibtex file to collect all references in Doxygen

Browse source 
* doc/tl/tl.bib: Move ...
* doc/spot.bib: ... here, and augment it with all references that
appeared verbatim in Doxygen comments.
* doc/Makefile.am, doc/tl/Makefile.am
doc/tl/tl.tex: Adjust for the move.
* doc/Doxyfile.in: Point to spot.bib.
* spot/gen/automata.hh, spot/gen/formulas.hh, spot/misc/game.hh,
spot/misc/minato.hh spot/taalgos/emptinessta.hh,
spot/taalgos/minimize.hh, spot/taalgos/tgba2ta.hh, spot/tl/formula.hh,
spot/tl/remove_x.hh, spot/tl/simplify.hh, spot/tl/snf.hh,
spot/twaalgos/cobuchi.hh, spot/twaalgos/cycles.hh,
spot/twaalgos/dualize.hh, spot/twaalgos/gtec/gtec.hh,
spot/twaalgos/gv04.hh, spot/twaalgos/ltl2taa.hh,
spot/twaalgos/ltl2tgba_fm.hh, spot/twaalgos/magic.hh,
spot/twaalgos/minimize.hh, spot/twaalgos/parity.hh,
spot/twaalgos/powerset.hh, spot/twaalgos/randomgraph.hh,
spot/twaalgos/se05.hh, spot/twaalgos/simulation.hh,
spot/twaalgos/strength.hh, spot/twaalgos/stutter.hh,
spot/twaalgos/tau03.hh, spot/twaalgos/totgba.hh,
spot/twaalgos/toweak.hh: Use \cite instead of a verbatim bibtex entry.
This commit is contained in:
Alexandre Duret-Lutz 2019-06-14 15:53:52 +02:00
parent d064b7dad2
commit df326e032b
36 changed files with 966 additions and 1225 deletions
Download patch file Download diff file Expand all files Collapse all files

80
spot/gen/automata.hh
View file

@ -27,6 +27,12 @@ namespace spot
{
namespace gen
{
/// \defgroup gen Hard-coded families of formulas or automata.
/// @{
/// \defgroup genaut Hard-coded families of automata.
/// @{
/// \brief Identifiers for automaton patterns
enum aut_pattern_id {
AUT_BEGIN = 256,
/// \brief A family of co-Büchi automata.
@ -34,23 +40,9 @@ namespace spot
/// Builds a co-Büchi automaton of size 2n+1 that is
/// good-for-games and that has no equivalent deterministic
/// co-Büchi automaton with less than 2^n / (2n+1) states.
/// \cite kuperberg.15.icalp
///
/// Only defined for n>0.
///
/** \verbatim
@InProceedings{ kuperberg.15.icalp,
author = {Denis Kuperberg and Micha{\l} Skrzypczak },
title = {On Determinisation of Good-for-Games Automata},
booktitle = {Proceedings of the 42nd International Colloquium on
Automata, Languages, and Programming (ICALP'15)},
pages = {299--310},
year = {2015},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 9135,
doi = {10.1007/978-3-662-47666-6_24}
}
\endverbatim */
AUT_KS_NCA = AUT_BEGIN,
/// \brief Hard-to-complement non-deterministic Büchi automata
///
@ -59,27 +51,10 @@ namespace spot
/// at least n! states if Streett acceptance is used.
///
/// Only defined for n>0. The automaton constructed corresponds
/// to the right part of Fig.1 in the following paper, except
/// to the right part of Fig.1 of \cite loding.99.fstts , except
/// that only state q_1 is initial. (The fact that states q_2,
/// q_3, ..., and q_n are not initial as in the paper does not
/// change the recognized language.)
///
/** \verbatim
@InProceedings{loding.99.fstts,
author = {Christof L{\"o}ding},
title = {Optimal Bounds for Transformations of
$\omega$-Automata},
booktitle = {Proceedings of the 19th Conference on Foundations of
Software Technology and Theoretical Computer Science
(FSTTCS'99)},
year = 1999,
publisher = {Springer},
pages = {97--109},
series = {Lecture Notes in Computer Science},
volume = 1738,
doi = {10.1007/3-540-46691-6_8}
}
\endverbatim */
AUT_L_NBA,
/// \brief DSA hard to convert to DRA.
///
@ -90,43 +65,15 @@ namespace spot
/// Only defined for 1<n<=16 because Spot does not support more
/// than 32 acceptance pairs.
///
/// This automaton corresponds to the right part of Fig.2 in the
/// following paper.
/** \verbatim
@InProceedings{loding.99.fstts,
author = {Christof L{\"o}ding},
title = {Optimal Bounds for Transformations of
$\omega$-Automata},
booktitle = {Proceedings of the 19th Conference on Foundations of
Software Technology and Theoretical Computer Science
(FSTTCS'99)},
year = 1999,
publisher = {Springer},
pages = {97--109},
series = {Lecture Notes in Computer Science},
volume = 1738,
doi = {10.1007/3-540-46691-6_8}
}
\endverbatim */
/// This automaton corresponds to the right part of Fig.2 of
/// \cite loding.99.fstts .
AUT_L_DSA,
/// \brief An NBA with (n+1) states whose complement needs ≥n! states
///
/// This automaton is usually attributed to Max Michel (1988),
/// who described it in some unpublished documents. Other
/// who described it in some unpublished document. Other
/// descriptions of this automaton can be found in a number
/// of papers, like:
/** \verbatim
@InBook{thomas.97.chapter,
author = {Wolfgang Thomas},
title = {Languages, Automata, and Logic},
booktitle = {Handbook of Formal Languages ---
Volume 3 Beyond Words},
editor = {Grzegorz Rozenberg and Arto Salomaa},
chapter = 7,
publisher = {Springer-Verlag},
year = {1997}
}
\endverbatim */
/// of papers \cite thomas.97.chapter .
///
/// Our implementation uses $\lceil \log_2(n+1)\rceil$ atomic
/// propositions to encode the $n+1$ letters used in the
@ -153,5 +100,8 @@ namespace spot
/// The returned name is suitable to be used as an option
/// key for the genaut binary.
SPOT_API const char* aut_pattern_name(aut_pattern_id pattern);
/// @}
/// @}
}
}

279
spot/gen/formulas.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Developpement de
// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Developpement de
// l'EPITA (LRDE).
//
// This file is part of Spot, a model checking library.
@ -21,241 +21,151 @@
#include <spot/tl/formula.hh>
// Families defined here come from the following papers:
//
// @InProceedings{cichon.09.depcos,
// author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski},
// title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL} Formulas},
// booktitle = {Proceedings of the Fourth International Conference on
// Dependability of Computer Systems},
// pages = {17--24},
// year = 2009,
// publisher = {IEEE Computer Society},
// }
//
// @InProceedings{geldenhuys.06.spin,
// author = {Jaco Geldenhuys and Henri Hansen},
// title = {Larger Automata and Less Work for LTL Model Checking},
// booktitle = {Proceedings of the 13th International SPIN Workshop},
// year = {2006},
// pages = {53--70},
// series = {Lecture Notes in Computer Science},
// volume = {3925},
// publisher = {Springer}
// }
//
// @InProceedings{gastin.01.cav,
// author = {Paul Gastin and Denis Oddoux},
// title = {Fast {LTL} to {B\"u}chi Automata Translation},
// booktitle = {Proceedings of the 13th International Conference on
// Computer Aided Verification (CAV'01)},
// pages = {53--65},
// year = 2001,
// editor = {G. Berry and H. Comon and A. Finkel},
// volume = {2102},
// series = {Lecture Notes in Computer Science},
// address = {Paris, France},
// publisher = {Springer-Verlag}
// }
//
// @InProceedings{rozier.07.spin,
// author = {Kristin Y. Rozier and Moshe Y. Vardi},
// title = {LTL Satisfiability Checking},
// booktitle = {Proceedings of the 12th International SPIN Workshop on
// Model Checking of Software (SPIN'07)},
// pages = {149--167},
// year = {2007},
// volume = {4595},
// series = {Lecture Notes in Computer Science},
// publisher = {Springer-Verlag}
// }
//
// @InProceedings{dwyer.98.fmsp,
// author = {Matthew B. Dwyer and George S. Avrunin and James C. Corbett},
// title = {Property Specification Patterns for Finite-state
// Verification},
// booktitle = {Proceedings of the 2nd Workshop on Formal Methods in
// Software Practice (FMSP'98)},
// publisher = {ACM Press},
// address = {New York},
// editor = {Mark Ardis},
// month = mar,
// year = {1998},
// pages = {7--15}
// }
//
// @InProceedings{etessami.00.concur,
// author = {Kousha Etessami and Gerard J. Holzmann},
// title = {Optimizing {B\"u}chi Automata},
// booktitle = {Proceedings of the 11th International Conference on
// Concurrency Theory (Concur'00)},
// pages = {153--167},
// year = {2000},
// editor = {C. Palamidessi},
// volume = {1877},
// series = {Lecture Notes in Computer Science},
// address = {Pennsylvania, USA},
// publisher = {Springer-Verlag}
// }
//
// @InProceedings{somenzi.00.cav,
// author = {Fabio Somenzi and Roderick Bloem},
// title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
// booktitle = {Proceedings of the 12th International Conference on
// Computer Aided Verification (CAV'00)},
// pages = {247--263},
// year = {2000},
// volume = {1855},
// series = {Lecture Notes in Computer Science},
// address = {Chicago, Illinois, USA},
// publisher = {Springer-Verlag}
// }
//
// @InProceedings{tabakov.10.rv,
// author = {Deian Tabakov and Moshe Y. Vardi},
// title = {Optimized Temporal Monitors for {SystemC}},
// booktitle = {Proceedings of the 1st International Conference on Runtime
// Verification (RV'10)},
// pages = {436--451},
// year = 2010,
// volume = {6418},
// series = {Lecture Notes in Computer Science},
// month = nov,
// publisher = {Springer}
// }
//
// @InProceedings{kupferman.10.mochart,
// author = {Orna Kupferman and And Rosenberg},
// title = {The Blow-Up in Translating LTL do Deterministic Automata},
// booktitle = {Proceedings of the 6th International Workshop on Model
// Checking and Artificial Intelligence (MoChArt 2010)},
// pages = {85--94},
// year = 2011,
// volume = {6572},
// series = {Lecture Notes in Artificial Intelligence},
// month = nov,
// publisher = {Springer}
// }
//
// @techreport{holevek.04.tr,
// title = {Verification Results in {Liberouter} Project},
// author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak
// and D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek},
// month = {September},
// year = 2004,
// number = 03,
// institution = {CESNET}
// }
//
// @InProceedings{pelanek.07.spin,
// author = {Radek Pel\'{a}nek},
// title = {{BEEM}: benchmarks for explicit model checkers},
// booktitle = {Proceedings of the 14th international SPIN conference on
// Model checking software},
// year = 2007,
// pages = {263--267},
// numpages = {5},
// volume = {4595},
// series = {Lecture Notes in Computer Science},
// publisher = {Springer-Verlag}
// }
//
// @InProceedings{muller.17.gandalf,
// author = {David M\"uller and Salomon Sickert},
// title = {{LTL} to Deterministic {E}merson-{L}ei Automata},
// booktitle = {Proceedings of the 8th International Sumposium on Games,
// Automata, Logics and Formal Verification (GandALF'17)},
// year = 2017,
// publisher = {Springer-Verlag}
// series = {Electronic Proceedings in Theoretical Computer Science},
// volume = {256},
// publisher = {Open Publishing Association},
// pages = {180--194},
// doi = {10.4204/EPTCS.256.13}
// }
//
// @InProceedings{sickert.16.cav,
// author = {Salomon Sickert and Javier Esparza and Stefaan Jaax
// and Jan K{\v{r}}et{\'i}nsk{\'y}},
// title = {Limit-Deterministic {B\"u}chi Automata for Linear Temporal Logic}
// booktitle = {Proceedings of the 28th International Conference on
// Computer Aided Verification (CAV'16)},
// year = 2016,
// publisher = {Springer-Verlag}
// series = {Lecture Notes in Computer Science},
// volume = {9780},
// pages = {312--332},
// doi = {10.1007/978-3-319-41540-6_17}
// }
//
// @InProceedings{kretisnky.12.cav,
// author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza},
// title = {Deterministic Automata for the {(F,G)}-Fragment of
// {LTL}},
// booktitle = {24th International Conference on Computer Aided
// Verification (CAV'12)},
// year = 2012,
// pages = {7--22},
// doi = {10.1007/978-3-642-31424-7_7},
// url = {https://doi.org/10.1007/978-3-642-31424-7_7},
// isbn = {978-3-642-31424-7},
// publisher = {Springer},
// }
namespace spot
{
namespace gen
{
/// \ingroup gen
/// \defgroup genltl Hard-coded families of formulas.
/// @{
/// \brief Identifiers for formula patterns
enum ltl_pattern_id {
LTL_BEGIN = 256,
/// `F(p1)&F(p2)&...&F(pn)`
/// \cite geldenhuys.06.spin
LTL_AND_F = LTL_BEGIN,
/// `FG(p1)&FG(p2)&...&FG(pn)`
LTL_AND_FG,
/// `GF(p1)&GF(p2)&...&GF(pn)`
/// \cite cichon.09.depcos ,
/// \cite geldenhuys.06.spin .
LTL_AND_GF,
/// `F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))`
/// \cite cichon.09.depcos
LTL_CCJ_ALPHA,
/// `F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))`
/// \cite cichon.09.depcos
LTL_CCJ_BETA,
/// `F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q)))`
/// \cite cichon.09.depcos
LTL_CCJ_BETA_PRIME,
/// 55 specification patterns from Dwyer et al.
/// \cite dwyer.98.fmsp
LTL_DAC_PATTERNS,
/// 12 formulas from Etessami and Holzmann.
/// \cite etessami.00.concur
LTL_EH_PATTERNS,
/// `F(p0 | XG(p1 | XG(p2 | ... XG(pn))))`
LTL_FXG_OR,
/// `(GFa1 & GFa2 & ... & GFan) <-> GFz`
LTL_GF_EQUIV,
/// `GF(a <-> X[n](a))`
LTL_GF_EQUIV_XN,
/// `(GFa1 & GFa2 & ... & GFan) -> GFz`
LTL_GF_IMPLIES,
/// `GF(a -> X[n](a))`
LTL_GF_IMPLIES_XN,
/// `(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))`
/// \cite geldenhuys.06.spin
LTL_GH_Q,
/// `(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))`
/// \cite geldenhuys.06.spin
LTL_GH_R,
/// `!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))`
/// \cite gastin.01.cav
LTL_GO_THETA,
/// `G(p0 & XF(p1 & XF(p2 & ... XF(pn))))`
LTL_GXF_AND,
/// 55 patterns from the Liberouter project.
/// \cite holevek.04.tr
LTL_HKRSS_PATTERNS,
/// Linear formula with doubly exponential DBA.
/// \cite kupferman.10.mochart
LTL_KR_N,
/// Quasilinear formula with doubly exponential DBA.
/// \cite kupferman.10.mochart
LTL_KR_NLOGN,
/// Quadratic formula with doubly exponential DBA.
/// \cite kupferman.10.mochart ,
/// \cite kupferman.05.tcl .
LTL_KV_PSI,
/// `GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))`
/// \cite muller.17.gandalf
LTL_MS_EXAMPLE,
/// `FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...`
/// \cite muller.17.gandalf
LTL_MS_PHI_H,
/// `(FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))`
/// \cite muller.17.gandalf
LTL_MS_PHI_R,
/// `(FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))`
/// \cite muller.17.gandalf
LTL_MS_PHI_S,
/// `FG(p1)|FG(p2)|...|FG(pn)`
/// \cite cichon.09.depcos
LTL_OR_FG,
/// `G(p1)|G(p2)|...|G(pn)`
/// \cite geldenhuys.06.spin
LTL_OR_G,
/// `GF(p1)|GF(p2)|...|GF(pn)`
/// \cite geldenhuys.06.spin
LTL_OR_GF,
/// 20 formulas from BEEM.
/// \cite pelanek.07.spin
LTL_P_PATTERNS,
/// `(((p1 R p2) R p3) ... R pn)`
LTL_R_LEFT,
/// `(p1 R (p2 R (... R pn)))`
LTL_R_RIGHT,
/// n-bit counter
/// \cite rozier.07.spin
LTL_RV_COUNTER,
/// n-bit counter with carry
/// \cite rozier.07.spin
LTL_RV_COUNTER_CARRY,
/// linear-size formular for an n-bit counter with carry
/// \cite rozier.07.spin
LTL_RV_COUNTER_CARRY_LINEAR,
/// linear-size formular for an n-bit counter
/// \cite rozier.07.spin
LTL_RV_COUNTER_LINEAR,
/// 27 formulas from Somenzi and Bloem
/// \cite somenzi.00.cav
LTL_SB_PATTERNS,
/// `f(0,j)=(GFa0 U X^j(b))`, `f(i,j)=(GFai U G(f(i-1,j)))`
/// \cite sickert.16.cav
LTL_SEJK_F,
/// `(GFa1&...&GFan) -> (GFb1&...&GFbn)`
/// \cite sickert.16.cav
LTL_SEJK_J,
/// `(GFa1|FGb1)&...&(GFan|FGbn)`
/// \cite sickert.16.cav
LTL_SEJK_K,
/// 3 formulas from Sikert et al.
/// \cite sickert.16.cav
LTL_SEJK_PATTERNS,
/// `G(p -> (q | Xq | ... | XX...Xq)`
/// \cite tabakov.10.rv
LTL_TV_F1,
/// `G(p -> (q | X(q | X(... | Xq)))`
/// \cite tabakov.10.rv
LTL_TV_F2,
/// `G(p -> (q & Xq & ... & XX...Xq)`
/// \cite tabakov.10.rv
LTL_TV_G1,
/// `G(p -> (q & X(q & X(... & Xq)))`
/// \cite tabakov.10.rv
LTL_TV_G2,
/// `G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...))))))`
/// \cite tabakov.10.rv
LTL_TV_UU,
/// `(((p1 U p2) U p3) ... U pn)`
/// \cite geldenhuys.06.spin
LTL_U_LEFT,
/// `(p1 U (p2 U (... U pn)))`
/// \cite geldenhuys.06.spin ,
/// \cite gastin.01.cav .
LTL_U_RIGHT,
LTL_END
};
@ -283,5 +193,6 @@ namespace spot
///
/// Return the number of arguments expected by an LTL pattern.
SPOT_API int ltl_pattern_argc(ltl_pattern_id pattern);
/// @}
}
}

16
spot/misc/game.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -93,19 +93,7 @@ public:
typedef std::unordered_map<unsigned, unsigned> strategy_t;
/// Compute the winning strategy and winning region of this game for player
/// 1 using Zielonka's recursive algorithm.
/** \verbatim
@article{ zielonka.98.tcs
title = "Infinite games on finitely coloured graphs with applications to
automata on infinite trees",
journal = "Theoretical Computer Science",
volume = "200",
number = "1",
pages = "135 - 183",
year = "1998",
author = "Wieslaw Zielonka",
}
\endverbatim */
/// 1 using Zielonka's recursive algorithm. \cite zielonka.98.tcs
void solve(region_t (&w)[2], strategy_t (&s)[2]) const;
private:

18
spot/misc/minato.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2009, 2013-2015, 2019 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -33,21 +33,7 @@ namespace spot
/// BDD function.
///
/// This algorithm implements a derecursived version the Minato-Morreale
/// algorithm presented in the following paper.
/** \verbatim
@InProceedings{ minato.92.sasimi,
author = {Shin-ichi Minato},
title = {Fast Generation of Irredundant Sum-of-Products Forms
from Binary Decision Diagrams},
booktitle = {Proceedings of the third Synthesis and Simulation
and Meeting International Interchange workshop
(SASIMI'92)},
pages = {64--73},
year = {1992},
address = {Kobe, Japan},
month = {April}
}
\endverbatim */
/// algorithm. \cite minato.92.sasimi
class SPOT_API minato_isop
{
public:

17
spot/taalgos/emptinessta.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2014, 2016, 2018 Laboratoire de Recherche
// Copyright (C) 2012-2014, 2016, 2018, 2019 Laboratoire de Recherche
// et Dévelopment de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -46,20 +46,7 @@ namespace spot
/// If spot::ta_check::check() returns false, then the product automaton
/// was found empty. Otherwise the automaton accepts some run.
///
/// This is based on the following paper.
/** \verbatim
@InProceedings{ geldenhuys.06.spin,
author = {Jaco Geldenhuys and Henri Hansen},
title = {Larger Automata and Less Work for {LTL} Model Checking},
booktitle = {Proceedings of the 13th International SPIN Workshop
(SPIN'06)},
year = {2006},
pages = {53--70},
series = {Lecture Notes in Computer Science},
volume = {3925},
publisher = {Springer}
}
\endverbatim */
/// This is based on \cite geldenhuys.06.spin .
///
/// the implementation of spot::ta_check::check() is inspired from the
/// two-pass algorithm of the paper above:

20
spot/taalgos/minimize.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2019 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -36,24 +36,6 @@ namespace spot
/// 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_);

19
spot/taalgos/tgba2ta.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012-2015, 2017 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2010, 2012-2015, 2017, 2019 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -28,20 +28,7 @@ namespace spot
/// \ingroup tgba_ta
/// \brief Build a spot::ta_explicit* (TA) from an LTL formula.
///
/// This is based on the following paper.
/** \verbatim
@InProceedings{ geldenhuys.06.spin,
author = {Jaco Geldenhuys and Henri Hansen},
title = {Larger Automata and Less Work for {LTL} Model Checking},
booktitle = {Proceedings of the 13th International SPIN Workshop
(SPIN'06)},
year = {2006},
pages = {53--70},
series = {Lecture Notes in Computer Science},
volume = {3925},
publisher = {Springer}
}
\endverbatim */
/// This is based on \cite geldenhuys.06.spin .
///
/// \param tgba_to_convert The TGBA automaton to convert into a TA automaton
///

47
spot/tl/formula.hh
View file

@ -1191,22 +1191,7 @@ namespace spot
/// \brief Create SERE for f[:*min..max]
///
/// This operator is a generalization of the (+) operator
/// defined in the following paper.
/** \verbatim
@InProceedings{ dax.09.atva,
author = {Christian Dax and Felix Klaedtke and Stefan Leue},
title = {Specification Languages for Stutter-Invariant Regular
Properties},
booktitle = {Proceedings of the 7th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'09)},
pages = {244--254},
year = {2009},
volume = {5799},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
\endverbatim */
/// defined by Dax et al. \cite dax.09.atva
/// @{
SPOT_DEF_BUNOP(FStar);
/// @}
@ -1617,44 +1602,18 @@ namespace spot
/// \brief Whether the formula is purely eventual.
///
/// Pure eventuality formulae are defined in
/** \verbatim
@InProceedings{ etessami.00.concur,
author = {Kousha Etessami and Gerard J. Holzmann},
title = {Optimizing {B\"u}chi Automata},
booktitle = {Proceedings of the 11th International Conference on
Concurrency Theory (Concur'2000)},
pages = {153--167},
year = {2000},
editor = {C. Palamidessi},
volume = {1877},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
\endverbatim */
///
/// A word that satisfies a pure eventuality can be prefixed by
/// anything and still satisfies the formula.
/// \cite etessami.00.concur
SPOT_DEF_PROP(is_eventual);
/// \brief Whether a formula is purely universal.
///
/// Purely universal formulae are defined in
/** \verbatim
@InProceedings{ etessami.00.concur,
author = {Kousha Etessami and Gerard J. Holzmann},
title = {Optimizing {B\"u}chi Automata},
booktitle = {Proceedings of the 11th International Conference on
Concurrency Theory (Concur'2000)},
pages = {153--167},
year = {2000},
editor = {C. Palamidessi},
volume = {1877},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
\endverbatim */
///
/// Any (non-empty) suffix of a word that satisfies a purely
/// universal formula also satisfies the formula.
/// \cite etessami.00.concur
SPOT_DEF_PROP(is_universal);
/// Whether a PSL/LTL formula is syntactic safety property.
SPOT_DEF_PROP(is_syntactic_safety);

18
spot/tl/remove_x.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2013, 2015, 2019 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -23,24 +23,14 @@
namespace spot
{
/// \ingroup tl_rewriting
/// \brief Rewrite a stutter-insensitive formula \a f without
/// using the X operator.
///
/// This function may also be applied to stutter-sensitive formulas,
/// but in that case the resulting formula is not equivalent.
///
/** \verbatim
@Article{ etessami.00.ipl,
author = {Kousha Etessami},
title = {A note on a question of {P}eled and {W}ilke regarding
stutter-invariant {LTL}},
journal = {Information Processing Letters},
volume = {75},
number = {6},
year = {2000},
pages = {261--263}
}
\endverbatim */
/// \see \cite etessami.00.ipl
SPOT_API
formula remove_x(formula f);
}

19
spot/tl/simplify.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement
// Copyright (C) 2011-2017, 2019 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -121,21 +121,8 @@ namespace spot
///
/// Returns whether \a f syntactically implies \a g.
///
/// This is adapted from
/** \verbatim
@InProceedings{ somenzi.00.cav,
author = {Fabio Somenzi and Roderick Bloem},
title = {Efficient {B\"u}chi Automata for {LTL} Formulae},
booktitle = {Proceedings of the 12th International Conference on
Computer Aided Verification (CAV'00)},
pages = {247--263},
year = {2000},
volume = {1855},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
\endverbatim */
///
/// This is adapted from the rules of Somenzi and
/// Bloem. \cite somenzi.00.cav
bool syntactic_implication(formula f, formula g);
/// \brief Syntactic implication with one negated argument.
///

23
spot/tl/snf.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2012-2015, 2019 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -26,29 +26,20 @@ namespace spot
{
typedef std::unordered_map<formula, formula> snf_cache;
/// Helper to rewrite a sere in Star Normal Form.
/// \ingroup tl_rewriting
/// \brief Helper to rewrite a sere in Star Normal Form.
///
/// This should only be called on children of a Star operator. It
/// corresponds to the E° operation defined in the following
/// paper.
///
/** \verbatim
@Article{ bruggeman.96.tcs,
author = {Anne Br{\"u}ggemann-Klein},
title = {Regular Expressions into Finite Automata},
journal = {Theoretical Computer Science},
year = {1996},
volume = {120},
pages = {87--98}
}
\endverbatim */
/// corresponds to the E° operation defined by Brüggemann-Klein.
/// \cite bruggeman.96.tcs
///
/// \param sere the SERE to rewrite
/// \param cache an optional cache
SPOT_API formula
star_normal_form(formula sere, snf_cache* cache = nullptr);
/// A variant of star_normal_form() for r[*0..j] where j < ω.
/// \ingroup tl_rewriting
/// \brief A variant of star_normal_form() for `r[*0..j]` where `j < ω`.
SPOT_API formula
star_normal_form_bounded(formula sere, snf_cache* cache = nullptr);
}

55
spot/twaalgos/cobuchi.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -58,18 +58,8 @@ namespace spot
/// \brief Converts a nondet Streett-like aut. to a nondet. co-Büchi aut.
///
/// This function works in top of the augmented subset construction algorithm
/// and is described in section 3.1 of:
/** \verbatim
@Article{boker.2011.fossacs,
author = {Udi Boker and Orna Kupferman},
title = {Co-Büching Them All},
booktitle = {Foundations of Software Science and Computational
Structures - 14th International Conference, FOSSACS 2011}
year = {2011},
pages = {184--198},
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
}
\endverbatim */
/// and is described in section 3.1 of \cite boker.2011.fossacs .
///
/// This implementation is quite different from the described algorithm. It
/// is made to work with automaton with Street-like acceptance (including
/// Büchi).
@ -86,18 +76,7 @@ namespace spot
///
/// This function converts the Rabin-like automaton into a Strett-like
/// automaton and then calls nsa_to_nca() on it. It is described in section
/// 3.2 of:
/** \verbatim
@Article{boker.2011.fossacs,
author = {Udi Boker and Orna Kupferman},
title = {Co-Büching Them All},
booktitle = {Foundations of Software Science and Computational
Structures - 14th International Conference, FOSSACS 2011}
year = {2011},
pages = {184--198},
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
}
\endverbatim */
/// 3.2 of \cite boker.2011.fossacs .
///
/// \a aut The automaton to convert.
/// \a named_states name each state for easier debugging.
@ -122,18 +101,7 @@ namespace spot
///
/// This function calls first nsa_to_nca() in order to retrieve som
/// information and then runs a breakpoint construction. The algorithm is
/// described in section 4 of:
/** \verbatim
@Article{boker.2011.fossacs,
author = {Udi Boker and Orna Kupferman},
title = {Co-Büching Them All},
booktitle = {Foundations of Software Science and Computational
Structures - 14th International Conference, FOSSACS 2011}
year = {2011},
pages = {184--198},
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
}
\endverbatim */
/// described in section 4 of \cite boker.2011.fossacs .
///
/// \a aut The automaton to convert.
/// \a named_states name each state for easier debugging.
@ -144,18 +112,7 @@ namespace spot
///
/// This function calls first nra_to_nca() in order to retrieve som
/// information and then runs a breakpoint construction. The algorithm is
/// described in section 4 of:
/** \verbatim
@Article{boker.2011.fossacs,
author = {Udi Boker and Orna Kupferman},
title = {Co-Büching Them All},
booktitle = {Foundations of Software Science and Computational
Structures - 14th International Conference, FOSSACS 2011}
year = {2011},
pages = {184--198},
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
}
\endverbatim */
/// described in section 4 of \cite boker.2011.fossacs .
///
/// \a aut The automaton to convert.
/// \a named_states name each state for easier debugging.

17
spot/twaalgos/cycles.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2018 Laboratoire de Recherche et
// Copyright (C) 2012-2015, 2018-2019 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -28,20 +28,7 @@ namespace spot
/// \brief Enumerate elementary cycles in a SCC.
///
/// This class implements a non-recursive version of the algorithm
/// on page 170 of:
/** \verbatim
@Article{loizou.82.is,
author = {George Loizou and Peter Thanisch},
title = {Enumerating the Cycles of a Digraph: A New
Preprocessing Strategy},
journal = {Information Sciences},
year = {1982},
volume = {27},
number = {3},
pages = {163--182},
month = aug
}
\endverbatim */
/// on page 170 of \cite loizou.82.is .
/// (the additional preprocessings described later in that paper are
/// not implemented).
///

14
spot/twaalgos/dualize.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -43,17 +43,7 @@ namespace spot
/// If the input automaton is existential, the output will be universal.
/// If the input automaton is universal, the output will be existential.
/// Finally, if the input automaton is alternating, the result is alternating.
/// More can be found on page 22 (Definition 1.6) of:
/** \verbatim
@mastersthesis{loding.98.methodsfor
author = {Christof Löding}
title = {Methods for the Transformation of ω-Automata: Complexity
and Connection to Second Order Logic}
school = {Institute of Computer Science and Applied Mathematics
Christian-Albrechts-University of Kiel}
year = {1998}
}
\endverbatim */
/// More can be found on page 22 (Definition 1.6) of \cite loding.98.msc .
SPOT_API twa_graph_ptr
dualize(const const_twa_graph_ptr& aut);
}

21
spot/twaalgos/gtec/gtec.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche
// Copyright (C) 2008, 2013-2016, 2018-2019 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -34,24 +34,7 @@ namespace spot
/// \brief Check whether the language of an automate is empty.
///
/// This is based on the following paper.
/** \verbatim
@InProceedings{couvreur.99.fm,
author = {Jean-Michel Couvreur},
title = {On-the-fly Verification of Temporal Logic},
pages = {253--271},
editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
booktitle = {Proceedings of the World Congress on Formal Methods in
the Development of Computing Systems (FM'99)},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1708},
year = {1999},
address = {Toulouse, France},
month = {September},
isbn = {3-540-66587-0}
}
\endverbatim */
/// This is based on \cite couvreur.99.fm .
///
/// A recursive definition of the algorithm would look as follows,
/// but the implementation is of course not recursive.

26
spot/twaalgos/gv04.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -33,25 +33,9 @@ namespace spot
/// \ingroup emptiness_check_algorithms
/// \pre The automaton \a a must have at most one acceptance condition.
///
/// The original algorithm, coming from the following paper, has only
/// been slightly modified to work on transition-based automata.
/** \verbatim
@InProceedings{geldenhuys.04.tacas,
author = {Jaco Geldenhuys and Antti Valmari},
title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification
More Efficient},
booktitle = {Proceedings of the 10th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'04)},
editor = {Kurt Jensen and Andreas Podelski},
pages = {205--219},
year = {2004},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {2988},
isbn = {3-540-21299-X}
}
\endverbatim */
/// The original algorithm, coming from \cite geldenhuys.04.tacas ,
/// has only been slightly modified to work on transition-based
/// automata.
SPOT_API emptiness_check_ptr
explicit_gv04_check(const const_twa_ptr& a, option_map o = option_map());
}

18
spot/twaalgos/ltl2taa.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2013, 2014, 2015 Laboratoire de Recherche
// Copyright (C) 2009, 2010, 2013-2015, 2019 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -27,21 +27,7 @@ namespace spot
/// \ingroup twa_ltl
/// \brief Build a spot::taa* from an LTL formula.
///
/// This is based on the following.
/** \verbatim
@techreport{HUT-TCS-A104,
address = {Espoo, Finland},
author = {Heikki Tauriainen},
month = {September},
note = {Doctoral dissertation},
number = {A104},
pages = {xii+229},
title = {Automata and Linear Temporal Logic: Translations
with Transition-Based Acceptance},
type = {Research Report},
year = {2006}
}
\endverbatim */
/// This is based on \cite tauriainen.06.tr .
///
/// \param f The formula to translate into an automaton.
/// \param dict The spot::bdd_dict the constructed automata should use.

85
spot/twaalgos/ltl2tgba_fm.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017 Laboratoire de
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017, 2019 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -30,26 +30,11 @@
namespace spot
{
/// \ingroup twa_ltl
/// \brief Build a spot::twa_graph_ptr from an LTL formula.
/// \brief Build a spot::twa_graph_ptr from an LTL or PSL formula.
///
/// This is based on the following paper.
/** \verbatim
@InProceedings{couvreur.99.fm,
author = {Jean-Michel Couvreur},
title = {On-the-fly Verification of Temporal Logic},
pages = {253--271},
editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
booktitle = {Proceedings of the World Congress on Formal Methods in the
Development of Computing Systems (FM'99)},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = {1708},
year = {1999},
address = {Toulouse, France},
month = {September},
isbn = {3-540-66587-0}
}
\endverbatim */
/// This originally derived from an algorithm by Couvreur
/// \cite couvreur.99.fm , but it has been improved in many
/// ways \cite duret.14.ijccbs .
///
/// \param f The formula to translate into an automaton.
///
@ -68,25 +53,7 @@ namespace spot
///
/// \param branching_postponement When set, several transitions leaving
/// from the same state with the same label (i.e., condition + acceptance
/// conditions) will be merged. This corresponds to an optimization
/// described in the following paper.
/** \verbatim
@InProceedings{ sebastiani.03.charme,
author = {Roberto Sebastiani and Stefano Tonetta},
title = {"More Deterministic" vs. "Smaller" B{\"u}chi Automata for
Efficient LTL Model Checking},
booktitle = {Proceedings for the 12th Advanced Research Working
Conference on Correct Hardware Design and Verification
Methods (CHARME'03)},
pages = {126--140},
year = {2003},
editor = {G. Goos and J. Hartmanis and J. van Leeuwen},
volume = {2860},
series = {Lectures Notes in Computer Science},
month = {October},
publisher = {Springer-Verlag}
}
\endverbatim */
/// conditions) will be merged. \cite sebastiani.03.charme
///
/// \param fair_loop_approx When set, a really simple characterization of
/// unstable state is used to suppress all acceptance conditions from
@ -100,43 +67,11 @@ namespace spot
/// \param simplifier If this parameter is set, the LTL formulae
/// representing each state of the automaton will be simplified
/// before computing the successor. \a simpl should be configured
/// for the type of reduction you want, see
/// spot::tl_simplifier. This idea is taken from the
/// following paper.
/** \verbatim
@InProceedings{ thirioux.02.fmics,
author = {Xavier Thirioux},
title = {Simple and Efficient Translation from {LTL} Formulas to
{B\"u}chi Automata},
booktitle = {Proceedings of the 7th International ERCIM Workshop in
Formal Methods for Industrial Critical Systems (FMICS'02)},
series = {Electronic Notes in Theoretical Computer Science},
volume = {66(2)},
publisher = {Elsevier},
editor = {Rance Cleaveland and Hubert Garavel},
year = {2002},
month = jul,
address = {M{\'a}laga, Spain}
}
\endverbatim */
/// for the type of reduction you want, see spot::tl_simplifier.
/// This idea is taken from \cite thirioux.02.fmics .
///
/// \param unambiguous When true, unambigous TGBA will be produced using
/// the trick described in the following paper.
/** \verbatim
@InProceedings{ benedikt.13.tacas,
author = {Michael Benedikt and Rastislav Lenhardt and James
Worrell},
title = {{LTL} Model Checking of Interval Markov Chains},
booktitle = {19th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS'13)},
year = {2013},
pages = {32--46},
series = {Lecture Notes in Computer Science},
volume = {7795},
editor = {Nir Piterman and Scott A. Smolka},
publisher = {Springer}
}
\endverbatim */
/// \param unambiguous When true, unambigous TGBA will be produced
/// using the trick described in \cite benedikt.13.tacas .
///
/// \return A spot::twa_graph that recognizes the language of \a f.
SPOT_API twa_graph_ptr

29
spot/twaalgos/magic.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -79,19 +79,7 @@ namespace spot
///
/// This algorithm is an adaptation to TBA of the one
/// (which deals with accepting states) presented in
///
/** \verbatim
Article{ courcoubetis.92.fmsd,
author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre
Wolper and Mihalis Yannakakis},
title = {Memory-Efficient Algorithm for the Verification of
Temporal Properties},
journal = {Formal Methods in System Design},
pages = {275--288},
year = {1992},
volume = {1}
}
\endverbatim */
/// \cite courcoubetis.92.fmsd .
///
/// \bug The name is misleading. Magic-search is the algorithm
/// from \c godefroid.93.pstv, not \c courcoubetis.92.fmsd.
@ -106,16 +94,7 @@ namespace spot
///
/// During the visit of \a a, the returned checker does not store explicitely
/// the traversed states but uses the bit-state hashing technic presented in:
///
/** \verbatim
@book{Holzmann91,
author = {G.J. Holzmann},
title = {Design and Validation of Computer Protocols},
publisher = {Prentice-Hall},
address = {Englewood Cliffs, New Jersey},
year = {1991}
}
\endverbatim */
/// \cite Holzmann.91.book.
///
/// Consequently, the detection of an acceptence cycle is not ensured.
///

55
spot/twaalgos/minimize.hh
View file

@ -36,21 +36,7 @@ namespace spot
/// determinized and minimized using the standard DFA construction
/// as if all states were accepting states.
///
/// For more detail about monitors, see the following paper:
/** \verbatim
@InProceedings{ tabakov.10.rv,
author = {Deian Tabakov and Moshe Y. Vardi},
title = {Optimized Temporal Monitors for SystemC{$^*$}},
booktitle = {Proceedings of the 10th International Conferance
on Runtime Verification},
pages = {436--451},
year = 2010,
volume = {6418},
series = {Lecture Notes in Computer Science},
month = nov,
publisher = {Spring-Verlag}
}
\endverbatim */
/// For more detail about monitors, see \cite tabakov.10.rv .
/// (Note: although the above paper uses Spot, this function did not
/// exist in Spot at that time.)
///
@ -75,24 +61,7 @@ namespace spot
///
/// The construction is inspired by the following paper, however we
/// guarantee that the output language is a subsets of the original
/// language while they don't.
/** \verbatim
@InProceedings{ dax.07.atva,
author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
title = {Mechanizing the Powerset Construction for Restricted
Classes of {$\omega$}-Automata},
year = 2007,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = 4762,
booktitle = {Proceedings of the 5th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'07)},
editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
and Yoshio Okamura},
month = oct
}
\endverbatim */
/// language while they don't. \cite dax.07.atva
///
/// If an \a output_aborter is given, the determinization is aborted
/// whenever it would produce an automaton that is too large. In
@ -104,25 +73,7 @@ namespace spot
///
/// This function attempts to minimize the automaton \a aut_f using the
/// algorithm implemented in the minimize_wdba() function, and presented
/// by the following paper:
///
/** \verbatim
@InProceedings{ dax.07.atva,
author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
title = {Mechanizing the Powerset Construction for Restricted
Classes of {$\omega$}-Automata},
year = 2007,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = 4762,
booktitle = {Proceedings of the 5th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'07)},
editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
and Yoshio Okamura},
month = oct
}
\endverbatim */
/// by \cite dax.07.atva .
///
/// Because it is hard to determine if an automaton corresponds
/// to an obligation property, you should supply either the formula

12
spot/twaalgos/parity.hh
View file

@ -140,17 +140,7 @@ namespace spot
///
/// This implements an algorithm derived from the following article,
/// but generalized to all types of parity acceptance.
/** \verbatim
@Article{carton.99.ita,
author = {Olivier Carton and Ram{\'o}n Maceiras},
title = {Computing the {R}abin index of a parity automaton},
journal = {Informatique théorique et applications},
year = {1999},
volume = {33},
number = {6},
pages = {495--505}
}
\endverbatim */
/// \cite carton.99.ita
///
/// The kind of parity (min/max) is preserved, but the style
/// (odd/even) may be altered to reduce the number of colors used.

20
spot/twaalgos/powerset.hh
View file

@ -112,24 +112,8 @@ namespace spot
/// determinized, and this procedure does not ensure that the
/// produced automaton is equivalent to \a aut.
///
/// The construction is adapted from Section 3.2 of:
/// \verbatim
/// @InProceedings{ dax.07.atva,
/// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
/// title = {Mechanizing the Powerset Construction for Restricted
/// Classes of {$\omega$}-Automata},
/// year = 2007,
/// series = {Lecture Notes in Computer Science},
/// publisher = {Springer-Verlag},
/// volume = 4762,
/// booktitle = {Proceedings of the 5th International Symposium on
/// Automated Technology for Verification and Analysis
/// (ATVA'07)},
/// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino
/// and Yoshio Okamura},
/// month = oct
/// }
/// \endverbatim
/// The construction is adapted from Section 3.2 of
/// \cite dax.07.atva
/// only adapted to work on TBA rather than BA.
///
/// If \a threshold_states is non null, abort the construction

18
spot/twaalgos/randomgraph.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
// Copyright (C) 2011, 2013-2015, 2019 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -55,21 +55,7 @@ namespace spot
/// belongs to a single acceptance set.
///
/// This algorithms is adapted from the one in Fig 6.2 page 48 of
/** \verbatim
@TechReport{ tauriainen.00.a66,
author = {Heikki Tauriainen},
title = {Automated Testing of {B\"u}chi Automata Translators for
{L}inear {T}emporal {L}ogic},
address = {Espoo, Finland},
institution = {Helsinki University of Technology, Laboratory for
Theoretical Computer Science},
number = {A66},
year = {2000},
url = {http://citeseer.nj.nec.com/tauriainen00automated.html},
type = {Research Report},
note = {Reprint of Master's thesis}
}
\endverbatim */
/// \cite tauriainen.00.tr .
///
/// Although the intent is similar, there are some differences
/// between the above published algorithm and this implementation.

31
spot/twaalgos/se05.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie.
@ -84,19 +84,7 @@ namespace spot
\endverbatim */
///
/// It is an adaptation to TBA of the one presented in
/** \verbatim
@techreport{SE04,
author = {Stefan Schwoon and Javier Esparza},
institution = {Universit{\"a}t Stuttgart, Fakult\"at Informatik,
Elektrotechnik und Informationstechnik},
month = {November},
number = {2004/06},
title = {A Note on On-The-Fly Verification Algorithms},
year = {2004},
url =
{http://www.fmi.uni-stuttgart.de/szs/publications/info/schwoosn.SE04.shtml}
}
\endverbatim */
/// \cite schwoon.04.tr .
///
/// \sa spot::explicit_magic_search
///
@ -109,17 +97,8 @@ namespace spot
/// it is a TBA).
///
/// During the visit of \a a, the returned checker does not store explicitely
/// the traversed states but uses the bit-state hashing technic presented in:
///
/** \verbatim
@book{Holzmann91,
author = {G.J. Holzmann},
title = {Design and Validation of Computer Protocols},
publisher = {Prentice-Hall},
address = {Englewood Cliffs, New Jersey},
year = {1991}
}
\endverbatim */
/// the traversed states but uses the bit-state hashing technic presented in
/// \cite holzmann.91.book
///
/// Consequently, the detection of an acceptence cycle is not ensured.
///

40
spot/twaalgos/simulation.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015, 2017 Laboratoire de Recherche et
// Copyright (C) 2012-2015, 2017, 2019 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -33,24 +33,7 @@ namespace spot
/// When the suffixes (letter and acceptance conditions) reachable
/// from one state are included in the suffixes seen by another one,
/// the former state can be merged into the latter. The algorithm is
/// based on the following paper, but generalized to handle TωA
/// directly.
///
/** \verbatim
@InProceedings{ etessami.00.concur,
author = {Kousha Etessami and Gerard J. Holzmann},
title = {Optimizing {B\"u}chi Automata},
booktitle = {Proceedings of the 11th International Conference on
Concurrency Theory (Concur'00)},
pages = {153--167},
year = {2000},
editor = {C. Palamidessi},
volume = {1877},
series = {Lecture Notes in Computer Science},
address = {Pennsylvania, USA},
publisher = {Springer-Verlag}
}
\endverbatim */
/// described in \cite babiak.13.spin .
///
/// Our reconstruction of the quotient automaton based on this
/// suffix-inclusion relation will also improve determinism.
@ -87,24 +70,7 @@ namespace spot
///
/// When the prefixes (letter and acceptance conditions) leading to
/// one state are included in the prefixes leading to one, the former
/// state can be merged into the latter.
///
/// Reverse simulation is discussed in the following paper,
/// but generalized to handle TωA directly.
/** \verbatim
@InProceedings{ somenzi.00.cav,
author = {Fabio Somenzi and Roderick Bloem},
title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
booktitle = {Proceedings of the 12th International Conference on
Computer Aided Verification (CAV'00)},
pages = {247--263},
year = {2000},
volume = {1855},
series = {Lecture Notes in Computer Science},
address = {Chicago, Illinois, USA},
publisher = {Springer-Verlag}
}
\endverbatim */
/// state can be merged into the latter. \cite babiak.13.spin .
///
/// Our reconstruction of the quotient automaton based on this
/// prefix-inclusion relation will also improve codeterminism.

27
spot/twaalgos/strength.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire
// de Recherche et Développement de l'Epita (LRDE)
// Copyright (C) 2010-2011, 2013-2019 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
@ -156,29 +156,10 @@ namespace spot
/// an incorrect SCC number is supplied.
///
/// The definition are basically those used in the following paper,
/// except that we extra the "inherently weak" part instead of the
/// except that we extract the "inherently weak" part instead of the
/// weak part because we can now test for inherent weakness
/// efficiently enough (not enumerating all cycles as suggested in
/// the paper).
/** \verbatim
@inproceedings{renault.13.tacas,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud},
title = {Strength-Based Decomposition of the Property {B\"u}chi
Automaton for Faster Model Checking},
booktitle = {Proceedings of the 19th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'13)},
editor = {Nir Piterman and Scott A. Smolka},
year = {2013},
month = mar,
pages = {580--593},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7795},
doi = {10.1007/978-3-642-36742-7_42}
}
\endverbatim */
/// the paper). \cite renault.13.tacas
///
/// \param aut the automaton to decompose
/// \param keep a string specifying the strengths/SCCs to keep

88
spot/twaalgos/stutter.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2017 Laboratoire de Recherche
// Copyright (C) 2014-2017, 2019 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -30,22 +30,7 @@ namespace spot
///
/// Any letter that enters a state will spawn a copy of this state
/// with a self-loop using the same letter. For more details
/// about this function, see
/** \verbatim
@InProceedings{ michaud.15.spin,
author = {Thibaud Michaud and Alexandre Duret-Lutz},
title = {Practical Stutter-Invariance Checks for
{$\omega$}-Regular Languages},
booktitle = {Proceedings of the 22th International SPIN
Symposium on Model Checking of Software (SPIN'15)},
year = 2015,
pages = {84--101},
series = {Lecture Notes in Computer Science},
volume = 9232,
publisher = {Springer},
month = aug
}
\endverbatim */
/// about this function, see \cite michaud.15.spin .
SPOT_API twa_graph_ptr
sl(const_twa_graph_ptr aut);
@ -55,22 +40,7 @@ namespace spot
///
/// For any transition (s,d) labeled by a letter ℓ, we add a state x
/// and three transitions (s,x), (x,x), (x,d) all labeled by ℓ.
/// For more details about this function, see
/** \verbatim
@InProceedings{ michaud.15.spin,
author = {Thibaud Michaud and Alexandre Duret-Lutz},
title = {Practical Stutter-Invariance Checks for
{$\omega$}-Regular Languages},
booktitle = {Proceedings of the 22th International SPIN
Symposium on Model Checking of Software (SPIN'15)},
year = 2015,
pages = {84--101},
series = {Lecture Notes in Computer Science},
volume = 9232,
publisher = {Springer},
month = aug
}
\endverbatim */
/// For more details about this function, see \cite michaud.15.spin .
///
/// The inplace version of the function modifies the input
/// automaton.
@ -89,23 +59,7 @@ namespace spot
/// a transition labeled by B, and (y,z) is a transition labeled by C,
/// we add a transition (x,z) labeled by B∧C.
///
/// For more details about this function, see
/** \verbatim
@InProceedings{ michaud.15.spin,
author = {Thibaud Michaud and Alexandre Duret-Lutz},
title = {Practical Stutter-Invariance Checks for
{$\omega$}-Regular Languages},
booktitle = {Proceedings of the 22th International SPIN
Symposium on Model Checking of Software (SPIN'15)},
year = 2015,
pages = {84--101},
series = {Lecture Notes in Computer Science},
volume = 9232,
publisher = {Springer},
month = aug
}
\endverbatim */
///
/// For more details about this function, see \cite michaud.15.spin .
///
/// The inplace version of the function modifies the input
/// automaton.
@ -133,22 +87,7 @@ namespace spot
/// The prop_stutter_invariant() property of \a aut_f is set as a
/// side-effect.
///
/// For more details about this function, see
/** \verbatim
@InProceedings{ michaud.15.spin,
author = {Thibaud Michaud and Alexandre Duret-Lutz},
title = {Practical Stutter-Invariance Checks for
{$\omega$}-Regular Languages},
booktitle = {Proceedings of the 22th International SPIN
Symposium on Model Checking of Software (SPIN'15)},
year = 2015,
pages = {84--101},
series = {Lecture Notes in Computer Science},
volume = 9232,
publisher = {Springer},
month = aug
}
\endverbatim */
/// For more details about this function, see \cite michaud.15.spin .
SPOT_API bool
is_stutter_invariant(formula f, twa_graph_ptr aut_f = nullptr);
@ -164,22 +103,7 @@ namespace spot
/// The prop_stutter_invariant() property of \a aut_f is set as a
/// side-effect.
///
/// For more details about this function, see
/** \verbatim
@InProceedings{ michaud.15.spin,
author = {Thibaud Michaud and Alexandre Duret-Lutz},
title = {Practical Stutter-Invariance Checks for
{$\omega$}-Regular Languages},
booktitle = {Proceedings of the 22th International SPIN
Symposium on Model Checking of Software (SPIN'15)},
year = 2015,
pages = {84--101},
series = {Lecture Notes in Computer Science},
volume = 9232,
publisher = {Springer},
month = aug
}
\endverbatim */
/// For more details about this function, see \cite michaud.15.spin .
SPOT_API bool
is_stutter_invariant(twa_graph_ptr aut_f,
const_twa_graph_ptr aut_nf = nullptr,

22
spot/twaalgos/tau03.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -75,25 +75,7 @@ namespace spot
end;
\endverbatim */
///
/// This algorithm is the one presented in
///
/** \verbatim
@techreport{HUT-TCS-A83,
address = {Espoo, Finland},
author = {Heikki Tauriainen},
institution = {Helsinki University of Technology, Laboratory for
Theoretical Computer Science},
month = {December},
number = {A83},
pages = {132},
title = {On Translating Linear Temporal Logic into Alternating and
Nondeterministic Automata},
type = {Research Report},
year = {2003},
url = {http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A83.shtml}
}
\endverbatim */
///
/// This algorithm is the one presented in \cite tauriainen.03.tr .
SPOT_API emptiness_check_ptr
explicit_tau03_search(const const_twa_ptr& a, option_map o = option_map());

17
spot/twaalgos/totgba.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2015-2016, 2018-2019 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -87,18 +87,7 @@ namespace spot
/// \brief Converts any DNF acceptance condition into Streett-like.
///
/// This function is an optimized version of the construction described
/// by Lemma 4 and 5 of the paper below.
/** \verbatim
@Article{boker.2011.fossacs,
author = {Udi Boker and Orna Kupferman},
title = {Co-Büching Them All},
booktitle = {Foundations of Software Science and Computational
Structures - 14th International Conference, FOSSACS 2011}
year = {2011},
pages = {184--198},
url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}}
}
\endverbatim */
/// by Lemma 4 and 5 of \cite boker.2011.fossacs .
///
/// In the described construction, as many copies as there are minterms in
/// the acceptance condition are made and the union of all those copies is

29
spot/twaalgos/toweak.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
// Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -31,30 +31,9 @@ namespace spot
/// automaton is already weak, it will simply be copied.
///
/// For details about the algorithm used, see the following papers:
/** \verbatim
@article{kupferman.01.tocl,
author = {Orna Kupferman and Moshe Y. Vardi},
title = {Weak alternating automata are not that weak},
journal = {ACM Transactions on Computational Logic (TOCL)},
month = {July},
year = 2001,
pages = {408--429},
volume = {2},
number = {3},
publisher = {ACM New York, NY, USA}
}
@article{kupferman.05.tcs,
author = {Orna Kupferman and Moshe Y. Vardi},
title = {From complementation to certification},
journal = {Theoretical Computer Science},
month = {November},
year = 2005,
pages = {83--100},
volume = {345},
number = {1},
publisher = {Elsevier}
}
\endverbatim */
/// \cite kupferman.01.tocl ,
/// \cite kupferman.05.tcs .
///
/// Although at the end of the above paper there is a hint at an optimization
/// that greatly reduces the number of transition in the resulting automaton,
/// but in return makes the run of remove_alternation algorithm way slower.