ltl_simplifier: add a boolean_to_isop option and method

* src/ltlvisit/simplify.hh (ltl_simplifier_options): add
a boolean_to_isop option
(ltl_simplifier::boolean_to_isop): New method.
* src/ltlvisit/simplify.cc: Implement these.
* src/bin/ltlfilt.cc: Add a --boolean-to-isop option.
* src/ltltest/isop.test: New file.
* src/ltltest/Makefile.am: Add it.
* NEWS: Mention it.

NEWS

@@ -4,6 +4,16 @@ New in spot 1.0.1a (not released):
     - the on-line ltl2tgba.html interface can output deterministic or
       non-deterministic monitors.  However, and unlike the ltl2tgba
       command-line tool, it doesn't different output formats.
+    - the class ltl::ltl_simplifier now has an option to rewrite Boolean
+      subformulaes as irredundante-sum-of-product during the simplification
+      of any LTL/PSL formula.  The service is also available as a method
+      ltl_simplifier::boolean_to_isop() that applies this rewriting
+      to a Boolean formula and implements a cache.
+      ltlfilt as a new option --boolean-to-isop to try to apply the
+      above rewriting from the command-line:
+      	    % ltlfilt --boolean-to-isop -f 'GF((a->b)&(b->c))'
+	    GF((!a & !b) | (b & c))
+      This is currently not used anywhere else in the library.
   * Bug fixes:
     - 'ltl2tgba --high' is documented to be the same as 'ltl2tgba',
       but by default ltl2tgba forgot to enable LTL simplifications based

src/bin/ltlfilt.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -76,6 +76,7 @@ Exit status:\n\
 #define OPT_EQUIVALENT_TO 25
 #define OPT_RELABEL 26
 #define OPT_REMOVE_WM 27
+#define OPT_BOOLEAN_TO_ISOP 28
 
 static const argp_option options[] =
   {
@@ -95,6 +96,9 @@ static const argp_option options[] =
       "specified otherwise", 0 },
     { "remove-wm", OPT_REMOVE_WM, 0, 0,
       "rewrite operators W and M using U and R", 0 },
+    { "boolean-to-isop", OPT_BOOLEAN_TO_ISOP, 0, 0,
+      "rewrite Boolean subformulas as irredundant sum of products "
+      "(implies at least -r1)", 0 },
     DECLARE_OPT_R,
     LEVEL_DOC(4),
     /**************************************************/
@@ -159,6 +163,7 @@ static error_style_t error_style = drop_errors;
 static bool quiet = false;
 static bool nnf = false;
 static bool negate = false;
+static bool boolean_to_isop = false;
 static bool unique = false;
 static bool psl = false;
 static bool ltl = false;
@@ -238,6 +243,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_BOOLEAN:
       boolean = true;
       break;
+    case OPT_BOOLEAN_TO_ISOP:
+      boolean_to_isop = true;
+      break;
     case OPT_BSIZE_MIN:
       bsize_min = to_int(arg);
       break;
@@ -389,7 +397,7 @@ namespace
       if (negate)
 	f = spot::ltl::unop::instance(spot::ltl::unop::Not, f);
 
-      if (simplification_level)
+      if (simplification_level || boolean_to_isop)
 	{
 	  const spot::ltl::formula* res = simpl.simplify(f);
 	  f->destroy();
@@ -507,7 +515,11 @@ main(int argc, char** argv)
   if (jobs.empty())
     jobs.push_back(job("-", 1));
 
-  spot::ltl::ltl_simplifier simpl(simplifier_options());
+  if (boolean_to_isop && simplification_level == 0)
+    simplification_level = 1;
+  spot::ltl::ltl_simplifier_options opt = simplifier_options();
+  opt.boolean_to_isop = boolean_to_isop;
+  spot::ltl::ltl_simplifier simpl(opt);
   ltl_processor processor(simpl);
   if (processor.run())
     return 2;

src/ltltest/Makefile.am

@@ -92,6 +92,7 @@ TESTS = \
   kind.test \
   lbt.test \
   lenient.test \
+  isop.test \
   syntimpl.test \
   reduc.test \
   reducpsl.test \

src/ltltest/isop.test

@@ -0,0 +1,55 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013 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
+(a -> b) & (b -> d)
+(a -> b) & Xc & (b -> d)
+GF((a | b) & (b | d))
+{((a -> b) & (b -> d))*;a*}<>->((a | b) & (!b | !a))
+EOF
+
+# Make sure --boolean-to-isop works as expected...
+run 0 ../../bin/ltlfilt --boolean-to-isop input > output
+
+cat> expected<<EOF
+(!a & !b) | (b & d)
+(b | !a) & (d | !b) & Xc
+GF(b | (a & d))
+{{{{!a && !b} | {b && d}}}[*];a[*]}<>-> ((a & !b) | (b & !a))
+EOF
+
+cat output
+diff output expected
+
+# Make sure it would not give the same output without the option...
+run 0 ../../bin/ltlfilt input > output
+
+cat> expected<<EOF
+(a -> b) & (b -> d)
+(a -> b) & Xc & (b -> d)
+GF((a | b) & (b | d))
+{{{{a -> b} && {b -> d}}}[*];a[*]}<>-> ((a | b) & (!b | !a))
+EOF
+
+cat output
+diff output expected

src/ltlvisit/simplify.cc

@@ -32,6 +32,7 @@
 #include "ltlvisit/contain.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/snf.hh"
+#include "tgba/formula2bdd.hh"
 #include <cassert>
 
 namespace spot
@@ -105,6 +106,16 @@ namespace spot
 	      old->first->destroy();
 	    }
 	}
+	{
+	  f2f_map::iterator i = bool_isop_.begin();
+	  f2f_map::iterator end = bool_isop_.end();
+	  while (i != end)
+	    {
+	      f2f_map::iterator old = i++;
+	      old->second->destroy();
+	      old->first->destroy();
+	    }
+	}
 
 	dict->unregister_all_my_variables(this);
       }
@@ -127,7 +138,8 @@ namespace spot
 	   << "negative normal form:   " << nenoform_.size() << " entries\n"
 	   << "syntactic implications: " << syntimpl_.size() << " entries\n"
 	   << "boolean to bdd:         " << as_bdd_.size() << " entries\n"
-	   << "star normal form:       " << snf_cache_.size() << " entries\n";
+	   << "star normal form:       " << snf_cache_.size() << " entries\n"
+	   << "boolean isop:           " << bool_isop_.size() << " entries\n";
       }
 
       void
@@ -374,12 +386,26 @@ namespace spot
 	return ltl::star_normal_form(f, &snf_cache_);
       }
 
+      const formula*
+      boolean_to_isop(const formula* f)
+      {
+	f2f_map::const_iterator it = bool_isop_.find(f);
+	if (it != bool_isop_.end())
+	  return it->second->clone();
+
+	assert(f->is_boolean());
+	const formula* res = bdd_to_formula(as_bdd(f), dict);
+	bool_isop_[f->clone()] = res->clone();
+	return res;
+      }
+
     private:
       f2b_map as_bdd_;
       f2f_map simplified_;
       f2f_map nenoform_;
       syntimpl_cache_t syntimpl_;
       snf_cache snf_cache_;
+      f2f_map bool_isop_;
     };
 
 
@@ -3976,9 +4002,16 @@ namespace spot
 	    trace << " miss" << std::endl;
 	  }
 
-	simplify_visitor v(c);
+	if (f->is_boolean() && c->options.boolean_to_isop)
-	f->accept(v);
+	  {
-	result = v.result();
+	    result = c->boolean_to_isop(f);
+	  }
+	else
+	  {
+	    simplify_visitor v(c);
+	    f->accept(v);
+	    result = v.result();
+	  }
 
         trace << "** simplify_recursively(" << to_string(f) << ") result: "
 	      << to_string(result) << std::endl;
@@ -4459,6 +4492,12 @@ namespace spot
       return cache_->star_normal_form(f);
     }
 
+    const formula*
+    ltl_simplifier::boolean_to_isop(const formula* f)
+    {
+      return cache_->boolean_to_isop(f);
+    }
+
     bdd_dict*
     ltl_simplifier::get_dict() const
     {
@@ -4477,6 +4516,5 @@ namespace spot
       cache_->clear_as_bdd_cache();
       cache_->lcc.clear();
     }
-
   }
 }

src/ltlvisit/simplify.hh

@@ -1,5 +1,5 @@
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -37,14 +37,16 @@ namespace spot
 			     bool containment_checks = false,
 			     bool containment_checks_stronger = false,
 			     bool nenoform_stop_on_boolean = false,
-			     bool reduce_size_strictly = false)
+			     bool reduce_size_strictly = false,
+			     bool boolean_to_isop = false)
 	: reduce_basics(basics),
 	  synt_impl(synt_impl),
 	  event_univ(event_univ),
 	  containment_checks(containment_checks),
 	  containment_checks_stronger(containment_checks_stronger),
 	  nenoform_stop_on_boolean(nenoform_stop_on_boolean),
-	  reduce_size_strictly(reduce_size_strictly)
+	  reduce_size_strictly(reduce_size_strictly),
+	  boolean_to_isop(boolean_to_isop)
       {
       }
 
@@ -60,6 +62,8 @@ namespace spot
       // will be disabled.  Those larger formulae are normally easier
       // to translate, so we recommend to set this to false.
       bool reduce_size_strictly;
+      // If true, Boolean subformulae will be rewritten in ISOP form.
+      bool boolean_to_isop;
     };
 
     // fwd declaration to hide technical details.
@@ -154,6 +158,13 @@ namespace spot
       /// Cached version of spot::ltl::star_normal_form().
       const formula* star_normal_form(const formula* f);
 
+      /// \brief Rewrite a Boolean formula \a f into as an irredundant
+      /// sum of product.
+      ///
+      /// This uses a cache, so it is OK to call this with identical
+      /// arguments.
+      const formula* boolean_to_isop(const formula* f);
+
       /// Dump statistics about the caches.
       void print_stats(std::ostream& os) const;