Commit 546260e7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Maintain basic LTL properties using a bitfield inside formula objects.

This bitfield is easily updated as the formulae are constructed.
Doing so avoids many AST recursions to compute these properties
individually.  This patch removes the eventual_universal_visitor,
as well as the kind_of() function.

* src/ltlast/formula.hh (is_boolean, is_sugar_free_boolean,
is_in_nenoform, is_X_free, is_sugar_free_ltl,
is_ltl_formula, is_eltl_formula, is_psl_formula, is_eventual,
is_universal, is_marked): New methods to query formula
properties in constant time.
(get_props, ltl_prop): A method and structure for
implementation as a field bit in an unsigned, for fast
computation.
(print_formula_props): New function.
* src/ltlast/formula.cc (print_formula_props): Implement it.
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/multop.cc,
src/ltlast/unop.cc, src/ltlast/automatop.cc: Compute the
properties as instances are constructed.
* src/ltlparse/ltlparse.yy: Update to use is_boolean() instead
of kind_of().
* src/ltltest/kind.cc: Update to use print_formula_props().
* src/ltltest/kind.test: Adjust to test eventual and universal
properties.
* src/ltlvisit/kind.cc, src/ltlvisit/kind.hh: Delete these files.
* src/ltlvisit/Makefile.am: Remove kind.hh and kind.cc.
* src/ltlvisit/reduce.cc (recurse_eu, eventual_universal_visitor):
Remove, no longer needed.
(reduce_visitor, is_eventual, is_universal): Adjust to
use formula::is_eventual(), and formula::is_universal().
* src/ltlvisit/reduce.hh (is_eventual, is_universal): Declare as
deprecated.
parent 1671aa5d
// Copyright (C) 2009 Laboratoire de Recherche et Dveloppement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
......@@ -34,6 +34,17 @@ namespace spot
atomic_prop::atomic_prop(const std::string& name, environment& env)
: name_(name), env_(&env)
{
is.boolean = true;
is.sugar_free_boolean = true;
is.in_nenoform = true;
is.X_free = true;
is.sugar_free_ltl = true;
is.ltl_formula = true;
is.eltl_formula = true;
is.psl_formula = true;
is.eventual = false;
is.universal = false;
is.not_marked = true;
}
atomic_prop::~atomic_prop()
......
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
......@@ -30,6 +30,21 @@ namespace spot
automatop::automatop(const nfa::ptr nfa, vec* v, bool negated)
: nfa_(nfa), children_(v), negated_(negated)
{
is.boolean = false;
is.sugar_free_boolean = true;
is.in_nenoform = true;
is.X_free = true;
is.sugar_free_ltl = true;
is.ltl_formula = false;
is.eltl_formula = true;
is.psl_formula = false;
is.eventual = false;
is.universal = false;
is.not_marked = true;
unsigned s = v->size();
for (unsigned i = 0; i < s; ++i)
props &= (*v)[i]->get_props();
}
automatop::~automatop()
......
......@@ -36,6 +36,65 @@ namespace spot
binop::binop(type op, formula* first, formula* second)
: op_(op), first_(first), second_(second)
{
// Beware: (f U g) is purely eventual if both operands
// are purely eventual, unlike in the proceedings of
// Concur'00. (The revision of the paper available at
// http://www.bell-labs.com/project/TMP/ is fixed.) See
// also http://arxiv.org/abs/1011.4214 for a discussion
// about this problem. (Which we fixed in 2005 thanks
// to LBTT.)
// This means that we can use the following line to handle
// all cases of (f U g), (f R g), (f W g), (f M g) for
// universality and eventuality.
props = first->get_props() & second->get_props();
switch (op)
{
case Xor:
case Implies:
case Equiv:
is.sugar_free_boolean = false;
is.in_nenoform = false;
break;
case EConcatMarked:
is.not_marked = false;
// fall through
case EConcat:
case UConcat:
is.ltl_formula = false;
is.boolean = false;
is.eltl_formula = false;
break;
case U:
// 1 U a = Fa
if (first == constant::true_instance())
is.eventual = 1;
is.boolean = false;
is.eltl_formula = false;
break;
case W:
// a W 0 = Ga
if (second == constant::false_instance())
is.universal = 1;
is.boolean = false;
is.eltl_formula = false;
break;
case R:
// 0 R a = Ga
if (first == constant::false_instance())
is.universal = 1;
is.boolean = false;
is.eltl_formula = false;
break;
case M:
// a M 1 = Fa
if (second == constant::true_instance())
is.eventual = 1;
is.boolean = false;
is.eltl_formula = false;
break;
}
}
binop::~binop()
......
......@@ -25,7 +25,6 @@
#include <sstream>
#include "constant.hh"
#include "unop.hh"
#include "ltlvisit/kind.hh"
namespace spot
{
......@@ -34,6 +33,20 @@ namespace spot
bunop::bunop(type op, formula* child, unsigned min, unsigned max)
: op_(op), child_(child), min_(min), max_(max)
{
props = child->get_props();
switch (op_)
{
case Equal:
case Star:
case Goto:
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
is.eventual = false;
is.universal = false;
break;
}
}
bunop::~bunop()
......
......@@ -36,6 +36,36 @@ namespace spot
constant::constant(type val)
: val_(val)
{
switch (val)
{
case constant::True:
case constant::False:
is.boolean = true;
is.sugar_free_boolean = true;
is.in_nenoform = true;
is.X_free = true;
is.sugar_free_ltl = true;
is.ltl_formula = true;
is.eltl_formula = true;
is.psl_formula = true;
is.eventual = true;
is.universal = true;
is.not_marked = true;
break;
case constant::EmptyWord:
is.boolean = false;
is.sugar_free_boolean = false;
is.in_nenoform = true;
is.X_free = true;
is.sugar_free_ltl = true;
is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = true;
is.eventual = false;
is.universal = false;
is.not_marked = true;
break;
}
}
constant::~constant()
......
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
......@@ -23,6 +23,7 @@
#include "formula.hh"
#include "misc/hash.hh"
#include <iostream>
namespace spot
{
......@@ -60,5 +61,32 @@ namespace spot
// Not reference counted by default.
return false;
}
std::ostream&
print_formula_props(std::ostream& out, const formula* f, bool abbr)
{
const char* comma = abbr ? "" : ", ";
const char* sep = "";
#define proprint(m, a, l) \
if (f->m()) \
{ \
out << sep; out << (abbr ? a : l); \
sep = comma; \
}
proprint(is_boolean, "B", "Boolean formula");
proprint(is_sugar_free_boolean, "&", "without Boolean sugar");
proprint(is_in_nenoform, "!", "in negative normal form");
proprint(is_X_free, "x", "without X operator");
proprint(is_sugar_free_ltl, "f", "without LTL sugar");
proprint(is_ltl_formula, "L", "LTL formula");
proprint(is_eltl_formula, "E", "ELTL formula");
proprint(is_psl_formula, "P", "PSL formula");
proprint(is_eventual, "e", "pure eventuality");
proprint(is_universal, "u", "purely universal");
proprint(is_marked, "+", "marked");
return out;
}
}
}
......@@ -100,6 +100,123 @@ namespace spot
/// Return a canonic representation of the formula
virtual std::string dump() const = 0;
////////////////
// Properties //
////////////////
/// Whether the formula use only boolean operators.
bool is_boolean() const
{
return is.boolean;
}
/// Whether the formula use only AND, OR, and NOT operators.
bool is_sugar_free_boolean() const
{
return is.sugar_free_boolean;
}
/// \brief Whether the formula is in negative normal form.
///
/// A formula is in negative normal form if the not operators
/// occur only in front of atomic propositions.
bool is_in_nenoform() const
{
return is.in_nenoform;
}
/// Whether the formula avoid the X operator.
bool is_X_free() const
{
return is.X_free;
}
/// Whether the formula avoid the F and G operators.
bool is_sugar_free_ltl() const
{
return is.sugar_free_ltl;
}
/// Whether the formula use only LTL operators.
bool is_ltl_formula() const
{
return is.ltl_formula;
}
/// Whether the formula use only ELTL operators.
bool is_eltl_formula() const
{
return is.eltl_formula;
}
/// Whether the formula use only PSL operators.
bool is_psl_formula() const
{
return is.psl_formula;
}
/// \brief Whether the formula is purely eventual.
///
/// Pure eventuality formulae are defined in
/// \verbatim
/// @InProceedings{ etessami.00.concur,
/// author = {Kousha Etessami and Gerard J. Holzmann},
/// title = {Optimizing {B\"u}chi Automata},
/// booktitle = {Proceedings of the 11th International Conference on
/// Concurrency Theory (Concur'2000)},
/// pages = {153--167},
/// year = {2000},
/// editor = {C. Palamidessi},
/// volume = {1877},
/// series = {Lecture Notes in Computer Science},
/// publisher = {Springer-Verlag}
/// }
/// \endverbatim
///
/// A word that satisfies a pure eventuality can be prefixed by
/// anything and still satisfies the formula.
bool is_eventual() const
{
return is.eventual;
}
/// \brief Whether a formula is purely universal.
///
/// Purely universal formulae are defined in
/// \verbatim
/// @InProceedings{ etessami.00.concur,
/// author = {Kousha Etessami and Gerard J. Holzmann},
/// title = {Optimizing {B\"u}chi Automata},
/// booktitle = {Proceedings of the 11th International Conference on
/// Concurrency Theory (Concur'2000)},
/// pages = {153--167},
/// year = {2000},
/// editor = {C. Palamidessi},
/// volume = {1877},
/// series = {Lecture Notes in Computer Science},
/// publisher = {Springer-Verlag}
/// }
/// \endverbatim
///
/// Any (non-empty) suffix of a word that satisfies a purely
/// universal formula also satisfies the formula.
bool is_universal() const
{
return is.universal;
}
/// Whether the formula has an occurrence of EConcatMarked.
bool is_marked() const
{
return !is.not_marked;
}
/// The properties as a field of bits. For internal use.
unsigned get_props() const
{
return props;
}
/// Return a hash key for the formula.
size_t
hash() const
......@@ -118,6 +235,40 @@ namespace spot
/// \brief The hash key of this formula.
size_t count_;
struct ltl_prop
{
// All properties here should be expressed in such a a way
// that property(f && g) is just property(f)&property(g).
// This allows us to compute all properties of a compound
// formula in one operation.
//
// For instance we do not use a property that says "has
// temporal operator", because it would require an OR between
// the two arguments. Instead we have a property that
// says "no temporal operator", and that one is computed
// with an AND between the arguments.
//
// Also choose a name that makes sense when prefixed with
// "the formula is".
bool boolean:1; // No temporal operators.
bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
bool in_nenoform:1; // Negative Normal Form
bool X_free:1; // No X operators.
bool sugar_free_ltl:1; // No F and G operators.
bool ltl_formula:1; // Only LTL operators.
bool eltl_formula:1; // Only ELTL operators.
bool psl_formula:1; // Only PSL operators.
bool eventual:1; // Purely eventual formula.
bool universal:1; // Purely universal formula.
bool not_marked:1; // No occurrence of EConcatMarked
};
union
{
// Use an unsigned for fast computation of all properties.
unsigned props;
ltl_prop is;
};
private:
/// \brief Number of formulae created so far.
static size_t max_count;
......@@ -189,6 +340,10 @@ namespace spot
}
};
/// Print the properties of formula \a f on stream \a out.
std::ostream& print_formula_props(std::ostream& out,
const formula* f,
bool abbreviated = false);
}
}
......
......@@ -37,6 +37,32 @@ namespace spot
multop::multop(type op, vec* v)
: op_(op), children_(v)
{
unsigned s = v->size();
assert(s > 1);
props = (*v)[0]->get_props();
for (unsigned i = 1; i < s; ++i)
props &= (*v)[i]->get_props();
switch (op)
{
case Concat:
case Fusion:
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
is.eventual = false;
is.universal = false;
break;
case AndNLM:
// The non-matching-length-And (&) can only appear in the
// rational parts of PSL formula. We don't remove the
// Boolean flag, because applied to atomic propositions a&b
// has the same effect as a&&b.
case And:
case Or:
break;
}
}
multop::~multop()
......
......@@ -26,6 +26,7 @@
#include <cassert>
#include <iostream>
#include "constant.hh"
#include "atomic_prop.hh"
namespace spot
{
......@@ -34,6 +35,41 @@ namespace spot
unop::unop(type op, formula* child)
: op_(op), child_(child)
{
props = child->get_props();
switch (op)
{
case Not:
is.in_nenoform = !!dynamic_cast<atomic_prop*>(child);
break;
case X:
is.boolean = false;
is.X_free = false;
is.eltl_formula = false;
break;
case F:
is.boolean = false;
is.eltl_formula = false;
is.sugar_free_ltl = false;
is.eventual = true;
break;
case G:
is.boolean = false;
is.eltl_formula = false;
is.sugar_free_ltl = false;
is.universal = true;
break;
case Finish:
is.boolean = false;
is.ltl_formula = false;
is.psl_formula = false;
break;
case Closure:
case NegClosure:
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
break;
}
}
unop::~unop()
......
......@@ -35,7 +35,6 @@
#include <string>
#include "public.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/kind.hh"
struct minmax_t { unsigned min, max; };
}
......@@ -367,7 +366,7 @@ rationalexp: booleanatom
$1.min, $1.max); }
| rationalexp equalargs
{
if ((kind_of($1) & Boolean_Kind) == Boolean_Kind)
if ($1->is_boolean())
{
$$ = bunop::instance(bunop::Equal, $1, $2.min, $2.max);
}
......@@ -384,7 +383,7 @@ rationalexp: booleanatom
}
| rationalexp gotoargs
{
if ((kind_of($1) & Boolean_Kind) == Boolean_Kind)
if ($1->is_boolean())
{
$$ = bunop::instance(bunop::Goto, $1, $2.min, $2.max);
}
......
......@@ -22,7 +22,6 @@
#include <cassert>
#include <cstdlib>
#include "ltlparse/public.hh"
#include "ltlvisit/kind.hh"
#include "ltlast/allnodes.hh"
void
......@@ -44,9 +43,8 @@ main(int argc, char **argv)
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
return 2;
unsigned k = spot::ltl::kind_of(f1);
spot::ltl::print_kind(std::cout, k, true) << " = ";
spot::ltl::print_kind(std::cout, k, false) << std::endl;
spot::ltl::print_formula_props(std::cout, f1, true) << " = ";
spot::ltl::print_formula_props(std::cout, f1, false) << std::endl;
f1->destroy();
assert(spot::ltl::atomic_prop::instance_count() == 0);
......
......@@ -37,12 +37,18 @@ check 'a' 'B&!xfLEP'
check 'a<->b' 'BxfLEP'
check '!a' 'B&!xfLEP'
check '!(a|b)' 'B&xfLEP'
check 'F(a)' '&!xLPe'
check 'G(a)' '&!xLPu'
check 'a U b' '&!xfLP'
check 'a U Fb' '&!xLP'
check 'Ga U b' '&!xLP'
check '1 U a' '&!xfLPe'
check 'a W b' '&!xfLP'
check 'a W 0' '&!xfLPu'
check 'a M b' '&!xfLP'
check 'a M 1' '&!xfLPe'
check 'a R b' '&!xfLP'
check '0 R b' '&!xfLPu'
check '{a}|->!Xb' '&fP'
check '{a}|->X!b' '&!fP'
check '{a}|->!Gb' '&xP'
......
......@@ -35,7 +35,6 @@ ltlvisit_HEADERS = \
destroy.hh \
dotty.hh \
dump.hh \
kind.hh \
length.hh \
lunabbrev.hh \
mark.hh \
......@@ -58,7 +57,6 @@ libltlvisit_la_SOURCES = \
destroy.cc \
dotty.cc \
dump.cc \
kind.cc \
length.cc \
lunabbrev.cc \
mark.cc \
......
// Copyright (C) 2010 Laboratoire de Recherche et Dveloppement
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "kind.hh"
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
#include <iostream>
namespace spot
{
namespace ltl
{
namespace
{
class kind_visitor : public visitor
{
unsigned result_;
public:
kind_visitor()
: result_(All_Kind)
{
}
~kind_visitor()
{
}
unsigned
result()
{
return result_;
}
void
visit(atomic_prop*)
{
}