From 9c6a09890ea2820771bc08df96d4d1fca8d9dc75 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 26 Mar 2022 15:57:56 +0100 Subject: [PATCH] parsetl: speedup parsing of n-ary operators with many operands Issue #500, reported by Yann Thierry-Mieg. * spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Use variant to store a new pnode objects that delays the construction of n-ary operators. * spot/parsetl/Makefile.am: Do not distribute stack.hh anymore. * spot/tl/formula.cc: Fix detection of overflow in Star and FStar. * HACKING: Update Bison requirements to 3.3. * tests/core/500.test: New test case. * tests/Makefile.am: Add it. * tests/core/ltl2tgba2.test, tests/core/ltlsynt.test, tests/core/tostring.test: Adjust to new expected order. * NEWS: Mention the change. --- HACKING | 2 +- NEWS | 9 + spot/parsetl/Makefile.am | 3 +- spot/parsetl/parsetl.yy | 416 +++++++++++++++++++++++++------------- spot/parsetl/scantl.ll | 55 ++--- spot/tl/formula.cc | 12 +- tests/Makefile.am | 1 + tests/core/500.test | 43 ++++ tests/core/ltl2tgba2.test | 6 +- tests/core/ltlsynt.test | 2 +- tests/core/tostring.test | 6 +- 11 files changed, 374 insertions(+), 181 deletions(-) create mode 100755 tests/core/500.test diff --git a/HACKING b/HACKING index c6e127a70..de461376b 100644 --- a/HACKING +++ b/HACKING @@ -25,7 +25,7 @@ since the generated files they produce are distributed.) GNU Automake >= 1.11 GNU Libtool >= 2.4 GNU Flex >= 2.6 - GNU Bison >= 3.0 + GNU Bison >= 3.3 GNU Emacs (preferably >= 24 but it may work with older versions) org-mode >= 9.1 (the version that comes bundled with your emacs version is likely out-of-date; but distribution often have diff --git a/NEWS b/NEWS index 345ec7fdd..81aaf9a22 100644 --- a/NEWS +++ b/NEWS @@ -66,6 +66,15 @@ New in spot 2.10.4.dev (net yet released) - purge_dead_states() will now also remove edges labeled by false (except self-loops). + - When parsing formulas with a huge number of operands for an n-ary + operator (for instance 'p1 | p2 | ... | p1000') the LTL parser + would construct that formula two operand at a time, and the + formula constructor for that operator would be responsible for + inlining, sorting, deduplicating, ... all operands at each step. + This resulted in a worst-than-quadratic slowdown. This is now + averted in the parser by delaying the construction of such n-ary + nodes until all children are known. + Bugs fixed: - reduce_parity() produced incorrect results when applied to diff --git a/spot/parsetl/Makefile.am b/spot/parsetl/Makefile.am index d98c9ebab..f218ca067 100644 --- a/spot/parsetl/Makefile.am +++ b/spot/parsetl/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2008-2015, 2018 Laboratoire de Recherche et +## Copyright (C) 2008-2015, 2018, 2022 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), @@ -30,7 +30,6 @@ noinst_LTLIBRARIES = libparsetl.la PARSETL_YY = parsetl.yy FROM_PARSETL_YY_MAIN = parsetl.cc FROM_PARSETL_YY_OTHERS = \ - stack.hh \ parsetl.hh FROM_PARSETL_YY = $(FROM_PARSETL_YY_MAIN) $(FROM_PARSETL_YY_OTHERS) diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index bbcdedcb5..e6defffb3 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -1,7 +1,6 @@ /* -*- coding: utf-8 -*- - -** Copyright (C) 2009-2019, 2021 Laboratoire de Recherche et Développement -** de l'Epita (LRDE). +** Copyright (C) 2009-2019, 2021, 2022 Laboratoire de Recherche et +** Développement de l'Epita (LRDE). ** Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université ** Pierre et Marie Curie. @@ -21,11 +20,13 @@ ** You should have received a copy of the GNU General Public License ** along with this program. If not, see . */ -%require "3.0" +%require "3.3" %language "C++" %locations %defines %define api.prefix {tlyy} +%define api.value.type variant +%define api.value.automove true %debug %define parse.error verbose %expect 0 @@ -37,25 +38,164 @@ #include "config.h" #include #include +#include #include #include #include struct minmax_t { unsigned min, max; }; + + // pnode (parsing node) is simular to fnode (formula node) except + // that n-ary operators will delay their construction until all + // children are known; this is a hack to speedup the parsing, + // because n-ary operator usually do a lot of work on construction + // (sorting all children if the operator is commutative, removing + // duplicates if applicable, etc.). Building n-ary nodes by + // repeatedly calling the binary constructor as we did in the past + // has a prohibitive cost. See issue #500. + + struct nary + { + std::vector children; + spot::op kind; + }; + + struct pnode + { + // Hold either a constructed formula, or an n-ary operator that we + // will construct only when it is combined with a different + // operator. + std::variant data; + // Record whether this pnode has been transformed into a fnode( or + // moved to another pnode). If that occurred, the ownership of + // any fnode we store has been transfered to the constructed fnode + // (or to the other pnode), and our destructor has nothing to do. + // This is the usual case while parsing a formula without error. + // However during error recovering, the parser may have to discard + // unused pnode, in which case we have to remember to free fnode + // during destruction. + // + // We have to track this used status because pnode are destructed + // whenever the parser pops a token, and as of Bison 3.7.6, the + // handling of "%destructor" is broken when + // "%define api.value.type variant" is used. See + // https://lists.gnu.org/archive/html/bug-bison/2022-03/msg00000.html + bool used = false; + + pnode() + : data(nullptr) + { + } + + pnode(const spot::fnode* ltl) + : data(ltl) + { + } + + // We only support move construction. + pnode(const pnode& other) = delete; + pnode& operator=(const pnode& other) = delete; + + pnode(pnode&& other) + : data(std::move(other.data)) + { + other.used = true; + } + + pnode& operator=(pnode&& other) + { + data = std::move(other.data); + other.used = true; + return *this; + } + + ~pnode() + { + if (used) + return; + if (auto* n = std::get_if(&data)) + { + for (auto f: n->children) + f->destroy(); + } + else + { + auto* f = std::get(data); + // The only case where we expect f to be nullptr, is if + // parse_ap() return nullptr: then $$ is unset when YYERROR + // is called. + if (f) + f->destroy(); + } + } + + // Create a new n-ary node from left and right. + // This will empty left and right so that their + // destructor do nothing. + pnode(spot::op o, pnode&& left, pnode&& right) + : data(nary{}) + { + nary& n = std::get(data); + n.kind = o; + if (auto* nleft = std::get_if(&left.data); + nleft && nleft->kind == o) + std::swap(n.children, nleft->children); + else + n.children.push_back(left); + if (auto* nright = std::get_if(&right.data); + nright && nright->kind == o) + { + auto& rch = nright->children; + n.children.insert(n.children.end(), rch.begin(), rch.end()); + rch.clear(); + } + else + { + n.children.push_back(right); + } + } + + operator const spot::fnode*() + { + used = true; + if (auto* n = std::get_if(&data)) + { + return spot::fnode::multop(n->kind, n->children); + } + else + { + return std::get(data); + } + } + + // Convert to a temporary formula, for printing, do not mark as + // used. + const spot::formula tmp() const + { + const spot::fnode* f; + if (auto* n = std::get_if(&data)) + { + for (auto c: n->children) + c->clone(); + f = spot::fnode::multop(n->kind, n->children); + } + else + { + f = std::get(data); + assert(f != nullptr); + f->clone(); + } + return spot::formula(f); + } + }; + + } %parse-param {spot::parse_error_list &error_list} %parse-param {spot::environment &parse_environment} %parse-param {spot::formula &result} -%union -{ - std::string* str; - const spot::fnode* ltl; - unsigned num; - minmax_t minmax; -} - %code { /* parsetl.hh and parsedecl.hh include each other recursively. We mut ensure that YYSTYPE is declared (by the above %union) @@ -84,28 +224,20 @@ using namespace spot; } \ while (0); -// right is missing, so complain and use false. -#define missing_right_binop_hard(res, left, op, str) \ - do \ - { \ - left->destroy(); \ - missing_right_op(res, op, str); \ - } \ - while (0); - - static bool + static const fnode* sere_ensure_bool(const fnode* f, const spot::location& loc, const char* oper, spot::parse_error_list& error_list) { if (f->is_boolean()) - return true; + return f; + f->destroy(); std::string s; s.reserve(80); s = "not a Boolean expression: in a SERE "; s += oper; s += " can only be applied to a Boolean expression"; error_list.emplace_back(loc, s); - return false; + return nullptr; } static const fnode* @@ -196,9 +328,9 @@ using namespace spot; %token START_SERE "SERE start marker" %token START_BOOL "BOOLEAN start marker" %token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis" -%token PAR_BLOCK "(...) block" -%token BRA_BLOCK "{...} block" -%token BRA_BANG_BLOCK "{...}! block" +%token PAR_BLOCK "(...) block" +%token BRA_BLOCK "{...} block" +%token BRA_BANG_BLOCK "{...}! block" %token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace" %token BRACE_BANG_CLOSE "closing brace-bang" %token OP_OR "or operator" OP_XOR "xor operator" @@ -221,7 +353,7 @@ using namespace spot; %token OP_GOTO_OPEN "opening bracket for goto operator" %token OP_SQBKT_CLOSE "closing bracket" %token OP_SQBKT_STRONG_CLOSE "closing !]" -%token OP_SQBKT_NUM "number for square bracket operator" +%token OP_SQBKT_NUM "number for square bracket operator" %token OP_UNBOUNDED "unbounded mark" %token OP_SQBKT_SEP "separator for square bracket operator" %token OP_UCONCAT "universal concat operator" @@ -229,12 +361,12 @@ using namespace spot; %token OP_UCONCAT_NONO "universal non-overlapping concat operator" %token OP_ECONCAT_NONO "existential non-overlapping concat operator" %token OP_FIRST_MATCH "first_match" -%token ATOMIC_PROP "atomic proposition" +%token ATOMIC_PROP "atomic proposition" %token OP_CONCAT "concat operator" OP_FUSION "fusion operator" %token CONST_TRUE "constant true" CONST_FALSE "constant false" %token END_OF_INPUT "end of formula" %token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix" -%token OP_DELAY_N "SVA delay operator" +%token OP_DELAY_N "SVA delay operator" %token OP_DELAY_OPEN "opening bracket for SVA delay operator" %token OP_DELAY_PLUS "##[+] operator" %token OP_DELAY_STAR "##[*] operator" @@ -276,19 +408,16 @@ using namespace spot; need any precedence). */ %precedence OP_NOT -%type subformula atomprop booleanatom sere lbtformula boolformula -%type bracedsere parenthesedsubformula -%type starargs fstarargs equalargs sqbracketargs gotoargs delayargs -%type sqbkt_num +%type subformula atomprop booleanatom sere lbtformula +%type boolformula bracedsere parenthesedsubformula +%type starargs fstarargs equalargs sqbracketargs gotoargs delayargs +%type sqbkt_num -%destructor { delete $$; } -%destructor { $$->destroy(); } - -%printer { debug_stream() << *$$; } -%printer { print_psl(debug_stream(), formula($$->clone())); } -%printer { print_sere(debug_stream(), formula($$->clone())); } sere bracedsere -%printer { debug_stream() << $$; } -%printer { debug_stream() << $$.min << ".." << $$.max; } +%printer { debug_stream() << $$; } +%printer { print_psl(debug_stream(), $$.tmp()); } +%printer { print_sere(debug_stream(), $$.tmp()); } sere bracedsere +%printer { debug_stream() << $$; } +%printer { debug_stream() << $$.min << ".." << $$.max; } %% result: START_LTL subformula END_OF_INPUT @@ -380,18 +509,19 @@ error_opt: %empty sqbkt_num: OP_SQBKT_NUM { - if ($1 >= fnode::unbounded()) + auto n = $1; + if (n >= fnode::unbounded()) { auto max = fnode::unbounded() - 1; std::ostringstream s; - s << $1 << " exceeds maximum supported repetition (" + s << n << " exceeds maximum supported repetition (" << max << ")"; error_list.emplace_back(@1, s.str()); $$ = max; } else { - $$ = $1; + $$ = n; } } @@ -484,10 +614,10 @@ delayargs: OP_DELAY_OPEN sqbracketargs atomprop: ATOMIC_PROP { - $$ = parse_ap(*$1, @1, parse_environment, error_list); - delete $1; - if (!$$) + auto* f = parse_ap($1, @1, parse_environment, error_list); + if (!f) YYERROR; + $$ = f; } booleanatom: atomprop @@ -504,13 +634,12 @@ booleanatom: atomprop sere: booleanatom | OP_NOT sere { - if (sere_ensure_bool($2, @2, "`!'", error_list)) + if (auto f = sere_ensure_bool($2, @2, "`!'", error_list)) { - $$ = fnode::unop(op::Not, $2); + $$ = fnode::unop(op::Not, f); } else { - $2->destroy(); $$ = error_false_block(@$, error_list); } } @@ -518,9 +647,8 @@ sere: booleanatom | PAR_BLOCK { $$ = - try_recursive_parse(*$1, @1, parse_environment, + try_recursive_parse($1, @1, parse_environment, debug_level(), parser_sere, error_list); - delete $1; if (!$$) YYERROR; } @@ -543,134 +671,142 @@ sere: booleanatom $$ = fnode::ff(); } | sere OP_AND sere - { $$ = fnode::multop(op::AndRat, {$1, $3}); } + { $$ = pnode(op::AndRat, $1, $3); } | sere OP_AND error { missing_right_binop($$, $1, @2, "length-matching and operator"); } | sere OP_SHORT_AND sere - { $$ = fnode::multop(op::AndNLM, {$1, $3}); } + { $$ = pnode(op::AndNLM, $1, $3); } | sere OP_SHORT_AND error { missing_right_binop($$, $1, @2, "non-length-matching and operator"); } | sere OP_OR sere - { $$ = fnode::multop(op::OrRat, {$1, $3}); } + { $$ = pnode(op::OrRat, $1, $3); } | sere OP_OR error { missing_right_binop($$, $1, @2, "or operator"); } | sere OP_CONCAT sere - { $$ = fnode::multop(op::Concat, {$1, $3}); } + { $$ = pnode(op::Concat, $1, $3); } | sere OP_CONCAT error { missing_right_binop($$, $1, @2, "concat operator"); } | sere OP_FUSION sere - { $$ = fnode::multop(op::Fusion, {$1, $3}); } + { $$ = pnode(op::Fusion, $1, $3); } | sere OP_FUSION error { missing_right_binop($$, $1, @2, "fusion operator"); } | OP_DELAY_N sere - { $$ = formula::sugar_delay(formula($2), $1, $1).to_node_(); } + { unsigned n = $1; $$ = formula::sugar_delay(formula($2), n, n).to_node_(); } | OP_DELAY_N error { missing_right_binop($$, fnode::tt(), @1, "SVA delay operator"); } | sere OP_DELAY_N sere - { $$ = formula::sugar_delay(formula($1), formula($3), - $2, $2).to_node_(); } + { unsigned n = $2; + $$ = formula::sugar_delay(formula($1), formula($3), + n, n).to_node_(); } | sere OP_DELAY_N error { missing_right_binop($$, $1, @2, "SVA delay operator"); } | delayargs sere %prec OP_DELAY_OPEN { - if ($1.max < $1.min) + auto [min, max] = $1; + if (max < min) { error_list.emplace_back(@1, "reversed range"); - std::swap($1.max, $1.min); + std::swap(max, min); } $$ = formula::sugar_delay(formula($2), - $1.min, $1.max).to_node_(); + min, max).to_node_(); } | delayargs error { missing_right_binop($$, fnode::tt(), @1, "SVA delay operator"); } | sere delayargs sere %prec OP_DELAY_OPEN { - if ($2.max < $2.min) + auto [min, max] = $2; + if (max < min) { error_list.emplace_back(@1, "reversed range"); - std::swap($2.max, $2.min); + std::swap(max, min); } $$ = formula::sugar_delay(formula($1), formula($3), - $2.min, $2.max).to_node_(); + min, max).to_node_(); } | sere delayargs error { missing_right_binop($$, $1, @2, "SVA delay operator"); } | starargs { - if ($1.max < $1.min) + auto [min, max] = $1; + if (max < min) { error_list.emplace_back(@1, "reversed range"); - std::swap($1.max, $1.min); + std::swap(max, min); } - $$ = fnode::bunop(op::Star, fnode::tt(), $1.min, $1.max); + $$ = fnode::bunop(op::Star, fnode::tt(), min, max); } | sere starargs { - if ($2.max < $2.min) + auto [min, max] = $2; + if (max < min) { error_list.emplace_back(@2, "reversed range"); - std::swap($2.max, $2.min); + std::swap(max, min); } - $$ = fnode::bunop(op::Star, $1, $2.min, $2.max); + $$ = fnode::bunop(op::Star, $1, min, max); } | sere fstarargs { - if ($2.max < $2.min) + auto [min, max] = $2; + if (max < min) { error_list.emplace_back(@2, "reversed range"); - std::swap($2.max, $2.min); + std::swap(max, min); } - $$ = fnode::bunop(op::FStar, $1, $2.min, $2.max); + $$ = fnode::bunop(op::FStar, $1, min, max); } | sere equalargs { - if ($2.max < $2.min) + auto [min, max] = $2; + if (max < min) { error_list.emplace_back(@2, "reversed range"); - std::swap($2.max, $2.min); + std::swap(max, min); } - if (sere_ensure_bool($1, @1, "[=...]", error_list)) + if (auto f = sere_ensure_bool($1, @1, "[=...]", error_list)) { - $$ = formula::sugar_equal(formula($1), - $2.min, $2.max).to_node_(); + $$ = formula::sugar_equal(formula(f), + min, max).to_node_(); } else { - $1->destroy(); $$ = error_false_block(@$, error_list); } } | sere gotoargs { - if ($2.max < $2.min) + auto [min, max] = $2; + if (max < min) { error_list.emplace_back(@2, "reversed range"); - std::swap($2.max, $2.min); + std::swap(max, min); } - if (sere_ensure_bool($1, @1, "[->...]", error_list)) + if (auto f = sere_ensure_bool($1, @1, "[->...]", error_list)) { - $$ = formula::sugar_goto(formula($1), - $2.min, $2.max).to_node_(); + $$ = formula::sugar_goto(formula(f), min, max).to_node_(); } else { - $1->destroy(); $$ = error_false_block(@$, error_list); } } | sere OP_XOR sere { - if (sere_ensure_bool($1, @1, "`^'", error_list) - && sere_ensure_bool($3, @3, "`^'", error_list)) + auto left = sere_ensure_bool($1, @1, "`^'", error_list); + auto right = sere_ensure_bool($3, @3, "`^'", error_list); + if (left && right) { - $$ = fnode::binop(op::Xor, $1, $3); + $$ = fnode::binop(op::Xor, left, right); } else { - $1->destroy(); - $3->destroy(); + if (left) + left->destroy(); + else if (right) + right->destroy(); $$ = error_false_block(@$, error_list); } } @@ -678,14 +814,13 @@ sere: booleanatom { missing_right_binop($$, $1, @2, "xor operator"); } | sere OP_IMPLIES sere { - if (sere_ensure_bool($1, @1, "`->'", error_list)) + auto left = sere_ensure_bool($1, @1, "`->'", error_list); + if (left) { - $$ = fnode::binop(op::Implies, $1, $3); + $$ = fnode::binop(op::Implies, left, $3); } else { - $1->destroy(); - $3->destroy(); $$ = error_false_block(@$, error_list); } } @@ -693,15 +828,18 @@ sere: booleanatom { missing_right_binop($$, $1, @2, "implication operator"); } | sere OP_EQUIV sere { - if (sere_ensure_bool($1, @1, "`<->'", error_list) - && sere_ensure_bool($3, @3, "`<->'", error_list)) + auto left = sere_ensure_bool($1, @1, "`<->'", error_list); + auto right = sere_ensure_bool($3, @3, "`<->'", error_list); + if (left && right) { - $$ = fnode::binop(op::Equiv, $1, $3); + $$ = fnode::binop(op::Equiv, left, right); } else { - $1->destroy(); - $3->destroy(); + if (left) + left->destroy(); + else if (right) + right->destroy(); $$ = error_false_block(@$, error_list); } } @@ -739,19 +877,17 @@ bracedsere: BRACE_OPEN sere BRACE_CLOSE } | BRA_BLOCK { - $$ = try_recursive_parse(*$1, @1, parse_environment, + $$ = try_recursive_parse($1, @1, parse_environment, debug_level(), parser_sere, error_list); - delete $1; if (!$$) YYERROR; } parenthesedsubformula: PAR_BLOCK { - $$ = try_recursive_parse(*$1, @1, parse_environment, + $$ = try_recursive_parse($1, @1, parse_environment, debug_level(), parser_ltl, error_list); - delete $1; if (!$$) YYERROR; } @@ -786,10 +922,9 @@ parenthesedsubformula: PAR_BLOCK boolformula: booleanatom | PAR_BLOCK { - $$ = try_recursive_parse(*$1, @1, parse_environment, + $$ = try_recursive_parse($1, @1, parse_environment, debug_level(), parser_bool, error_list); - delete $1; if (!$$) YYERROR; } @@ -821,19 +956,19 @@ boolformula: booleanatom $$ = fnode::ff(); } | boolformula OP_AND boolformula - { $$ = fnode::multop(op::And, {$1, $3}); } + { $$ = pnode(op::And, $1, $3); } | boolformula OP_AND error { missing_right_binop($$, $1, @2, "and operator"); } | boolformula OP_SHORT_AND boolformula - { $$ = fnode::multop(op::And, {$1, $3}); } + { $$ = pnode(op::And, $1, $3); } | boolformula OP_SHORT_AND error { missing_right_binop($$, $1, @2, "and operator"); } | boolformula OP_STAR boolformula - { $$ = fnode::multop(op::And, {$1, $3}); } + { $$ = pnode(op::And, $1, $3); } | boolformula OP_STAR error { missing_right_binop($$, $1, @2, "and operator"); } | boolformula OP_OR boolformula - { $$ = fnode::multop(op::Or, {$1, $3}); } + { $$ = pnode(op::Or, $1, $3); } | boolformula OP_OR error { missing_right_binop($$, $1, @2, "or operator"); } | boolformula OP_XOR boolformula @@ -856,19 +991,19 @@ boolformula: booleanatom subformula: booleanatom | parenthesedsubformula | subformula OP_AND subformula - { $$ = fnode::multop(op::And, {$1, $3}); } + { $$ = pnode(op::And, $1, $3); } | subformula OP_AND error { missing_right_binop($$, $1, @2, "and operator"); } | subformula OP_SHORT_AND subformula - { $$ = fnode::multop(op::And, {$1, $3}); } + { $$ = pnode(op::And, $1, $3); } | subformula OP_SHORT_AND error { missing_right_binop($$, $1, @2, "and operator"); } | subformula OP_STAR subformula - { $$ = fnode::multop(op::And, {$1, $3}); } + { $$ = pnode(op::And, $1, $3); } | subformula OP_STAR error { missing_right_binop($$, $1, @2, "and operator"); } | subformula OP_OR subformula - { $$ = fnode::multop(op::Or, {$1, $3}); } + { $$ = pnode(op::Or, $1, $3); } | subformula OP_OR error { missing_right_binop($$, $1, @2, "or operator"); } | subformula OP_XOR subformula @@ -904,13 +1039,15 @@ subformula: booleanatom | OP_F error { missing_right_op($$, @1, "sometimes operator"); } | OP_FREP sqbkt_num OP_SQBKT_CLOSE subformula %prec OP_FREP - { $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4); + { unsigned n = $2; + $$ = fnode::nested_unop_range(op::X, op::Or, n, n, $4); error_list.emplace_back(@1 + @3, "F[n:m] expects two parameters"); } | OP_FREP sqbkt_num OP_SQBKT_STRONG_CLOSE subformula %prec OP_FREP - { $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, $2, $4); + { unsigned n = $2; + $$ = fnode::nested_unop_range(op::strong_X, op::Or, n, n, $4); error_list.emplace_back(@1 + @3, "F[n:m!] expects two parameters"); } @@ -966,14 +1103,16 @@ subformula: booleanatom { $$ = fnode::nested_unop_range(op::strong_X, op::And, $2, fnode::unbounded(), $5); } | OP_GREP sqbkt_num OP_SQBKT_CLOSE subformula %prec OP_GREP - { $$ = fnode::nested_unop_range(op::X, op::And, $2, $2, $4); + { unsigned n = $2; + $$ = fnode::nested_unop_range(op::X, op::And, n, n, $4); error_list.emplace_back(@1 + @3, "G[n:m] expects two parameters"); } | OP_GREP sqbkt_num OP_SQBKT_STRONG_CLOSE subformula %prec OP_GREP - { $$ = fnode::nested_unop_range(op::strong_X, op::And, - $2, $2, $4); + { unsigned n = $2; + $$ = fnode::nested_unop_range(op::strong_X, op::And, + n, n, $4); error_list.emplace_back(@1 + @3, "G[n:m!] expects two parameters"); } @@ -1003,7 +1142,8 @@ subformula: booleanatom | OP_STRONG_X error { missing_right_op($$, @1, "strong next operator"); } | OP_XREP sqbkt_num OP_SQBKT_CLOSE subformula %prec OP_XREP - { $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4); } + { unsigned n = $2; + $$ = fnode::nested_unop_range(op::X, op::Or, n, n, $4); } | OP_XREP sqbkt_num OP_SQBKT_CLOSE error { missing_right_op($$, @1 + @3, "X[.] operator"); } | OP_XREP error OP_SQBKT_CLOSE subformula %prec OP_XREP @@ -1013,8 +1153,9 @@ subformula: booleanatom { $$ = fnode::unop(op::strong_X, $3); } | OP_XREP sqbkt_num OP_SQBKT_STRONG_CLOSE subformula %prec OP_XREP - { $$ = fnode::nested_unop_range(op::strong_X, - op::Or, $2, $2, $4); } + { unsigned n = $2; + $$ = fnode::nested_unop_range(op::strong_X, + op::Or, n, n, $4); } | OP_XREP error OP_SQBKT_STRONG_CLOSE subformula %prec OP_XREP { error_list.emplace_back(@$, "treating this X[.!] as a simple X[!]"); $$ = fnode::unop(op::strong_X, $4); } @@ -1032,41 +1173,40 @@ subformula: booleanatom | bracedsere parenthesedsubformula { $$ = fnode::binop(op::UConcat, $1, $2); } | bracedsere OP_UCONCAT error - { missing_right_binop_hard($$, $1, @2, - "universal overlapping concat operator"); } + { missing_right_op($$, @2, + "universal overlapping concat operator"); } | bracedsere OP_ECONCAT subformula { $$ = fnode::binop(op::EConcat, $1, $3); } | bracedsere OP_ECONCAT error - { missing_right_binop_hard($$, $1, @2, - "existential overlapping concat operator"); + { missing_right_op($$, @2, + "existential overlapping concat operator"); } | bracedsere OP_UCONCAT_NONO subformula /* {SERE}[]=>EXP = {SERE;1}[]->EXP */ { $$ = fnode::binop(op::UConcat, - fnode::multop(op::Concat, {$1, fnode::tt()}), + pnode(op::Concat, $1, fnode::tt()), $3); } | bracedsere OP_UCONCAT_NONO error - { missing_right_binop_hard($$, $1, @2, - "universal non-overlapping concat operator"); + { missing_right_op($$, @2, + "universal non-overlapping concat operator"); } | bracedsere OP_ECONCAT_NONO subformula /* {SERE}<>=>EXP = {SERE;1}<>->EXP */ { $$ = fnode::binop(op::EConcat, - fnode::multop(op::Concat, {$1, fnode::tt()}), + pnode(op::Concat, $1, fnode::tt()), $3); } | bracedsere OP_ECONCAT_NONO error - { missing_right_binop_hard($$, $1, @2, - "existential non-overlapping concat operator"); + { missing_right_op($$, @2, + "existential non-overlapping concat operator"); } | BRACE_OPEN sere BRACE_BANG_CLOSE /* {SERE}! = {SERE} <>-> 1 */ { $$ = fnode::binop(op::EConcat, $2, fnode::tt()); } | BRA_BANG_BLOCK { - $$ = try_recursive_parse(*$1, @1, parse_environment, + $$ = try_recursive_parse($1, @1, parse_environment, debug_level(), parser_sere, error_list); - delete $1; if (!$$) YYERROR; $$ = fnode::binop(op::EConcat, $$, fnode::tt()); @@ -1076,9 +1216,9 @@ lbtformula: atomprop | '!' lbtformula { $$ = fnode::unop(op::Not, $2); } | '&' lbtformula lbtformula - { $$ = fnode::multop(op::And, {$2, $3}); } + { $$ = pnode(op::And, $2, $3); } | '|' lbtformula lbtformula - { $$ = fnode::multop(op::Or, {$2, $3}); } + { $$ = pnode(op::Or, $2, $3); } | '^' lbtformula lbtformula { $$ = fnode::binop(op::Xor, $2, $3); } | 'i' lbtformula lbtformula diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index 34fbfef32..871f1300d 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -130,26 +130,26 @@ eol2 (\n\r)+|(\r\n)+ recursively. */ BEGIN(in_par); parent_level = 1; - yylval->str = new std::string(); + yylval->emplace(); } { "(" { ++parent_level; - yylval->str->append(yytext, yyleng); + yylval->as().append(yytext, yyleng); } ")" { if (--parent_level) { - yylval->str->append(yytext, yyleng); + yylval->as().append(yytext, yyleng); } else { BEGIN(not_prop); - spot::trim(*yylval->str); + spot::trim(yylval->as()); return token::PAR_BLOCK; } } - [^()]+ yylval->str->append(yytext, yyleng); + [^()]+ yylval->as().append(yytext, yyleng); <> { unput(')'); if (!missing_parent) @@ -172,38 +172,38 @@ eol2 (\n\r)+|(\r\n)+ recursively. */ BEGIN(in_bra); parent_level = 1; - yylval->str = new std::string(); + yylval->emplace(); } { "{" { ++parent_level; - yylval->str->append(yytext, yyleng); + yylval->as().append(yytext, yyleng); } "}"[ \t]*"!" { if (--parent_level) { - yylval->str->append(yytext, yyleng); + yylval->as().append(yytext, yyleng); } else { BEGIN(not_prop); - spot::trim(*yylval->str); + spot::trim(yylval->as()); return token::BRA_BANG_BLOCK; } } "}" { if (--parent_level) { - yylval->str->append(yytext, yyleng); + yylval->as().append(yytext, yyleng); } else { BEGIN(not_prop); - spot::trim(*yylval->str); + spot::trim(yylval->as()); return token::BRA_BLOCK; } } - [^{}]+ yylval->str->append(yytext, yyleng); + [^{}]+ yylval->as().append(yytext, yyleng); <> { unput('}'); if (!missing_parent) @@ -231,35 +231,36 @@ eol2 (\n\r)+|(\r\n)+ /* SVA operators */ "##"[0-9] { - yylval->num = yytext[2] - '0'; + yylval->emplace(yytext[2] - '0'); return token::OP_DELAY_N; } "##"[0-9][0-9] { - yylval->num = - yytext[2] * 10 + yytext[3] - '0' * 11; + yylval->emplace(yytext[2] * 10 + + yytext[3] + - '0' * 11); return token::OP_DELAY_N; } "##"[0-9]{3,} { errno = 0; unsigned long n = strtoul(yytext + 2, 0, 10); - yylval->num = n; - if (errno || yylval->num != n) + yylval->emplace(n); + if (errno || yylval->as() != n) { error_list.push_back( spot::one_parse_error(*yylloc, "value too large ignored")); - yylval->num = 1; + yylval->emplace(1); } - if (yylval->num >= spot::fnode::unbounded()) + if (yylval->as() >= spot::fnode::unbounded()) { auto max = spot::fnode::unbounded() - 1; std::ostringstream s; - s << yylval->num + s << yylval->as() << (" exceeds maximum supported " "repetition (") << max << ")"; error_list.emplace_back(*yylloc, s.str()); - yylval->num = max; + yylval->emplace(max); } return token::OP_DELAY_N; } @@ -288,8 +289,8 @@ eol2 (\n\r)+|(\r\n)+ [0-9]+ { errno = 0; unsigned long n = strtoul(yytext, 0, 10); - yylval->num = n; - if (errno || yylval->num != n) + yylval->emplace(n); + if (errno || yylval->as() != n) { error_list.push_back( spot::one_parse_error(*yylloc, @@ -380,7 +381,7 @@ eol2 (\n\r)+|(\r\n)+ */ [a-zA-EH-LN-QSTYZ_.][a-zA-EH-WYZ0-9_.]* | [a-zA-EH-LN-QSTYZ_.][a-zA-EH-WYZ0-9_.][a-zA-Z0-9_.]* { - yylval->str = new std::string(yytext, yyleng); + yylval->emplace(yytext, yyleng); BEGIN(not_prop); return token::ATOMIC_PROP; } @@ -401,7 +402,7 @@ eol2 (\n\r)+|(\r\n)+ { \" { BEGIN(orig_cond); - yylval->str = new std::string(s); + yylval->emplace(s); return token::ATOMIC_PROP; } {eol} { @@ -419,7 +420,7 @@ eol2 (\n\r)+|(\r\n)+ spot::one_parse_error(*yylloc, "unclosed string")); BEGIN(orig_cond); - yylval->str = new std::string(s); + yylval->emplace(s); return token::ATOMIC_PROP; } } @@ -430,7 +431,7 @@ eol2 (\n\r)+|(\r\n)+ for compatibility with ltl2dstar we also accept any alphanumeric string that is not an operator. */ [a-zA-Z._][a-zA-Z0-9._]* { - yylval->str = new std::string(yytext, yyleng); + yylval->emplace(yytext, yyleng); return token::ATOMIC_PROP; } diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 8fe91bf70..fb4ab0d49 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et +// Copyright (C) 2015-2019, 2021, 2022 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -136,7 +136,7 @@ namespace spot // - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = // AndRat(And(Bool1,Bool2),Exps1...,Exps2...,Exps3...) // - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = - // AndRat(Or(Bool1,Bool2),Exps1...,Exps2...,Exps3...) + // OrRat(Or(Bool1,Bool2),Exps1...,Exps2...,Exps3...) if (!b.empty()) v.insert(v.begin(), fnode::multop(o, std::move(b))); } @@ -588,9 +588,9 @@ namespace spot } else if (min != unbounded()) { - min += min2; - if (SPOT_UNLIKELY(min >= unbounded())) + if (SPOT_UNLIKELY(min + min2 >= unbounded())) break; + min += min2; } if (max2 == unbounded()) { @@ -598,9 +598,9 @@ namespace spot } else if (max != unbounded()) { - max += max2; - if (SPOT_UNLIKELY(max >= unbounded())) + if (SPOT_UNLIKELY(max + max2 >= unbounded())) break; + max += max2; } (*i)->destroy(); i = v.erase(i); diff --git a/tests/Makefile.am b/tests/Makefile.am index afcd0c8d2..c8a722f5c 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -165,6 +165,7 @@ TESTS_tl = \ core/parse.test \ core/parseerr.test \ core/utf8.test \ + core/500.test \ core/length.test \ core/equals.test \ core/tostring.test \ diff --git a/tests/core/500.test b/tests/core/500.test new file mode 100755 index 000000000..60d5c6365 --- /dev/null +++ b/tests/core/500.test @@ -0,0 +1,43 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). +# +# 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 . + +. ./defs + +set -e + +# The LTL parser used to exhibit a worse-than-quadratic behavior on +# n-ary operators with many children. See issue #500. Before the +# fix, this test would run for ages. + +awk 'BEGIN{x="s0"; for(i = 1; i < 40000; ++i) x=x " | s" i; print x;}' | + ltlfilt --stats=%x > out +test 40000 = `cat out` + +awk 'BEGIN{x="s0"; for(i = 1; i < 40000; ++i) x=x " & s" i; print x;}' | + ltlfilt --stats=%x > out +test 40000 = `cat out` + +awk 'BEGIN{x="s0"; for(i = 1; i < 40000; ++i) x=x ";s" i; print "{" x "}";}' | + ltlfilt --stats=%x > out +test 40000 = `cat out` + +awk 'BEGIN{x="s0"; for(i = 1; i < 40000; ++i) x=x ":s" i; print "{" x "}";}' | + ltlfilt --stats=%x > out +test 40000 = `cat out` diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 79a07a17a..8397bbc85 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2022 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 @@ -375,8 +375,8 @@ diff output expected cat >formulas < outx diff outx exp cat >exp < GFe +trying to create strategy directly for GFe <-> (Fa & Fb & Fc & Fd) direct strategy was found. EOF ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \ diff --git a/tests/core/tostring.test b/tests/core/tostring.test index e559ea198..7067a8b2c 100755 --- a/tests/core/tostring.test +++ b/tests/core/tostring.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2013, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2009-2011, 2013, 2016, 2022 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 # et Marie Curie. @@ -63,7 +63,7 @@ X"R" {a;b;{c && d[*]};[+]}[]-> G{a[*]:b[*]} GF!(b & (a | c)) GF!({b && {a | c[*]}}<>-> {{!a}[*]}) -GF({{a | c[*]} & b[*]}[]-> d) +GF({b[*] & {a | c[*]}}[]-> d) {a[*2..3]} {a[*0..1]} {a[*]}