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

Implement [->i..j] and [=i..j] as sugar with [*i..j].

Browse source 
* src/ltlast/bunop.hh, src/ltlast/bunop.cc (sugar_goto, sugar_equal):
New functions..
* src/ltlparse/ltlparse.yy: Use them.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-14 23:18:37 +02:00
parent 39417037d7
commit 210723e30c
3 changed files with 63 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/ltlast/bunop.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -25,6 +25,7 @@
#include <sstream>
#include "constant.hh"
#include "unop.hh"
#include "multop.hh"
namespace spot
{
@ -389,6 +390,39 @@ namespace spot
return static_cast<bunop*>(ap->clone());
}
formula*
bunop::sugar_goto(formula* b, unsigned min, unsigned max)
{
assert(b->is_boolean());
// b[->min..max] is implemented as ((!b)[*];b)[*min..max]
formula* s = bunop::instance(bunop::Star,
unop::instance(unop::Not, b->clone()));
return bunop::instance(bunop::Star,
multop::instance(multop::Concat, s, b),
min, max);
}
formula*
bunop::sugar_equal(formula* b, unsigned min, unsigned max)
{
assert(b->is_boolean());
// b[=0..] = 1[*]
if (min == 0 && max == unbounded)
{
b->destroy();
return instance(Star, constant::true_instance());
}
// b[=min..max] is implemented as ((!b)[*];b)[*min..max];(!b)[*]
formula* s = bunop::instance(bunop::Star,
unop::instance(unop::Not, b->clone()));
formula* t = bunop::instance(bunop::Star,
multop::instance(multop::Concat,
s->clone(), b),
min, max);
return multop::instance(multop::Concat, t, s);
}
unsigned
bunop::instance_count()
{

23
src/ltlast/bunop.hh
View file

@ -71,6 +71,29 @@ namespace spot
unsigned min = 0,
unsigned max = unbounded);
/// \brief Implement <code>b[->i..j]</code> using the Kleen star.
///
/// <code>b[->i..j]</code> is implemented as
/// <code>((!b)[*];b)[*i..j]</code>.
///
/// Note that \a min defaults to 1, not 0, because [->] means
/// [->1..].
///
/// \pre \a child must be a Boolean formula.
static formula* sugar_goto(formula* child,
unsigned min = 1,
unsigned max = unbounded);
/// \brief Implement b[=i..j] using the Kleen star.
///
/// <code>b[=i..j]</code> is implemented as
/// <code>((!b)[*];b)[*i..j];(!b)[*]</code>.
///
/// \pre \a child must be a Boolean formula.
static formula* sugar_equal(formula* child,
unsigned min = 0,
unsigned max = unbounded);
virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const;