ltlfilt: add --sonf and --sonf-aps flags

* bin/ltlfilt.cc: Here.
* NEWS: Mention new ltlfilt flags.
* tests/Makefile.am, tests/core/sonf.test: Test these flags.

NEWS

@@ -9,8 +9,17 @@ New in spot 2.10.4.dev  (net yet released)
   - autfilt has a new --to-finite option, illustrated on
     https://spot.lrde.epita.fr/tut12.html
 
+  - ltlfilt has a new --sonf option to produce a formula's Suffix
+    Operator Normal Form, described in [cimatti.06.fmcad].  The
+    associated option --sonf-aps allows listing the newly introduced
+    atomic propositions.
+
   Library:
 
+  - The new function suffix_operator_normal_form() implements
+    transformation of formulas to Suffix Operator Normal Form,
+    described in [cimatti.06.fmcad].
+
   - "original-classes" is a new named property similar to
     "original-states".  It maps an each state to an unsigned integer
     such that if two classes are in the same class, they are expected

bin/ltlfilt.cc

@@ -38,6 +38,7 @@
 #include <spot/misc/hash.hh>
 #include <spot/misc/timer.hh>
 #include <spot/tl/simplify.hh>
+#include <spot/tl/sonf.hh>
 #include <spot/tl/length.hh>
 #include <spot/tl/relabel.hh>
 #include <spot/tl/unabbrev.hh>
@@ -100,6 +101,8 @@ enum {
   OPT_SIZE_MAX,
   OPT_SIZE_MIN,
   OPT_SKIP_ERRORS,
+  OPT_SONF,
+  OPT_SONF_APS,
   OPT_STUTTER_INSENSITIVE,
   OPT_SUSPENDABLE,
   OPT_SYNTACTIC_GUARANTEE,
@@ -127,6 +130,11 @@ static const argp_option options[] =
     { "negate", OPT_NEGATE, nullptr, 0, "negate each formula", 0 },
     { "nnf", OPT_NNF, nullptr, 0,
       "rewrite formulas in negative normal form", 0 },
+    { "sonf", OPT_SONF, "PREFIX", OPTION_ARG_OPTIONAL,
+      "rewrite formulas in suffix operator normal form", 0 },
+    { "sonf-aps", OPT_SONF_APS, "FILENAME", OPTION_ARG_OPTIONAL,
+      "when used with --sonf, output the newly introduced atomic "
+      "propositions", 0 },
     { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL,
       "relabel all atomic propositions, alphabetically unless " \
       "specified otherwise", 0 },
@@ -316,6 +324,7 @@ static range opt_nth = { 0, std::numeric_limits<int>::max() };
 static int opt_max_count = -1;
 static long int match_count = 0;
 static const char* from_ltlf = nullptr;
+static const char* sonf = nullptr;
 
 
 // We want all these variables to be destroyed when we exit main, to
@@ -327,6 +336,7 @@ static struct opt_t
   spot::bdd_dict_ptr dict = spot::make_bdd_dict();
   spot::exclusive_ap excl_ap;
   std::unique_ptr<output_file> output_define = nullptr;
+  std::unique_ptr<output_file> output_sonf = nullptr;
   spot::formula implied_by = nullptr;
   spot::formula imply = nullptr;
   spot::formula equivalent_to = nullptr;
@@ -460,6 +470,12 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_NNF:
       nnf = true;
       break;
+    case OPT_SONF:
+      sonf = arg ? arg : "sonf_";
+      break;
+    case OPT_SONF_APS:
+      opt->output_sonf.reset(new output_file(arg ? arg : "-"));
+      break;
     case OPT_OBLIGATION:
       obligation = true;
       break;
@@ -650,6 +666,25 @@ namespace
       if (nnf)
         f = simpl.negative_normal_form(f);
 
+      if (sonf != nullptr)
+        {
+          std::vector<std::string> new_aps;
+          std::tie(f, new_aps) = suffix_operator_normal_form(f, sonf);
+
+          if (opt->output_sonf
+              && output_format != count_output
+              && output_format != quiet_output)
+            {
+              for (size_t i = 0; i < new_aps.size(); ++i)
+                {
+                  if (i > 0)
+                    opt->output_sonf->ostream() << ' ';
+                  opt->output_sonf->ostream() << new_aps[i];
+                }
+              opt->output_sonf->ostream() << '\n';
+            }
+        }
+
       switch (relabeling)
         {
         case ApRelabeling:

doc/spot.bib

@@ -214,6 +214,18 @@
   doi		= {10.1109/DepCoS-RELCOMEX.2009.31}
 }
 
+@InProceedings{	cimatti.06.fmcad,
+  author	= {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone and
+		  Tonetta, Stefano},
+  title	= {From {PSL} to {NBA}: a Modular Symbolic Encoding},
+  booktitle	= {Proceedings of the 6th conference on Formal Methods in Computer
+		  Aided Design (FMCAD'06)},
+  pages	= {125--133},
+  year		= {2006},
+  publisher	= {IEEE Computer Society},
+  doi		= {10.1109/FMCAD.2006.19}
+}
+
 @Article{	  cimatti.08.tcad,
   author	= {Alessandro Cimatti and Marco Roveri and Stefano Tonetta},
   journal	= {IEEE Transactions on Computer Aided Design of Integrated

python/spot/impl.i

@@ -94,6 +94,7 @@
 #include <spot/tl/nenoform.hh>
 #include <spot/tl/print.hh>
 #include <spot/tl/simplify.hh>
+#include <spot/tl/sonf.hh>
 #include <spot/tl/unabbrev.hh>
 #include <spot/tl/randomltl.hh>
 #include <spot/tl/length.hh>
@@ -517,6 +518,7 @@ namespace std {
   %template(vectorbdd) vector<bdd>;
   %template(aliasvector) vector<pair<string, bdd>>;
   %template(vectorstring) vector<string>;
+  %template(pair_formula_vectorstring) pair<spot::formula, vector<string>>;
   %template(atomic_prop_set) set<spot::formula>;
   %template(relabeling_map) map<spot::formula, spot::formula>;
 }
@@ -577,6 +579,7 @@ namespace std {
 %include <spot/tl/contain.hh>
 %include <spot/tl/dot.hh>
 %include <spot/tl/nenoform.hh>
+%include <spot/tl/sonf.hh>
 %include <spot/tl/print.hh>
 %include <spot/tl/simplify.hh>
 %include <spot/tl/unabbrev.hh>

spot/tl/Makefile.am

@@ -44,6 +44,7 @@ tl_HEADERS =					\
   remove_x.hh					\
   simplify.hh					\
   snf.hh					\
+  sonf.hh					\
   unabbrev.hh
 
 noinst_LTLIBRARIES = libtl.la
@@ -68,4 +69,5 @@ libtl_la_SOURCES =				\
   remove_x.cc					\
   simplify.cc					\
   snf.cc					\
+  sonf.cc					\
   unabbrev.cc

spot/tl/sonf.cc

@@ -0,0 +1,185 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Developpement 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 "config.h"
+#include <spot/tl/nenoform.hh>
+#include <spot/tl/sonf.hh>
+
+#include <string>
+#include <unordered_set>
+#include <utility>
+#include <vector>
+
+namespace spot
+{
+  namespace
+  {
+    /// Uses `extractor` to extract some parts of the formula and replace them
+    /// with atomic propositions.
+    ///
+    /// Returns (f & g1 & g2 & .. & gn) with g1..gn the extracted subformulas.
+    ///
+    /// `extractor` should be a lambda taking the following parameters as input:
+    ///
+    /// - `formula` the formula to process
+    /// - `std::vector<formula>&` the vector that stores extracted subformulas
+    /// - `auto&&` itself, in case it needs to call itself recursively
+    ///   (formula::map for example)
+    /// - `bool` a boolean indicating whether the lambda is currently being
+    ///   called at the formula's "root"
+    /// - `bool` a boolean indicating whether the lambda is currently being
+    ///   called inside a toplevel `and` construct.
+    ///
+    /// Note that the last 2 boolean arguments can be used as you see fit in
+    /// your recursive calls, the first one being set to true in the original
+    /// call, and the second one to false.
+    ///
+    /// `extractor` should return the new rewritten formula.
+    ///
+    /// auto sample_extractor = [](formula f,
+    ///                            std::vector<formula>& extracted,
+    ///                            auto&& extractor,
+    ///                            bool top_level,
+    ///                            bool in_top_level_and) -> formula
+    template<typename Ext>
+    static formula
+    extract(formula f, Ext extractor)
+    {
+      std::vector<formula> extracted;
+      formula new_f = extractor(f, extracted, extractor, true, false);
+      extracted.push_back(new_f);
+      return formula::And(extracted);
+    }
+  }
+
+  std::pair<formula, std::vector<std::string>>
+  suffix_operator_normal_form(formula f, const std::string prefix)
+  {
+    // SONF can only be applied to formulas in negative normal form
+    f = negative_normal_form(f);
+
+    std::unordered_set<std::string> used_aps;
+    std::vector<std::string> added_aps;
+    size_t count = 0;
+
+    // identify all used ap names to avoid them when generating new ones
+    auto ap_indexer = [&used_aps](formula f) noexcept {
+      if (f.is(op::ap))
+        {
+          used_aps.insert(f.ap_name());
+          return true;
+        }
+
+      return false;
+    };
+
+    f.traverse(ap_indexer);
+
+    auto new_ap_name =
+      [&used_aps, &added_aps, &prefix, &count]() noexcept -> std::string
+    {
+      std::string new_name = prefix + std::to_string(count++);
+      while (used_aps.find(new_name) != used_aps.end())
+        new_name = prefix + std::to_string(count++);
+      used_aps.insert(new_name);
+      added_aps.push_back(new_name);
+      return new_name;
+    };
+
+    // extracts the SERE part and replaces it with an atomic proposition,
+    // storing the extracted formula in `extracted` and returning the rewritten
+    // original formula
+    auto sonf_extract = [&](formula f,
+                            std::vector<formula>& extracted,
+                            auto&& extractor,
+                            bool top_level,
+                            bool in_top_level_and) noexcept -> formula
+    {
+      const auto kind = f.kind();
+
+      switch (kind)
+        {
+        case op::G:
+          {
+            // skip if shape is G(!ap | (regex []-> formula)) and at top level
+            if ((top_level || in_top_level_and)
+                && f[0].is(op::Or)     // G(_ | _)
+                && f[0][0].is(op::Not)       // G(!_ | _)
+                && f[0][0][0].is(op::ap)       // G(!ap | _)
+                && f[0][1].is(op::EConcat, op::UConcat)) // G(!ap | (_ []-> _))
+                return f;
+            else
+              return f.map(extractor, extracted, extractor, false, false);
+          }
+        case op::EConcat:
+        case op::UConcat:
+          {
+            // recurse into rhs first (_ []-> rhs)
+            formula rhs =
+              f[1].map(extractor, extracted, extractor, false, false);
+            f = formula::binop(kind, f[0], rhs);
+
+            formula ap = formula::ap(new_ap_name());
+            extracted.push_back(formula::G(formula::Or({formula::Not(ap), f})));
+            return ap;
+          }
+        default:
+          // tracking if we're in a op::And at the formula root
+          in_top_level_and = top_level && f.is(op::And);
+          return f.map(extractor, extracted, extractor,
+                       false, in_top_level_and);
+        }
+    };
+
+    f = extract(f, sonf_extract);
+
+    auto ltl_extract = [&](formula f,
+                           std::vector<formula>& extracted,
+                           auto&& extractor,
+                           [[maybe_unused]]
+                           bool top_level,
+                           [[maybe_unused]]
+                           bool in_top_level_and) noexcept -> formula
+    {
+      switch (f.kind())
+        {
+        case op::EConcat:
+        case op::UConcat:
+          {
+            formula rhs = f[1];
+
+            if (rhs.is(op::ap))
+              return f;
+
+            formula ap = formula::ap(new_ap_name());
+            extracted.push_back(
+              formula::G(formula::Or({formula::Not(ap), rhs})));
+
+            return formula::binop(f.kind(), f[0], ap);
+          }
+        default:
+          return f.map(extractor, extracted, extractor, false, false);
+        }
+    };
+
+    f = extract(f, ltl_extract);
+
+    return {f, added_aps};
+  }
+}

spot/tl/sonf.hh

@@ -0,0 +1,44 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 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 <string>
+#include <utility>
+#include <vector>
+
+#include <spot/tl/formula.hh>
+
+namespace spot
+{
+  /// \ingroup tl_rewriting
+  /// \brief Helper to rewrite a PSL formula in Suffix Operator Normal Form.
+  ///
+  /// SONF is described in section 4 of \cite cimatti.06.fmcad
+  ///
+  /// The formula output by this function is guaranteed to be in Negative Normal
+  /// Form.
+  ///
+  /// \param f the PSL formula to rewrite
+  /// \param prefix the prefix to use to name newly introduced aps
+  /// \return a pair with the rewritten formula, and a vector containing the
+  ///         names of newly introduced aps
+  SPOT_API std::pair<formula, std::vector<std::string>>
+  suffix_operator_normal_form(formula f, const std::string prefix);
+}

tests/Makefile.am

@@ -198,7 +198,8 @@ TESTS_tl = \
   core/stutter-ltl.test \
   core/hierarchy.test \
   core/mempool.test \
-  core/format.test
+  core/format.test \
+  core/sonf.test
 
 TESTS_graph = \
   core/graph.test \
@@ -445,6 +446,7 @@ TESTS_python = \
   python/setxor.py \
   python/simplacc.py \
   python/simstate.py \
+  python/sonf.py \
   python/split.py \
   python/streett_totgba.py \
   python/streett_totgba2.py \

tests/core/sonf.test

@@ -0,0 +1,85 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2021 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/>.
+
+. ./defs
+set -e
+
+cat >input <<EOF
+G(c -> Fa) & G(b -> ({x[*]}[]-> c))
+{x[*]}[]-> F({y[*]}<>-> GFz)
+<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17)))
+{{true} || {[*0]}}[]-> (false)
+{{p14} & {{p0}[*]}}[]-> (p11)
+{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18)))))
+X({{true} || {[*0]}}[]-> ((p17) U ((p8) && (p17))))
+({{{p4} || {p5} || {{p16} <-> {{p15} -> {p11}}}}[*]}[]-> (false)) -> (p8)
+{[*1..6]}[]-> ((p9) V ((p9) || (!((p4) && (p19)))))
+X({{{[*0]} || {{{p10};{p14}}[:*2..3]}}[:*]}<>-> (p8))
+{{true} && {{p8}[*]}}<>-> (!(p10))
+<>(!(({{p7}[*1..2]}<>-> (p11)) V ((!(p9)) && ([]((p11) || (X(p10)))))))
+<>({{!{{p5} || {{!{p2}} <-> {p7}}}} & {[*]}}<>-> (p17))
+{{p0} || {{{[*0..2]}[:*2]}[*]}}<>-> ((p1) && (p6))
+EOF
+
+cat >expected <<EOF
+G(!c|Fa)&G(!b|({x[*]}[]-> c))
+s1&G(!s2|GFz)&G(!s0|({y[*]}<>-> s2))&G(!s3|Fs0)&G(!s1|({x[*]}[]-> s3))
+F(s0 R (1 U p17))&G(p9|!p17|!s1)&G(!s0|({p12[*0..3]}[]-> s1))
+s0&G!s1&G(!s0|({1|[*0]}[]-> s1))
+s0&G(!s0|({p14&p0[*]}[]-> p11))
+s0&G(!s1|(p3 R (p3|(X(0)&(p2 R p18)))))&G(!s0|({{!p3|p6}[*]}[]-> s1))
+Xs0&G(!s1|(p17 U (p8&p17)))&G(!s0|({1|[*0]}[]-> s1))
+(p8|s0)&G(!s0|({{p4|p5|{p16 && {p11|!p15}}|{!p11 && p15 && !p16}}[*]}<>-> s1))
+s0&G(!s1|(p9 R (!p4|p9|!p19)))&G(!s0|({[*1..6]}[]-> s1))
+G(!s0|({{[*0]|{p10;p14}[:*2..3]}[:*]}<>-> p8))&Xs0
+s0&G(!p10|!s1)&G(!s0|({1 && p8[*]}<>-> s1))
+F(s0 U (p9|F(!p11&X!p10)))&G(!p11|!s1)&G(!s0|({p7[*1..2]}[]-> s1))
+G(!s0|({{!p5 && {{!p2 && !p7}|{p2 && p7}}}&[*]}<>-> p17))&Fs0
+s0&G(!s1|(p1&p6))&G(!s0|({p0|[*0..2][:*2][*]}<>-> s1))
+EOF
+
+cat >expected-aps <<EOF
+
+s0 s1 s2 s3
+s0 s1
+s0 s1
+s0
+s0 s1
+s0 s1
+s0 s1
+s0 s1
+s0
+s0 s1
+s0 s1
+s0
+s0 s1
+EOF
+
+ltlfilt -F input --sonf=s --sonf-aps=stdout-aps \
+    | sed 's/ \([|&]\) /\1/g' > stdout
+diff expected stdout
+diff expected-aps stdout-aps
+
+# check idempotence
+ltlfilt -F expected --sonf=s --sonf-aps=stdout-aps \
+    | sed 's/ \([|&]\) /\1/g' > stdout
+diff expected stdout
+# should be 14 empty lines, no new aps introduced this time
+test "$(wc -l -m stdout-aps | awk '{print $1 " " $2}')" = "14 14"

tests/python/formulas.ipynb

@@ -976,6 +976,62 @@
     "print(ap)        # print as a string\n",
     "display(ap)      # LaTeX-style, for notebooks"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Converting to Suffix Operator Normal Form:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 27,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/latex": [
+       "$\\mathsf{G} (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathsf{F} a)$"
+      ],
+      "text/plain": [
+       "spot.formula(\"G({x[*]}[]-> Fa)\")"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/latex": [
+       "$\\mathsf{G} \\mathit{sonf\\_}_{0} \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{1} \\lor \\mathsf{F} a) \\land \\mathsf{G} (\\lnot \\mathit{sonf\\_}_{0} \\lor (\\{x^{\\star}\\}\\mathrel{\\Box\\kern-1.7pt\\raise.4pt\\hbox{$\\mathord{\\rightarrow}$}} \\mathit{sonf\\_}_{1}))$"
+      ],
+      "text/plain": [
+       "spot.formula(\"Gsonf_0 & G(!sonf_1 | Fa) & G(!sonf_0 | ({x[*]}[]-> sonf_1))\")"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "('sonf_0', 'sonf_1')"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "f = spot.formula('G({x*} []-> Fa)')\n",
+    "display(f)\n",
+    "\n",
+    "# In addition to the formula, returns a list of newly introduced APs\n",
+    "f, aps = spot.suffix_operator_normal_form(f, 'sonf_')\n",
+    "display(f)\n",
+    "display(aps)"
+   ]
   }
  ],
  "metadata": {

tests/python/sonf.py

@@ -0,0 +1,41 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2020 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/>.
+
+import spot
+
+formulas = """\
+{x[*]}[]-> F({y[*]}<>-> GFz)
+<>(({{p12}[*0..3]}[]-> ((p9) || (!(p17)))) V ((true) U (p17)))
+{{true} || {[*0]}}[]-> (false)
+{{p14} & {{p0}[*]}}[]-> (p11)
+{{{!{p6}} -> {!{p3}}}[*]}[]-> ((p3)V((p3) || ((X((false))) && ((p2)V(p18)))))
+"""
+
+for f1 in formulas.splitlines():
+    f1 = spot.formula(f1)
+    a1 = spot.translate(f1)
+
+    f2, aps = spot.suffix_operator_normal_form(f1, 'sonf_')
+    a2 = spot.translate(f2)
+    rm = spot.remove_ap()
+    for ap in aps:
+        rm.add_ap(ap)
+    a2 = rm.strip(a2)
+
+    assert(spot.are_equivalent(a1, a2))