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

Add support for {SERE} and !{SERE} closure operators.

Browse source 
* src/ltlast/unop.hh, src/ltlast/unop.cc: Introduce Closure and
NegClosure operators.
* src/ltlparse/ltlparse.yy: Recognize {foo} as a Closure.
* src/ltlvisit/mark.cc: Consider NegClosure as a marked operator.
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor): Add option to
select whether the empty_word should act like true (for {SERE}
and {!SERE}) or false (for {SERE}<>->Exp or {SERE}[]->Exp).
(ltl_trad_visitor): Translate Closure and NegClosure.
* src/tgbatest/ltl2tgba.test: Add more tests.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc: Straightforward update to support or
assert on these new operators.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-09 09:48:08 +01:00
parent f618e6bc1a
commit 2f8c4ac8b7
17 changed files with 343 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/ltlast/unop.cc
View file

@ -1,8 +1,8 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<EFBFBD>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<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
// 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.
//
@ -101,6 +101,10 @@ namespace spot
return "Finish";
case Star:
return "Star";
case Closure:
return "Closure";
case NegClosure:
return "NegClosure";
}
// Unreachable code.
assert(0);
@ -145,7 +149,7 @@ namespace spot
if (child == constant::empty_word_instance())
return constant::true_instance();
}
break;
case Not:
{
@ -155,14 +159,31 @@ namespace spot
// !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)
if (u)
{
// "Not" is an involution.
if (u->op() == op)
{
formula* c = u->child()->clone();
u->destroy();
return c;
}
if (u->op() == Closure)
{
formula* c = unop::instance(NegClosure,
u->child()->clone());
u->destroy();
return c;
}
if (u->op() == NegClosure)
{
formula* c = unop::instance(Closure,
u->child()->clone());
u->destroy();
return c;
}
}
break;
}
@ -179,6 +200,22 @@ namespace spot
case Finish:
// No simplifications for Finish.
break;
case Closure:
if (child == constant::true_instance()
|| child == constant::empty_word_instance())
return constant::true_instance();
if (child == constant::false_instance())
return child;
break;
case NegClosure:
if (child == constant::true_instance()
|| child == constant::empty_word_instance())
return constant::false_instance();
if (child == constant::false_instance())
return constant::true_instance();
break;
}
pair p(op, child);

16
src/ltlast/unop.hh
View file

@ -1,8 +1,8 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<EFBFBD>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<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie.
// 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.
//
@ -47,6 +47,8 @@ namespace spot
Finish,
// Kleene Star
Star,
// Closure
Closure, NegClosure,
};
/// \brief Build an unary operator with operation \a op and
@ -69,6 +71,14 @@ namespace spot
/// - !1 = 0
/// - !0 = 1
/// - !!Exp = Exp
/// - !Closure(Exp) = NegClosure(Exp)
/// - !NegClosure(Exp) = Closure(Exp)
/// - Closure(#e) = 1
/// - Closure(1) = 1
/// - Closure(0) = 0
/// - NegClosure(#e) = 0
/// - NegClosure(1) = 0
/// - NegClosure(0) = 1
///
/// This rewriting implies that it is not possible to build an
/// LTL formula object that is SYNTACTICALLY equal to one of

3
src/ltlparse/ltlparse.yy
View file

@ -361,6 +361,8 @@ subformula: booleanatom
{ $$ = unop::instance(unop::Not, $2); }
| OP_NOT error
{ missing_right_op($$, @1, "not operator"); }
| bracedrationalexp
{ $$ = unop::instance(unop::Closure, $1); }
| bracedrationalexp OP_UCONCAT subformula
{ $$ = binop::instance(binop::UConcat, $1, $3); }
| bracedrationalexp OP_UCONCAT error
@ -369,6 +371,7 @@ subformula: booleanatom
{ $$ = binop::instance(binop::EConcat, $1, $3); }
| bracedrationalexp OP_ECONCAT error
{ missing_right_binop($$, $1, @2, "universal concat operator"); }
;
%%

7
src/ltlvisit/basicreduce.cc
View file

@ -239,11 +239,10 @@ namespace spot
return;
case unop::Finish:
result_ = unop::instance(unop::Finish, result_);
return;
case unop::Star:
result_ = unop::instance(unop::Star, result_);
case unop::Closure:
case unop::NegClosure:
result_ = unop::instance(uo->op(), result_);
return;
}
/* Unreachable code. */

2
src/ltlvisit/consterm.cc
View file

@ -80,6 +80,8 @@ namespace spot
case unop::F:
case unop::G:
case unop::Finish:
case unop::Closure:
case unop::NegClosure:
assert(!"unsupported operator");
break;
case unop::Star:

38
src/ltlvisit/mark.cc
View file

@ -59,8 +59,24 @@ namespace spot
}
void
visit(unop*)
visit(unop* uo)
{
switch (uo->op())
{
case unop::NegClosure:
result_ = true;
return;
case unop::Finish:
case unop::Star:
case unop::Closure:
case unop::Not:
case unop::X:
case unop::F:
case unop::G:
return;
}
/* Unreachable code. */
assert(0);
}
void
@ -148,7 +164,23 @@ namespace spot
void
visit(unop* uo)
{
switch (uo->op())
{
case unop::NegClosure:
has_mark_ = true;
/* fall through */
case unop::Finish:
case unop::Star:
case unop::Closure:
case unop::Not:
case unop::X:
case unop::F:
case unop::G:
result_ = uo->clone();
return;
}
/* Unreachable code. */
assert(0);
}
void
@ -181,7 +213,9 @@ namespace spot
binop* bo = dynamic_cast<binop*>(f);
if (!bo)
{
res->push_back(recurse(f));
}
else
{
switch (bo->op())
@ -317,7 +351,7 @@ namespace spot
case binop::Xor:
case binop::Implies:
case binop::Equiv:
assert(!"mark no defined on logic abbreviations");
assert(!"mark not defined on logic abbreviations");
case binop::U:
case binop::W:
case binop::M:

20
src/ltlvisit/nenoform.cc
View file

@ -108,15 +108,21 @@ 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_);
case unop::Closure:
result_ = unop::instance(negated_ ?
unop::NegClosure : unop::Closure,
recurse_(f, false));
return;
case unop::Star:
case unop::NegClosure:
result_ = unop::instance(negated_ ?
unop::Closure : uo->op(),
recurse_(f, false));
return;
/* !Finish(x), is not simplified */
/* !(a*) is not simplified */
result_ = unop::instance(unop::Star, recurse_(f, false));
case unop::Finish:
case unop::Star:
result_ = unop::instance(uo->op(), recurse_(f, false));
if (negated_)
result_ = unop::instance(unop::Not, result_);
return;

18
src/ltlvisit/reduce.cc
View file

@ -235,14 +235,6 @@ namespace spot
switch (uo->op())
{
case unop::Not:
result_ = unop::instance(unop::Not, result_);
return;
case unop::X:
result_ = unop::instance(unop::X, result_);
return;
case unop::F:
/* If f is a pure eventuality formula then F(f)=f. */
if (!(opt_ & Reduce_Eventuality_And_Universality)
@ -257,14 +249,14 @@ namespace spot
result_ = unop::instance(unop::G, result_);
return;
case unop::Not:
case unop::X:
case unop::Finish:
result_ = unop::instance(unop::Finish, result_);
return;
case unop::Star:
result_ = unop::instance(unop::Star, result_);
case unop::Closure:
case unop::NegClosure:
result_ = unop::instance(uo->op(), result_);
return;
}
/* Unreachable code. */
assert(0);

6
src/ltlvisit/syntimpl.cc
View file

@ -106,8 +106,9 @@ namespace spot
result_ = true;
return;
case unop::Finish:
return;
case unop::Star:
case unop::Closure:
case unop::NegClosure:
return;
}
/* Unreachable code. */
@ -337,8 +338,9 @@ namespace spot
return;
}
case unop::Finish:
return;
case unop::Star:
case unop::Closure:
case unop::NegClosure:
return;
}
/* Unreachable code. */

62
src/ltlvisit/tostring.cc
View file

@ -164,6 +164,7 @@ namespace spot
void
visit(const unop* uo)
{
top_level_ = false;
// The parser treats F0, F1, G0, G1, X0, and X1 as atomic
// propositions. So make sure we output F(0), G(1), etc.
bool need_parent = !!dynamic_cast<const constant*>(uo->child());
@ -196,24 +197,43 @@ namespace spot
os_ << "finish";
need_parent = true;
break;
case unop::Closure:
os_ << "{";
top_level_ = true;
break;
case unop::NegClosure:
os_ << "!{";
break;
case unop::Star:
// Do not output anything yet, star is a postfix operator.
// 1* is OK, no need to print (1)*.
need_parent = false;
// Do not output anything yet, star is a postfix operator.
break;
}
top_level_ = false;
if (need_parent)
if (need_parent || full_parent_)
os_ << "(";
uo->child()->accept(*this);
if (need_parent)
os_ << ")";
switch (uo->op())
{
case unop::Star:
os_ << "*";
break;
case unop::Closure:
case unop::NegClosure:
os_ << "}";
top_level_ = false;
break;
default:
break;
}
if (full_parent_ && !top_level)
os_ << ")";
if (uo->op() == unop::Star)
os_ << "*";
}
void
@ -377,15 +397,17 @@ namespace spot
bool top_level = top_level_;
if (full_parent_ && !top_level)
os_ << "(";
bool need_parent = false;
top_level_ = false;
switch (uo->op())
{
case unop::Not:
os_ << "!";
break;
case unop::X:
// The parser treats X0, and X1 as atomic propositions. So
// make sure we output X(0) and X(1).
// The parser treats X0, and X1 as atomic
// propositions. So make sure we output X(0) and X(1).
need_parent = !!dynamic_cast<const constant*>(uo->child());
if (full_parent_)
need_parent = false;
@ -401,14 +423,19 @@ namespace spot
os_ << "finish";
need_parent = true;
break;
case unop::Closure:
os_ << "{";
top_level_ = true;
break;
case unop::NegClosure:
os_ << "!{";
top_level_ = 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;
if (need_parent)
os_ << "(";
uo->child()->accept(*this);
@ -416,6 +443,21 @@ namespace spot
os_ << ")";
if (uo->op() == unop::Star)
os_ << "*";
switch (uo->op())
{
case unop::Star:
os_ << "*";
break;
case unop::Closure:
case unop::NegClosure:
os_ << "}";
top_level_ = false;
break;
default:
break;
}
if (full_parent_ && !top_level)
os_ << ")";
}

6
src/ltlvisit/tunabbrev.cc
View file

@ -1,4 +1,6 @@
// Copyright (C) 2003, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
@ -43,6 +45,8 @@ namespace spot
case unop::X:
case unop::Not:
case unop::Star:
case unop::Closure:
case unop::NegClosure:
this->super::visit(uo);
return;
case unop::F:

2
src/tgba/formula2bdd.cc
View file

@ -80,6 +80,8 @@ namespace spot
case unop::G:
case unop::X:
case unop::Star:
case unop::Closure:
case unop::NegClosure:
assert(!"unsupported operator");
case unop::Not:
{

2
src/tgbaalgos/eltl2tgba_lacim.cc
View file

@ -102,6 +102,8 @@ namespace spot
case unop::F:
case unop::G:
case unop::Star:
case unop::Closure:
case unop::NegClosure:
assert(!"unsupported operator");
}
/* Unreachable code. */

2
src/tgbaalgos/ltl2taa.cc
View file

@ -142,6 +142,8 @@ namespace spot
return;
case unop::Finish:
case unop::Star:
case unop::Closure:
case unop::NegClosure:
assert(!"unsupported operator");
return;
}

158
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -240,7 +240,8 @@ namespace spot
bdd label = bdd_exist(cube, d.next_set);
bdd dest_bdd = bdd_existcomp(cube, d.next_set);
const formula* dest = d.conj_bdd_to_formula(dest_bdd);
bdd_print_set(std::cerr, d.dict, label) << " => "
bdd_print_set(std::cerr, d.dict, label) << " => ";
bdd_print_set(std::cerr, d.dict, dest_bdd) << " = "
<< to_string(dest)
<< std::endl;
dest->destroy();
@ -297,8 +298,11 @@ namespace spot
{
public:
ratexp_trad_visitor(translate_dict& dict,
bool empty_word_is_true,
formula* to_concat = 0)
: dict_(dict), to_concat_(to_concat)
: dict_(dict),
empty_word_is_true_(empty_word_is_true),
to_concat_(to_concat)
{
}
@ -325,17 +329,10 @@ namespace spot
bdd now_to_concat()
{
if (to_concat_)
{
if (to_concat_ == constant::empty_word_instance())
return bddfalse;
bdd n = recurse(to_concat_);
return n;
}
else
{
return bddfalse;
}
if (to_concat_ && to_concat_ != constant::empty_word_instance())
return recurse(to_concat_);
return empty_word_is_true_ ? bddtrue : bddfalse;
}
void
@ -374,6 +371,9 @@ namespace spot
case unop::Not:
case unop::X:
case unop::Finish:
case unop::Closure:
case unop::NegClosure:
break;
assert(!"not a rational operator");
return;
case unop::Star:
@ -556,7 +556,7 @@ namespace spot
bdd
recurse(const formula* f, formula* to_concat = 0)
{
ratexp_trad_visitor v(dict_, to_concat);
ratexp_trad_visitor v(dict_, empty_word_is_true_, to_concat);
f->accept(v);
return v.result();
}
@ -565,6 +565,7 @@ namespace spot
private:
translate_dict& dict_;
bdd res_;
bool empty_word_is_true_;
formula* to_concat_;
};
@ -646,7 +647,9 @@ namespace spot
void
visit(const unop* node)
{
switch (node->op())
unop::type op = node->op();
switch (op)
{
case unop::F:
{
@ -691,6 +694,120 @@ namespace spot
res_ = bdd_ithvar(x);
break;
}
case unop::Closure:
{
rat_seen_ = true;
ratexp_trad_visitor v(dict_, true);
node->child()->accept(v);
bdd f1 = v.result();
res_ = bddfalse;
if (exprop_)
{
bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
bdd all_props = bdd_existcomp(f1, dict_.var_set);
while (all_props != bddfalse)
{
bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label;
formula* dest =
dict_.bdd_to_formula(bdd_exist(f1 & label,
dict_.var_set));
const formula* dest2;
if (constant_term_as_bool(dest))
{
dest->destroy();
res_ |= label;
}
else
{
dest2 = unop::instance(op, dest);
if (dest2 == constant::false_instance())
continue;
int x = dict_.register_next_variable(dest2);
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
}
}
else
{
minato_isop isop(f1);
bdd cube;
while ((cube = isop.next()) != bddfalse)
{
bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_formula(dest_bdd);
const formula* dest2;
if (constant_term_as_bool(dest))
{
dest->destroy();
res_ |= label;
}
else
{
dest2 = unop::instance(op, dest);
if (dest2 == constant::false_instance())
continue;
int x = dict_.register_next_variable(dest2);
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
}
}
}
break;
case unop::NegClosure:
{
rat_seen_ = true;
has_marked_ = true;
ratexp_trad_visitor v(dict_, true);
node->child()->accept(v);
bdd f1 = v.result();
// trace_ltl_bdd(dict_, f1);
bdd var_set = bdd_existcomp(bdd_support(f1), dict_.var_set);
bdd all_props = bdd_existcomp(f1, dict_.var_set);
res_ = !all_props &
// stick X(1) to preserve determinism.
bdd_ithvar(dict_.register_next_variable
(constant::true_instance()));
while (all_props != bddfalse)
{
bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label;
formula* dest =
dict_.bdd_to_formula(bdd_exist(f1 & label,
dict_.var_set));
// !{ Exp } is false if Exp accepts the empty word.
if (constant_term_as_bool(dest))
{
dest->destroy();
continue;
}
const formula* dest2 = unop::instance(op, dest);
if (dest == constant::false_instance())
continue;
int x = dict_.register_next_variable(dest2);
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
}
break;
case unop::Finish:
assert(!"unsupported operator");
break;
@ -776,7 +893,7 @@ namespace spot
// Recognize f2 on transitions going to destinations
// that accept the empty word.
bdd f2 = recurse(node->second());
ratexp_trad_visitor v(dict_);
ratexp_trad_visitor v(dict_, false);
node->first()->accept(v);
bdd f1 = v.result();
res_ = bddfalse;
@ -851,7 +968,7 @@ namespace spot
// word should recognize f2, and the automaton for f1
// should be understood as universal.
bdd f2 = recurse(node->second());
ratexp_trad_visitor v(dict_);
ratexp_trad_visitor v(dict_, false);
node->first()->accept(v);
bdd f1 = v.result();
res_ = bddtrue;
@ -931,10 +1048,13 @@ namespace spot
for (unsigned n = 0; n < s; ++n)
{
bdd res = recurse(node->nth(n));
//std::cerr << "=== in And" << std::endl;
//trace_ltl_bdd(dict_, res);
//std::cerr << "== in And (" << to_string(node->nth(n))
// << ")" << std::endl;
// trace_ltl_bdd(dict_, res);
res_ &= res;
}
//std::cerr << "=== And final" << std::endl;
// trace_ltl_bdd(dict_, res_);
break;
}
case multop::Or:

2
src/tgbaalgos/ltl2tgba_lacim.cc
View file

@ -151,6 +151,8 @@ namespace spot
}
case unop::Finish:
case unop::Star:
case unop::Closure:
case unop::NegClosure:
assert(!"unsupported operator");
}
/* Unreachable code. */

10
src/tgbatest/ltl2tgba.test
View file

@ -70,6 +70,16 @@ check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)'
check_psl '{(#e + a):c*:(#e + b)}<>->d'
check_psl '{a;e;f:(g*);h}<>->d'
check_psl '{(a:b)* & (c*:d)}<>->e'
check_psl '{(a:b)*}'
check_psl 'G{(a:b)*}'
check_psl '{a;b}'
check_psl '{(a;b)*}'
check_psl 'G{(a;b)*}'
check_psl '{a*}[]->{b*}'
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
# Ruah, Zarpas (2007).
check_psl '{1*;req;ack;1}[]->{start;busy*;done}'
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization.