From 39417037d78faa7d2d428d68d9b03a8809cf6042 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 13 Apr 2012 23:01:28 +0200 Subject: [PATCH] to_string: abbreviate [->i..j] and [=i..j] expressed using [*i..j] * src/ltlast/bunop.hh (is_bunop, is_Star): New functions. * src/ltlast/multop.hh (is_And, is_Or): Fix constness. (is_Concat, is_Fusion): New functions. * src/ltlast/unop.hh (is_unop, is_X, is_F, is_G, is_GF, is_FG): Fix constness. (is_Not): New function. * src/ltlvisit/tostring.cc (strip_star_not, match_goto, emit_bunop_child, resugar_concat): New methods. (visit(bunop)): Rewrite without calling format(). Detect the [->i..j] pattern. (visit(multop)): Call resugar_concat to detect [=i..j] patterns. --- src/ltlast/bunop.hh | 41 ++++++- src/ltlast/multop.hh | 24 +++- src/ltlast/unop.hh | 28 +++-- src/ltlvisit/tostring.cc | 229 +++++++++++++++++++++++++++++++++++---- 4 files changed, 287 insertions(+), 35 deletions(-) diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh index 968f03956..6a85ef1a9 100644 --- a/src/ltlast/bunop.hh +++ b/src/ltlast/bunop.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement +// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -120,6 +120,45 @@ namespace spot unsigned max_; }; + /// \brief Cast \a f into a bunop. + /// + /// Cast \a f into a bunop iff it is a bunop instance. Return 0 + /// otherwise. This is faster than \c dynamic_cast. + inline + bunop* + is_bunop(const formula* f) + { + if (f->kind() != formula::BUnOp) + return 0; + return static_cast(const_cast(f)); + } + + /// \brief Cast \a f into a bunop if it has type \a op. + /// + /// Cast \a f into a bunop iff it is a bunop instance with operator \a op. + /// Returns 0 otherwise. + inline + bunop* + is_bunop(const formula* f, bunop::type op) + { + if (f->kind() != formula::BUnOp) + return 0; + bunop* bo = static_cast(const_cast(f)); + if (bo->op() != op) + return 0; + return bo; + } + + /// \brief Cast \a f into a bunop if it is a Star. + /// + /// Return 0 otherwise. + inline + bunop* + is_Star(const formula* f) + { + return is_bunop(f, bunop::Star); + } + } } #endif // SPOT_LTLAST_BUNOP_HH diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index fd864338b..29414afed 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -216,7 +216,7 @@ namespace spot /// Return 0 otherwise. inline multop* - is_And(formula* f) + is_And(const formula* f) { return is_multop(f, multop::And); } @@ -226,10 +226,30 @@ namespace spot /// Return 0 otherwise. inline multop* - is_Or(formula* f) + is_Or(const formula* f) { return is_multop(f, multop::Or); } + + /// \brief Cast \a f into a multop if it is a Concat. + /// + /// Return 0 otherwise. + inline + multop* + is_Concat(const formula* f) + { + return is_multop(f, multop::Concat); + } + + /// \brief Cast \a f into a multop if it is a Fusion. + /// + /// Return 0 otherwise. + inline + multop* + is_Fusion(const formula* f) + { + return is_multop(f, multop::Fusion); + } } } diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index dd322dc35..e2d753380 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -131,11 +131,11 @@ namespace spot /// otherwise. This is faster than \c dynamic_cast. inline unop* - is_unop(formula* f) + is_unop(const formula* f) { if (f->kind() != formula::UnOp) return 0; - return static_cast(f); + return static_cast(const_cast(f)); } /// \brief Cast \a f into a unop if it has type \a op. @@ -144,22 +144,32 @@ namespace spot /// Returns 0 otherwise. inline unop* - is_unop(formula* f, unop::type op) + is_unop(const formula* f, unop::type op) { if (f->kind() != formula::UnOp) return 0; - unop* uo = static_cast(f); + unop* uo = static_cast(const_cast(f)); if (uo->op() != op) return 0; return uo; } + /// \brief Cast \a f into a unop if it is a Not. + /// + /// Return 0 otherwise. + inline + unop* + is_Not(const formula* f) + { + return is_unop(f, unop::Not); + } + /// \brief Cast \a f into a unop if it is a X. /// /// Return 0 otherwise. inline unop* - is_X(formula* f) + is_X(const formula* f) { return is_unop(f, unop::X); } @@ -169,7 +179,7 @@ namespace spot /// Return 0 otherwise. inline unop* - is_F(formula* f) + is_F(const formula* f) { return is_unop(f, unop::F); } @@ -179,7 +189,7 @@ namespace spot /// Return 0 otherwise. inline unop* - is_G(formula* f) + is_G(const formula* f) { return is_unop(f, unop::G); } @@ -189,7 +199,7 @@ namespace spot /// Return 0 otherwise. inline unop* - is_GF(formula* f) + is_GF(const formula* f) { unop* op = is_G(f); if (!op) @@ -202,7 +212,7 @@ namespace spot /// Return 0 otherwise. inline unop* - is_FG(formula* f) + is_FG(const formula* f) { unop* op = is_F(f); if (!op) diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 0dc90b7b8..d50685bc0 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -92,8 +92,8 @@ namespace spot " & ", " && ", " & ", - " ; ", - " : " + ";", + ":" }; const char* spin_kw[] = { @@ -121,8 +121,8 @@ namespace spot " && ", " && ", // not supported " & ", // not supported - " ; ", // not supported - " : ", // not supported + ";", // not supported + ":", // not supported }; static bool @@ -146,6 +146,32 @@ namespace spot return true; } + // If the formula has the form (!b)[*], return b. + static + formula* + strip_star_not(const formula* f) + { + if (bunop* s = is_Star(f)) + if (unop* n = is_Not(s->child())) + return n->child(); + return 0; + } + + // If the formula as position i in multop mo has the form + // (!b)[*];b with b being a Boolean formula, return b. + static + formula* + match_goto(const multop *mo, unsigned i) + { + assert(i + 1 < mo->size()); + formula* b = strip_star_not(mo->nth(i)); + if (!b || !b->is_boolean()) + return 0; + if (mo->nth(i + 1) == b) + return b; + return 0; + } + class to_string_visitor: public const_visitor { public: @@ -315,30 +341,115 @@ namespace spot closep(); } + void + emit_bunop_child(const formula* b) + { + // b[*] is OK, no need to print {b}[*]. However want braces + // for {!b}[*], the only unary operator that can be nested + // with [*] or any other BUnOp like [->i..j] or [=i..j]. + formula::opkind ck = b->kind(); + bool need_parent = (full_parent_ + || ck == formula::UnOp + || ck == formula::BinOp + || ck == formula::MultOp); + if (need_parent) + openp(); + b->accept(*this); + if (need_parent) + closep(); + } + void visit(const bunop* bo) { + const formula* c = bo->child(); + enum { Star, Goto, Equal } sugar = Star; + unsigned default_min = 0; + unsigned default_max = bunop::unbounded; + // Abbreviate "1[*]" as "[*]". - if (bo->child() != constant::true_instance()) + if (c != constant::true_instance()) { - // a[*] is OK, no need to print {a}[*]. - // However want braces for {!a}[*], the only unary - // operator that can be nested with [*]. + bunop::type op = bo->op(); + switch (op) + { + case bunop::Star: + if (multop* mo = is_Concat(c)) + { + unsigned s = mo->size(); + if (s == 2) + if (formula* b = match_goto(mo, 0)) + { + c = b; + sugar = Goto; + } + } + break; + case bunop::Goto: + sugar = Goto; + break; + case bunop::Equal: + sugar = Equal; + break; + } - formula::opkind ck = bo->child()->kind(); - bool need_parent = (full_parent_ - || ck == formula::UnOp - || ck == formula::BinOp - || ck == formula::MultOp); - - if (need_parent) - openp(); - bo->child()->accept(*this); - if (need_parent) - closep(); + emit_bunop_child(c); } - os_ << bo->format(); + unsigned min = bo->min(); + unsigned max = bo->max(); + switch (sugar) + { + case Star: + if (min == 1 && max == bunop::unbounded) + { + os_ << "[+]"; + return; + } + os_ << "[*"; + break; + case Equal: + os_ << "[="; + break; + case Goto: + os_ << "[->"; + default_min = 1; + default_max = 1; + break; + } + + // Beware that the default parameters of the Goto operator are + // not the same as Star or Equal: + // + // [->] = [->1..1] + // [->..] = [->1..unbounded] + // [*] = [*0..unbounded] + // [*..] = [*0..unbounded] + // [=] = [=0..unbounded] + // [=..] = [=0..unbounded] + // + // Strictly speaking [=] is not specified by PSL, and anyway we + // automatically rewrite Exp[=0..unbounded] as + // Exp[*0..unbounded], so we should never have to print [=] + // here. + // + // Also + // [*..] = [*0..unbounded] + + if (min != default_min || max != default_max) + { + // Always print the min_, even when it is equal to + // default_min, this way we avoid ambiguities (like + // when reading [*..3] near [->..2]) + os_ << min; + if (min != max) + { + os_ << ".."; + if (max != bunop::unbounded) + os_ << max; + } + } + os_ << "]"; } void @@ -433,6 +544,65 @@ namespace spot os_ << ")"; } + void + resugar_concat(const multop* mo) + { + unsigned max = mo->size(); + + for (unsigned i = 0; i < max; ++i) + { + if (i > 0) + emit(KConcat); + if (i + 1 < max) + { + // Try to match (!b)[*];b + formula* b = match_goto(mo, i); + if (b) + { + emit_bunop_child(b); + + // Wait... maybe we are looking at (!b)[*];b;(!b)[*] + // in which case it's b[=1]. + if (i + 2 < max && mo->nth(i) == mo->nth(i + 2)) + { + os_ << "[=1]"; + i += 2; + } + else + { + os_ << "[->]"; + ++i; + } + continue; + } + // Try to match ((!b)[*];b)[*i..j];(!b)[*] + if (bunop* s = is_Star(mo->nth(i))) + if (formula* b2 = strip_star_not(mo->nth(i + 1))) + if (multop* sc = is_Concat(s->child())) + if (formula* b1 = match_goto(sc, 0)) + if (b1 == b2) + { + emit_bunop_child(b1); + os_ << "[="; + unsigned min = s->min(); + os_ << min; + unsigned max = s->max(); + if (max != min) + { + os_ << ".."; + if (max != bunop::unbounded) + os_ << max; + } + os_ << "]"; + ++i; + continue; + } + } + mo->nth(i)->accept(*this); + } + } + + void visit(const multop* mo) { @@ -440,10 +610,21 @@ namespace spot top_level_ = false; if (!top_level) openp(); - unsigned max = mo->size(); + multop::type op = mo->op(); + + // Handle the concatenation separately, because we want to + // "resugar" some patterns. + if (op == multop::Concat) + { + resugar_concat(mo); + if (!top_level) + closep(); + return; + } + mo->nth(0)->accept(*this); keyword k = KFalse; // Initialize to something to please GCC. - switch (mo->op()) + switch (op) { case multop::Or: k = KOr; @@ -455,7 +636,8 @@ namespace spot k = KAndNLM; break; case multop::Concat: - k = KConcat; + // Handled by resugar_concat. + assert(0); break; case multop::Fusion: k = KFusion; @@ -463,6 +645,7 @@ namespace spot } assert(k != KFalse); + unsigned max = mo->size(); for (unsigned n = 1; n < max; ++n) { emit(k);