Commit 6afc2d45 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

complete reference to Esparza/Křetínský/Sickert LICS'18 paper

* NEWS, bin/man/spot-x.x, bin/spot-x.cc, spot/twaalgos/gfguarantee.hh:
Add the conference.
parent c766f58d
Pipeline #1223 passed with stages
in 235 minutes and 54 seconds
...@@ -32,8 +32,7 @@ New in spot 2.5.2.dev (not yet released) ...@@ -32,8 +32,7 @@ New in spot 2.5.2.dev (not yet released)
and fg_safety_to_dca() is a specialized construction for and fg_safety_to_dca() is a specialized construction for
translating formulas of the form FG(safety) to DCA. These translating formulas of the form FG(safety) to DCA. These
are slight generalizations of some constructions proposed are slight generalizations of some constructions proposed
by J. Esparza, J. Křentínský, and S. Sickert in a submitted by J. Esparza, J. Křentínský, and S. Sickert (LICS'18).
paper.
These are now used by the main translation routine, and can be These are now used by the main translation routine, and can be
disabled by passing -x '!gf-guarantee' to ltl2tgba. As an disabled by passing -x '!gf-guarantee' to ltl2tgba. As an
......
...@@ -281,6 +281,16 @@ checks for ω-regular languages, Proceedings of SPIN'15. LNCS 9232. ...@@ -281,6 +281,16 @@ checks for ω-regular languages, Proceedings of SPIN'15. LNCS 9232.
Describes the stutter-invariance checks that can be selected through Describes the stutter-invariance checks that can be selected through
\fBSPOT_STUTTER_CHECK\fR. \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] [SEE ALSO]
.BR ltl2tgba (1) .BR ltl2tgba (1)
......
...@@ -107,10 +107,9 @@ the determinization algorithm.") }, ...@@ -107,10 +107,9 @@ the determinization algorithm.") },
the determinization algorithm.") }, the determinization algorithm.") },
{ DOC("det-stutter", "Set to 0 to disable optimizations based on \ { DOC("det-stutter", "Set to 0 to disable optimizations based on \
the stutter-invariance in the determinization algorithm.") }, 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 \ { DOC("gf-guarantee", "Set to 0 to disable alternate constructions \
for GF(guarantee)->[D]BA and FG(safety)->DCA. Those 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 \ This is enabled by default for medium and high optimization \
levels. Unless we are building deterministic automata, the \ levels. Unless we are building deterministic automata, the \
resulting automata are compared to the automata built using the \ resulting automata are compared to the automata built using the \
......
...@@ -39,8 +39,8 @@ namespace spot ...@@ -39,8 +39,8 @@ namespace spot
/// If \a state_based is not set, all transition going to terminal /// If \a state_based is not set, all transition going to terminal
/// states are made accepting and redirected to the initial state. /// states are made accepting and redirected to the initial state.
/// ///
/// This construction is inspired by a similar construction in a /// This construction is inspired by a similar construction in the
/// submitted paper by J. Esparza, J. Křetínský, & S. Sickert. /// LICS'18 paper by J. Esparza, J. Křetínský, and S. Sickert.
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
g_f_terminal_inplace(twa_graph_ptr f_terminal, bool state_based = false); g_f_terminal_inplace(twa_graph_ptr f_terminal, bool state_based = false);
...@@ -56,10 +56,10 @@ namespace spot ...@@ -56,10 +56,10 @@ namespace spot
/// Return nullptr if the input formula is not of the supported /// Return nullptr if the input formula is not of the supported
/// form. /// form.
/// ///
/// This construction generalized a similar construction in a /// This construction generalizes a construction in the LICS'18
/// submitted paper by J. Esparza, J. Křetínský, & S. Sickert in the /// paper of J. Esparza, J. Křetínský, and S. Sickert. This version
/// sense that it will work if Φ represent a safety property, even /// will work if Φ represent a safety property, even if it is not a
/// if it is not a syntactic safety. /// syntactic safety.
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict, gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr& dict,
bool deterministic = true, bool state_based = false); bool deterministic = true, bool state_based = false);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment