From 6afc2d45e09c0f9f805538d9058f92b36e9c9f55 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 Apr 2018 16:40:39 +0200 Subject: [PATCH] =?UTF-8?q?complete=20reference=20to=20Esparza/K=C5=99et?= =?UTF-8?q?=C3=ADnsk=C3=BD/Sickert=20LICS'18=20paper?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * NEWS, bin/man/spot-x.x, bin/spot-x.cc, spot/twaalgos/gfguarantee.hh: Add the conference. --- NEWS | 3 +-- bin/man/spot-x.x | 10 ++++++++++ bin/spot-x.cc | 3 +-- spot/twaalgos/gfguarantee.hh | 12 ++++++------ 4 files changed, 18 insertions(+), 10 deletions(-) diff --git a/NEWS b/NEWS index 0aa3e31f0..4ff6eb53e 100644 --- a/NEWS +++ b/NEWS @@ -32,8 +32,7 @@ New in spot 2.5.2.dev (not yet released) and fg_safety_to_dca() is a specialized construction for translating formulas of the form FG(safety) to DCA. These are slight generalizations of some constructions proposed - by J. Esparza, J. Křentínský, and S. Sickert in a submitted - paper. + by J. Esparza, J. Křentínský, and S. Sickert (LICS'18). These are now used by the main translation routine, and can be disabled by passing -x '!gf-guarantee' to ltl2tgba. As an diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index 881265282..e6c534cec 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -281,6 +281,16 @@ checks for ω-regular languages, Proceedings of SPIN'15. LNCS 9232. Describes the stutter-invariance checks that can be selected through \fBSPOT_STUTTER_CHECK\fR. +.TP +5. +Javier Esparza, Jan Křetínský and Salomon Sickert: One Theorem to Rule +Them All: A Unified Translation of LTL into ω-Automata. Proceedings +of LICS'18. To appear. + +Describes (among other things) the constructions used for translating +formulas of the form GF(guarantee) or FG(safety), that can be +disabled with \fB-x gf-guarantee=0\fR. + [SEE ALSO] .BR ltl2tgba (1) diff --git a/bin/spot-x.cc b/bin/spot-x.cc index d5b23ffa3..b9d1a77b0 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -107,10 +107,9 @@ the determinization algorithm.") }, the determinization algorithm.") }, { DOC("det-stutter", "Set to 0 to disable optimizations based on \ the stutter-invariance in the determinization algorithm.") }, - // FIXME: Add bibliographic reference to their paper ASAP. { DOC("gf-guarantee", "Set to 0 to disable alternate constructions \ for GF(guarantee)->[D]BA and FG(safety)->DCA. Those constructions \ -are based on work by J. Esparza, J. Křentínský, and S. Sickert. \ +are from an LICS'18 paper by J. Esparza, J. Křentínský, and S. Sickert. \ This is enabled by default for medium and high optimization \ levels. Unless we are building deterministic automata, the \ resulting automata are compared to the automata built using the \ diff --git a/spot/twaalgos/gfguarantee.hh b/spot/twaalgos/gfguarantee.hh index 97611dbdb..8e163dce8 100644 --- a/spot/twaalgos/gfguarantee.hh +++ b/spot/twaalgos/gfguarantee.hh @@ -39,8 +39,8 @@ namespace spot /// If \a state_based is not set, all transition going to terminal /// states are made accepting and redirected to the initial state. /// - /// This construction is inspired by a similar construction in a - /// submitted paper by J. Esparza, J. Křetínský, & S. Sickert. + /// This construction is inspired by a similar construction in the + /// LICS'18 paper by J. Esparza, J. Křetínský, and S. Sickert. SPOT_API twa_graph_ptr g_f_terminal_inplace(twa_graph_ptr f_terminal, bool state_based = false); @@ -56,10 +56,10 @@ namespace spot /// Return nullptr if the input formula is not of the supported /// form. /// - /// This construction generalized a similar construction in a - /// submitted paper by J. Esparza, J. Křetínský, & S. Sickert in the - /// sense that it will work if Φ represent a safety property, even - /// if it is not a syntactic safety. + /// This construction generalizes a construction in the LICS'18 + /// paper of J. Esparza, J. Křetínský, and S. Sickert. This version + /// will work if Φ represent a safety property, even if it is not a + /// syntactic safety. SPOT_API twa_graph_ptr gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict, bool deterministic = true, bool state_based = false); -- GitLab