diff --git a/NEWS b/NEWS
index 14d4a8ac9..817d9d18f 100644
--- a/NEWS
+++ b/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
diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc
index abe3bede4..1026715e4 100644
--- a/src/bin/ltlfilt.cc
+++ b/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;
diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index 196fc6629..5dc76cd75 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -92,6 +92,7 @@ TESTS = \
kind.test \
lbt.test \
lenient.test \
+ isop.test \
syntimpl.test \
reduc.test \
reducpsl.test \
diff --git a/src/ltltest/isop.test b/src/ltltest/isop.test
new file mode 100755
index 000000000..989bbc459
--- /dev/null
+++ b/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 .
+
+. ./defs
+set -e
+
+cat >input< 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<-> ((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< 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
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 6a572a510..041f2e87a 100644
--- a/src/ltlvisit/simplify.cc
+++ b/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
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);
- f->accept(v);
- result = v.result();
+ if (f->is_boolean() && c->options.boolean_to_isop)
+ {
+ 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();
}
-
}
}
diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh
index 88da6b4b1..3f5133ea1 100644
--- a/src/ltlvisit/simplify.hh
+++ b/src/ltlvisit/simplify.hh
@@ -1,5 +1,5 @@
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement
-// de l'Epita (LRDE).
+// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// 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;