From 2e69e045836e67c95b59d00fed5e640f76804949 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 5 Nov 2016 17:52:38 +0100 Subject: [PATCH] from_ltlf: new LTL transformation. Fixes #187. * spot/tl/ltlf.cc, spot/tl/ltlf.hh: New files. * spot/tl/Makefile.am: Add them. * bin/ltlfilt.cc: Add a new option. * bin/man/ltlfilt.x: Add bibliographic reference. * tests/core/ltlfilt.test: Add more tests. * tests/python/ltlf.py: New file. * tests/Makefile.am: Add it. * python/spot/impl.i: Python bindings. * NEWS: Mention it. --- NEWS | 9 ++++++ bin/ltlfilt.cc | 12 ++++++++ bin/man/ltlfilt.x | 7 +++++ python/spot/impl.i | 2 ++ spot/tl/Makefile.am | 4 ++- spot/tl/ltlf.cc | 66 +++++++++++++++++++++++++++++++++++++++++ spot/tl/ltlf.hh | 50 +++++++++++++++++++++++++++++++ tests/Makefile.am | 1 + tests/core/ltlfilt.test | 29 ++++++++++++++++++ tests/python/ltlf.py | 47 +++++++++++++++++++++++++++++ 10 files changed, 226 insertions(+), 1 deletion(-) create mode 100644 spot/tl/ltlf.cc create mode 100644 spot/tl/ltlf.hh create mode 100644 tests/python/ltlf.py diff --git a/NEWS b/NEWS index af123c2a6..8cb302c9e 100644 --- a/NEWS +++ b/NEWS @@ -1,7 +1,16 @@ New in spot 2.1.2.dev (not yet released) + Command-line tools: + + * ltlfilt has a new option --from-ltlf to help reducing LTLf (i.e., + LTL over finite words) model checking to LTL model checking. This + is based on a transformation by De Giacomo & Vardi (IJCAI'13). + Library: + * from_ltlf() is a new function implementing the --from-ltlf + transformation described above. + * is_unambiguous() was rewritten in a more efficient way. * scc_info learned to determine the acceptance of simple SCCs made diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index c3da8fd8a..6fdf5b2dc 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -43,6 +43,7 @@ #include #include #include +#include #include #include #include @@ -71,6 +72,7 @@ enum { OPT_EQUIVALENT_TO, OPT_EXCLUSIVE_AP, OPT_EVENTUAL, + OPT_FROM_LTLF, OPT_GUARANTEE, OPT_IGNORE_ERRORS, OPT_IMPLIED_BY, @@ -143,6 +145,9 @@ static const argp_option options[] = "two of them may not be true at the same time. Use this option " "multiple times to declare independent groups of exclusive " "propositions.", 0 }, + { "from-ltlf", OPT_FROM_LTLF, "alive", OPTION_ARG_OPTIONAL, + "transform LTLf (finite LTL) to LTL by introducing some 'alive'" + " proposition", 0 }, DECLARE_OPT_R, LEVEL_DOC(4), /**************************************************/ @@ -277,6 +282,7 @@ static bool stutter_insensitive = false; static range ap_n = { -1, -1 }; static int opt_max_count = -1; static long int match_count = 0; +static const char* from_ltlf = nullptr; // We want all these variables to be destroyed when we exit main, to @@ -404,6 +410,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_LTL: ltl = true; break; + case OPT_FROM_LTLF: + from_ltlf = arg ? arg : "alive"; + break; case OPT_NEGATE: negate = true; break; @@ -560,6 +569,9 @@ namespace if (negate) f = spot::formula::Not(f); + if (from_ltlf) + f = spot::from_ltlf(f, from_ltlf); + if (remove_x) { // If simplification are enabled, we do them before and after. diff --git a/bin/man/ltlfilt.x b/bin/man/ltlfilt.x index ed234d45e..6fd20a014 100644 --- a/bin/man/ltlfilt.x +++ b/bin/man/ltlfilt.x @@ -50,6 +50,13 @@ Automata. Proceedings of CONCUR'00. LNCS 1877. Describe the syntactic LTL classes matched by \fB\-\-eventual\fR, and \fB\-\-universal\fR. +.TP +\(bu +Giuseppe De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and +Linear Dynamic Logic on Finite Traces. Proceedings of IJCAI'13. + +Describe the transformation implemented by \fB\-\-from\-ltlf\fR +to reduce LTLf model checking to LTL model checking. [SEE ALSO] .BR randltl (1), .BR ltldo (1) diff --git a/python/spot/impl.i b/python/spot/impl.i index b4eda4b25..96c821462 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -102,6 +102,7 @@ #include #include #include +#include #include #include @@ -386,6 +387,7 @@ namespace std { %include %include %include +%include %include %include diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index d4bd84089..5ab305edf 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2015 Laboratoire de Recherche et Développement de +## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de ## l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -32,6 +32,7 @@ tl_HEADERS = \ exclusive.hh \ formula.hh \ length.hh \ + ltlf.hh \ mutation.hh \ nenoform.hh \ parse.hh \ @@ -53,6 +54,7 @@ libtl_la_SOURCES = \ exclusive.cc \ formula.cc \ length.cc \ + ltlf.cc \ mark.cc \ mark.hh \ mutation.cc \ diff --git a/spot/tl/ltlf.cc b/spot/tl/ltlf.cc new file mode 100644 index 000000000..dcdcc68bd --- /dev/null +++ b/spot/tl/ltlf.cc @@ -0,0 +1,66 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include + +namespace spot +{ + namespace + { + formula from_ltlf_aux(formula f, formula alive) + { + auto t = [&alive] (formula f) { return from_ltlf_aux(f, alive); }; + switch (auto o = f.kind()) + { + case op::X: + case op::F: + return formula::unop(o, formula::And({alive, t(f[0])})); + case op::G: + return formula::G(formula::Or({formula::Not(alive), t(f[0])})); + // Note that the t() function given in the proof of Theorem 1 of + // the IJCAI'13 paper by De Giacomo & Vardi has a typo. + // t(a U b) should be equal to t(a) U t(b & alive). + // This typo is fixed in the Memocode'14 paper by Dutta & Vardi. + case op::U: + return formula::U(t(f[0]), formula::And({alive, t(f[1])})); + case op::R: + return formula::R(t(f[0]), + formula::Or({formula::Not(alive), t(f[1])})); + case op::M: + return formula::M(formula::And({alive, t(f[0])}), t(f[1])); + case op::W: + return formula::W(formula::Or({formula::Not(alive), t(f[0])}), + t(f[1])); + default: + return f.map(t); + } + } + } + + formula from_ltlf(formula f, const char* alive) + { + if (!f.is_ltl_formula()) + throw std::runtime_error("from_ltlf() only supports LTL formulas"); + auto al = ((*alive == '!') + ? formula::Not(formula::ap(alive + 1)) + : formula::ap(alive)); + return formula::And({from_ltlf_aux(f, al), + formula::U(al, formula::G(formula::Not(al)))}); + } +} diff --git a/spot/tl/ltlf.hh b/spot/tl/ltlf.hh new file mode 100644 index 000000000..385ed1c12 --- /dev/null +++ b/spot/tl/ltlf.hh @@ -0,0 +1,50 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2016 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include + +namespace spot +{ + /// \ingroup tl_rewriting + /// \brief Convert an LTLf into an LTL formula. + /// + /// This is based on De Giacomo & Vardi (IJCAI'13) reduction from + /// LTLf (finite-LTL) to LTL. + /// + /// In this reduction, finite words are extended into infinite words + /// in which a new atomic proposition alive marks the + /// prefix of the infinite word that corresponds to the original + /// finite word. The formula is rewritten to ensure that the + /// eventualities occur during the "alive" portion. For instance + /// a U b becomes + /// (a U (b & alive))&(alive U G!alive). + /// + /// The \a alive argument can be used to change the name of the + /// atomic property used to introduce. Additionally if \a alive is + /// a string starting with and exclamation mark, e.g., + /// !dead then the atomic property will be built from + /// the rest of the string, and its negation will be used in the + /// transformation. Using !dead rather than + /// alive makes more sense if the state-space + /// introduces a dead property on states representing + /// the end of finite computations. + SPOT_API formula from_ltlf(formula f, const char* alive = "alive"); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index f29445b27..fc5966e46 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -325,6 +325,7 @@ TESTS_python = \ python/implies.py \ python/interdep.py \ python/ltl2tgba.test \ + python/ltlf.py \ python/ltlparse.py \ python/ltlsimple.py \ python/minato.py \ diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 8854d1ab7..0ccaa3a36 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -178,6 +178,35 @@ F(GFa | Gb) F(b W GFa) EOF +# Restrict to LTL +run 0 ltlfilt --ltl formulas > formulas2 +mv formulas2 formulas + +checkopt --ltl --from-ltlf <in <. + +import spot + +lcc = spot.language_containment_checker() + +formulas = ['GFa', 'FGa', '(GFa) U b', + '(a U b) U c', 'a U (b U c)', + '(a W b) W c', 'a W (b W c)', + '(a R b) R c', 'a R (b R c)', + '(a M b) M c', 'a M (b M c)', + '(a R b) U c', 'a U (b R c)', + '(a M b) W c', 'a W (b M c)', + '(a U b) R c', 'a R (b U c)', + '(a W b) M c', 'a M (b W c)', + ] + +# The rewriting assume the atomic proposition will not change +# once we reache the non-alive part. +cst = spot.formula('G(X!alive => ((a <=> Xa) && (b <=> Xb) && (c <=> Xc)))') + +for f in formulas: + f1 = spot.formula(f) + f2 = f1.unabbreviate() + f3 = spot.formula_And([spot.from_ltlf(f1), cst]) + f4 = spot.formula_And([spot.from_ltlf(f2), cst]) + print("{}\t=>\t{}".format(f1, f3)) + print("{}\t=>\t{}".format(f2, f4)) + assert lcc.equal(f3, f4) + print()