alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Introduce rational operators and trivial simplification rules.

Browse source 
Trivial simplifications rules (such as "FFa=Fa" or "x&1=x")
are performed any time a formule is instanciated.

* src/ltlast/constant.hh, src/ltlast/constant.cc
(true_instance, true_instance_): Declare the true_instance_ as a
static member, and move true_instance() into the .hh so it gets
inlined.  Have true_instance_ as a class variable will ensure that
it is the first formula instantiated.  Binop simplifications rely
on this to order arguments.
(false_instance, false_instance_): Likewise.
(empty_word_instance, empty_word_instance_): New method and static
member.
* src/ltlast/formula.hh (formula::formula): If max_count_ ever
loops, skip the first three values so that constants always have
smaller hash codes.
* src/ltlast/binop.hh, src/ltlast/binop.cc (instance): Add
simplifications and document them.
* src/ltlast/multop.hh (multop::Concat): New operator.
* src/ltlast/multop.cc (op_name): Handle Concat.
(instance): Inline Concat arguments without reordering.  Handle
absorbent and neutral elements for all operators.
* src/ltlast/unop.hh (unop::Star): New operator.
* src/ltlast/unop.cc (op_name): Handle Star.
(instance): Handle Star, and add trivial simplifications for
other unary operators.
* src/ltlparse/ltlparse.yy (OP_CONCAT, OP_STAR, CONST_EMPTYWORD):
Declare these new operators and add rules for them.
* src/ltlparse/ltlscan.ll (OP_CONCAT, OP_STAR, CONST_EMPTYWORD):
Output these new operators.
* src/ltltest/equals.test: New tests.
* src/ltltest/parse.test: Remove redundant test.
* src/ltltest/tunabbrev.test, src/tgbatest/emptchk.test: Adjust tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc: Complete visitors to handle new
operators.
* src/ltltest/nenoform.test: More tests.
* src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::visit):
Clone formulae before instance() function actually have a chance
to destroy them.
* src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Adjust switches to assert on new
operators.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-11 14:29:46 +01:00
parent 4fcc4f829c
commit 546559b8c3
29 changed files with 575 additions and 120 deletions
Download patch file Download diff file Expand all files Collapse all files

114
src/ltlast/binop.cc
View file

@ -24,6 +24,8 @@
#include <cassert>
#include <utility>
#include "binop.hh"
#include "unop.hh"
#include "constant.hh"
#include "visitor.hh"
#include <iostream>
@ -127,25 +129,127 @@ namespace spot
binop::map binop::instances;
binop*
formula*
binop::instance(type op, formula* first, formula* second)
{
// Sort the operands of commutative operators, so that for
// example the formula instance for 'a xor b' is the same as
// that for 'b xor a'.
/// Trivial identities:
switch (op)
{
case Xor:
{
// Xor is commutative: sort operands.
formula_ptr_less_than cmp;
if (cmp(second, first) > 0)
std::swap(first, second);
}
// - (1 ^ Exp) = !Exp
// - (0 ^ Exp) = Exp
if (first == constant::true_instance())
return unop::instance(unop::Not, second);
if (first == constant::false_instance())
return second;
// We expect constants to appear first, because they are
// instantiated first.
assert(second != constant::false_instance());
assert(second != constant::true_instance());
break;
case Equiv:
if (second < first)
std::swap(first, second);
{
// Equiv is commutative: sort operands.
formula_ptr_less_than cmp;
if (cmp(second, first) > 0)
std::swap(first, second);
}
// - (0 <=> Exp) = !Exp
// - (1 <=> Exp) = Exp
if (first == constant::false_instance())
return unop::instance(unop::Not, second);
if (first == constant::true_instance())
return second;
// We expect constants to appear first, because they are
// instantiated first.
assert(second != constant::false_instance());
assert(second != constant::true_instance());
break;
case Implies:
/// - (1 => Exp) = Exp
/// - (0 => Exp) = 0
/// - (Exp => 1) = 1
/// - (Exp => 0) = !Exp
if (first == constant::true_instance())
return second;
if (first == constant::false_instance())
{
second->destroy();
return first;
}
if (second == constant::true_instance())
{
first->destroy();
return second;
}
if (second == constant::false_instance())
return unop::instance(unop::Not, first);
break;
case U:
case R:
/// - (Exp U 1) = 1
/// - (Exp U 0) = 0
/// - (0 U Exp) = Exp
if (second == constant::true_instance()
|| second == constant::false_instance()
|| first == constant::false_instance())
{
first->destroy();
return second;
}
break;
case W:
/// - (Exp W 1) = 1
/// - (0 W Exp) = Exp
/// - (1 W Exp) = 1
if (second == constant::true_instance()
|| first == constant::false_instance())
{
first->destroy();
return second;
}
if (first == constant::true_instance())
{
second->destroy();
return first;
}
break;
case R:
/// - (Exp R 1) = 1
/// - (Exp R 0) = 0
/// - (1 R Exp) = Exp
if (second == constant::true_instance()
|| second == constant::false_instance()
|| first == constant::true_instance())
{
first->destroy();
return second;
}
break;
case M:
// Non commutative operators.
/// - (Exp M 0) = 0
/// - (1 M Exp) = Exp
/// - (0 M Exp) = 0
if (second == constant::false_instance()
|| first == constant::true_instance())
{
first->destroy();
return second;
}
if (first == constant::false_instance())
{
second->destroy();
return first;
}
break;
}

32
src/ltlast/binop.hh
View file

@ -56,9 +56,37 @@ namespace spot
M //< strong release (dual of weak until)
};
/// Build an unary operator with operation \a op and
/// \brief Build a unary operator with operation \a op and
/// children \a first and \a second.
static binop* instance(type op, formula* first, formula* second);
///
/// Some reordering will be performed on arguments of commutative
/// operators (Xor and Equiv) to ensure that for instance (a <=> b)
/// is the same formula as (b <=> a).
///
/// Furthermore, the following trivial simplifications are
/// performed (the left formula is rewritten as the right
/// formula):
/// - (1 => Exp) = Exp
/// - (0 => Exp) = 0
/// - (Exp => 1) = 1
/// - (Exp => 0) = !Exp
/// - (1 ^ Exp) = !Exp
/// - (0 ^ Exp) = Exp
/// - (0 <=> Exp) = !Exp
/// - (1 <=> Exp) = Exp
/// - (Exp U 1) = 1
/// - (Exp U 0) = 0
/// - (0 U Exp) = Exp
/// - (Exp W 1) = 1
/// - (0 W Exp) = Exp
/// - (1 W Exp) = 1
/// - (Exp R 1) = 1
/// - (Exp R 0) = 0
/// - (1 R Exp) = Exp
/// - (Exp M 0) = 0
/// - (1 M Exp) = Exp
/// - (0 M Exp) = 0
static formula* instance(type op, formula* first, formula* second);
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;

28
src/ltlast/constant.cc
View file

@ -1,8 +1,8 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 6 (LIP6), d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -29,6 +29,10 @@ namespace spot
{
namespace ltl
{
constant constant::true_instance_(constant::True);
constant constant::false_instance_(constant::False);
constant constant::empty_word_instance_(constant::EmptyWord);
constant::constant(type val)
: val_(val)
{
@ -47,6 +51,8 @@ namespace spot
return "constant(1)";
case False:
return "constant(0)";
case EmptyWord:
return "constant(e)";
}
// Unreachable code.
assert(0);
@ -80,24 +86,12 @@ namespace spot
return "1";
case False:
return "0";
case EmptyWord:
return "#e";
}
// Unreachable code.
assert(0);
return 0;
}
constant*
constant::false_instance()
{
static constant f(constant::False);
return &f;
}
constant*
constant::true_instance()
{
static constant t(constant::True);
return &t;
}
}
}

18
src/ltlast/constant.hh
View file

@ -1,8 +1,6 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -38,7 +36,7 @@ namespace spot
class constant : public formula
{
public:
enum type { False, True };
enum type { False, True, EmptyWord };
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;
@ -50,9 +48,11 @@ namespace spot
virtual std::string dump() const;
/// Get the sole instance of spot::ltl::constant::constant(True).
static constant* true_instance();
static constant* true_instance() { return &true_instance_; }
/// Get the sole instance of spot::ltl::constant::constant(False).
static constant* false_instance();
static constant* false_instance() { return &false_instance_; }
/// Get the sole instance of spot::ltl::constant::constant(EmptyWord).
static constant* empty_word_instance() { return &empty_word_instance_; }
protected:
constant(type val);
@ -60,6 +60,12 @@ namespace spot
private:
type val_;
static constant true_instance_;
static constant false_instance_;
static constant empty_word_instance_;
// If you add new constants here, be sure to update the
// formula::formula() constructor.
};
}

14
src/ltlast/formula.hh
View file

@ -1,8 +1,6 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -73,7 +71,15 @@ namespace spot
class formula
{
public:
formula() : count_(++max_count) {}
formula() : count_(max_count++)
{
// If the counter of formulae ever loops, we want to skip the
// first three values, because they are permanently associated
// to constants, and its convenient to have constants smaller
// than all other formulae.
if (max_count == 0)
max_count = 3;
}
/// Entry point for vspot::ltl::visitor instances.
virtual void accept(visitor& v) = 0;

37
src/ltlast/multop.cc
View file

@ -1,8 +1,8 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// Paris 6 (LIP6), d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -110,6 +110,8 @@ namespace spot
return "And";
case Or:
return "Or";
case Concat:
return "Concat";
}
// Unreachable code.
assert(0);
@ -146,13 +148,24 @@ namespace spot
}
else
{
// All operator except "Concat" not commutative, so
// we just keep a list of the inlined arguments that
// should later be added to the vector.
// For concat we have to keep track of the order of
// all the arguments.
if (op == Concat)
inlined.push_back(*i);
++i;
}
}
v->insert(v->end(), inlined.begin(), inlined.end());
if (op == Concat)
*v = inlined;
else
v->insert(v->end(), inlined.begin(), inlined.end());
}
std::sort(v->begin(), v->end(), formula_ptr_less_than());
if (op != Concat)
std::sort(v->begin(), v->end(), formula_ptr_less_than());
formula* neutral;
formula* abs;
@ -166,15 +179,19 @@ namespace spot
neutral = constant::false_instance();
abs = constant::true_instance();
break;
case Concat:
neutral = constant::empty_word_instance();
abs = constant::false_instance();
break;
default:
neutral = 0;
abs = 0;
break;
}
// Remove duplicates. We can't use std::unique(), because we
// must destroy() any formula we drop. Also ignore neutral
// elements and handle absorbent elements.
// Remove duplicates (except for Concat). We can't use
// std::unique(), because we must destroy() any formula we drop.
// Also ignore neutral elements and handle absorbent elements.
{
formula* last = 0;
vec::iterator i = v->begin();
@ -194,7 +211,9 @@ namespace spot
}
else
{
last = *i++;
if (op != Concat) // Don't remove duplicates for Concat.
last = *i;
++i;
}
}
}

47
src/ltlast/multop.hh
View file

@ -1,8 +1,8 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 6 (LIP6), d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -38,12 +38,10 @@ namespace spot
/// \brief Multi-operand operators.
/// \ingroup ltl_ast
///
/// These operators are considered commutative and associative.
class multop : public ref_formula
{
public:
enum type { Or, And };
enum type { Or, And, Concat };
/// List of formulae.
typedef std::vector<formula*> vec;
@ -51,29 +49,46 @@ namespace spot
/// \brief Build a spot::ltl::multop with two children.
///
/// If one of the children itself is a spot::ltl::multop
/// with the same type, it will be merged. I.e., children
/// if that child will be added, and that child itself will
/// with the same type, it will be inlined. I.e., children
/// of that child will be added, and that child itself will
/// be destroyed. This allows incremental building of
/// n-ary ltl::multop.
///
/// This functions can perform slight optimizations and
/// may not return an ltl::multop objects. For instance
/// if \c first and \c second are equal, that formula is
/// returned as-is.
/// may not return an ltl::multop object. See the other
/// instance function for the list of rewritings.
static formula* instance(type op, formula* first, formula* second);
/// \brief Build a spot::ltl::multop with many children.
///
/// Same as the other instance() function, but take a vector of
/// formula in argument. This vector is acquired by the
/// formulae as argument. This vector is acquired by the
/// spot::ltl::multop class, the caller should allocate it with
/// \c new, but not use it (especially not destroy it) after it
/// has been passed to spot::ltl::multop.
///
/// This functions can perform slight optimizations and
/// may not return an ltl::multop objects. For instance
/// if the vector contain only one unique element, this
/// this formula will be returned as-is.
/// All operators (Or, And, Concat) are associative, and are
/// automatically inlined. Or and And are commutative, so their
/// argument are also sorted, to ensure that "a & b" is equal to
/// "b & a". For Or and And, duplicate arguments are also
/// removed.
///
/// Furthermore this function can perform slight optimizations
/// and may not return an ltl::multop object. For instance if
/// the vector contains only one unique element, this this
/// formula will be returned as-is. Neutral and absorbent element
/// are also taken care of. The following rewriting are performed
/// (the left patterns are rewritten as shown on the right):
///
/// - Concat(Exps1...,#e,Exps2...) = Concat(Exps1...,Exps2...)
/// - Concat(Exps1...,0,Exps2...) = 0
/// - Concat(Exp) = Exp
/// - And(Exps1...,1,Exps2...) = And(Exps1...,Exps2...)
/// - And(Exps1...,0,Exps2...) = 0
/// - And(Exp) = Exp
/// - Or(Exps1...,1,Exps2...) = 1
/// - Or(Exps1...,0,Exps2...) = And(Exps1...,Exps2...)
/// - Or(Exp) = Exp
static formula* instance(type op, vec* v);
virtual void accept(visitor& v);

80
src/ltlast/unop.cc
View file

@ -1,8 +1,8 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 6 (LIP6), d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -25,6 +25,7 @@
#include "visitor.hh"
#include <cassert>
#include <iostream>
#include "constant.hh"
namespace spot
{
@ -98,6 +99,8 @@ namespace spot
return "G";
case Finish:
return "Finish";
case Star:
return "Star";
}
// Unreachable code.
assert(0);
@ -106,9 +109,78 @@ namespace spot
unop::map unop::instances;
unop*
formula*
unop::instance(type op, formula* child)
{
// Some trivial simplifications.
switch (op)
{
// We have (0*) == (#e)
// (#e*) == (#e)
case Star:
if (child == constant::false_instance()
|| child == constant::empty_word_instance())
return constant::empty_word_instance();
// -- fall thru --
case F:
case G:
{
// F, G, * are idempotent.
unop* u = dynamic_cast<unop*>(child);
if (u && u->op() == op)
return u;
if (op == Star)
break;
// F(0) = G(0) = 0
// F(1) = G(1) = 1
if (child == constant::false_instance()
|| child == constant::true_instance())
return child;
// F(#e) = G(#e) = 1
if (child == constant::empty_word_instance())
return constant::true_instance();
}
case Not:
{
// !1 = 0
if (child == constant::true_instance())
return constant::false_instance();
// !0 = 1
if (child == constant::false_instance())
return constant::true_instance();
// Not is an involution.
unop* u = dynamic_cast<unop*>(child);
if (u && u->op() == op)
{
formula* c = u->child()->clone();
u->destroy();
return c;
}
break;
}
case X:
// X(1) = 1, X(0) = 0
if (child == constant::true_instance()
|| child == constant::false_instance())
return child;
// X(#e) = 1
if (child == constant::empty_word_instance())
return constant::true_instance();
break;
case Finish:
// No simplifications for Finish.
break;
}
pair p(op, child);
map::iterator i = instances.find(p);
if (i != instances.end())

41
src/ltlast/unop.hh
View file

@ -1,8 +1,8 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// 6 (LIP6), d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -40,11 +40,40 @@ namespace spot
class unop : public ref_formula
{
public:
enum type { Not, X, F, G, Finish }; // Finish is used in ELTL formulae.
enum type {
// LTL
Not, X, F, G,
// ELTL
Finish,
// Kleene Star
Star,
};
/// Build an unary operator with operation \a op and
/// \brief Build an unary operator with operation \a op and
/// child \a child.
static unop* instance(type op, formula* child);
///
/// The following trivial simplifications are performed
/// automatically (the left expression is rewritten as the right
/// expression):
/// - 0* = #e
/// - #e* = #e
/// - Exp** = Exp*
/// - FF(Exp) = F(Exp)
/// - GG(Exp) = G(Exp)
/// - F(0) = 0
/// - G(0) = 0
/// - F(1) = 1
/// - G(1) = 1
/// - F(#e) = 1
/// - G(#e) = 1
/// - !1 = 0
/// - !0 = 1
/// - !!Exp = Exp
///
/// This rewriting implies that it is not possible to build an
/// LTL formula object that is SYNTACTICALLY equal to one of
/// these left expressions.
static formula* instance(type op, formula* child);
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;

17
src/ltlparse/ltlparse.yy
View file

@ -83,12 +83,16 @@ using namespace spot::ltl;
%token OP_F "sometimes operator" OP_G "always operator"
%token OP_X "next operator" OP_NOT "not operator"
%token <str> ATOMIC_PROP "atomic proposition"
%token OP_STAR "star operator" OP_CONCAT "concat operator"
%token CONST_TRUE "constant true" CONST_FALSE "constant false"
%token END_OF_INPUT "end of formula"
%token END_OF_INPUT "end of formula" CONST_EMPTYWORD "empty word"
%token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix"
/* Priorities. */
/* Low priority regex operator. */
%left OP_CONCAT
/* Logical operators. */
%left OP_IMPLIES OP_EQUIV
%left OP_OR
@ -100,6 +104,9 @@ using namespace spot::ltl;
%nonassoc OP_F OP_G
%nonassoc OP_X
/* High priority regex operator. */
%nonassoc OP_STAR
/* Not has the most important priority after Wring's `=0' and `=1'. */
%nonassoc OP_NOT
@ -194,6 +201,8 @@ subformula: ATOMIC_PROP
{ $$ = constant::true_instance(); }
| CONST_FALSE
{ $$ = constant::false_instance(); }
| CONST_EMPTYWORD
{ $$ = constant::empty_word_instance(); }
| PAR_OPEN subformula PAR_CLOSE
{ $$ = $2; }
| PAR_OPEN error PAR_CLOSE
@ -220,6 +229,10 @@ subformula: ATOMIC_PROP
{ $$ = multop::instance(multop::Or, $1, $3); }
| subformula OP_OR error
{ missing_right_binop($$, $1, @2, "or operator"); }
| subformula OP_CONCAT subformula
{ $$ = multop::instance(multop::Concat, $1, $3); }
| subformula OP_CONCAT error
{ missing_right_binop($$, $1, @2, "concat operator"); }
| subformula OP_XOR subformula
{ $$ = binop::instance(binop::Xor, $1, $3); }
| subformula OP_XOR error
@ -264,6 +277,8 @@ subformula: ATOMIC_PROP
{ $$ = unop::instance(unop::Not, $2); }
| OP_NOT error
{ missing_right_op($$, @1, "not operator"); }
| subformula OP_STAR
{ $$ = unop::instance(unop::Star, $1); }
;
%%

6
src/ltlparse/ltlscan.ll
View file

@ -1,7 +1,7 @@
/* Copyright (C) 2010, 2011, Laboratoire de Recherche et Développement de
** l'Epita (LRDE).
** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** département Syst�mes R�partis Coop�ratifs (SRC), Université Pierre
** et Marie Curie.
**
** This file is part of Spot, a model checking library.
@ -75,6 +75,8 @@ flex_set_buffer(const char* buf)
/* ~ comes from Goal, ! from everybody else */
"!"|"~" BEGIN(0); return token::OP_NOT;
"#e" BEGIN(0); return token::CONST_EMPTYWORD;
/* & and | come from Spin. && and || from LTL2BA.
/\, \/, and xor are from LBTT.
--> and <--> come from Goal. */
@ -83,6 +85,8 @@ flex_set_buffer(const char* buf)
"^"|"xor" BEGIN(0); return token::OP_XOR;
"=>"|"->"|"-->" BEGIN(0); return token::OP_IMPLIES;
"<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV;
"*" BEGIN(0); return token::OP_STAR;
";" BEGIN(0); return token::OP_CONCAT;
/* <>, [], and () are used in Spin. */
"F"|"<>" BEGIN(0); return token::OP_F;

48
src/ltltest/equals.test
View file

@ -1,5 +1,5 @@
#! /bin/sh
# Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -68,3 +68,49 @@ run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a'
# Corner cases parsing
run 0 ../equals 'FFG__GFF' 'F(F(G("__GFF")))'
# Trivial simplifications
run 0 ../equals '0*' '#e'
run 0 ../equals '#e*' '#e'
run 0 ../equals 'Exp**' 'Exp*'
run 0 ../equals 'FF(Exp)' 'F(Exp)'
run 0 ../equals 'GG(Exp)' 'G(Exp)'
run 0 ../equals 'F(0)' '0'
run 0 ../equals 'G(0)' '0'
run 0 ../equals 'F(1)' '1'
run 0 ../equals 'G(1)' '1'
run 0 ../equals 'F(#e)' '1'
run 0 ../equals 'G(#e)' '1'
run 0 ../equals '!1' '0'
run 0 ../equals '!0' '1'
run 0 ../equals '!!Exp' 'Exp'
run 0 ../equals '(1 => Exp)' 'Exp'
run 0 ../equals '(0 => Exp)' '0'
run 0 ../equals '(Exp => 1)' '1'
run 0 ../equals '(Exp => 0)' '!Exp'
run 0 ../equals '(1 ^ Exp)' '!Exp'
run 0 ../equals '(0 ^ Exp)' 'Exp'
run 0 ../equals '(0 <=> Exp)' '!Exp'
run 0 ../equals '(1 <=> Exp)' 'Exp'
run 0 ../equals '(Exp U 1)' '1'
run 0 ../equals '(Exp U 0)' '0'
run 0 ../equals '(Exp R 1)' '1'
run 0 ../equals '(Exp R 0)' '0'
run 0 ../equals '(1 R Exp)' 'Exp'
run 0 ../equals FFx Fx
run 0 ../equals FFFFFx Fx
run 0 ../equals GGx Gx
run 0 ../equals GGGGGx Gx
run 0 ../equals '!!x' x
run 0 ../equals '!!!!!x' '!x'
run 0 ../equals '#e;x' x
run 0 ../equals 'x;#e' x
run 0 ../equals '#e;x;#e;#e' x
run 0 ../equals '#e;x;#e;x;#e' 'x;x'
run 0 ../equals 'x;x;x;#e;x;x' 'x;x;x;x;x'
run 0 ../equals 'x;0;x;x;x' '0'
run 0 ../equals '0*' '#e'
run 0 ../equals '#e*' '#e'
run 0 ../equals 'x;x;FF(0)' '0'

9
src/ltltest/nenoform.test
View file

@ -1,8 +1,8 @@
#! /bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC), Universit<69> Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
@ -66,3 +66,8 @@ run 0 ../nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
run 0 ../nenoform '!(a U (!b U ((a & b & c) R d)))' \
'!a R (b R ((!a | !b | !c) U !d))'
run 0 ../nenoform '!(GF a => FG b)' 'GFa & GF!b'
# Rational operators
run 0 ../nenoform '!(X((!Xa)*))' 'X!((X!a)*)'
run 0 ../nenoform 'X((Xa)*)' 'X((Xa)*)'
run 0 ../nenoform '!F!X!(GF(a);!FG(a);x)' 'GX!(GFa;GF!a;x)'

4
src/ltltest/parse.test
View file

@ -2,7 +2,7 @@
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC), Universit<69> Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
@ -42,8 +42,6 @@ for f in \
'a && .b.' \
'a + b' \
'a3214 | b' \
'a & b' \
'a && b' \
'a /\ b' \
'a || b' \
'a \/ b' \

9
src/ltltest/tunabbrev.test
View file

@ -1,8 +1,8 @@
#! /bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC), Universit<69> Pierre
# et Marie Curie.
#
# This file is part of Spot, a model checking library.
@ -55,5 +55,6 @@ run 0 ../tunabbrev '(a ^ b) | (b ^ c)' \
run 0 ../tunabbrev 'G a ' 'false R a'
run 0 ../tunabbrev 'GF a => F G(b)' \
'!(false R (true U a)) | (true U (false V b))'
run 0 ../tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
run 0 ../tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
run 0 ../tunabbrev 'GGGGa' 'false V a'
run 0 ../tunabbrev 'FFFfalse' '0'
run 0 ../tunabbrev 'FFFf' 'true U f'

17
src/ltlvisit/basicreduce.cc
View file

@ -1,8 +1,8 @@
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
// Paris 6 (LIP6), d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -241,6 +241,10 @@ namespace spot
case unop::Finish:
result_ = unop::instance(unop::Finish, result_);
return;
case unop::Star:
result_ = unop::instance(unop::Star, result_);
return;
}
/* Unreachable code. */
assert(0);
@ -477,7 +481,7 @@ namespace spot
|| b->op() == binop::M)
&& b->first() == a)
{
binop* r =
formula* r =
binop::instance(binop::M,
a->clone(),
b->second()->clone());
@ -490,7 +494,7 @@ namespace spot
|| b->op() == binop::U)
&& b->second() == a)
{
binop* r =
formula* r =
binop::instance(binop::U,
b->first()->clone(),
a->clone());
@ -656,7 +660,7 @@ namespace spot
|| b->op() == binop::W)
&& b->first() == a)
{
binop* r =
formula* r =
binop::instance(binop::W,
a->clone(),
b->second()->clone());
@ -779,6 +783,9 @@ namespace spot
}
break;
case multop::Concat:
std::copy(res->begin(), res->end(), tmpOther->end());
break;
}
res->clear();

2
src/ltlvisit/contain.cc
View file

@ -355,6 +355,8 @@ namespace spot
}
}
break;
case multop::Concat:
break;
}
if (changed)
{

40
src/ltlvisit/lunabbrev.cc
View file

@ -1,7 +1,7 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC), Universit<69> Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
@ -49,14 +49,15 @@ namespace spot
{
/* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */
case binop::Xor:
result_ = multop::instance(multop::Or,
multop::instance(multop::And, f1->clone(),
unop::instance(unop::Not,
f2)),
multop::instance(multop::And, f2->clone(),
unop::instance(unop::Not,
f1)));
return;
{
formula* a = multop::instance(multop::And, f1->clone(),
unop::instance(unop::Not,
f2->clone()));
formula* b = multop::instance(multop::And, f2,
unop::instance(unop::Not, f1));
result_ = multop::instance(multop::Or, a, b);
return;
}
/* f1 => f2 == !f1 | f2 */
case binop::Implies:
result_ = multop::instance(multop::Or,
@ -64,15 +65,18 @@ namespace spot
return;
/* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */
case binop::Equiv:
result_ = multop::instance(multop::Or,
multop::instance(multop::And,
f1->clone(), f2->clone()),
multop::instance(multop::And,
unop::instance(unop::Not,
f1),
unop::instance(unop::Not,
f2)));
return;
{
formula* f1c = f1->clone();
formula* f2c = f2->clone();
result_ =
multop::instance(multop::Or,
multop::instance(multop::And, f1c, f2c),
multop::instance(multop::And,
unop::instance(unop::Not, f1),
unop::instance(unop::Not, f2)));
return;
}
/* f1 U f2 == f1 U f2 */
/* f1 R f2 == f1 R f2 */
/* f1 W f2 == f1 W f2 */

33
src/ltlvisit/nenoform.cc
View file

@ -76,6 +76,10 @@ namespace spot
case constant::False:
result_ = constant::true_instance();
return;
case constant::EmptyWord:
result_ = unop::instance(unop::Not,
constant::empty_word_instance());
return;
}
/* Unreachable code. */
assert(0);
@ -104,12 +108,18 @@ namespace spot
result_ = unop::instance(negated_ ? unop::F : unop::G,
recurse(f));
return;
case unop::Finish:
/* Finish(x) is not simplified */
result_ = unop::instance(unop::Finish, recurse_(f, false));
if (negated_)
result_ = unop::instance(unop::Not, result_);
return;
case unop::Star:
/* !(a*) is not simplified */
result_ = unop::instance(unop::Star, recurse_(f, false));
if (negated_)
result_ = unop::instance(unop::Not, result_);
return;
}
/* Unreachable code. */
assert(0);
@ -184,9 +194,9 @@ namespace spot
void
visit(multop* mo)
{
multop::type op = mo->op();
/* !(a & b & c) == !a | !b | !c */
/* !(a | b | c) == !a & !b & !c */
multop::type op = mo->op();
if (negated_)
switch (op)
{
@ -196,12 +206,25 @@ namespace spot
case multop::Or:
op = multop::And;
break;
case multop::Concat:
break;
}
multop::vec* res = new multop::vec;
unsigned mos = mo->size();
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
result_ = multop::instance(op, res);
if (op != multop::Concat)
{
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
result_ = multop::instance(op, res);
}
else
{
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse_(mo->nth(i), false));
result_ = multop::instance(op, res);
if (negated_)
result_ = unop::instance(unop::Not, result_);
}
}
formula*

8
src/ltlvisit/reduce.cc
View file

@ -256,6 +256,11 @@ namespace spot
case unop::Finish:
result_ = unop::instance(unop::Finish, result_);
return;
case unop::Star:
result_ = unop::instance(unop::Star, result_);
return;
}
/* Unreachable code. */
assert(0);
@ -470,7 +475,8 @@ namespace spot
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
if (opt_ & Reduce_Syntactic_Implications)
if ((opt_ & Reduce_Syntactic_Implications)
&& (mo->op() != multop::Concat))
{
bool removed = true;

38
src/ltlvisit/syntimpl.cc
View file

@ -74,6 +74,8 @@ namespace spot
case constant::False:
result_ = false;
return;
case constant::EmptyWord:
result_ = true;
}
}
@ -105,6 +107,8 @@ namespace spot
return;
case unop::Finish:
return;
case unop::Star:
return;
}
/* Unreachable code. */
assert(0);
@ -195,6 +199,8 @@ namespace spot
if (syntactic_implication(f, mo->nth(i)))
result_ = true;
break;
case multop::Concat:
break;
}
}
@ -230,6 +236,15 @@ namespace spot
return false;
}
bool
special_case_check(const formula* f2)
{
const binop* f2b = dynamic_cast<const binop*>(f2);
if (!f2b)
return false;
return special_case(f2b);
}
int
result() const
{
@ -257,6 +272,9 @@ namespace spot
case constant::False:
result_ = true;
return;
case constant::EmptyWord:
result_ = true;
return;
}
/* Unreachable code. */
assert(0);
@ -283,10 +301,10 @@ namespace spot
case unop::F:
{
/* F(a) = true U a */
const binop* tmp = binop::instance(binop::U,
constant::true_instance(),
f1->clone());
if (special_case(tmp))
const formula* tmp = binop::instance(binop::U,
constant::true_instance(),
f1->clone());
if (special_case_check(tmp))
{
result_ = true;
tmp->destroy();
@ -300,10 +318,10 @@ namespace spot
case unop::G:
{
/* G(a) = false R a */
const binop* tmp = binop::instance(binop::R,
constant::false_instance(),
f1->clone());
if (special_case(tmp))
const formula* tmp = binop::instance(binop::R,
constant::false_instance(),
f1->clone());
if (special_case_check(tmp))
{
result_ = true;
tmp->destroy();
@ -316,6 +334,8 @@ namespace spot
}
case unop::Finish:
return;
case unop::Star:
return;
}
/* Unreachable code. */
assert(0);
@ -431,6 +451,8 @@ namespace spot
return;
result_ = true;
break;
case multop::Concat:
break;
}
}

20
src/ltlvisit/tostring.cc
View file

@ -174,6 +174,10 @@ namespace spot
os_ << "finish";
need_parent = true;
break;
case unop::Star:
// Do not output anything yet, star is a postfix operator.
need_parent = false;
break;
}
top_level_ = false;
@ -185,6 +189,9 @@ namespace spot
if (full_parent_ && !top_level)
os_ << ")";
if (uo->op() == unop::Star)
os_ << "*";
}
void
@ -227,6 +234,9 @@ namespace spot
case multop::And:
ch = " & ";
break;
case multop::Concat:
ch = ";";
break;
}
for (unsigned n = 1; n < max; ++n)
@ -351,6 +361,11 @@ namespace spot
os_ << "finish";
need_parent = true;
break;
case unop::Star:
// Do not output anything yet, star is a postfix operator.
// FIXME: is there a better way to output "Star" for Spin?
need_parent = false;
break;
}
top_level_ = false;
@ -359,6 +374,8 @@ namespace spot
uo->child()->accept(*this);
if (need_parent)
os_ << ")";
if (uo->op() == unop::Star)
os_ << "*";
if (full_parent_ && !top_level)
os_ << ")";
}
@ -403,6 +420,9 @@ namespace spot
case multop::And:
ch = " && ";
break;
case multop::Concat:
ch = ";";
break;
}
for (unsigned n = 1; n < max; ++n)

3
src/ltlvisit/tunabbrev.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -42,6 +42,7 @@ namespace spot
case unop::Finish:
case unop::X:
case unop::Not:
case unop::Star:
this->super::visit(uo);
return;
case unop::F:

5
src/tgba/formula2bdd.cc
View file

@ -63,6 +63,8 @@ namespace spot
case constant::False:
res_ = bddfalse;
return;
case constant::EmptyWord:
assert(!"unsupported operator");
}
/* Unreachable code. */
assert(0);
@ -77,6 +79,7 @@ namespace spot
case unop::F:
case unop::G:
case unop::X:
case unop::Star:
assert(!"unsupported operator");
case unop::Not:
{
@ -135,6 +138,8 @@ namespace spot
op = bddop_or;
res_ = bddfalse;
break;
case multop::Concat:
assert(!"unsupported operator");
}
assert(op != -1);
unsigned s = node->size();

5
src/tgbaalgos/eltl2tgba_lacim.cc
View file

@ -71,6 +71,8 @@ namespace spot
case constant::False:
res_ = bddfalse;
return;
case constant::EmptyWord:
assert(!"unsupported operator");
}
/* Unreachable code. */
assert(0);
@ -99,6 +101,7 @@ namespace spot
case unop::X:
case unop::F:
case unop::G:
case unop::Star:
assert(!"unsupported operator");
}
/* Unreachable code. */
@ -152,6 +155,8 @@ namespace spot
op = bddop_or;
res_ = bddfalse;
break;
case multop::Concat:
assert(!"unsupported operator");
}
assert(op != -1);
unsigned s = node->size();

8
src/tgbaalgos/ltl2taa.cc
View file

@ -102,6 +102,9 @@ namespace spot
}
case constant::False:
return;
case constant::EmptyWord:
assert(!"unsupported operator");
return;
}
/* Unreachable code. */
assert(0);
@ -138,7 +141,9 @@ namespace spot
succ_ = v.succ_;
return;
case unop::Finish:
case unop::Star:
assert(!"unsupported operator");
return;
}
/* Unreachable code. */
assert(0);
@ -313,6 +318,9 @@ namespace spot
succ_.push_back(*i);
}
return;
case multop::Concat:
assert(!"unsupported operator");
return;
}
/* Unreachable code. */
assert(0);

5
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -307,6 +307,8 @@ namespace spot
case constant::False:
res_ = bddfalse;
return;
case constant::EmptyWord:
assert(!"unsupported operator");
}
/* Unreachable code. */
assert(0);
@ -361,6 +363,7 @@ namespace spot
return;
}
case unop::Finish:
case unop::Star:
assert(!"unsupported operator");
}
/* Unreachable code. */
@ -440,6 +443,8 @@ namespace spot
op = bddop_or;
res_ = bddfalse;
break;
case multop::Concat:
assert(!"unsupported operator");
}
assert(op != -1);
unsigned s = node->size();

5
src/tgbaalgos/ltl2tgba_lacim.cc
View file

@ -76,6 +76,8 @@ namespace spot
case constant::False:
res_ = bddfalse;
return;
case constant::EmptyWord:
assert(!"unsupported operator");
}
/* Unreachable code. */
assert(0);
@ -148,6 +150,7 @@ namespace spot
return;
}
case unop::Finish:
case unop::Star:
assert(!"unsupported operator");
}
/* Unreachable code. */
@ -248,6 +251,8 @@ namespace spot
op = bddop_or;
res_ = bddfalse;
break;
case multop::Concat:
assert(!"unsupported operator");
}
assert(op != -1);
unsigned s = node->size();

2
src/tgbatest/emptchk.test
View file

@ -96,6 +96,6 @@ expect_ce 'Fa & Xb & GFc & Gd' 1
expect_ce 'Fa & Xa & GFc & Gc' 2
expect_ce 'Fc & X(a | Xb) & GF(a | Xb) & Gc' 1
expect_ce '!((FF a) <=> (F x))' 3
expect_no '!((FF a) <=> (F a))' 4
expect_no '!((FF a) <=> (F a))' 3
expect_no 'Xa && (!a U b) && !b && X!b' 4
expect_no '(a U !b) && Gb' 3