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

@@ -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

bin/ltlfilt.cc

@@ -43,6 +43,7 @@
 #include <spot/tl/remove_x.hh>
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/exclusive.hh>
+#include <spot/tl/ltlf.hh>
 #include <spot/tl/print.hh>
 #include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/twaalgos/minimize.hh>
@@ -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.

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)

python/spot/impl.i

@@ -102,6 +102,7 @@
 #include <spot/tl/unabbrev.hh>
 #include <spot/tl/randomltl.hh>
 #include <spot/tl/length.hh>
+#include <spot/tl/ltlf.hh>
 #include <spot/tl/remove_x.hh>
 #include <spot/tl/relabel.hh>
 
@@ -386,6 +387,7 @@ namespace std {
 %include <spot/tl/unabbrev.hh>
 %include <spot/tl/randomltl.hh>
 %include <spot/tl/length.hh>
+%include <spot/tl/ltlf.hh>
 %include <spot/tl/remove_x.hh>
 %include <spot/tl/relabel.hh>
 

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					\

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 <http://www.gnu.org/licenses/>.
+
+#include <spot/tl/ltlf.hh>
+
+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)))});
+  }
+}

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 <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <spot/tl/formula.hh>
+
+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 <code>alive</code> 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
+  /// <code>a U b</code> becomes
+  /// <code>(a U (b & alive))&(alive U G!alive)</code>.
+  ///
+  /// 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.,
+  /// <code>!dead</code> then the atomic property will be built from
+  /// the rest of the string, and its negation will be used in the
+  /// transformation.  Using <code>!dead</code> rather than
+  /// <code>alive</code> makes more sense if the state-space
+  /// introduces a <code>dead</code> property on states representing
+  /// the end of finite computations.
+  SPOT_API formula from_ltlf(formula f, const char* alive = "alive");
+}

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 \

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 <<EOF
+(G(!alive | F(a & alive)) | F(alive & G(!alive | b))) & (alive U G!alive)
+F(alive & (G(!alive | F(a & alive)) | G(!alive | b))) & (alive U G!alive)
+F(alive & ((!alive | b) W G(!alive | F(a & alive)))) & (alive U G!alive)
+(G(!alive | F(a & alive)) | G(!alive | b)) & (alive U G!alive)
+((!alive | b) W G(!alive | F(a & alive))) & (alive U G!alive)
+(a U (alive & F(alive & b))) & (alive U G!alive)
+G(!alive | (a & X(alive & b))) & (alive U G!alive)
+X(a & alive) & (alive U G!alive)
+F(a & alive & !X(a & alive) & X(alive & b)) & (alive U G!alive)
+a & (b | c) & (alive U G!alive)
+EOF
+
+checkopt --ltl --from-ltlf='!dead' <<EOF
+(G(dead | F(a & !dead)) | F(!dead & G(b | dead))) & (!dead U Gdead)
+F(!dead & (G(dead | F(a & !dead)) | G(b | dead))) & (!dead U Gdead)
+F(!dead & ((b | dead) W G(dead | F(a & !dead)))) & (!dead U Gdead)
+(G(dead | F(a & !dead)) | G(b | dead)) & (!dead U Gdead)
+((b | dead) W G(dead | F(a & !dead))) & (!dead U Gdead)
+(a U (!dead & F(b & !dead))) & (!dead U Gdead)
+G(dead | (a & X(b & !dead))) & (!dead U Gdead)
+X(a & !dead) & (!dead U Gdead)
+F(a & !dead & !X(a & !dead) & X(b & !dead)) & (!dead U Gdead)
+a & (b | c) & (!dead U Gdead)
+EOF
 
 cat >in <<EOF
 a & Xb & c

tests/python/ltlf.py

@@ -0,0 +1,47 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2016 Laboratoire de Recherche et Développement de
+# l'Epita
+#
+# 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 <http://www.gnu.org/licenses/>.
+
+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()