diff --git a/NEWS b/NEWS index 871bb9ef7..16fabf07c 100644 --- a/NEWS +++ b/NEWS @@ -3,6 +3,8 @@ New in spot 0.9a: * Bug fixes: - The random SERE generator was using the wrong operators for "and" and "or", mistaking And/Or with AndRat/OrRat. + - The translation of !{r} was incorrect when this subformula + was recurring (e.g. in G!{r}) and r had loops. New in spot 0.9 (2012-05-09): diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index eb759ea44..8ef4e2528 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -98,6 +98,7 @@ \newcommand{\sere}[1]{\texttt{\{}#1\texttt{\}}} \newcommand{\nsere}[1]{\texttt{!\{}#1\texttt{\}}} +\newcommand{\nsereMarked}[1]{\texttt{!+\{}#1\texttt{\}}} \newcommand{\seren}[1]{\texttt{\{}#1\texttt{\}!}} % rewriting rules that enlarge the formula @@ -974,15 +975,16 @@ instance using the following methods: \\\texttt{is\_syntactic\_persistence()}& Whether the formula is a syntactic persistence property. \\\texttt{is\_marked()}& Whether the formula contains a special - ``marked'' version of the $\Esuffix$ operator.\footnotemark + ``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\footnotemark \\\texttt{accepts\_eword()}& Whether the formula accepts $\eword$. (This can only be true for a SERE formula.) \end{tabulary} -\footnotetext{This special operator is used when translating recurring - $\Esuffix$, it is rendered as $\EsuffixMarked$ and it obeys the same - simplification rules and properties as $\Esuffix$ (except for the - \texttt{is\_marked()} property).} +\footnotetext{These ``marked'' operators are used when + translating recurring $\Esuffix$ or $\nsere{r}$ operators. They are + rendered as $\EsuffixMarked$ and $\nsereMarked{r}$ and obey the + same simplification rules and properties as their unmarked + counterpart (except for the \texttt{is\_marked()} property).} \section{Pure Eventualities and Purely Universal Formul\ae{}} \label{sec:eventuniv} diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index ef07b72c6..ab71b172e 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -112,7 +112,8 @@ namespace spot is.accepting_eword = false; break; case NegClosure: - is.not_marked = false; + case NegClosureMarked: + is.not_marked = (op == NegClosure); is.boolean = false; is.ltl_formula = false; is.eltl_formula = false; @@ -198,6 +199,8 @@ namespace spot return "Closure"; case NegClosure: return "NegClosure"; + case NegClosureMarked: + return "NegClosureMarked"; } // Unreachable code. assert(0); @@ -297,6 +300,7 @@ namespace spot break; case NegClosure: + case NegClosureMarked: // {1} = 0, {[*0]} = 0 if (child == constant::true_instance() || child == constant::empty_word_instance()) diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index e1534005b..09ab6bc8f 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -47,7 +47,7 @@ namespace spot // ELTL Finish, // Closure - Closure, NegClosure, + Closure, NegClosure, NegClosureMarked }; /// \brief Build an unary operator with operation \a op and diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test index 122364d95..592c1a50a 100755 --- a/src/ltltest/kind.test +++ b/src/ltltest/kind.test @@ -115,7 +115,7 @@ check '{a;b*;c}' '&!xfPsopr' check '{a;b*;c}!' '&!xfPgopr' check '!{a;b*;c}!' '&xfPsopr' # The negative normal form is {a;b*;c}[]->0 check '{a;b*;c}[]->0' '&!xfPsopr' -check '!{a;b*;c}' '&!xfPgopr+' +check '!{a;b*;c}' '&!xfPgopr' run 0 ../consterm '1' run 0 ../consterm '0' diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index eebce4ba7..89a60fc92 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -22,6 +22,8 @@ #include "ltlast/allnodes.hh" #include #include +#include +#include #include "ltlvisit/tostring.hh" #include "misc/casts.hh" @@ -103,21 +105,25 @@ namespace spot { typedef std::set > pset; - pset Epairs, EMpairs; + pset empairs; + typedef std::set sset; + sset nmset; + typedef std::vector unbinop; + unbinop elist; + typedef std::vector ununop; + ununop nlist; for (unsigned i = 0; i < mos; ++i) { const formula* f = mo->nth(i); - - if (f->kind() != formula::BinOp) + if (const binop* bo = is_binop(f)) { - res->push_back(recurse(f)); - } - else - { - const binop* bo = static_cast(f); switch (bo->op()) { + case binop::EConcatMarked: + empairs.insert(std::make_pair(bo->first(), + bo->second())); + // fall through case binop::Xor: case binop::Implies: case binop::Equiv: @@ -129,29 +135,49 @@ namespace spot res->push_back(recurse(f)); break; case binop::EConcat: - assert(mo->op() == multop::And); - Epairs.insert(std::make_pair(bo->first(), - bo->second())); - break; - case binop::EConcatMarked: - assert(mo->op() == multop::And); - EMpairs.insert(std::make_pair(bo->first(), - bo->second())); + elist.push_back(bo); break; } } + if (const unop* uo = is_unop(f)) + { + switch (uo->op()) + { + case unop::NegClosureMarked: + nmset.insert(uo->child()); + // fall through + case unop::Not: + case unop::X: + case unop::F: + case unop::G: + case unop::Finish: + case unop::Closure: + res->push_back(recurse(f)); + break; + case unop::NegClosure: + nlist.push_back(uo); + break; + } + } + else + { + res->push_back(recurse(f)); + } } - for (pset::const_iterator i = EMpairs.begin(); - i != EMpairs.end(); ++i) - res->push_back(binop::instance(binop::EConcatMarked, - i->first->clone(), - i->second->clone())); - for (pset::const_iterator i = Epairs.begin(); - i != Epairs.end(); ++i) - if (EMpairs.find(*i) == EMpairs.end()) - res->push_back(binop::instance(binop::EConcat, - i->first->clone(), - i->second->clone())); + // Keep only the non-marked EConcat for which we + // have not seen a similar EConcatMarked. + for (unbinop::const_iterator i = elist.begin(); + i != elist.end(); ++i) + if (empairs.find(std::make_pair((*i)->first(), + (*i)->second())) + == empairs.end()) + res->push_back((*i)->clone()); + // Keep only the non-marked NegClosure for which we + // have not seen a similar NegClosureMarked. + for (ununop::const_iterator i = nlist.begin(); + i != nlist.end(); ++i) + if (nmset.find((*i)->child()) == nmset.end()) + res->push_back((*i)->clone()); } } result_ = multop::instance(mo->op(), res); @@ -212,7 +238,24 @@ namespace spot void visit(const unop* uo) { - result_ = uo->clone(); + switch (uo->op()) + { + case unop::Not: + case unop::X: + case unop::F: + case unop::G: + case unop::Finish: + case unop::Closure: + case unop::NegClosureMarked: + result_ = uo->clone(); + return; + case unop::NegClosure: + result_ = unop::instance(unop::NegClosureMarked, + uo->child()->clone()); + return; + } + /* Unreachable code. */ + assert(0); } void @@ -245,13 +288,13 @@ namespace spot case binop::M: case binop::R: case binop::UConcat: + case binop::EConcatMarked: result_ = bo->clone(); return; - case binop::EConcatMarked: case binop::EConcat: { const formula* f1 = bo->first()->clone(); - const formula* f2 = recurse(bo->second()); + const formula* f2 = bo->second()->clone(); result_ = binop::instance(binop::EConcatMarked, f1, f2); return; } diff --git a/src/ltlvisit/mark.hh b/src/ltlvisit/mark.hh index 143a269ff..7eb262800 100644 --- a/src/ltlvisit/mark.hh +++ b/src/ltlvisit/mark.hh @@ -32,7 +32,7 @@ namespace spot class mark_tools { public: - /// \brief Mark operators UConcat and EConcat. + /// \brief Mark operators NegClosure and EConcat. /// \ingroup ltl_rewriting /// /// \param f The formula to rewrite. diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 69d30983a..0d7df47dd 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -418,7 +418,8 @@ namespace spot visit(const unop* uo) { const formula* f = uo->child(); - switch (uo->op()) + unop::type op = uo->op(); + switch (op) { case unop::Not: // "Not"s should be caught by nenoform_recursively(). @@ -445,8 +446,9 @@ namespace spot recurse_(f, false)); return; case unop::NegClosure: + case unop::NegClosureMarked: result_ = unop::instance(negated_ ? - unop::Closure : uo->op(), + unop::Closure : op, recurse_(f, false)); return; /* !Finish(x), is not simplified */ @@ -1273,6 +1275,7 @@ namespace spot break; case unop::Closure: case unop::NegClosure: + case unop::NegClosureMarked: // {e} = 1 if e accepts [*0] // !{e} = 0 if e accepts [*0] if (result_->accepts_eword()) @@ -1332,7 +1335,7 @@ namespace spot multop::instance(multop::Concat, v); tail = unop::instance(op, tail); - bool doneg = op == unop::NegClosure; + bool doneg = op != unop::Closure; for (unsigned n = start; n > 0;) { --n; @@ -1398,7 +1401,7 @@ namespace spot tail = // {b[*0..j-i]} or !{b[*0..j-i]} unop::instance(op, tail); tail = - dup_b_x_tail(op == unop::NegClosure, + dup_b_x_tail(op != unop::Closure, c, tail, min); mo->destroy(); result_ = recurse_destroy(tail); @@ -1417,14 +1420,14 @@ namespace spot unsigned min = s->min(); assert(min > 0); const formula* tail; - if (op == unop::NegClosure) - tail = - dup_b_x_tail(true, - c, constant::false_instance(), min); - else + if (op == unop::Closure) tail = dup_b_x_tail(false, c, constant::true_instance(), min); + else + tail = + dup_b_x_tail(true, + c, constant::false_instance(), min); result_->destroy(); result_ = recurse_destroy(tail); return; diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index bc99c6457..0b8091adb 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -539,6 +539,12 @@ namespace spot in_ratexp_ = true; top_level_ = true; break; + case unop::NegClosureMarked: + emit(KNot); + os_ << (kw_ == utf8_kw ? "̃{": "+{"); + in_ratexp_ = true; + top_level_ = true; + break; } if (need_parent || full_parent_) diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index 8343e620b..806e7c8c8 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -46,6 +46,7 @@ namespace spot case unop::Not: case unop::Closure: case unop::NegClosure: + case unop::NegClosureMarked: this->super::visit(uo); return; case unop::F: diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index d05e46a07..a57fa61b8 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -88,6 +88,7 @@ namespace spot case unop::X: case unop::Closure: case unop::NegClosure: + case unop::NegClosureMarked: assert(!"unsupported operator"); case unop::Not: { diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index b13ebb82f..e187dd00b 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -103,6 +103,7 @@ namespace spot case unop::G: case unop::Closure: case unop::NegClosure: + case unop::NegClosureMarked: assert(!"unsupported operator"); } /* Unreachable code. */ diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 82f8bfded..2722c8365 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -143,6 +143,7 @@ namespace spot case unop::Finish: case unop::Closure: case unop::NegClosure: + case unop::NegClosureMarked: assert(!"unsupported operator"); return; } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index a61f72547..ba017d4af 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -508,6 +508,7 @@ namespace spot case unop::Finish: case unop::Closure: case unop::NegClosure: + case unop::NegClosureMarked: assert(!"not a rational operator"); return; case unop::Not: @@ -1178,7 +1179,7 @@ namespace spot } case unop::Closure: { - rat_seen_ = true; + // rat_seen_ = true; const formula* f = node->child(); if (f->accepts_eword()) { @@ -1217,18 +1218,23 @@ namespace spot } break; + case unop::NegClosureMarked: + has_marked_ = true; case unop::NegClosure: + rat_seen_ = true; { - rat_seen_ = true; - has_marked_ = true; - - if (node->child()->accepts_eword()) + const formula* c = node->child(); + if (c->accepts_eword()) { res_ = bddfalse; return; } - - bdd f1 = translate_ratexp(node->child(), dict_); + if (mark_all_) + { + op = unop::NegClosureMarked; + has_marked_ = true; + } + bdd f1 = translate_ratexp(c, dict_); // trace_ltl_bdd(dict_, f1); diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index ac5bf99cb..e30403448 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -153,6 +153,7 @@ namespace spot case unop::Finish: case unop::Closure: case unop::NegClosure: + case unop::NegClosureMarked: assert(!"unsupported operator"); } /* Unreachable code. */ diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 3f29283ba..008b5c64b 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -1,8 +1,9 @@ #!/bin/sh -# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# -*- coding: utf-8 -*- +# Copyright (C) 2009, 2010, 2011, 2012 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. @@ -108,6 +109,16 @@ check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}' # other side. check_psl '{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c}' + +# these were mis-translated in Spot 0.9 +check_psl 'G!{(b;1)*;a}' +check_psl '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))' +# In particular, Spot 0.9 would incorrectly reject the sequence: +# (aÌ…b;aÌ…b;aÌ…bÌ…);(aÌ…b;aÌ…b;aÌ…bÌ…);(aÌ…b;aÌ…b;aÌ…bÌ…);... in 'G!{(b;1)*;a}' +# This means the following automaton was incorrectly empty in Spot 0.9. +run 0 ../ltl2tgba -e -R3 '(G!{(b;1)*;a} && ({1;1[*3]*}[]->{(b&!a)[*2];!b&!a}))' + + # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization. for opt in '' -D -DS; do