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

* spot/twaalgos/gfguarantee.hh: Typos in comments.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2022-03-22 12:22:48 +01:00
parent 96e051d2bb
commit 53118d9314
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/twaalgos/gfguarantee.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2018 Laboratoire de Recherche et Développement // Copyright (C) 2018, 2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -48,7 +48,7 @@ namespace spot
/// \brief Convert GF(φ) into a (D)BA if φ is a guarantee property. /// \brief Convert GF(φ) into a (D)BA if φ is a guarantee property.
/// ///
/// If the formula \a gf has the form GΦ where Φ matches either F(φ) /// If the formula \a gf has the form GΦ where Φ matches either F(φ)
/// or F(φ₁)|F(φ₂)|...|F(φₙ), we translate Φ into A_Φ and attempt to /// or F(φ₁)&F(φ₂)&...&F(φₙ), we translate Φ into A_Φ and attempt to
/// minimize it to a WDBA W_Φ. If the resulting automaton is /// minimize it to a WDBA W_Φ. If the resulting automaton is
/// terminal, we then call g_f_terminal_inplace(W_Φ). If \a /// terminal, we then call g_f_terminal_inplace(W_Φ). If \a
/// deterministic is not set, we keep the minimized automaton only /// deterministic is not set, we keep the minimized automaton only