From 09242d3f78ba35908729f9d505ea4787632a00d1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 24 Oct 2014 10:47:49 +0200 Subject: [PATCH 01/15] org: compatibility with org 8 * doc/org/init.el.in: Add compatibility with org 8. * NEWS: Mention it. --- NEWS | 4 ++++ doc/org/init.el.in | 9 ++++++--- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 453650ec5..9be50ccd5 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,10 @@ New in spot 1.2.5a (not yet released) state labels. - the acceptance specification in the HOA format output have been adjusted to match recent changes in the format specifications. + - the build rules for documentation have been made compatible with + version 8.0 of Org-mode. (This was only a problem if you build + from the git repository, or if you want to edit the + documentation.) New in spot 1.2.5 (2014-08-21) diff --git a/doc/org/init.el.in b/doc/org/init.el.in index a0bb373e4..5968b8d2b 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -1,6 +1,7 @@ ;; htmlize is not always in the load-path. On Debian it can be found here. (setq load-path (cons "/usr/share/emacs/site-lisp/emacs-goodies-el" load-path)) -(require 'org-publish) +(or (require 'org-publish nil t) ; Org 7 + (require 'ox-publish)) ; Org 8 (require 'org-install) (print (concat "Org " (org-version))) @@ -29,12 +30,14 @@ ") (setq org-publish-project-alist - '(("spot-html" + `(("spot-html" :base-directory "@abs_top_srcdir@/doc/org/" :base-extension "org" :publishing-directory "@abs_top_srcdir@/doc/userdoc/" :recursive t - :publishing-function org-publish-org-to-html + :publishing-function + ,(if (require 'org-publish nil t) 'org-publish-org-to-html ; Org 7 + 'org-html-publish-to-html) ; Org 8 :style "\n\n" :auto-preamble t) ("spot-static" From 27453810978427081672c85b6706d2f22cb1ce3a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 31 Oct 2014 11:47:03 +0100 Subject: [PATCH 02/15] tgbasafracomplement: avoid some std::set copies * src/tgba/tgbasafracomplement.cc: Here. Beside being more efficient, the use of std::swap instead of an assignment also protects us from a bug recently introduced in the development version of G++. https://gcc.gnu.org/bugzilla/show_bug.cgi?id=63698 --- src/tgba/tgbasafracomplement.cc | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index d2eb770b2..66b0ad632 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -149,11 +149,9 @@ namespace spot /// \brief Copy the tree \a other, and set \c marked to false. safra_tree::safra_tree(const safra_tree& other) - : marked(false) + : marked(false), name(other.name), nodes(other.nodes) { - name = other.name; parent = 0; - nodes = other.nodes; for (child_list::const_iterator i = other.children.begin(); i != other.children.end(); ++i) { @@ -376,7 +374,7 @@ namespace spot } } } - nodes = new_subset; + std::swap(nodes, new_subset); for (child_list::iterator i = children.begin(); i != children.end(); ++i) (*i)->succ_create(condition, cache_transition); From 4ea63f840480388fb7db8eeb09f7b2b50a3ac310 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 13 Nov 2014 18:03:15 +0100 Subject: [PATCH 03/15] ltl2tgba_fm: fix non-deterministic output The ltl_to_tgba_fm() translation function was using a hash_map of maps (ugh!) to merge transitions on output. However recent libstd++ changed the implementation of hash_map (a.k.a. unordered_map) causing transitions to be output in a different order. This implementation-dependent order caused the ltl2ta.test to fail because the BA->TA transformation can produce TA of different sizes if you simply change the order of transitions in the input BA! This does not sound like a nice property for the BA->TA transformation, but Ala Eddine isn't sure how to fix it yet. In the meantime, this patch makes sure ltl_to_tgba_fm() will return the same output regardless of the implementation of hash_map. The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux, and with gcc-snapshot (5.0.0 20141016) on Debian. * src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging using a std::vector and std::sort instead of nested maps tables. * NEWS: Mention the fix. --- NEWS | 4 + src/tgbaalgos/ltl2tgba_fm.cc | 228 +++++++++++++++++++---------------- 2 files changed, 128 insertions(+), 104 deletions(-) diff --git a/NEWS b/NEWS index 9be50ccd5..85f19549d 100644 --- a/NEWS +++ b/NEWS @@ -20,6 +20,10 @@ New in spot 1.2.5a (not yet released) version 8.0 of Org-mode. (This was only a problem if you build from the git repository, or if you want to edit the documentation.) + - recent to changes to libstd++ (as shipped by g++ 4.9.2) have + demonstrated that the order of transitions output by the + LTL->TGBA translation used to be dependent on the implementation + of the STL. This is now fixed. New in spot 1.2.5 (2014-08-21) diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index aa5bab72b..f44f488d9 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -33,6 +33,7 @@ #include "ltlvisit/tostring.hh" #include #include +#include #include "ltl2tgba_fm.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/scc.hh" @@ -2109,28 +2110,56 @@ namespace spot } - typedef std::map prom_map; - typedef Sgi::hash_map dest_map; - - static void - fill_dests(translate_dict& d, dest_map& dests, bdd label, const formula* dest) + namespace { - bdd conds = bdd_existcomp(label, d.var_set); - bdd promises = bdd_existcomp(label, d.a_set); + struct transition + { + const formula* dest; + bdd prom; + bdd cond; - dest_map::iterator i = dests.find(dest); - if (i == dests.end()) + transition(const formula* dest, bdd cond, bdd prom) + : dest(dest), prom(prom), cond(cond) { - dests[dest][promises] = conds; } - else + + transition(const transition& other) + : dest(other.dest), prom(other.prom), cond(other.cond) { - i->second[promises] |= conds; - dest->destroy(); } + + bool operator<(const transition& other) const + { + ltl::formula_ptr_less_than lt; + if (lt(dest, other.dest)) + return true; + if (lt(other.dest, dest)) + return false; + if (prom.id() < other.prom.id()) + return true; + if (prom.id() > other.prom.id()) + return false; + return cond.id() < other.cond.id(); + } + }; + + bool postponement_cmp(const transition& lhs, const transition& rhs) + { + if (lhs.prom.id() < rhs.prom.id()) + return true; + if (lhs.prom.id() > rhs.prom.id()) + return false; + if (lhs.cond.id() < rhs.cond.id()) + return true; + if (lhs.cond.id() > rhs.cond.id()) + return false; + ltl::formula_ptr_less_than lt; + return lt(lhs.dest, rhs.dest); + } + + typedef std::vector dest_map; } - tgba_explicit_formula* ltl_to_tgba_fm(const formula* f, bdd_dict* dict, bool exprop, bool symb_merge, bool branching_postponement, @@ -2220,6 +2249,7 @@ namespace spot formulae_to_translate.insert(f2); a->set_init_state(f2); + dest_map dests; while (!formulae_to_translate.empty()) { // Pick one formula. @@ -2230,6 +2260,9 @@ namespace spot const translate_dict::translated& t = fc.translate(now); bdd res = t.symbolic; + if (res == bddfalse) + continue; + // Handle exclusive events. if (unobs) { @@ -2267,7 +2300,7 @@ namespace spot // // In `exprop' mode, considering all possible combinations of // outgoing propositions generalizes the above trick. - dest_map dests; + dests.clear(); // Compute all outgoing arcs. @@ -2288,9 +2321,6 @@ namespace spot one_prop_set = bdd_satoneset(all_props, var_set, bddtrue); all_props -= one_prop_set; - typedef std::map succ_map; - succ_map succs; - // Compute prime implicants. // The reason we use prime implicants and not bdd_satone() // is that we do not want to get any negation in front of Next @@ -2329,38 +2359,36 @@ namespace spot if (symb_merge) dest = fc.canonize(dest); - // If we are not postponing the branching, we can - // declare the outgoing transitions immediately. - // Otherwise, we merge transitions with identical - // label, and declare the outgoing transitions in a - // second loop. - if (!branching_postponement) - { - fill_dests(d, dests, label, dest); - } - else - { - succ_map::iterator si = succs.find(label); - if (si == succs.end()) - succs[label] = dest; - else - si->second = - multop::instance(multop::Or, si->second, dest); - } + bdd conds = bdd_existcomp(label, d.var_set); + bdd promises = bdd_existcomp(label, d.a_set); + dests.push_back(transition(dest, conds, promises)); } - if (branching_postponement) - for (succ_map::const_iterator si = succs.begin(); - si != succs.end(); ++si) - fill_dests(d, dests, si->first, si->second); } - // Check for an arc going to 1 (True). Register it first, that - // way it will be explored before others during model checking. - dest_map::const_iterator i = dests.find(constant::true_instance()); - // COND_FOR_TRUE is the conditions of the True arc, so we - // can remove them from all other arcs. It might sounds that - // this is not needed when exprop is used, but in fact it is - // complementary. + assert(dests.size() > 0); + if (branching_postponement && dests.size() > 1) + { + std::sort(dests.begin(), dests.end(), postponement_cmp); + // Iterate over all dests, and merge the destination of + // transitions with identical labels. + dest_map::iterator out = dests.begin(); + dest_map::const_iterator in = out; + do + { + transition t = *in; + while (++in != dests.end() + && t.cond == in->cond && t.prom == in->prom) + t.dest = multop::instance(multop::Or, t.dest, in->dest); + *out++ = t; + } + while (in != dests.end()); + dests.erase(out, dests.end()); + } + std::sort(dests.begin(), dests.end()); + // If we have some transitions to true, they are the first + // ones. Remove the sum of their conditions from other + // transitions. It might sounds that this is not needed when + // exprop is used, but in fact it is complementary. // // Consider // f = r(X(1) R p) = p.(1 + r(X(1) R p)) @@ -2373,67 +2401,59 @@ namespace spot // f ----> 1 // // because there is no point in looping on f if we can go to 1. - bdd cond_for_true = bddfalse; - if (i != dests.end()) + if (dests.front().dest == constant::true_instance()) { - // When translating LTL for an event-based logic with - // unobservable events, the 1 state should accept all events, - // even unobservable events. - if (unobs && now == constant::true_instance()) - cond_for_true = all_events; - else - { - // There should be only one transition going to 1 (true) ... - assert(i->second.size() == 1); - prom_map::const_iterator j = i->second.begin(); - // ... and it is not expected to make any promises (unless - // fair loop approximations are used). - assert(fair_loop_approx || j->first == bddtrue); - cond_for_true = j->second; - } - if (!a->has_state(constant::true_instance())) - formulae_to_translate.insert(constant::true_instance()); - state_explicit_formula::transition* t = - a->create_transition(now, constant::true_instance()); - t->condition = cond_for_true; + dest_map::iterator i = dests.begin(); + bdd c = bddfalse; + while (i != dests.end() && i->dest == constant::true_instance()) + c |= i++->cond; + for (; i != dests.end(); ++i) + i->cond -= c; } - // Register other transitions. - for (i = dests.begin(); i != dests.end(); ++i) - { - const formula* dest = i->first; - // The cond_for_true optimization can cause some - // transitions to be removed. So we have to remember - // whether a formula is actually reachable. - bool reachable = false; - // Will this be a new state? - bool seen = a->has_state(dest); + // Create transitions in the automaton + { + dest_map::const_iterator in = dests.begin(); + do + { + // Merge transitions with same destination and + // acceptance. + transition t = *in; + while (++in != dests.end() + && t.prom == in->prom && t.dest == in->dest) + { + t.cond |= in->cond; + in->dest->destroy(); + } + // Actually create the transition + if (t.cond != bddfalse) + { + // When translating LTL for an event-based logic + // with unobservable events, the 1 state should + // accept all events, even unobservable events. + if (unobs + && t.dest == constant::true_instance() + && now == constant::true_instance()) + t.cond = all_events; - if (dest != constant::true_instance()) - { - for (prom_map::const_iterator j = i->second.begin(); - j != i->second.end(); ++j) - { - bdd cond = j->second - cond_for_true; - if (cond == bddfalse) // Skip false transitions. - continue; - state_explicit_formula::transition* t = - a->create_transition(now, dest); - t->condition = cond; - d.conj_bdd_to_acc(a, j->first, t); - reachable = true; - } - } - else - { - // "1" is reachable. - reachable = true; - } - if (reachable && !seen) - formulae_to_translate.insert(dest); - else - dest->destroy(); - } + // Will this be a new state? + bool seen = a->has_state(t.dest); + + state_explicit_formula::transition* tt = + a->create_transition(now, t.dest); + tt->condition = t.cond; + d.conj_bdd_to_acc(a, t.prom, tt); + + if (!seen) + formulae_to_translate.insert(t.dest); + else + t.dest->destroy(); + } + else + t.dest->destroy(); + } + while (in != dests.end()); + } } dict->register_propositions(fc.used_vars(), a); From 6e2151dc18cd638d7020f9f534adf679a86a0ced Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 13 Nov 2014 23:41:07 +0100 Subject: [PATCH 04/15] futurecondcol: avoid gcc-snapshot bug * src/tgba/futurecondcol.cc: Use swap instead of assignement. It is more efficient, and it avoid the bug of gcc-snapshot mentionned two commits below. --- src/tgba/futurecondcol.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/tgba/futurecondcol.cc b/src/tgba/futurecondcol.cc index 019eff8b3..57a163876 100644 --- a/src/tgba/futurecondcol.cc +++ b/src/tgba/futurecondcol.cc @@ -1,4 +1,6 @@ -// Copyright (C) 2009 Laboratoire de recherche et dveloppement de l'Epita. +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2014 Laboratoire de recherche et développement +// de l'Epita. // // This file is part of Spot, a model checking library. // @@ -37,7 +39,7 @@ namespace spot res.insert(i->second); res.insert(future_conds_[dest].begin(), future_conds_[dest].end()); } - future_conds_[src] = res; + std::swap(future_conds_[src], res); } future_conditions_collector::future_conditions_collector(const tgba* aut, From becfcbcf7971f5d34a121849c916a7286d59ac9a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Nov 2014 08:38:16 +0100 Subject: [PATCH 05/15] * NEWS: Mention the std::set assignment workaround. --- NEWS | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/NEWS b/NEWS index 85f19549d..d54a1bf64 100644 --- a/NEWS +++ b/NEWS @@ -24,6 +24,11 @@ New in spot 1.2.5a (not yet released) demonstrated that the order of transitions output by the LTL->TGBA translation used to be dependent on the implementation of the STL. This is now fixed. + - some developpement version of libstd++ had a bug (PR 63698) in + the assignment of std::set, and that was triggered in two places + in Spot. The workaround (not assigning sets) is actually more + efficient, so we can consider it as a bug fix, even though + libstd++ has also been fixed. New in spot 1.2.5 (2014-08-21) From f8cf2aa9b37d9331a786648b3d8f0e142c68fdde Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 18 Nov 2014 11:07:02 +0100 Subject: [PATCH 06/15] fix line number tracking in files with DOS newlines * src/dstarparse/dstarscan.ll, src/kripkeparse/kripkescan.ll, src/neverparse/neverclaimscan.ll, src/tgbaparse/tgbascan.ll: Distinguish between 1-sized EOL and 2-sized EOL. * src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Add more tests. * NEWS: Mention it. * src/kripkeparse/scankripke.ll: Remove this unused file. --- NEWS | 2 + src/dstarparse/dstarscan.ll | 6 +- src/kripkeparse/kripkescan.ll | 6 +- src/kripkeparse/scankripke.ll | 115 ------------------------------- src/kripketest/bad_parsing.test | 13 +++- src/neverparse/neverclaimscan.ll | 9 ++- src/tgbaparse/tgbascan.ll | 9 ++- src/tgbatest/neverclaimread.test | 8 +++ src/tgbatest/readsave.test | 8 +++ 9 files changed, 48 insertions(+), 128 deletions(-) delete mode 100644 src/kripkeparse/scankripke.ll diff --git a/NEWS b/NEWS index d54a1bf64..8b469d5fd 100644 --- a/NEWS +++ b/NEWS @@ -29,6 +29,8 @@ New in spot 1.2.5a (not yet released) in Spot. The workaround (not assigning sets) is actually more efficient, so we can consider it as a bug fix, even though libstd++ has also been fixed. + - all parsers would report wrong line numbers while processing + files with DOS style newlines. New in spot 1.2.5 (2014-08-21) diff --git a/src/dstarparse/dstarscan.ll b/src/dstarparse/dstarscan.ll index 431da852e..25e83dd26 100644 --- a/src/dstarparse/dstarscan.ll +++ b/src/dstarparse/dstarscan.ll @@ -1,4 +1,4 @@ -/* Copyright (C) 2013 Laboratoire de Recherche et Dveloppement +/* Copyright (C) 2013, 2014 Laboratoire de Recherche et Dveloppement ** de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. @@ -31,7 +31,8 @@ typedef dstaryy::parser::token token; %} -eol \n|\r|\n\r|\r\n +eol \n+|\r+ +eol2 (\n\r)+|(\r\n)+ %x in_COMMENT in_STRING %% @@ -42,6 +43,7 @@ eol \n|\r|\n\r|\r\n %} {eol} yylloc->lines(yyleng); return token::EOL; +{eol2} yylloc->lines(yyleng / 2); return token::EOL; /* skip blanks and comments */ [ \t]+ yylloc->step(); diff --git a/src/kripkeparse/kripkescan.ll b/src/kripkeparse/kripkescan.ll index 37df81ae3..fff7e65ad 100644 --- a/src/kripkeparse/kripkescan.ll +++ b/src/kripkeparse/kripkescan.ll @@ -1,4 +1,4 @@ -/* Copyright (C) 2011 Laboratoire de Recherche et Developpement +/* Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement * de l'Epita (LRDE) * * This file is part of Spot, a model checking library. @@ -36,7 +36,8 @@ %} -eol \n|\r|\n\r|\r\n +eol \n+|\r+ +eol2 (\n\r)+|(\r\n)+ %% @@ -51,6 +52,7 @@ eol \n|\r|\n\r|\r\n /* discard whitespace */ {eol} yylloc->lines(yyleng); yylloc->step(); +{eol2} yylloc->lines(yyleng / 2); yylloc->step(); [ \t]+ yylloc->step(); \" { diff --git a/src/kripkeparse/scankripke.ll b/src/kripkeparse/scankripke.ll deleted file mode 100644 index a3b4a2983..000000000 --- a/src/kripkeparse/scankripke.ll +++ /dev/null @@ -1,115 +0,0 @@ -/* Copyright (C) 2011 Laboratoire d'Informatique de Paris 6 (LIP6), -** dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre -** et Marie Curie. -** -** This file is part of Spot, a model checking library. -** -** Spot is free software; you can redistribute it and/or modify it -** under the terms of the GNU General Public License as published by -** the Free Software Foundation; either version 3 of the License, or -** (at your option) any later version. -** -** Spot is distributed in the hope that it will be useful, but WITHOUT -** ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -** or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -** License for more details. -** -** You should have received a copy of the GNU General Public License -** along with this program. If not, see . -*/ -%option noyywrap - //%option prefix="tgbayy" -%option prefix="kripkeyy" -%option outfile="lex.yy.c" -%x STATE_STRING - -%{ -#include -#include "parsekripke.tab.hh" - - -#define YY_USER_ACTION \ - yylloc->columns(yyleng); - -#define YY_NEVER_INTERACTIVE 1 - - typedef kripkeyy::parser::token token; - - -%} - -eol \n|\r|\n\r|\r\n - -%% - -%{ - yylloc->step (); -%} - -[a-zA-Z][a-zA-Z0-9_]* { - yylval->str = new std::string(yytext, yyleng); - return token::IDENT; - } - - /* discard whitespace */ -{eol} yylloc->lines(yyleng); yylloc->step(); -[ \t]+ yylloc->step(); - -\" { - yylval->str = new std::string; - BEGIN(STATE_STRING); - } - -"," { - return token::COMA; - } - -";" return token::SEMICOL; - -. return *yytext; - - /* Handle \" and \\ in strings. */ -{ - \" { - BEGIN(INITIAL); - return token::STRING; - } - \\["\\] yylval->str->append(1, yytext[1]); - [^"\\]+ yylval->str->append(yytext, yyleng); - <> { - BEGIN(INITIAL); - return token::UNTERMINATED_STRING; - } -} - -%{ - /* Dummy use of yyunput to shut up a gcc warning. */ - (void) &yyunput; -%} - -%% - - //namespace spot - //{ - int - kripkeyyopen(const std::string &name) - { - if (name == "-") - { - yyin = stdin; - } - else - { - yyin = fopen(name.c_str(), "r"); - if (!yyin) - return 1; - } - return 0; - } - - void - kripkeyyclose() - { - fclose(yyin); - } -//} diff --git a/src/kripketest/bad_parsing.test b/src/kripketest/bad_parsing.test index ae5fdca7a..1e5ca5541 100755 --- a/src/kripketest/bad_parsing.test +++ b/src/kripketest/bad_parsing.test @@ -1,6 +1,6 @@ #! /bin/sh - -# Copyright (C) 2011 Laboratoire de Recherche et Developpement +# -*- coding: utf-8 -*- +# Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement # de l'Epita (LRDE) # # This file is part of Spot, a model checking library. @@ -67,6 +67,14 @@ run 1 ../parse_print input 2> output cat output | grep -v + > res diff expected res +# The diagnostic should be the same with DOS return lines +sed 's/$/\r/' input > input.dos +mv input.dos input +run 1 ../parse_print input 2> output +cat output | grep -v + > res +diff expected res + + rm -f output res expected cat >input <<\EOF @@ -86,4 +94,3 @@ cat output | grep -v + > res diff expected res rm -f output res expected - diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll index 998c379c4..50ad283f3 100644 --- a/src/neverparse/neverclaimscan.ll +++ b/src/neverparse/neverclaimscan.ll @@ -1,5 +1,6 @@ -/* Copyright (C) 2010, 2011, 2013 Laboratoire de Recherche et -** Dveloppement de l'Epita (LRDE). +/* -*- coding: utf-8 -*- +** Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et +** Développement de l'Epita (LRDE). ** ** This file is part of Spot, a model checking library. ** @@ -38,7 +39,8 @@ static bool missing_parent = false; %x in_par -eol \n|\r|\n\r|\r\n +eol \n+|\r+ +eol2 (\n\r)+|(\r\n)+ %% @@ -48,6 +50,7 @@ eol \n|\r|\n\r|\r\n /* skip blanks */ {eol} yylloc->lines(yyleng); yylloc->step(); +{eol2} yylloc->lines(yyleng / 2); yylloc->step(); [ \t]+ yylloc->step(); "/*".*"*/" yylloc->step(); diff --git a/src/tgbaparse/tgbascan.ll b/src/tgbaparse/tgbascan.ll index 83c055e4d..edc613b14 100644 --- a/src/tgbaparse/tgbascan.ll +++ b/src/tgbaparse/tgbascan.ll @@ -1,7 +1,8 @@ -/* Copyright (C) 2011, Laboratoire de Recherche et Dveloppement de +/* -*- coding: utf-8 -*- +** Copyright (C) 2011, 2014, Laboratoire de Recherche et Développement de ** l'Epita (LRDE). ** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -** dpartement Systmes Rpartis Coopratifs (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. @@ -37,7 +38,8 @@ typedef tgbayy::parser::token token; %} -eol \n|\r|\n\r|\r\n +eol \n+|\r+ +eol2 (\n\r)+|(\r\n)+ %% @@ -54,6 +56,7 @@ acc[ \t]*= return token::ACC_DEF; /* discard whitespace */ {eol} yylloc->lines(yyleng); yylloc->step(); +{eol2} yylloc->lines(yyleng / 2); yylloc->step(); [ \t]+ yylloc->step(); \" { diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index ab8db0332..d56b9cfde 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -287,6 +287,14 @@ EOF grep input: stderr > stderrfilt diff stderrfilt expected-err +# DOS-style new lines should have the same output. +sed 's/$/\r/g' input > input.dos +mv input.dos input +run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr +cat stderr +grep input: stderr > stderrfilt +diff stderrfilt expected-err + cat >formulae< input.dos +mv input.dos input +run 2 ../ltl2tgba -b -X input > stdout 2>stderr +cat stderr +grep input: stderr > stderrfilt +diff stderrfilt expected From ef5b0417e791296042ae6b525fc20785080c5fa8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 25 Nov 2014 11:37:29 +0100 Subject: [PATCH 07/15] hoa: fix handling of escaped characters in atomic propositions (No test, this is just a simple backport of a fix from the development branch, where it is tested.) * src/tgbaalgos/hoaf.cc: Do not call to_string() to display names, as this would add another level of escaping. * NEWS: Mention it. --- NEWS | 1 + src/tgbaalgos/hoaf.cc | 7 ++++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 8b469d5fd..c1c464f92 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,7 @@ New in spot 1.2.5a (not yet released) state labels. - the acceptance specification in the HOA format output have been adjusted to match recent changes in the format specifications. + - atomic propositions are correctly escaped in the HOA output. - the build rules for documentation have been made compatible with version 8.0 of Org-mode. (This was only a problem if you build from the git repository, or if you want to edit the diff --git a/src/tgbaalgos/hoaf.cc b/src/tgbaalgos/hoaf.cc index 152d5e506..afbe546be 100644 --- a/src/tgbaalgos/hoaf.cc +++ b/src/tgbaalgos/hoaf.cc @@ -32,6 +32,7 @@ #include "misc/minato.hh" #include "tgba/formula2bdd.hh" #include "ltlvisit/tostring.hh" +#include "ltlast/atomic_prop.hh" namespace spot { @@ -265,7 +266,11 @@ namespace spot bdd_dict* d = aut->get_dict(); for (metadata::vap_t::const_iterator i = md.vap.begin(); i != md.vap.end(); ++i) - escape_str(os << " \"", to_string(d->bdd_map[*i].f)) << '"'; + { + const ltl::atomic_prop* f = ltl::is_atomic_prop(d->bdd_map[*i].f); + assert(f); + escape_str(os << " \"", f->name()) << '"'; + } os << nl; unsigned num_acc = md.acc.size(); if (num_acc == 0) From 946f7e80dd090cae5b05b183f44b88088b9fac6f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 29 Nov 2014 15:45:16 +0100 Subject: [PATCH 08/15] * src/bin/randltl.cc: Fix typos in examples. --- src/bin/randltl.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index 676c044e5..a12fd7680 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -55,12 +55,12 @@ and c, with the default tree-size, and all available operators.\n\ \n\ If you do not mind about the name of the atomic propositions, just give\n\ a number instead:\n\ - % ./randltl -n10 3\n\ + % randltl -n10 3\n\ \n\ You can disable or favor certain operators by changing their priority.\n\ The following disables xor, implies, and equiv, and multiply the probability\n\ of X to occur by 10.\n\ - % ./randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b c\n\ + % randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b c\n\ "; #define OPT_DUMP_PRIORITIES 1 From bc9cb1e5bba3f74b0e7b664ab1c0f4f3d1ede8ac Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 28 Oct 2014 23:53:04 +0100 Subject: [PATCH 09/15] * configure.ac: Prefer swig-3.0 when available. --- NEWS | 1 + configure.ac | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index c1c464f92..00ed86547 100644 --- a/NEWS +++ b/NEWS @@ -32,6 +32,7 @@ New in spot 1.2.5a (not yet released) libstd++ has also been fixed. - all parsers would report wrong line numbers while processing files with DOS style newlines. + - add support for SWIG 3.0. New in spot 1.2.5 (2014-08-21) diff --git a/configure.ac b/configure.ac index 94b4a60d1..9278ade25 100644 --- a/configure.ac +++ b/configure.ac @@ -117,9 +117,9 @@ AC_CHECK_PROG([EMACS], [emacs], [emacs]) AC_CHECK_PROG([LBTT_TRANSLATE], [lbtt-translate], [lbtt-translate]) AX_CHECK_VALGRIND AC_CHECK_PROG([WRING2LBTT], [wring2lbtt], [wring2lbtt]) -# Debian has a binary for SWIG 2.0 named swig2.0 and they kept swig as -# an alias for swig-1.3. Let's use the former when available. -AC_CHECK_PROGS([SWIG], [swig2.0 swig], [swig]) +# Debian has a binary for SWIG 3.0 named swig3.0 and they kept swig as +# an alias for swig-2.0. Let's use the former when available. +AC_CHECK_PROGS([SWIG], [swig3.0 swig], [swig]) AC_SUBST([CROSS_COMPILING], [$cross_compiling]) From 2731c9be676b6607fd19613dba41e4e7428e5d26 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Dec 2014 18:20:05 +0100 Subject: [PATCH 10/15] * src/tgbaalgos/hoaf.hh: Fix comment. --- src/tgbaalgos/hoaf.hh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tgbaalgos/hoaf.hh b/src/tgbaalgos/hoaf.hh index 84da433bc..d974c9beb 100644 --- a/src/tgbaalgos/hoaf.hh +++ b/src/tgbaalgos/hoaf.hh @@ -44,7 +44,7 @@ namespace spot /// \param g The automaton to output. /// \param f The (optional) formula associated to the automaton. If given /// it will be output as a comment. - /// \param a acceptance Force the type of acceptance mode used + /// \param acceptance Force the type of acceptance mode used /// in output. /// \param alias Whether aliases should be used in output. /// \param newlines Whether to use newlines in output. From 7619a5a0623f00ae035f73b7525d724314aad001 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Dec 2014 22:50:43 +0100 Subject: [PATCH 11/15] simplify: remove an incorect SERE simplification * src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule. * src/ltltest/reduc0.test: Add a regression test. * src/ltltest/reduccmp.test: Adjust test cases for its removal. * NEWS: Mention it. --- NEWS | 4 ++++ doc/tl/tl.tex | 5 +++-- src/ltltest/reduc0.test | 8 +++++++- src/ltltest/reduccmp.test | 12 ++++++------ src/ltlvisit/simplify.cc | 27 +++++---------------------- 5 files changed, 25 insertions(+), 31 deletions(-) diff --git a/NEWS b/NEWS index 00ed86547..6c1faf0f0 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,10 @@ New in spot 1.2.5a (not yet released) * Bug fixes: + - Remove one incorrect simplification rule for PSL discovered + via checks on random formulaes. (The bug was very unlikely + to trigger on non-random formulas, because it requires a SERE + with an entire subexpression that is unsatisfiable.) - When the automaton resulting from the translation of a positive formula is deterministic, ltlcross will compute its complement to perform additional checks against other translations of the diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 784f204b2..07e2fc95d 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1570,8 +1570,9 @@ Here are basic the rewritings for the weak closure and its negation: \nsere{r_1;r_2}&\equiv \nsere{r_1}\AND\nsere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2\\ \sere{b;r}&\equiV b\AND\X\sere{r}& \nsere{b;r}&\equiV (\NOT b)\OR\X\nsere{r}\\ - \sere{b\STAR{};r}&\equiv b\W\sere{r}& - \nsere{b\STAR{};r}&\equiv (\NOT b)\M\nsere{r}\\ +% These two would be correct only if $r$ is satisfiable. +% \sere{b\STAR{};r}&\equiv b\W\sere{r}& +% \nsere{b\STAR{};r}&\equiv (\NOT b)\M\nsere{r}\\ \sere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{b\AND \X(b\ldots}_{\mathclap{i\text{~occurences of~}b}}\AND\X\sere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r})& \nsere{b\STAR{\mvar{i}..\mvar{j}};r}&\equiV \underbrace{(\NOT b)\OR \X((\NOT b)\ldots}_{\mathclap{i\text{~occurences of~}\NOT b}}\OR\X\nsere{b\STAR{\mvar{0}..\mvar{j-i}}\CONCAT r}) \\ \sere{b\STAR{\mvar{i}..\mvar{j}}}&\equiV \underbrace{b\AND \X(b\AND \X(\ldots b))}_{i\text{~occurences of~}b}& diff --git a/src/ltltest/reduc0.test b/src/ltltest/reduc0.test index 744f654c2..296d03e0d 100755 --- a/src/ltltest/reduc0.test +++ b/src/ltltest/reduc0.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2013 Laboratoire de Recherche et +# Copyright (C) 2013, 2014 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -24,3 +24,9 @@ set -e run 0 ../reduc 0 'XFa & FXa' 'XFa' run 0 ../reduc 0 '(Xf W 0) | X(f W 0)' 'XGf' +# Two incorrect reductions. Those used +# to reduce respectively to a W (b && !b) and !a M (b || !b). +# But both are wrong. The reduction {a*;r} = a W r seems only +# valid if r has a non-empty language. +run 0 ../reduc 0 '{a[*];{b && !b}}' +run 0 ../reduc 0 '!{a[*];{b && !b}}' diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 0ff861728..b557ab0f1 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -355,14 +355,14 @@ for x in ../reduccmp ../reductaustr; do run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)' run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} <>-> f' \ '{{[*0] | a};b;{[*0] | a}} <>-> X(c & (f | X(f M e)))' - run 0 $x '{a;b[*];c[*];e;f*}' 'a & X(b W (c W e))' - run 0 $x '{a;b*;(a* && (b;c));c*}' 'a & X(b W {a[*] && {b;c}})' + run 0 $x '{a;b[*];c[*];e;f*}' 'a & X({b*;c*;e})' + run 0 $x '{a;b*;(a* && (b;c));c*}' 'a & X({b*;(a* && (b;c))})' run 0 $x '{a;a;b[*2..];b}' 'a & X(a & X(b & X(b & Xb)))' run 0 $x '!{a;a;b[*2..];b}' '!a | X(!a | X(!b | X(!b | X!b)))' - run 0 $x '!{a;b[*];c[*];e;f*}' '!a | X(!b M (!c M !e))' - run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})' - run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)' - run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)' + run 0 $x '!{a;c[*];e;f*}' '!a | X!{c[*];e}' + run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!{b*;(a* && (b;c))})' + run 0 $x '{(a;c*;d)|(b;c)}' '(a & X{c*;d}) | (b & Xc)' + run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!{c*;d}) | !a) & (X!c | !b)' run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc' run 0 $x '{{c*|1}[*0..1]}<>-> v' '{{c[+]|1}[*0..1]}<>-> v' run 0 $x '{{b*;c*}[*3..5]}<>-> v' '{{b*;c*}[*0..5]} <>-> v' diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 6625ab8f9..1ddf29376 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -1621,10 +1621,10 @@ namespace spot // Some term does not accept the empty word. unsigned end = mo->size() - 1; - // {b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄} - // = b₁&X(b₂&X(b₃ W {e₁;f₁;e₂;f₂})) - // !{b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄} - // = !b₁|X(!b₂|X(!b₃ M !{e₁;f₁;e₂;f₂})) + // {b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄} + // = b₁&X(b₂&X({e₁;f₁;e₂;f₂})) + // !{b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄} + // = !b₁|X(!b₂|X(!{e₁;f₁;e₂;f₂})) // if e denotes a term that accepts [*0] // and b denotes a Boolean formula. while (mo->nth(end)->accepts_eword()) @@ -1633,9 +1633,7 @@ namespace spot while (start <= end) { const formula* r = mo->nth(start); - const bunop* es = is_KleenStar(r); - if ((r->is_boolean() && !opt_.reduce_size_strictly) - || (es && es->child()->is_boolean())) + if (r->is_boolean() && !opt_.reduce_size_strictly) ++start; else break; @@ -1681,21 +1679,6 @@ namespace spot tail = multop::instance(multop::And, e, tail); } - // {b*;f} = b W {f} - // !{b*;f} = !b M !{f} - else - { - const bunop* es = is_KleenStar(e); - assert(es); - const formula* c = es->child()->clone(); - if (doneg) - tail = - binop::instance(binop::M, - unop::instance(unop::Not, c), - tail); - else - tail = binop::instance(binop::W, c, tail); - } } mo->destroy(); result_ = recurse_destroy(tail); From ff03ab4f56acecb286c6caf42d4acdc95925ecf7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 Dec 2014 10:25:33 +0100 Subject: [PATCH 12/15] work around BSD sed not interpreting \r in s/$/\r/ * src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test, src/tgbatest/readsave.test: Use Perl for the unix2dos conversion. --- src/kripketest/bad_parsing.test | 2 +- src/tgbatest/neverclaimread.test | 2 +- src/tgbatest/readsave.test | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/kripketest/bad_parsing.test b/src/kripketest/bad_parsing.test index 1e5ca5541..d1d967174 100755 --- a/src/kripketest/bad_parsing.test +++ b/src/kripketest/bad_parsing.test @@ -68,7 +68,7 @@ cat output | grep -v + > res diff expected res # The diagnostic should be the same with DOS return lines -sed 's/$/\r/' input > input.dos +perl -pe 's/$/\r/' input > input.dos mv input.dos input run 1 ../parse_print input 2> output cat output | grep -v + > res diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index d56b9cfde..195b31a45 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -288,7 +288,7 @@ grep input: stderr > stderrfilt diff stderrfilt expected-err # DOS-style new lines should have the same output. -sed 's/$/\r/g' input > input.dos +perl -pe 's/$/\r/' input > input.dos mv input.dos input run 2 ../ltl2tgba -ks -XN input > stdout 2>stderr cat stderr diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index 432a8e670..9e4a0db7a 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -1,6 +1,6 @@ #!/bin/sh -# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Dveloppement -# de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et +# Dveloppement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre # et Marie Curie. @@ -116,7 +116,7 @@ EOF diff stderrfilt expected # The diagnostic should be the same with DOS input -sed 's/$/\r/' input > input.dos +perl -pe 's/$/\r/' input > input.dos mv input.dos input run 2 ../ltl2tgba -b -X input > stdout 2>stderr cat stderr From 8c9bca9405ecddaac38b37f284b1b2b3c048f1d9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 5 Dec 2014 20:25:13 +0100 Subject: [PATCH 13/15] * HACKING: Mention the new gitlab page and repository. --- HACKING | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/HACKING b/HACKING index ce1ad4692..e3443b2c0 100644 --- a/HACKING +++ b/HACKING @@ -3,6 +3,14 @@ Bootstraping from the GIT repository (If you are building from a tarball, skip this section.) +Spot's gitlab page is at + + https://gitlab.lrde.epita.fr/spot/spot + +The GIT repository can be cloned with + + git clone https://gitlab.lrde.epita.fr/spot/spot.git + Some files in SPOT's source tree are generated. They are distributed so that users do not need to tools to rebuild them, but we don't keep all of them under GIT because it can generate lots of changes or From 44b374d1b9723d7a0781ea50526e87dbe5a9acd8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Dec 2014 12:35:05 +0100 Subject: [PATCH 14/15] Release Spot 1.2.6. * NEWS, configure.ac, doc/org/tools.org: Bump version number. --- NEWS | 2 +- configure.ac | 2 +- doc/org/tools.org | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 6c1faf0f0..5c430dfd3 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 1.2.5a (not yet released) +New in spot 1.2.6 (2014-12-06) * New features: diff --git a/configure.ac b/configure.ac index 9278ade25..6dcc2ac64 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [1.2.5a], [spot@lrde.epita.fr]) +AC_INIT([spot], [1.2.6], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/tools.org b/doc/org/tools.org index 26dd29f2b..bd65af004 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -1,4 +1,4 @@ -#+TITLE: Command-line tools installed by Spot 1.2.5 +#+TITLE: Command-line tools installed by Spot 1.2.6 #+EMAIL spot@lrde.epita.fr #+OPTIONS: H:2 num:nil toc:t From 84902fd69048301d578a9473054e61550e29c9ac Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Dec 2014 13:26:12 +0100 Subject: [PATCH 15/15] * NEWS, configure.ac: Bump version to 1.2.6a. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 5c430dfd3..ba796a6e9 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 1.2.6a (not yet released) + + Nothing yet. + New in spot 1.2.6 (2014-12-06) * New features: diff --git a/configure.ac b/configure.ac index 6dcc2ac64..8b12d5306 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [1.2.6], [spot@lrde.epita.fr]) +AC_INIT([spot], [1.2.6a], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])