From bf31ff12ad7f4436e2cd4229b5c261515301624b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Mar 2017 17:13:59 +0100 Subject: [PATCH 01/20] parsetl: improve coverage * spot/parsetl/parsetl.yy: Adjust one diagnostic. * spot/parsetl/scantl.ll: Fix recovering of missing closing brace in lenient mode. * tests/python/ltlparse.py: Add tests. * NEWS: Mention the lenient mode bug. --- NEWS | 5 +- spot/parsetl/parsetl.yy | 2 +- spot/parsetl/scantl.ll | 8 +-- tests/python/ltlparse.py | 139 ++++++++++++++++++++++++++++++++++++++- 4 files changed, 145 insertions(+), 9 deletions(-) diff --git a/NEWS b/NEWS index 76faccc9b..4935340f1 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.3.2.dev (not yet released) - Nothing yet. + Bug fixes: + + - In "lenient" mode the parser would fail to recover from + a missing closing brace. New in spot 2.3.2 (2017-03-15) diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index 0830e70c7..4fe86356d 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -393,7 +393,7 @@ fstarargs: OP_BFSTAR equalargs: OP_EQUAL_OPEN sqbracketargs { $$ = $2; } | OP_EQUAL_OPEN error OP_SQBKT_CLOSE - { error_list.emplace_back(@$, "treating this equal block as [*]"); + { error_list.emplace_back(@$, "treating this equal block as [=]"); $$.min = 0U; $$.max = fnode::unbounded(); } | OP_EQUAL_OPEN error_opt END_OF_INPUT { error_list. diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index fc40db1b8..256543726 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, Laboratoire de -** Recherche et Développement de l'Epita (LRDE). +** Copyright (C) 2010-2015, 2017, 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. @@ -142,7 +142,7 @@ eol2 (\n\r)+|(\r\n)+ if (!missing_parent) error_list.push_back( spot::one_parse_error(*yylloc, - "missing closing parenthese")); + "missing closing parenthesis")); missing_parent = true; } } @@ -192,7 +192,7 @@ eol2 (\n\r)+|(\r\n)+ } [^{}]+ yylval->str->append(yytext, yyleng); <> { - unput(')'); + unput('}'); if (!missing_parent) error_list.push_back( spot::one_parse_error(*yylloc, diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index de4bff9d6..828ebda41 100755 --- a/tests/python/ltlparse.py +++ b/tests/python/ltlparse.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et +# Copyright (C) 2009-2012, 2014-2017 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 @@ -33,12 +33,145 @@ for str1 in l: sys.exit(1) str2 = str(pf.f) del pf - sys.stdout.write(str2 + "\n") # Try to reparse the stringified formula pf = spot.parse_infix_psl(str2, e) if pf.format_errors(spot.get_cout()): sys.exit(1) - sys.stdout.write(str(pf.f) + "\n") del pf +for str1 in ['a * b', 'a xor b', 'a <-> b']: + pf = spot.parse_infix_boolean(str1, e, False) + if pf.format_errors(spot.get_cout()): + sys.exit(1) + str2 = str(pf.f) + del pf + # Try to reparse the stringified formula + pf = spot.parse_infix_boolean(str2, e) + if pf.format_errors(spot.get_cout()): + sys.exit(1) + del pf + +f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]') +assert not f6.errors +del f6 + +f6 = spot.parse_infix_sere('-') +assert f6.errors +del f6 + +for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), + ('{foo[->', 'missing closing bracket for goto operator'), + ('{foo[->3..1]}', "reversed range"), + ('{foo[*bug]}', "treating this star block as [*]"), + ('{foo[*bug', "missing closing bracket for star"), + ('{foo[*3..1]}', "reversed range"), + ('{[*3..1]}', "reversed range"), + ('{foo[:*bug]}', "treating this fusion-star block as [:*]"), + ('{foo[:*3..1]}', "reversed range"), + ('{foo[:*bug', "missing closing bracket for fusion-star"), + ('{foo[=bug]}', "treating this equal block as [=]"), + ('{foo[=bug', "missing closing bracket for equal operator"), + ('{foo[=3..1]}', "reversed range"), + ('{()}', "treating this brace block as false"), + ('{(a b)}', "treating this parenthetical block as false"), + ('{(a*}', "missing closing parenthesis"), + ('{(a*&)}', "missing right operand for " + + "\"non-length-matching and operator\""), + ('{(a*&&)}', "missing right operand for " + + "\"length-matching and operator\""), + ('{(a*|)}', "missing right operand for \"or operator\""), + ('{a*;}', "missing right operand for \"concat operator\""), + ('{a*::b}', "missing right operand for \"fusion operator\""), + ('{a* xor }', "missing right operand for \"xor operator\""), + ('{a* -> }', "missing right operand for " + + "\"implication operator\""), + ('{a <-> <-> b }', + "missing right operand for \"equivalent operator\""), + ('{a;b b}', "ignoring this"), + ('{*', "missing closing brace"), + ('{(a', "missing closing parenthesis"), + ('{* a', "ignoring trailing garbage and missing closing brace"), + ('F(a b)', "ignoring this"), + ('F(-)', "treating this parenthetical block as false"), + ('F(', "missing closing parenthesis"), + ('F(a b', "ignoring trailing garbage and " + + "missing closing parenthesis"), + ('F(-', "missing closing parenthesis"), + ('F(-', "parenthetical block as false"), + ('a&', "missing right operand for \"and operator\""), + ('a*', "missing right operand for \"and operator\""), + ('a|', "missing right operand for \"or operator\""), + ('a^', "missing right operand for \"xor operator\""), + ('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('!', "missing right operand for \"not operator\""), + ('a W', "missing right operand for \"weak until operator\""), + ('a U', "missing right operand for \"until operator\""), + ('a R', "missing right operand for \"release operator\""), + ('a M', "missing right operand for " + + "\"strong release operator\""), + ('{a}[]->', "missing right operand for " + + "\"universal overlapping concat operator\""), + ('{a}[]=>', "missing right operand for " + + "\"universal non-overlapping concat operator\""), + ('{a}<>->', "missing right operand for " + + "\"existential overlapping concat operator\""), + ('{a}<>=>', "missing right operand for " + + "\"existential non-overlapping concat operator\""), + ('(X)', "missing right operand for \"next operator\""), + ('("X)', "unclosed string"), + ('("X)', "missing closing parenthesis"), + ('{"X', "unclosed string"), + ('{"X}', "missing closing brace"), + ]: + f7 = spot.parse_infix_psl(x) + assert f7.errors + ostr = spot.ostringstream() + f7.format_errors(ostr) + err = ostr.str() + print(err) + assert msg in err + del f7 + +for (x, msg) in [('a&', "missing right operand for \"and operator\""), + ('a*', "missing right operand for \"and operator\""), + ('a|', "missing right operand for \"or operator\""), + ('a^', "missing right operand for \"xor operator\""), + ('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('(-', "parenthetical block as false"), + ('(-', "missing closing parenthesis"), + ('(-)', "treating this parenthetical block as false"), + ('(a', "missing closing parenthesis"), + ('(a b)', "ignoring this"), + ('(a b', "ignoring trailing garbage and " + + "missing closing parenthesis"), + ('!', "missing right operand for \"not operator\""), + ]: + f8 = spot.parse_infix_boolean(x) + assert f8.errors + ostr = spot.ostringstream() + f8.format_errors(ostr) + err = ostr.str() + print(err) + assert msg in err + del f8 + +for (x, msg) in [('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('(aa', "missing closing parenthesis"), + ('("aa', "missing closing parenthesis"), + ('"(aa', "unclosed string"), + ('{aa', "missing closing brace"), + ]: + f9 = spot.parse_infix_psl(x, spot.default_environment.instance(), + False, True) + assert f9.errors + ostr = spot.ostringstream() + f9.format_errors(ostr) + err = ostr.str() + print(err) + assert msg in err + del f9 + assert spot.fnode_instances_check() From 0121d278a78fc568813d2e359910960ed3148c55 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Mar 2017 13:29:51 +0100 Subject: [PATCH 02/20] * doc/org/tut11.org: Typo in title. --- doc/org/tut11.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/org/tut11.org b/doc/org/tut11.org index beb9433ec..703664a73 100644 --- a/doc/org/tut11.org +++ b/doc/org/tut11.org @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -#+TITLE: Translating an LTL formula into a monitors +#+TITLE: Translating an LTL formula into a monitor #+DESCRIPTION: Code example for using Spot to translating formulas in monitors #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html From 1596f0ed75ddbd704eff049f4862fa6755cbcf2f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 18 Mar 2017 18:44:25 +0100 Subject: [PATCH 03/20] org: move babel's temporary directory in builddir Fixes #244, reported by Vincent Tourneur. * doc/org/.dir-locals.el.in, doc/org/init.el.in: Define org-babel-temporary-directory and create the directory. --- doc/org/.dir-locals.el.in | 4 +++- doc/org/init.el.in | 6 ++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/doc/org/.dir-locals.el.in b/doc/org/.dir-locals.el.in index a8b2a07de..62d969e67 100644 --- a/doc/org/.dir-locals.el.in +++ b/doc/org/.dir-locals.el.in @@ -24,14 +24,16 @@ (getenv "DYLD_LIBRARY_PATH"))) (setenv "SPOT_DOTDEFAULT" "Brf(Lato)C(#ffffa0)") (setenv "SPOT_DOTEXTRA" "edge[arrowhead=vee, arrowsize=.7]") + (setq org-babel-temporary-directory "@abs_top_builddir@/doc/org/tmp") + (make-directory org-babel-temporary-directory t) (org-babel-do-load-languages 'org-babel-load-languages `((,(if (version< org-version "8.3") 'sh 'shell) . t) (python . t) (plantuml . t) (dot . t) (C . t))))) - (org-plantuml-jar-path . "@abs_top_builddir@/doc/org/plantuml.jar") (org-confirm-babel-evaluate . nil) + (org-plantuml-jar-path . "@abs_top_builddir@/doc/org/plantuml.jar") (org-babel-python-command . "@PYTHON@") (org-babel-C++-compiler . "./g++wrap") (shell-file-name . "@SHELL@") diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 7ad94703c..19e922c26 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -28,6 +28,8 @@ (C . t))) (setq org-confirm-babel-evaluate nil) (setq org-plantuml-jar-path "@abs_top_builddir@/doc/org/plantuml.jar") +(setq org-babel-temporary-directory "@abs_top_builddir@/doc/org/tmp") +(make-directory org-babel-temporary-directory t) (setq org-babel-python-command "@PYTHON@") (setq org-babel-C++-compiler "./g++wrap") (setq shell-file-name "@SHELL@") @@ -90,3 +92,7 @@ ("spot-all" :components ("spot-html" "spot-static")))) (org-publish-all t) +;;; org-babel-remove-temporary-directory does not correctly remove +;;; nested directories and we have some files in tmp/.libs/ because of +;;; libtool. So let us clean that ourselves. +(delete-directory org-babel-temporary-directory t) From cdf699ff23adf15bb04a685652b8e2955adca1a3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Mar 2017 14:06:02 +0100 Subject: [PATCH 04/20] genltl: fix %F for --r-left and --r-right Fixes #247. * bin/genltl.cc: Here. * tests/core/genltl.test: Make sure %F always return a correct pattern name.. * NEWS: Mention the bug. --- NEWS | 3 +++ bin/genltl.cc | 4 ++-- tests/core/genltl.test | 8 ++++++++ 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 4935340f1..cad2abe75 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,9 @@ New in spot 2.3.2.dev (not yet released) - In "lenient" mode the parser would fail to recover from a missing closing brace. + - The output of 'genltl --r-left=1 --r-right=1 --format=%F' + had typos. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/bin/genltl.cc b/bin/genltl.cc index 4c1fc995c..dc812d7be 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -223,8 +223,8 @@ const char* const class_name[LAST_CLASS - FIRST_CLASS] = "or-fg", "or-g", "or-gf", - "or-r-left", - "or-r-right", + "r-left", + "r-right", "rv-counter", "rv-counter-carry", "rv-counter-carry-linear", diff --git a/tests/core/genltl.test b/tests/core/genltl.test index 67b30fe8c..88ddae403 100755 --- a/tests/core/genltl.test +++ b/tests/core/genltl.test @@ -21,6 +21,14 @@ . ./defs set -e +# Make sure the name of each pattern is correctly output by %F. +opts=`genltl --help | sed -n '/=RANGE/{ +s/^ *// +s/[=[].*/=1/p +}'` +res=`genltl $opts --format="--%F=%L"` +test "$opts" = "$res" + run 0 genltl --dac=1..5 --eh=1..5 --pos --neg --format="%F:%L %f" >output cat >expected < Date: Mon, 27 Mar 2017 21:39:16 +0200 Subject: [PATCH 05/20] complement: reset the terminal property Reported by Thomas Medioni. * spot/twaalgos/complement.cc: Here. * tests/core/complement.test: Add a test case. * NEWS: Mention it. --- NEWS | 4 ++++ spot/twaalgos/complement.cc | 14 ++++++++++++-- tests/core/complement.test | 33 ++++++++++++++++++++++----------- 3 files changed, 38 insertions(+), 13 deletions(-) diff --git a/NEWS b/NEWS index cad2abe75..a9504c67a 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,10 @@ New in spot 2.3.2.dev (not yet released) - The output of 'genltl --r-left=1 --r-right=1 --format=%F' had typos. + - 'ltl2tgba Fa | autfilt --complement' would incorrectly claim that + the output is "terminal" because dtwa_complement() failed to reset + that property. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 03f9c24c4..9fff15ef6 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -18,7 +18,7 @@ // along with this program. If not, see . #include -#include +#include #include #include @@ -27,9 +27,19 @@ namespace spot twa_graph_ptr dtwa_complement(const const_twa_graph_ptr& aut) { + if (!is_deterministic(aut)) + throw + std::runtime_error("dtwa_complement() requires a deterministic input"); + // Simply complete the automaton, and complement its acceptance. auto res = cleanup_acceptance_here(complete(aut)); res->set_acceptance(res->num_sets(), res->get_acceptance().complement()); + // Complementing the acceptance is likely to break the terminal + // property, but not weakness. We make a useless call to + // prop_keep() just so we remember to update it in the future if a + // new argument is added. + res->prop_keep({true, true, true, true, true}); + res->prop_terminal(trival::maybe()); return res; } } diff --git a/tests/core/complement.test b/tests/core/complement.test index 2c03e0604..6a1f4c1c2 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -22,12 +22,8 @@ set -e -autfilt=autfilt -ltl2tgba=ltl2tgba -randaut=randaut - -$randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut -run 0 $autfilt --complement -H aut >/dev/null +randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut +run 0 autfilt --complement -H aut >/dev/null cat >in <out +autfilt --complement -H in >out cat >expected <out +ltl2tgba -H 'GFa & GFb' Xa Fa | autfilt --complement -H >out cat >expected <out +ltl2tgba -H 'FGa' | autfilt --complement >out cat >expected < Date: Tue, 28 Mar 2017 23:34:41 +0200 Subject: [PATCH 06/20] twa_graph: fix purge_unreachable_states on alternating automata The algorithm had two problems: it was removing only useless destination from universal destination (instead of removing the entire edge), and it was not properly iterating over the entire reachable automaton. * spot/twa/twagraph.cc: Fix it. * spot/twa/twagraph.hh: Adjust documentation. * tests/core/alternating.test: Add more tests. * tests/python/twagraph.py: Adjust. * NEWS: Mention the bug. --- NEWS | 3 + spot/twa/twagraph.cc | 151 ++++++++++++++++++++++++++---------- spot/twa/twagraph.hh | 14 +++- tests/core/alternating.test | 125 ++++++++++++++++++++++++++++- tests/python/twagraph.py | 1 + 5 files changed, 250 insertions(+), 44 deletions(-) diff --git a/NEWS b/NEWS index a9504c67a..c2a08072e 100644 --- a/NEWS +++ b/NEWS @@ -12,6 +12,9 @@ New in spot 2.3.2.dev (not yet released) the output is "terminal" because dtwa_complement() failed to reset that property. + - spot::twa_graph::purge_unreachable_states() was misbehaving on + alternating automata. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 28733cab6..69f5da01d 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -245,6 +245,8 @@ namespace spot std::vector order; order.reserve(num_states); + bool purge_unreachable_needed = false; + if (is_existential()) { std::vector> todo; // state, edge @@ -307,13 +309,16 @@ namespace spot const unsigned*& end = std::get<3>(todo.back()); if (tid == 0U && begin == end) { + unsigned src = std::get<0>(todo.back()); todo.pop_back(); + // Last transition from a state? + if ((int)src >= 0 && (todo.empty() + || src != std::get<0>(todo.back()))) + order.emplace_back(src); if (todo.empty()) break; - unsigned src = std::get<0>(todo.back()); - if ((int)src >= 0) - order.emplace_back(src); - continue; + else + continue; } unsigned dst = *begin++; if (begin == end) @@ -338,53 +343,76 @@ namespace spot } } - // Process states in topological order - for (auto s: order) + // At this point, all reachable states with successors are marked + // as useful. + for (;;) { - auto t = g_.out_iteraser(s); - bool useless = true; - while (t) + bool univ_edge_erased = false; + // Process states in topological order to mark those without + // successors as useless. + for (auto s: order) { - bool usefuldst = false; - for (unsigned d: univ_dests(t->dst)) - if (useful[d]) - { - usefuldst = true; - break; - } - // Erase any edge to a useless state. - if (!usefuldst) + auto t = g_.out_iteraser(s); + bool useless = true; + while (t) { - t.erase(); - continue; + // An edge is useful if all its + // destinations are useful. + bool usefuledge = true; + for (unsigned d: univ_dests(t->dst)) + if (!useful[d]) + { + usefuledge = false; + break; + } + // Erase any useless edge + if (!usefuledge) + { + if (is_univ_dest(t->dst)) + univ_edge_erased = true; + t.erase(); + continue; + } + // if we have a edge to a useful state, then the + // state is useful. + useless = false; + ++t; } - // if we have a edge to a useful state, then the - // state is useful. - useless = false; - ++t; + if (useless) + useful[s] = 0; } - if (useless) - useful[s] = 0; + // If we have erased any universal destination, it is possible + // that we have have created some new dead states, so we + // actually need to redo the whole thing again until there is + // no more universal edge to remove. Also we might have + // created some unreachable states, so we will simply call + // purge_unreachable_states() later to clean this. + if (!univ_edge_erased) + break; + else + purge_unreachable_needed = true; } - // Make sure at least one initial destination is useful (even if - // it has been marked as useless by the previous loop because it - // has no successor). - bool usefulinit = false; + // Is the initial state actually useful? If not, make this an + // empty automaton by resetting the graph. + bool usefulinit = true; for (unsigned d: univ_dests(init_number_)) - if (useful[d]) + if (!useful[d]) { - usefulinit = true; + usefulinit = false; break; } if (!usefulinit) - for (unsigned d: univ_dests(init_number_)) - { - useful[d] = true; - break; - } + { + g_ = graph_t(); + init_number_ = new_state(); + prop_deterministic(true); + prop_stutter_invariant(true); + prop_weak(true); + return; + } - // Now renumber each used state. + // Renumber each used state. unsigned current = 0; for (unsigned s = 0; s < num_states; ++s) if (useful[s]) @@ -394,6 +422,9 @@ namespace spot if (current == num_states) return; // No useless state. defrag_states(std::move(useful), current); + + if (purge_unreachable_needed) + purge_unreachable_states(); } void twa_graph::defrag_states(std::vector&& newst, @@ -401,14 +432,46 @@ namespace spot { if (!is_existential()) { + // Running defrag_states() on alternating automata is tricky, + // because we want to + // #1 rename the regular states + // #2 rename the states in universal destinations + // #3 get rid of the unused universal destinations + // #4 merge identical universal destinations + // + // graph::degrag_states() actually does only #1. It it could + // do #2, but that would prevent use from doing #3 and #4. It + // cannot do #3 and #4 because the graph object does not know + // what an initial state is, and our initial state might be + // universal. + // + // As a consequence this code preforms #2, #3, and #4 before + // calling graph::degrag_states() to finish with #1. We clear + // the "dests vector" of the current automaton, recreate all + // the new destination groups using a univ_dest_mapper to + // simplify an unify them, and extend newst with some new + // entries that will point the those new universal destination + // so that graph::defrag_states() does not have to deal with + // universal destination in any way. auto& g = get_graph(); auto& dests = g.dests_vector(); + // Clear the destination vector, saving the old one. std::vector old_dests; std::swap(dests, old_dests); - std::vector seen(old_dests.size(), -1U); + // dests will be updated as a side effect of declaring new + // destination groups to uniq. internal::univ_dest_mapper uniq(g); + // The newst entry associated to each of the old destination + // group. + std::vector seen(old_dests.size(), -1U); + + // Rename a state if it denotes a universal destination. This + // function has to be applied to the destination of each edge, + // as well as to the initial state. The need to work on the + // initial state is the reason it cannot be implemented in + // graph::defrag_states(). auto fixup = [&](unsigned& in_dst) { unsigned dst = in_dst; @@ -416,8 +479,9 @@ namespace spot return; dst = ~dst; unsigned& nd = seen[dst]; - if (nd == -1U) + if (nd == -1U) // An unprocessed destination group { + // store all renamed destination states in tmp std::vector tmp; auto begin = old_dests.data() + dst + 1; auto end = begin + old_dests[dst]; @@ -430,10 +494,17 @@ namespace spot } if (tmp.empty()) { + // All destinations of this group were marked for + // removal. Mark this universal transition for + // removal as well. Is this really what we expect? nd = -1U; } else { + // register this new destination group, add et two + // newst, and use the index in newst to relabel + // the state so that graph::degrag_states() will + // eventually update it to the correct value. nd = newst.size(); newst.emplace_back(uniq.new_univ_dests(tmp.begin(), tmp.end())); diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 0594ab092..43e1e6bc2 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -541,18 +541,26 @@ namespace spot /// states without successors, unreachable states, and states /// that only have dead successors. /// + /// This function runs in linear time on non-alternating automata, + /// but its current implementation can be quadratic when removing + /// dead states from alternating automata. (In the latter case, a + /// universal edge has to be remove when any of its destination is + /// dead, but this might cause the other destinations to become + /// dead or unreachable themselves.) + /// /// \see purge_unreachable_states void purge_dead_states(); /// \brief Remove all unreachable states. /// - /// A state is unreachable if it cannot be reached from the initial state. + /// A state is unreachable if it cannot be reached from the + /// initial state. /// /// Use this function if you have declared more states than you - /// actually need in the automaton. + /// actually need in the automaton. It runs in linear time. /// /// purge_dead_states() will remove more states than - /// purge_unreachable_states(). + /// purge_unreachable_states(), but it is more costly. /// /// \see purge_dead_states void purge_unreachable_states(); diff --git a/tests/core/alternating.test b/tests/core/alternating.test index d8c0f3605..6b51c42a5 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -276,6 +276,27 @@ autfilt -q --intersect=ex1 ex3 cat >ex4<expect4<expect4d< out4 diff expect4 out4 run 0 autfilt --remove-dead-states ex4 > out4 -diff ex2 out4 +diff expect4d out4 cat >ex5< out5 @@ -347,6 +445,31 @@ AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak +--BODY-- +State: 0 +--END-- +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[!0] 1 +State: 1 +[!0] 1 +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 1 "a" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak --BODY-- State: 0 --END-- diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py index b87cfdb45..d6eec94f7 100644 --- a/tests/python/twagraph.py +++ b/tests/python/twagraph.py @@ -87,4 +87,5 @@ assert aut.edge_data(1).cond == bddtrue aut.release_iter(it) aut.purge_dead_states() +i = aut.get_init_state() assert aut.state_is_accepting(i) == False From f5d53e3a5e9e9f0ca740058466d97f5ce22f376f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 29 Mar 2017 11:56:11 +0200 Subject: [PATCH 07/20] python: update some incorrect or obsolete code * tests/python/ipnbdoctest.py: Use importlib instead of imp. * tests/python/ltlparse.py: Fix invalid escape sequence. --- tests/python/ipnbdoctest.py | 4 ++-- tests/python/ltlparse.py | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index d5c405c23..eb4256cf2 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -22,9 +22,9 @@ except ImportError: print('Python 3.x is needed to run this script.') sys.exit(77) -import imp +import importlib try: - imp.find_module('IPython') + importlib.util.find_spec('IPython') except: print('IPython is needed to run this script.') sys.exit(77) diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index 828ebda41..dd2368d64 100755 --- a/tests/python/ltlparse.py +++ b/tests/python/ltlparse.py @@ -25,7 +25,7 @@ import spot e = spot.default_environment.instance() -l = ['GFa', 'a U (((b)) xor c)', '!(FFx <=> Fx)', 'a \/ a \/ b \/ a \/ a']; +l = ['GFa', 'a U (((b)) xor c)', '!(FFx <=> Fx)', 'a \\/ a \\/ b \\/ a \\/ a'] for str1 in l: pf = spot.parse_infix_psl(str1, e, False) From b910330a789d44e0ced2ff7bf4c085cb47e565ce Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 30 Mar 2017 21:25:50 +0200 Subject: [PATCH 08/20] [buddy] Typos in comments * src/kernel.c (bdd_addref): Fix typo documentation. * src/bddop.c (bdd_appall, bdd_appallcomp): Likewise. --- buddy/src/bddop.c | 4 ++-- buddy/src/kernel.c | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index 1a90e53bd..b61eb9a96 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -2138,7 +2138,7 @@ SECTION {* operator *} SHORT {* apply operation and universal quantification *} PROTO {* BDD bdd_appall(BDD left, BDD right, int opr, BDD var) *} DESCR {* Applies the binary operator {\tt opr} to the arguments - {\tt left} and {\tt right} and then performs an universal + {\tt left} and {\tt right} and then performs a universal quantification of the variables from the variable set {\tt var}. This is done in a bottom up manner such that both the apply and quantification is done on the lower nodes before @@ -2160,7 +2160,7 @@ SECTION {* operator *} SHORT {* apply operation and universal (complemented) quantification *} PROTO {* BDD bdd_appall(BDD left, BDD right, int opr, BDD var) *} DESCR {* Applies the binary operator {\tt opr} to the arguments - {\tt left} and {\tt right} and then performs an universal + {\tt left} and {\tt right} and then performs a universal quantification of the variables which are {\bf not} in the variable set {\tt var}. This is done in a bottom up manner such that both the apply and quantification is done on the lower nodes before diff --git a/buddy/src/kernel.c b/buddy/src/kernel.c index b414de1c4..5422c2d76 100644 --- a/buddy/src/kernel.c +++ b/buddy/src/kernel.c @@ -1147,7 +1147,7 @@ SHORT {* increases the reference count on a node *} PROTO {* BDD bdd_addref(BDD r) *} DESCR {* Reference counting is done on externaly referenced nodes only and the count for a specific node {\tt r} can and must be - increased using this function to avoid loosing the node in the next + increased using this function to avoid losing the node in the next garbage collection. *} ALSO {* bdd\_delref *} RETURN {* The BDD node {\tt r}. *} From 1ed6e518dd4fc53dfea8ba68bb4b057cb6713e19 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 30 Mar 2017 21:22:55 +0200 Subject: [PATCH 09/20] various typos * bench/dtgbasat/gen.py, spot/twaalgos/complement.hh: Fix looser->loser and lossing->losing. * tests/sanity/style.test: Catch 'an uni[^n]'. * spot/ta/ta.hh, spot/taalgos/tgba2ta.cc, spot/taalgos/tgba2ta.hh, spot/twa/twagraph.cc, spot/twaalgos/complement.hh, spot/twaalgos/sccinfo.cc: Fix various occurences of this pattern. --- bench/dtgbasat/gen.py | 4 ++-- spot/ta/ta.hh | 4 ++-- spot/taalgos/tgba2ta.cc | 2 +- spot/taalgos/tgba2ta.hh | 4 ++-- spot/twa/twagraph.cc | 2 +- spot/twaalgos/complement.hh | 6 +++--- spot/twaalgos/sccinfo.cc | 2 +- tests/sanity/style.test | 11 +++++------ 8 files changed, 17 insertions(+), 18 deletions(-) diff --git a/bench/dtgbasat/gen.py b/bench/dtgbasat/gen.py index 4777c35c0..f581506db 100755 --- a/bench/dtgbasat/gen.py +++ b/bench/dtgbasat/gen.py @@ -115,7 +115,7 @@ def ne(string): # --------------------------------------------------------------SUMMARY -def add_winner(res, winner, looser): +def add_winner(res, winner, loser): """ Each time this function is called, it increments the scrore of one method against another one. @@ -125,7 +125,7 @@ def add_winner(res, winner, looser): for i in range(1, res_length): # except the first row (header) if winner in res[i]: for j in range(1, header_length): - if looser in res[0][j]: + if loser in res[0][j]: if type(res[i][j]) is str: res[i][j] = 1 else: diff --git a/spot/ta/ta.hh b/spot/ta/ta.hh index e790f920f..045cedf6b 100644 --- a/spot/ta/ta.hh +++ b/spot/ta/ta.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2010, 2012-2017 Laboratoire de Recherche et // Developpement de l Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -99,7 +99,7 @@ namespace spot /// \brief Get the artificial initial state set of the automaton. /// Return 0 if this artificial state is not implemented /// (in this case, use \c get_initial_states_set) - /// The aim of adding this state is to have an unique initial state. This + /// The aim of adding this state is to have a unique initial state. This /// artificial initial state have one transition to each real initial state, /// and this transition is labeled by the corresponding initial condition. /// (For more details, see the paper cited above) diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index b3dda288d..434d47a46 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -94,7 +94,7 @@ namespace spot && (!dest->is_accepting_state()) && (!dest_trans_empty)) transitions_to_livelock_states->push_front(*it_trans); - // optimization to have, after minimization, an unique + // optimization to have, after minimization, a unique // livelock state which has no successors if (dest->is_livelock_accepting_state() && (dest_trans_empty)) dest->set_accepting_state(false); diff --git a/spot/taalgos/tgba2ta.hh b/spot/taalgos/tgba2ta.hh index 397bae900..90112a42f 100644 --- a/spot/taalgos/tgba2ta.hh +++ b/spot/taalgos/tgba2ta.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2010, 2012-2015, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -58,7 +58,7 @@ namespace spot /// for TA (spot::ta_check::check) can also be used to check GTA. /// /// \param artificial_initial_state_mode When set, the algorithm will build - /// a TA automaton with an unique initial state. This + /// a TA automaton with a unique initial state. This /// artificial initial state have one transition to each real initial state, /// and this transition is labeled by the corresponding initial condition. /// (see spot::ta::get_artificial_initial_state()) diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 69f5da01d..dc220095b 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -449,7 +449,7 @@ namespace spot // calling graph::degrag_states() to finish with #1. We clear // the "dests vector" of the current automaton, recreate all // the new destination groups using a univ_dest_mapper to - // simplify an unify them, and extend newst with some new + // simplify and unify them, and extend newst with some new // entries that will point the those new universal destination // so that graph::defrag_states() does not have to deal with // universal destination in any way. diff --git a/spot/twaalgos/complement.hh b/spot/twaalgos/complement.hh index 1508919ba..94dbe6b47 100644 --- a/spot/twaalgos/complement.hh +++ b/spot/twaalgos/complement.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -35,7 +35,7 @@ namespace spot /// /// Functions like to_generalized_buchi() or remove_fin() are /// frequently called after dtwa_complement() to obtain an easier - /// acceptance condition (maybe at the cost of loosing determinism.) + /// acceptance condition (maybe at the cost of losing determinism.) SPOT_API twa_graph_ptr dtwa_complement(const const_twa_graph_ptr& aut); } diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index c15308403..1e5bc0108 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -182,7 +182,7 @@ namespace spot unsigned dest = e.dst; if ((int) dest < 0) { - // Iterate over all destinations of an universal edge. + // Iterate over all destinations of a universal edge. if (todo_.top().univ_pos == 0) todo_.top().univ_pos = ~dest + 1; const auto& v = gr.dests_vector(); diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 2cd2b0987..25ca7f833 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -81,12 +81,11 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do fail=false # Check this before stripping comments and strings. - $GREP -i 'accepting cond' $file && - diag 'accepting -> acceptance' - - # Check this before stripping comments and strings. - $GREP -i 'dictionnar[yi]' $file && - diag 'dictionnary -> dictionary' + $GREP -i 'accepting cond' $file && diag 'accepting -> acceptance' + $GREP -i 'dictionnar[yi]' $file && diag 'dictionnary -> dictionary' + # "an uninstalled" seems to be the exception so far, but we want + # "a unique", "a universal", etc. + $GREP -i 'an uni[^n]' $file && diag 'an uni... -> a uni...' $GREP -i 'version 2 of the License' $file && diag 'license text should refer to version 2' From 01ee49290f5a20c32e18536291c7205c4a42aa8b Mon Sep 17 00:00:00 2001 From: Thomas Medioni Date: Fri, 31 Mar 2017 13:40:05 +0200 Subject: [PATCH 10/20] bench: fix stutter bench compiler errors. * NEWS: mention this fix. * bench/stutter/stutter_bench.sh, bench/stutter/user.sh: Path to spot binaries would include an inexistant src directory. * bench/stutter/stutter_invariance_formulas.cc: Add override qualifier to satisfy -Wsuggest-override. --- NEWS | 3 +++ bench/stutter/stutter_bench.sh | 4 ++-- bench/stutter/stutter_invariance_formulas.cc | 4 ++-- bench/stutter/user.sh | 6 +++--- 4 files changed, 10 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index c2a08072e..9e2b5e7ee 100644 --- a/NEWS +++ b/NEWS @@ -15,6 +15,9 @@ New in spot 2.3.2.dev (not yet released) - spot::twa_graph::purge_unreachable_states() was misbehaving on alternating automata. + - In bench/stutter/ the .cc files were not compiling due to warnings being + caught as errors. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/bench/stutter/stutter_bench.sh b/bench/stutter/stutter_bench.sh index 635cebd4c..5c6c0c1ec 100755 --- a/bench/stutter/stutter_bench.sh +++ b/bench/stutter/stutter_bench.sh @@ -1,7 +1,7 @@ #!/bin/sh -RANDLTL=../../src/bin/randltl -LTLFILT=../../src/bin/ltlfilt +RANDLTL=../../bin/randltl +LTLFILT=../../bin/ltlfilt echo 'ltl-user-bench.csv:; ./user.sh' > run.mk diff --git a/bench/stutter/stutter_invariance_formulas.cc b/bench/stutter/stutter_invariance_formulas.cc index 826185d23..9d9385123 100644 --- a/bench/stutter/stutter_invariance_formulas.cc +++ b/bench/stutter/stutter_invariance_formulas.cc @@ -54,14 +54,14 @@ namespace int process_string(const std::string& input, - const char* filename, int linenum) + const char* filename, int linenum) override { formula = input; return job_processor::process_string(input, filename, linenum); } int - process_formula(spot::formula f, const char*, int) + process_formula(spot::formula f, const char*, int) override { spot::twa_graph_ptr a = trans.run(f); spot::twa_graph_ptr na = trans.run(spot::formula::Not(f)); diff --git a/bench/stutter/user.sh b/bench/stutter/user.sh index fae92303e..d52a72876 100755 --- a/bench/stutter/user.sh +++ b/bench/stutter/user.sh @@ -1,7 +1,7 @@ #!/bin/sh -RANDLTL=../../src/bin/randltl -LTLFILT=../../src/bin/ltlfilt -LTLDO=../../src/bin/ltldo +RANDLTL=../../bin/randltl +LTLFILT=../../bin/ltlfilt +LTLDO=../../bin/ltldo set -e -x From 1daffe12f0a5835b0646503e835d3dc1cfb8714a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 4 Apr 2017 13:53:16 +0200 Subject: [PATCH 11/20] remfin: fix a corner case for rabin_to_buchi_maybe when fin_alone sets where presents (i.e., not really Rabin condition), the rabin_to_buchi_maybe() could fail to notice DBA-typeness. * spot/twaalgos/remfin.cc: Don't set scc_ba_type to false when fin_alone is present. * tests/core/remfin.test: Add a test case. --- NEWS | 6 +++++ spot/twaalgos/remfin.cc | 13 ++++------- tests/core/remfin.test | 50 +++++++++++++++++++++++++++++++++++++++-- 3 files changed, 58 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index 9e2b5e7ee..4df7fcfaf 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,12 @@ New in spot 2.3.2.dev (not yet released) - In bench/stutter/ the .cc files were not compiling due to warnings being caught as errors. + - The code in charge of detecting DBA-type Rabin automata is + actually written to handle a slightly larger class of acceptance + conditions (e.g., Fin(0)|(Fin(1)&Inf(2))), however it failed to + correctly detect DBA-typeness in some of these non-Rabin + acceptance. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 69fc04486..5e5c3bb98 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -73,7 +73,7 @@ namespace spot // accepting, but which becomes non-accepting when extended with // more states. i -= f; - i |= (inf_alone & sets); + i |= inf_alone & sets; if (!i) { // Check whether the SCC is accepting. We do that by simply @@ -192,14 +192,9 @@ namespace spot ba_final_states[s] = true; scc_ba_type = true; } - // Conversely, if all fin_alone appear in the SCC, then it - // cannot be accepting. - else if (sets & fin_alone) - { - scc_ba_type = false; - } - // In the generale case (no fin_alone involved), we need - // a dedicated check. + // In the general case, we need a dedicated check. Note + // that the used fin_alone sets can be ignored, as they + // cannot contribute to Büchi-typeness, else { scc_ba_type = is_scc_ba_type(aut, si.states_of(scc), diff --git a/tests/core/remfin.test b/tests/core/remfin.test index 16d2fb978..6bd214bbf 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -1,7 +1,8 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). + +# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -236,6 +237,19 @@ State: 15 [t] 15 {4 15} [1] 16 {4} [!1] 22 {15} State: 16 [t] 16 {4 16} [t] 31 {14} [!1] 32 State: 32 [t] 32 {15} [1] 33 State: 33 [t] 33 {16} [!1] 36 State: 34 [t] 34 State: 35 [1] 34 {11} [!1] 35 {5} State: 36 [1] 34 {23} [!1] 36 {17} --END-- +HOA: v1 +States: 2 +Acceptance: 3 Fin(0) | (Fin(1)&Inf(2)) +Start: 0 +AP: 1 "a" +--BODY-- +State: 0 {0} +[0] 1 +[!0] 0 +State: 1 {2} +[0] 1 +[!0] 0 +--END-- EOF acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)' @@ -713,6 +727,22 @@ State: 36 [1] 34 [!1] 36 {0 1 2 3 4 5 6 7 8 9 10} --END-- +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[0] 1 +[!0] 0 +State: 1 {0} +[0] 1 +[!0] 0 +--END-- EOF cat >expected-tgba < output From 6806113a1453ead126bc190f100033634f10d504 Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Wed, 5 Apr 2017 11:00:55 +0200 Subject: [PATCH 12/20] Fix wrong URL for Debian packages. * debian/control: Fix URL. --- debian/control | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/debian/control b/debian/control index f412a72c9..4e85589a0 100644 --- a/debian/control +++ b/debian/control @@ -4,7 +4,7 @@ Priority: optional Maintainer: Alexandre Duret-Lutz Build-Depends: debhelper (>= 9), python3-all-dev, ipython3-notebook | python3-ipykernel, ipython3-notebook | python3-nbconvert, libltdl-dev Standards-Version: 3.9.6 -Homepage: http://spot.lrde.lip6.fr/ +Homepage: http://spot.lrde.epita.fr/ Package: spot Architecture: any From 276f40602ea53410e6968161444dbc1acaa0ec55 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 6 Apr 2017 14:30:40 +0200 Subject: [PATCH 13/20] bin: add shorthands for ltl2dpa ltl2da and ltl2ldba * bin/common_trans.cc: Here. * doc/org/ltlcross.org, doc/org/ltldo.org, NEWS: Adjust. --- NEWS | 5 +++++ bin/common_trans.cc | 3 +++ doc/org/ltlcross.org | 3 +++ doc/org/ltldo.org | 3 +++ 4 files changed, 14 insertions(+) diff --git a/NEWS b/NEWS index 4df7fcfaf..112e6f8aa 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 2.3.2.dev (not yet released) + Tools: + + - ltldo and ltlcross learned shorthands to talk to ltl2da, ltl2dpa, + and ltl2ldba (from Owl) without needing to specify %f>%O. + Bug fixes: - In "lenient" mode the parser would fail to recover from diff --git a/bin/common_trans.cc b/bin/common_trans.cc index e351ef3ce..73ebad376 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -43,6 +43,9 @@ static struct shorthands_t shorthands[] = { { "lbt", " <%L>%O" }, { "ltl2ba", " -f %s>%O" }, + { "ltl2da", " %f>%O" }, + { "ltl2dpa", " %f>%O" }, + { "ltl2ldba", " %f>%O" }, { "ltl2dstar", " --output-format=hoa %[MW]L %O"}, { "ltl2tgba", " -H %f>%O" }, { "ltl3ba", " -f %s>%O" }, diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 3afde30e9..64c98e0a5 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -182,6 +182,9 @@ the following words, then the string on the right is appended. lbt <%L>%O ltl2ba -f %s>%O + ltl2da %f>%O + ltl2dpa %f>%O + ltl2ldba %f>%O ltl2dstar --output-format=hoa %[MW]L %O ltl2tgba -H %f>%O ltl3ba -f %s>%O diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index bd932deeb..1c20622ab 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -309,6 +309,9 @@ the following words, then the string on the right is appended. lbt <%L>%O ltl2ba -f %s>%O + ltl2da %f>%O + ltl2dpa %f>%O + ltl2ldba %f>%O ltl2dstar --output-format=hoa %[MW]L %O ltl2tgba -H %f>%O ltl3ba -f %s>%O From 14addce640eff83107705ad001939072262e6fec Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Mar 2017 07:27:07 +0100 Subject: [PATCH 14/20] genltl: add --spec-patterns as an alias to --dac-patterns * bin/genltl.cc: Here. * NEWS: Mention it. --- NEWS | 2 ++ bin/genltl.cc | 1 + 2 files changed, 3 insertions(+) diff --git a/NEWS b/NEWS index 112e6f8aa..bd9a73354 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,8 @@ New in spot 2.3.2.dev (not yet released) - ltldo and ltlcross learned shorthands to talk to ltl2da, ltl2dpa, and ltl2ldba (from Owl) without needing to specify %f>%O. + - genltl learned --spec-patterns as an alias for --dac-patterns + Bug fixes: - In "lenient" mode the parser would fail to recover from diff --git a/bin/genltl.cc b/bin/genltl.cc index dc812d7be..fd9f3f091 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -264,6 +264,7 @@ static const argp_option options[] = { "dac-patterns", OPT_DAC_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, "Dwyer et al. [FMSP'98] Spec. Patterns for LTL " "(range should be included in 1..55)", 0 }, + OPT_ALIAS(spec-patterns), { "eh-patterns", OPT_EH_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, "Etessami and Holzmann [Concur'00] patterns " "(range should be included in 1..12)", 0 }, From 4b7a6238b4bf017b54fd471262e8ff9922b91165 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Mar 2017 07:57:38 +0100 Subject: [PATCH 15/20] genltl: add --hkrss-patterns Fixes #245. * bin/genltl.cc: Add the option. * bin/man/genltl.x: Add reference. * tests/core/ltl2tgba2.test: Use these patterns. * doc/org/genltl.org, NEWS: Document the options. --- NEWS | 4 +- bin/genltl.cc | 94 +++++++++++++ bin/man/genltl.x | 46 ++++--- doc/org/genltl.org | 271 ++++++++++++++++++++++++-------------- tests/core/ltl2tgba2.test | 117 +++++++++++++++- 5 files changed, 404 insertions(+), 128 deletions(-) diff --git a/NEWS b/NEWS index bd9a73354..79469778e 100644 --- a/NEWS +++ b/NEWS @@ -5,7 +5,9 @@ New in spot 2.3.2.dev (not yet released) - ltldo and ltlcross learned shorthands to talk to ltl2da, ltl2dpa, and ltl2ldba (from Owl) without needing to specify %f>%O. - - genltl learned --spec-patterns as an alias for --dac-patterns + - genltl learned --spec-patterns as an alias for --dac-patterns; it + also learned a new set of LTL formulas under --hkrss-patterns + (a.k.a. --liberouter-patterns). Bug fixes: diff --git a/bin/genltl.cc b/bin/genltl.cc index fd9f3f091..d29586f41 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -132,6 +132,16 @@ // month = nov, // publisher = {Springer} // } +// +// @techreport{holevek.04.tr, +// title = {Verification Results in {Liberouter} Project}, +// author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak +// and D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek}, +// month = {September}, +// year = 2004, +// number = 03, +// institution = {CESNET} +// } #include "common_sys.hh" @@ -179,6 +189,7 @@ enum { OPT_GH_Q, OPT_GH_R, OPT_GO_THETA, + OPT_HKRSS_PATTERNS, OPT_KR_N, OPT_KR_NLOGN, OPT_KV_PSI, @@ -217,6 +228,7 @@ const char* const class_name[LAST_CLASS - FIRST_CLASS] = "gh-q", "gh-r", "go-theta", + "hkrss-patterns", "kr-n", "kr-nlogn", "kv-psi", @@ -274,6 +286,10 @@ static const argp_option options[] = "(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))", 0 }, { "go-theta", OPT_GO_THETA, "RANGE", 0, "!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))", 0 }, + { "hkrss-patterns", OPT_HKRSS_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, + "Holeček et al. patterns from the Liberouter project " + "(range should be included in 1..55)", 0 }, + OPT_ALIAS(liberouter-patterns), { "kr-n", OPT_KR_N, "RANGE", 0, "linear formula with doubly exponential DBA", 0 }, { "kr-nlogn", OPT_KR_NLOGN, "RANGE", 0, @@ -408,6 +424,7 @@ parse_opt(int key, char* arg, struct argp_state*) enqueue_job(key, arg); break; case OPT_DAC_PATTERNS: + case OPT_HKRSS_PATTERNS: if (arg) enqueue_job(key, arg); else @@ -1027,6 +1044,80 @@ dac_pattern(int n) return spot::relabel(parse_formula(formulas[n - 1]), Pnn); } +static formula +hkrss_pattern(int n) +{ + static const char* formulas[] = { + "G(Fp0 & F!p0)", + "GFp0 & GF!p0", + "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0))", + "GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3))", + "G!p0", + "G((p0 -> F!p0) & (!p0 -> Fp0))", + "G(p0 -> F(p0 & p1))", + "G(p0 -> F((!p0 & p1 & p2 & p3) -> Fp4))", + "G(p0 -> F!p1)", + "G(p0 -> Fp1)", + "G(p0 -> F(p1 -> Fp2))", + "G(p0 -> F((p1 & p2) -> Fp3))", + "G((p0 -> Fp1) & (p2 -> Fp3) & (p4 -> Fp5) & (p6 -> Fp7))", + "G(!p0 & !p1)", + "G!(p0 & p1)", + "G(p0 -> p1)", + "G((p0 -> !p1) & (p1 -> !p0))", + "G(!p0 -> (p1 <-> !p2))", + "G((!p0 & (p1 | p2 | p3)) -> p4)", + "G((p0 & p1) -> (p2 | !(p3 & p4)))", + "G((!p0 & p1 & !p2 & !p3 & !p4) -> F(!p5 & !p6 & !p7 & !p8))", + "G((p0 & p1 & !p2 & !p3 & !p4) -> F(p5 & !p6 & !p7 & !p8))", + "G(!p0 -> !(p1 & p2 & p3 & p4 & p5))", + "G(!p0 -> ((p1 & p2 & p3 & p4) -> !p5))", + "G((p0 & p1) -> (p2 | p3 | !(p4 & p5)))", + "G((!p0 & (p1 | p2 | p3 | p4)) -> (!p5 <-> p6))", + "G((p0 & p1) -> (p2 | p3 | p4 | !(p5 & p6)))", + "G((p0 & p1) -> (p2 | p3 | p4 | p5 | !(p6 & p7)))", + "G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3)))", + "G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3))))))", + "G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3)))))", + "G(p0 -> (p1 U (!p1 U (!p2 | p3))))", + "G(p0 -> (p1 U (!p1 U (p2 | p3))))", + "G((!p0 & p1) -> Xp2)", + "G(p0 -> X(p0 | p1))", + ("G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) -> " + "(X!p4 & X(!(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | " + "!(p3 <-> Xp3)) U p4)))"), + "G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3))", + "G(p0 -> X(!p0 U p1))", + "G((!p0 & Xp0) -> X((p0 U p1) | Gp0))", + "G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1))))", + ("G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 & (p0 U (p0 & !p1 & " + "X(p0 & p1)))))))"), + ("G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 " + "& X(!p0 & p1)))))))"), + ("G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & " + "X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1))))))))))"), + "G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1)))", + ("G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | " + "X(!p0 | X(!p0 | X!p0)))))))))))"), + "G((Xp0 -> p0) -> (p1 <-> Xp1))", + "G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1)))", + ("!p0 U G!((p1 & p2) | (p3 & p4) | (p2 & p3) | (p2 & p4) | (p1 & p4) | " + "(p1 & p3))"), + "!p0 U p1", + "(p0 U p1) | Gp0", + "p0 & XG!p0", + "XG(p0 -> (G!p1 | (!Xp1 U p2)))", + "XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))", + "XG((p0 & p1) -> ((p1 U p2) | Gp1))", + "Xp0 & G((!p0 & Xp0) -> XXp0)", + }; + + constexpr unsigned max = (sizeof formulas)/(sizeof *formulas); + if (n < 1 || (unsigned) n > max) + bad_number("--hkrss-patterns", n, max); + return spot::relabel(parse_formula(formulas[n - 1]), Pnn); +} + static formula eh_pattern(int n) { @@ -1376,6 +1467,9 @@ output_pattern(int pattern, int n) case OPT_GO_THETA: f = fair_response("p", "q", "r", n); break; + case OPT_HKRSS_PATTERNS: + f = hkrss_pattern(n); + break; case OPT_KR_N: f = kr2_exp(n, "a", "b", "c", "d"); break; diff --git a/bin/man/genltl.x b/bin/man/genltl.x index 6272f4ac2..b9f224a71 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -12,22 +12,10 @@ Proceedings of ATVA'13. LNCS 8172. .PP Prefixes used in pattern names refer to the following papers: .TP -gh -J. Geldenhuys and H. Hansen: Larger automata and less -work for LTL model checking. Proceedings of Spin'06. LNCS 3925. -.TP ccj J. Cichoń, A. Czubak, and A. Jasiński: Minimal Büchi Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS'09. .TP -go -P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. -Proceedings of CAV'01. LNCS 2102. -.TP -rv -K. Rozier and M. Vardi: LTL Satisfiability Checking. -Proceedings of Spin'07. LNCS 4595. -.TP dac M. B. Dwyer and G. S. Avrunin and J. C. Corbett: Property Specification Patterns for Finite-state Verification. @@ -37,6 +25,31 @@ eh K. Etessami and G. J. Holzmann: Optimizing Büchi Automata. Proceedings of Concur'00. LNCS 1877. .TP +gh +J. Geldenhuys and H. Hansen: Larger automata and less +work for LTL model checking. Proceedings of Spin'06. LNCS 3925. +.TP +hkrss +J. Holeček, T. Kratochvila, V. Řehák, D. Šafránek, and P. Šimeček: +Verification Results in Liberouter Project. Tech. Report 03, CESNET, 2004. +.TP +go +P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. +Proceedings of CAV'01. LNCS 2102. +.TP +kr +O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic +Automata. +Proceedings of MoChArt'10. LNAI 6572. +.TP +kv +O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. +ACM Transactions on Computational Logic, 6(2):273-294, 2005. +.TP +rv +K. Rozier and M. Vardi: LTL Satisfiability Checking. +Proceedings of Spin'07. LNCS 4595. +.TP sb F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae. Proceedings of CAV'00. LNCS 1855. @@ -44,15 +57,6 @@ Proceedings of CAV'00. LNCS 1855. tv D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC. Proceedings of RV'10. LNCS 6418. -.TP -kr -O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic -Automata. -Proceedings of MoChArt'10. LNAI 6572. -.TP -rv -O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. -ACM Transactions on Computational Logic, 6(2):273-294, 2005. [SEE ALSO] .BR randltl (1) diff --git a/doc/org/genltl.org b/doc/org/genltl.org index 3751df185..963b0156a 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -27,14 +27,22 @@ genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' --ccj-beta=RANGE F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q)))) --ccj-beta-prime=RANGE F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q))) - --dac-patterns[=RANGE] Dwyer et al. [FMSP'98] Spec. Patterns for LTL - (range should be included in 1..45) + --dac-patterns[=RANGE], --spec-patterns[=RANGE] + Dwyer et al. [FMSP'98] Spec. Patterns for LTL + (range should be included in 1..55) --eh-patterns[=RANGE] Etessami and Holzmann [Concur'00] patterns (range should be included in 1..12) --gh-q=RANGE (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1})) --gh-r=RANGE (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1})) --go-theta=RANGE !((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r))) + --hkrss-patterns[=RANGE], --liberouter-patterns[=RANGE] + Holeček et al. patterns from the Liberouter + project (range should be included in 1..55) + --kr-n=RANGE linear formula with doubly exponential DBA + --kr-nlogn=RANGE quasilinear formula with doubly exponential DBA + --kv-psi=RANGE, --kr-n2=RANGE + quadratic formula with doubly exponential DBA --or-fg=RANGE, --ccj-xi=RANGE FG(p1)|FG(p2)|...|FG(pn) --or-g=RANGE, --gh-s=RANGE G(p1)|G(p2)|...|G(pn) @@ -49,6 +57,11 @@ genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d' --rv-counter-linear=RANGE n-bit counter (linear size) --sb-patterns[=RANGE] Somenzi and Bloem [CAV'00] patterns (range should be included in 1..27) + --tv-f1=RANGE G(p -> (q | Xq | ... | XX...Xq) + --tv-f2=RANGE G(p -> (q | X(q | X(... | Xq))) + --tv-g1=RANGE G(p -> (q & Xq & ... & XX...Xq) + --tv-g2=RANGE G(p -> (q & X(q & X(... & Xq))) + --tv-uu=RANGE G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...)))))) --u-left=RANGE, --gh-u=RANGE (((p1 U p2) U p3) ... U pn) --u-right=RANGE, --gh-u2=RANGE, --go-phi=RANGE @@ -120,112 +133,168 @@ This is because most tools using =lbt='s syntax require atomic propositions to have the form =pNN=. -Three options provide lists of unrelated LTL formulas, taken from the +Four options provide lists of unrelated LTL formulas, taken from the literature (see the [[./man/genltl.1.html][=genltl=]](1) man page for references): -=--dac-patterns=, =--eh-patterns=, and =--sb-patterns=. With these -options, the range is used to select a subset of the list of formulas. -Without range, all formulas are used. Here is the complete list: +=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, and +=--sb-patterns=. With these options, the range is used to select a +subset of the list of formulas. Without range, all formulas are used. +Here is the complete list: #+BEGIN_SRC sh :results verbatim :exports both - genltl --dac --eh --sb --format=%F,%L,%f + genltl --dac --eh --hkrss --sb --format=%F:%L,%f #+END_SRC #+RESULTS: #+begin_example -dac-patterns,1,G!p0 -dac-patterns,2,Fp0 -> (!p1 U p0) -dac-patterns,3,G(p0 -> G!p1) -dac-patterns,4,G((p0 & !p1 & Fp1) -> (!p2 U p1)) -dac-patterns,5,G((p0 & !p1) -> (!p2 W p1)) -dac-patterns,6,Fp0 -dac-patterns,7,!p0 W (!p0 & p1) -dac-patterns,8,G!p0 | F(p0 & Fp1) -dac-patterns,9,G((p0 & !p1) -> (!p1 W (!p1 & p2))) -dac-patterns,10,G((p0 & !p1) -> (!p1 U (!p1 & p2))) -dac-patterns,11,!p0 W (p0 W (!p0 W (p0 W G!p0))) -dac-patterns,12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0))))))))) -dac-patterns,13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1)))))) -dac-patterns,14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1)))))))))) -dac-patterns,15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1))))))))) -dac-patterns,16,Gp0 -dac-patterns,17,Fp0 -> (p1 U p0) -dac-patterns,18,G(p0 -> Gp1) -dac-patterns,19,G((p0 & !p1 & Fp1) -> (p2 U p1)) -dac-patterns,20,G((p0 & !p1) -> (p2 W p1)) -dac-patterns,21,!p0 W p1 -dac-patterns,22,Fp0 -> (!p1 U (p0 | p2)) -dac-patterns,23,G!p0 | F(p0 & (!p1 W p2)) -dac-patterns,24,G((p0 & !p1 & Fp1) -> (!p2 U (p1 | p3))) -dac-patterns,25,G((p0 & !p1) -> (!p2 W (p1 | p3))) -dac-patterns,26,G(p0 -> Fp1) -dac-patterns,27,Fp0 -> ((p1 -> (!p0 U (!p0 & p2))) U p0) -dac-patterns,28,G(p0 -> G(p1 -> Fp2)) -dac-patterns,29,G((p0 & !p1 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3))) U p1)) -dac-patterns,30,G((p0 & !p1) -> ((p2 -> (!p1 U (!p1 & p3))) W p1)) -dac-patterns,31,Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2))) -dac-patterns,32,Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3)))) -dac-patterns,33,G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 & X(!p1 U p3))))) -dac-patterns,34,G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4))))) -dac-patterns,35,G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1 U p4)))))) -dac-patterns,36,F(p0 & XFp1) -> (!p0 U p2) -dac-patterns,37,Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p0 | p3)) -dac-patterns,38,G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3)))) -dac-patterns,39,G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4))) -dac-patterns,40,G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4)) | G!(p2 & XFp3))) -dac-patterns,41,G((p0 & XFp1) -> XF(p1 & Fp2)) -dac-patterns,42,Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & Fp3))) U p0) -dac-patterns,43,G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3)))) -dac-patterns,44,G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 U (p3 & Fp4))) U p1)) -dac-patterns,45,G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4))) U (p2 | G((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4)))))) -dac-patterns,46,G(p0 -> F(p1 & XFp2)) -dac-patterns,47,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3)))) U p0) -dac-patterns,48,G(p0 -> G(p1 -> (p2 & XFp3))) -dac-patterns,49,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!p1 U p4)))) U p1)) -dac-patterns,50,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4))))) -dac-patterns,51,G(p0 -> F(p1 & !p2 & X(!p2 U p3))) -dac-patterns,52,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0 & !p3) U p4)))) U p0) -dac-patterns,53,G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4)))) -dac-patterns,54,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4 & X((!p1 & !p4) U p5)))) U p1)) -dac-patterns,55,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5)))))) -eh-patterns,1,p0 U (p1 & Gp2) -eh-patterns,2,p0 U (p1 & X(p2 U p3)) -eh-patterns,3,p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))) -eh-patterns,4,F(p0 & XGp1) -eh-patterns,5,F(p0 & X(p1 & XFp2)) -eh-patterns,6,F(p0 & X(p1 U p2)) -eh-patterns,7,FGp0 | GFp1 -eh-patterns,8,G(p0 -> (p1 U p2)) -eh-patterns,9,G(p0 & XF(p1 & XF(p2 & XFp3))) -eh-patterns,10,GFp0 & GFp1 & GFp2 & GFp3 & GFp4 -eh-patterns,11,(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1)) -eh-patterns,12,G(p0 -> (p1 U (Gp2 | Gp3))) -sb-patterns,1,p0 U p1 -sb-patterns,2,p0 U (p1 U p2) -sb-patterns,3,!(p0 U (p1 U p2)) -sb-patterns,4,GFp0 -> GFp1 -sb-patterns,5,Fp0 U Gp1 -sb-patterns,6,Gp0 U p1 -sb-patterns,7,!(Fp0 <-> Fp1) -sb-patterns,8,!(GFp0 -> GFp1) -sb-patterns,9,!(GFp0 <-> GFp1) -sb-patterns,10,p0 R (p0 | p1) -sb-patterns,11,(Xp0 U Xp1) | !X(p0 U p1) -sb-patterns,12,(Xp0 U p1) | !X(p0 U (p0 & p1)) -sb-patterns,13,G(p0 -> Fp1) & ((Xp0 U p1) | !X(p0 U (p0 & p1))) -sb-patterns,14,G(p0 -> Fp1) & ((Xp0 U Xp1) | !X(p0 U p1)) -sb-patterns,15,G(p0 -> Fp1) -sb-patterns,16,!G(p0 -> X(p1 R p2)) -sb-patterns,17,!(FGp0 | FGp1) -sb-patterns,18,G(Fp0 & Fp1) -sb-patterns,19,Fp0 & F!p0 -sb-patterns,20,(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0)) -sb-patterns,21,Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0 -sb-patterns,22,Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1)) -sb-patterns,23,!(Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0) -sb-patterns,24,!(Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1))) -sb-patterns,25,G(p0 | XGp1) & G(p2 | XG!p1) -sb-patterns,26,G(p0 | (Xp1 & X!p1)) -sb-patterns,27,p0 | (p1 U p0) +dac-patterns:1,G!p0 +dac-patterns:2,Fp0 -> (!p1 U p0) +dac-patterns:3,G(p0 -> G!p1) +dac-patterns:4,G((p0 & !p1 & Fp1) -> (!p2 U p1)) +dac-patterns:5,G((p0 & !p1) -> (!p2 W p1)) +dac-patterns:6,Fp0 +dac-patterns:7,!p0 W (!p0 & p1) +dac-patterns:8,G!p0 | F(p0 & Fp1) +dac-patterns:9,G((p0 & !p1) -> (!p1 W (!p1 & p2))) +dac-patterns:10,G((p0 & !p1) -> (!p1 U (!p1 & p2))) +dac-patterns:11,!p0 W (p0 W (!p0 W (p0 W G!p0))) +dac-patterns:12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0))))))))) +dac-patterns:13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1)))))) +dac-patterns:14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1)))))))))) +dac-patterns:15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1))))))))) +dac-patterns:16,Gp0 +dac-patterns:17,Fp0 -> (p1 U p0) +dac-patterns:18,G(p0 -> Gp1) +dac-patterns:19,G((p0 & !p1 & Fp1) -> (p2 U p1)) +dac-patterns:20,G((p0 & !p1) -> (p2 W p1)) +dac-patterns:21,!p0 W p1 +dac-patterns:22,Fp0 -> (!p1 U (p0 | p2)) +dac-patterns:23,G!p0 | F(p0 & (!p1 W p2)) +dac-patterns:24,G((p0 & !p1 & Fp1) -> (!p2 U (p1 | p3))) +dac-patterns:25,G((p0 & !p1) -> (!p2 W (p1 | p3))) +dac-patterns:26,G(p0 -> Fp1) +dac-patterns:27,Fp0 -> ((p1 -> (!p0 U (!p0 & p2))) U p0) +dac-patterns:28,G(p0 -> G(p1 -> Fp2)) +dac-patterns:29,G((p0 & !p1 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3))) U p1)) +dac-patterns:30,G((p0 & !p1) -> ((p2 -> (!p1 U (!p1 & p3))) W p1)) +dac-patterns:31,Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2))) +dac-patterns:32,Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3)))) +dac-patterns:33,G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 & X(!p1 U p3))))) +dac-patterns:34,G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4))))) +dac-patterns:35,G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1 U p4)))))) +dac-patterns:36,F(p0 & XFp1) -> (!p0 U p2) +dac-patterns:37,Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p0 | p3)) +dac-patterns:38,G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3)))) +dac-patterns:39,G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4))) +dac-patterns:40,G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4)) | G!(p2 & XFp3))) +dac-patterns:41,G((p0 & XFp1) -> XF(p1 & Fp2)) +dac-patterns:42,Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & Fp3))) U p0) +dac-patterns:43,G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3)))) +dac-patterns:44,G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 U (p3 & Fp4))) U p1)) +dac-patterns:45,G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4))) U (p2 | G((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4)))))) +dac-patterns:46,G(p0 -> F(p1 & XFp2)) +dac-patterns:47,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3)))) U p0) +dac-patterns:48,G(p0 -> G(p1 -> (p2 & XFp3))) +dac-patterns:49,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!p1 U p4)))) U p1)) +dac-patterns:50,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4))))) +dac-patterns:51,G(p0 -> F(p1 & !p2 & X(!p2 U p3))) +dac-patterns:52,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0 & !p3) U p4)))) U p0) +dac-patterns:53,G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4)))) +dac-patterns:54,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4 & X((!p1 & !p4) U p5)))) U p1)) +dac-patterns:55,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5)))))) +eh-patterns:1,p0 U (p1 & Gp2) +eh-patterns:2,p0 U (p1 & X(p2 U p3)) +eh-patterns:3,p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6))))) +eh-patterns:4,F(p0 & XGp1) +eh-patterns:5,F(p0 & X(p1 & XFp2)) +eh-patterns:6,F(p0 & X(p1 U p2)) +eh-patterns:7,FGp0 | GFp1 +eh-patterns:8,G(p0 -> (p1 U p2)) +eh-patterns:9,G(p0 & XF(p1 & XF(p2 & XFp3))) +eh-patterns:10,GFp0 & GFp1 & GFp2 & GFp3 & GFp4 +eh-patterns:11,(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1)) +eh-patterns:12,G(p0 -> (p1 U (Gp2 | Gp3))) +hkrss-patterns:1,G(Fp0 & F!p0) +hkrss-patterns:2,GFp0 & GF!p0 +hkrss-patterns:3,GF(!(p1 <-> Xp1) | !(p0 <-> Xp0)) +hkrss-patterns:4,GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) +hkrss-patterns:5,G!p0 +hkrss-patterns:6,G((p0 -> F!p0) & (!p0 -> Fp0)) +hkrss-patterns:7,G(p0 -> F(p0 & p1)) +hkrss-patterns:8,G(p0 -> F((!p0 & p1 & p2 & p3) -> Fp4)) +hkrss-patterns:9,G(p0 -> F!p1) +hkrss-patterns:10,G(p0 -> Fp1) +hkrss-patterns:11,G(p0 -> F(p1 -> Fp2)) +hkrss-patterns:12,G(p0 -> F((p1 & p2) -> Fp3)) +hkrss-patterns:13,G((p0 -> Fp1) & (p2 -> Fp3) & (p4 -> Fp5) & (p6 -> Fp7)) +hkrss-patterns:14,G(!p0 & !p1) +hkrss-patterns:15,G!(p0 & p1) +hkrss-patterns:16,G(p0 -> p1) +hkrss-patterns:17,G((p0 -> !p1) & (p1 -> !p0)) +hkrss-patterns:18,G(!p0 -> (p1 <-> !p2)) +hkrss-patterns:19,G((!p0 & (p1 | p2 | p3)) -> p4) +hkrss-patterns:20,G((p0 & p1) -> (p2 | !(p3 & p4))) +hkrss-patterns:21,G((!p0 & p1 & !p2 & !p3 & !p4) -> F(!p5 & !p6 & !p7 & !p8)) +hkrss-patterns:22,G((p0 & p1 & !p2 & !p3 & !p4) -> F(p5 & !p6 & !p7 & !p8)) +hkrss-patterns:23,G(!p0 -> !(p1 & p2 & p3 & p4 & p5)) +hkrss-patterns:24,G(!p0 -> ((p1 & p2 & p3 & p4) -> !p5)) +hkrss-patterns:25,G((p0 & p1) -> (p2 | p3 | !(p4 & p5))) +hkrss-patterns:26,G((!p0 & (p1 | p2 | p3 | p4)) -> (!p5 <-> p6)) +hkrss-patterns:27,G((p0 & p1) -> (p2 | p3 | p4 | !(p5 & p6))) +hkrss-patterns:28,G((p0 & p1) -> (p2 | p3 | p4 | p5 | !(p6 & p7))) +hkrss-patterns:29,G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3))) +hkrss-patterns:30,G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3)))))) +hkrss-patterns:31,G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3))))) +hkrss-patterns:32,G(p0 -> (p1 U (!p1 U (!p2 | p3)))) +hkrss-patterns:33,G(p0 -> (p1 U (!p1 U (p2 | p3)))) +hkrss-patterns:34,G((!p0 & p1) -> Xp2) +hkrss-patterns:35,G(p0 -> X(p0 | p1)) +hkrss-patterns:36,G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) -> (X!p4 & X(!(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) U p4))) +hkrss-patterns:37,G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3)) +hkrss-patterns:38,G(p0 -> X(!p0 U p1)) +hkrss-patterns:39,G((!p0 & Xp0) -> X((p0 U p1) | Gp0)) +hkrss-patterns:40,G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1)))) +hkrss-patterns:41,G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 & (p0 U (p0 & !p1 & X(p0 & p1))))))) +hkrss-patterns:42,G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1))))))) +hkrss-patterns:43,G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1)))))))))) +hkrss-patterns:44,G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1))) +hkrss-patterns:45,G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X!p0))))))))))) +hkrss-patterns:46,G((Xp0 -> p0) -> (p1 <-> Xp1)) +hkrss-patterns:47,G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1))) +hkrss-patterns:48,!p0 U G!((p1 & p2) | (p3 & p4) | (p2 & p3) | (p2 & p4) | (p1 & p4) | (p1 & p3)) +hkrss-patterns:49,!p0 U p1 +hkrss-patterns:50,(p0 U p1) | Gp0 +hkrss-patterns:51,p0 & XG!p0 +hkrss-patterns:52,XG(p0 -> (G!p1 | (!Xp1 U p2))) +hkrss-patterns:53,XG((p0 & !p1) -> (G!p1 | (!p1 U p2))) +hkrss-patterns:54,XG((p0 & p1) -> ((p1 U p2) | Gp1)) +hkrss-patterns:55,Xp0 & G((!p0 & Xp0) -> XXp0) +sb-patterns:1,p0 U p1 +sb-patterns:2,p0 U (p1 U p2) +sb-patterns:3,!(p0 U (p1 U p2)) +sb-patterns:4,GFp0 -> GFp1 +sb-patterns:5,Fp0 U Gp1 +sb-patterns:6,Gp0 U p1 +sb-patterns:7,!(Fp0 <-> Fp1) +sb-patterns:8,!(GFp0 -> GFp1) +sb-patterns:9,!(GFp0 <-> GFp1) +sb-patterns:10,p0 R (p0 | p1) +sb-patterns:11,(Xp0 U Xp1) | !X(p0 U p1) +sb-patterns:12,(Xp0 U p1) | !X(p0 U (p0 & p1)) +sb-patterns:13,G(p0 -> Fp1) & ((Xp0 U p1) | !X(p0 U (p0 & p1))) +sb-patterns:14,G(p0 -> Fp1) & ((Xp0 U Xp1) | !X(p0 U p1)) +sb-patterns:15,G(p0 -> Fp1) +sb-patterns:16,!G(p0 -> X(p1 R p2)) +sb-patterns:17,!(FGp0 | FGp1) +sb-patterns:18,G(Fp0 & Fp1) +sb-patterns:19,Fp0 & F!p0 +sb-patterns:20,(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0)) +sb-patterns:21,Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0 +sb-patterns:22,Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1)) +sb-patterns:23,!(Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0) +sb-patterns:24,!(Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1))) +sb-patterns:25,G(p0 | XGp1) & G(p2 | XG!p1) +sb-patterns:26,G(p0 | (Xp1 & X!p1)) +sb-patterns:27,p0 | (p1 U p0) #+end_example Note that ~--sb-patterns=2 --sb-patterns=4 --sb-patterns=21..22~ also diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index d823080c7..c5d523401 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 -# Laboratoire de Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2009-2017 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. @@ -24,11 +24,12 @@ . ./defs # If the size of automata produced by ltl2tgba on the formulas we -# commonly use as benchmark, we want to notice it. +# commonly use as benchmark change, we want to notice it. set -e -genltl --dac-patterns --eh-patterns --sb-patterns --format=%F,%L,%f >pos -(cat pos; ltlfilt --negate pos/3 --format='!%<,%f') | ltlfilt -u -F-/3 >formulas +genltl --dac --eh --sb --hkrss --format=%F,%L,%f >pos +(cat pos; ltlfilt --negate pos/3 --format='!%<,%f') | + ltlfilt -u -F-/3 >formulas ltl2tgba -Fformulas/3 --stats='%<,%f, %s,%t' | ltl2tgba -D -F-/3 --stats='%<,%f,%>, %s,%t' | @@ -129,6 +130,59 @@ sb-patterns,24, 4,16, 4,16, 4,16, 4,16 sb-patterns,25, 3,10, 3,10, 3,10, 3,10 sb-patterns,26, 1,1, 1,1, 1,1, 1,1 sb-patterns,27, 2,7, 2,7, 2,7, 2,7 +hkrss-patterns,1, 1,2, 1,2, 3,6, 3,6 +hkrss-patterns,2, 1,2, 1,2, 3,6, 3,6 +hkrss-patterns,3, 5,36, 5,36, 5,36, 5,36 +hkrss-patterns,4, 9,400, 9,400, 9,400, 9,400 +hkrss-patterns,6, 1,2, 1,2, 3,6, 3,6 +hkrss-patterns,7, 2,8, 2,8, 2,8, 2,8 +hkrss-patterns,8, 1,1, 1,1, 1,1, 1,1 +hkrss-patterns,9, 2,8, 2,8, 2,8, 2,8 +hkrss-patterns,11, 2,16, 2,16, 2,16, 2,16 +hkrss-patterns,12, 2,32, 2,32, 2,32, 2,32 +hkrss-patterns,13, 16,4096, 16,4096, 40,10240, 40,10240 +hkrss-patterns,14, 1,1, 1,1, 1,1, 1,1 +hkrss-patterns,15, 1,3, 1,3, 1,3, 1,3 +hkrss-patterns,16, 1,3, 1,3, 1,3, 1,3 +hkrss-patterns,17, 1,3, 1,3, 1,3, 1,3 +hkrss-patterns,18, 1,6, 1,6, 1,6, 1,6 +hkrss-patterns,19, 1,25, 1,25, 1,25, 1,25 +hkrss-patterns,20, 1,31, 1,31, 1,31, 1,31 +hkrss-patterns,21, 2,1024, 2,1024, 2,1024, 2,1024 +hkrss-patterns,22, 2,1024, 2,1024, 2,1024, 2,1024 +hkrss-patterns,23, 1,63, 1,63, 1,63, 1,63 +hkrss-patterns,24, 1,63, 1,63, 1,63, 1,63 +hkrss-patterns,25, 1,63, 1,63, 1,63, 1,63 +hkrss-patterns,26, 1,98, 1,98, 1,98, 1,98 +hkrss-patterns,27, 1,127, 1,127, 1,127, 1,127 +hkrss-patterns,28, 1,255, 1,255, 1,255, 1,255 +hkrss-patterns,29, 3,44, 3,44, 3,44, 3,44 +hkrss-patterns,30, 5,78, 5,78, 5,78, 5,78 +hkrss-patterns,31, 1,1, 1,1, 1,1, 1,1 +hkrss-patterns,32, 3,46, 3,46, 3,46, 3,46 +hkrss-patterns,33, 3,46, 3,46, 3,46, 3,46 +hkrss-patterns,34, 2,12, 2,12, 2,12, 2,12 +hkrss-patterns,35, 2,7, 2,7, 2,7, 2,7 +hkrss-patterns,36, 34,192, 34,192, 35,208, 35,208 +hkrss-patterns,37, 2,30, 2,30, 2,30, 2,30 +hkrss-patterns,38, 2,7, 2,7, 3,10, 3,10 +hkrss-patterns,39, 3,11, 3,11, 3,11, 3,11 +hkrss-patterns,40, 4,13, 4,13, 4,13, 4,13 +hkrss-patterns,41, 6,17, 6,17, 6,17, 6,17 +hkrss-patterns,42, 6,17, 6,17, 6,17, 6,17 +hkrss-patterns,43, 8,21, 8,21, 8,21, 8,21 +hkrss-patterns,44, 6,22, 6,22, 6,22, 6,22 +hkrss-patterns,45, 12,23, 12,23, 12,23, 12,23 +hkrss-patterns,46, 4,14, 5,14, 4,14, 5,14 +hkrss-patterns,47, 4,14, 5,14, 4,14, 5,14 +hkrss-patterns,48, 2,36, 2,36, 2,36, 2,36 +hkrss-patterns,49, 2,7, 2,7, 2,7, 2,7 +hkrss-patterns,50, 2,7, 2,7, 2,7, 2,7 +hkrss-patterns,51, 2,2, 2,2, 2,2, 2,2 +hkrss-patterns,52, 4,25, 4,25, 5,29, 5,29 +hkrss-patterns,53, 3,22, 3,22, 3,22, 3,22 +hkrss-patterns,54, 3,22, 3,22, 3,22, 3,22 +hkrss-patterns,55, 5,8, 5,8, 5,8, 5,8 !dac-patterns,1, 2,4, 2,4, 2,4, 2,4 !dac-patterns,2, 3,10, 3,10, 3,10, 3,10 !dac-patterns,3, 3,12, 3,12, 3,12, 3,12 @@ -214,6 +268,59 @@ sb-patterns,27, 2,7, 2,7, 2,7, 2,7 !sb-patterns,25, 4,32, 4,32, 4,32, 4,32 !sb-patterns,26, 2,4, 2,4, 2,4, 2,4 !sb-patterns,27, 2,6, 2,6, 2,6, 2,6 +!hkrss-patterns,1, 3,6, 3,6, 3,6, 3,6 +!hkrss-patterns,2, 3,6, 3,6, 3,6, 3,6 +!hkrss-patterns,3, 5,12, 5,12, 5,12, 5,12 +!hkrss-patterns,4, 17,48, 17,48, 17,48, 17,48 +!hkrss-patterns,6, 3,6, 3,6, 3,6, 3,6 +!hkrss-patterns,7, 2,8, 2,8, 2,8, 2,8 +!hkrss-patterns,8, 1,0, 1,0, 1,0, 1,0 +!hkrss-patterns,9, 2,7, 2,7, 2,7, 2,7 +!hkrss-patterns,11, 2,11, 2,11, 2,11, 2,11 +!hkrss-patterns,12, 2,19, 2,19, 2,19, 2,19 +!hkrss-patterns,13, 5,1024, 5,1024, 5,1024, 5,1024 +!hkrss-patterns,14, 2,8, 2,8, 2,8, 2,8 +!hkrss-patterns,15, 2,8, 2,8, 2,8, 2,8 +!hkrss-patterns,16, 2,8, 2,8, 2,8, 2,8 +!hkrss-patterns,17, 2,8, 2,8, 2,8, 2,8 +!hkrss-patterns,18, 2,16, 2,16, 2,16, 2,16 +!hkrss-patterns,19, 2,64, 2,64, 2,64, 2,64 +!hkrss-patterns,20, 2,64, 2,64, 2,64, 2,64 +!hkrss-patterns,21, 2,1007, 2,1007, 2,1007, 2,1007 +!hkrss-patterns,22, 2,1007, 2,1007, 2,1007, 2,1007 +!hkrss-patterns,23, 2,128, 2,128, 2,128, 2,128 +!hkrss-patterns,24, 2,128, 2,128, 2,128, 2,128 +!hkrss-patterns,25, 2,128, 2,128, 2,128, 2,128 +!hkrss-patterns,26, 2,256, 2,256, 2,256, 2,256 +!hkrss-patterns,27, 2,256, 2,256, 2,256, 2,256 +!hkrss-patterns,28, 2,512, 2,512, 2,512, 2,512 +!hkrss-patterns,29, 4,64, 4,64, 4,64, 4,64 +!hkrss-patterns,30, 6,48, 6,48, 6,48, 6,48 +!hkrss-patterns,31, 1,0, 1,0, 1,0, 1,0 +!hkrss-patterns,32, 4,42, 4,42, 4,42, 4,42 +!hkrss-patterns,33, 4,42, 4,42, 4,42, 4,42 +!hkrss-patterns,34, 3,24, 3,24, 3,24, 3,24 +!hkrss-patterns,35, 3,12, 3,12, 3,12, 3,12 +!hkrss-patterns,36, 19,784, 19,784, 19,784, 19,784 +!hkrss-patterns,37, 3,48, 3,48, 3,48, 3,48 +!hkrss-patterns,38, 3,12, 3,12, 3,12, 3,12 +!hkrss-patterns,39, 4,16, 4,16, 4,16, 4,16 +!hkrss-patterns,40, 5,19, 5,19, 5,19, 5,19 +!hkrss-patterns,41, 7,27, 7,27, 7,27, 7,27 +!hkrss-patterns,42, 7,27, 7,27, 7,27, 7,27 +!hkrss-patterns,43, 9,35, 9,35, 9,35, 9,35 +!hkrss-patterns,44, 7,24, 7,24, 7,24, 7,24 +!hkrss-patterns,45, 13,26, 13,26, 13,26, 13,26 +!hkrss-patterns,46, 6,24, 6,24, 6,24, 6,24 +!hkrss-patterns,47, 6,24, 6,24, 6,24, 6,24 +!hkrss-patterns,48, 3,96, 3,96, 4,128, 4,128 +!hkrss-patterns,49, 2,6, 2,6, 2,6, 2,6 +!hkrss-patterns,50, 2,6, 2,6, 2,6, 2,6 +!hkrss-patterns,51, 3,6, 3,6, 3,6, 3,6 +!hkrss-patterns,52, 5,37, 5,37, 5,37, 5,37 +!hkrss-patterns,53, 4,32, 4,32, 4,32, 4,32 +!hkrss-patterns,54, 4,32, 4,32, 4,32, 4,32 +!hkrss-patterns,55, 5,12, 6,12, 5,12, 6,12 EOF diff output expected From 08c153d3bb34ed8922d3198d8090f0c1a0c0d6af Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Mar 2017 08:41:49 +0100 Subject: [PATCH 16/20] genltl: add support for --p-patterns Fixes #246. * bin/genltl.cc: Implement it. * bin/man/genltl.x, doc/org/genltl.org, NEWS: Document it. * tests/core/ltl2tgba2.test: Test it. --- NEWS | 5 ++-- bin/genltl.cc | 61 +++++++++++++++++++++++++++++++++++++++ bin/man/genltl.x | 4 +++ doc/org/genltl.org | 32 ++++++++++++++++---- tests/core/ltl2tgba2.test | 38 +++++++++++++++++++++++- 5 files changed, 131 insertions(+), 9 deletions(-) diff --git a/NEWS b/NEWS index 79469778e..e1a83ff3a 100644 --- a/NEWS +++ b/NEWS @@ -6,8 +6,9 @@ New in spot 2.3.2.dev (not yet released) and ltl2ldba (from Owl) without needing to specify %f>%O. - genltl learned --spec-patterns as an alias for --dac-patterns; it - also learned a new set of LTL formulas under --hkrss-patterns - (a.k.a. --liberouter-patterns). + also learned two new sets of LTL formulas under --hkrss-patterns + (a.k.a. --liberouter-patterns) and --p-patterns + (a.k.a. --beem-patterns). Bug fixes: diff --git a/bin/genltl.cc b/bin/genltl.cc index d29586f41..ee6c23cd7 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -142,6 +142,19 @@ // number = 03, // institution = {CESNET} // } +// +// @InProceedings{pelanek.07.spin, +// author = {Radek Pel\'{a}nek}, +// title = {{BEEM}: benchmarks for explicit model checkers}, +// booktitle = {Proceedings of the 14th international SPIN conference on +// Model checking software}, +// year = 2007, +// pages = {263--267}, +// numpages = {5}, +// volume = {4595}, +// series = {Lecture Notes in Computer Science}, +// publisher = {Springer-Verlag} +// } #include "common_sys.hh" @@ -196,6 +209,7 @@ enum { OPT_OR_FG, OPT_OR_G, OPT_OR_GF, + OPT_P_PATTERNS, OPT_R_LEFT, OPT_R_RIGHT, OPT_RV_COUNTER, @@ -235,6 +249,7 @@ const char* const class_name[LAST_CLASS - FIRST_CLASS] = "or-fg", "or-g", "or-gf", + "p-patterns", "r-left", "r-right", "rv-counter", @@ -303,6 +318,11 @@ static const argp_option options[] = OPT_ALIAS(gh-s), { "or-gf", OPT_OR_GF, "RANGE", 0, "GF(p1)|GF(p2)|...|GF(pn)", 0 }, OPT_ALIAS(gh-c1), + { "p-patterns", OPT_P_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL, + "Pelánek [Spin'07] patterns from BEEM " + "(range should be included in 1..20)", 0 }, + OPT_ALIAS(beem-patterns), + OPT_ALIAS(p), { "r-left", OPT_R_LEFT, "RANGE", 0, "(((p1 R p2) R p3) ... R pn)", 0 }, { "r-right", OPT_R_RIGHT, "RANGE", 0, "(p1 R (p2 R (... R pn)))", 0 }, { "rv-counter", OPT_RV_COUNTER, "RANGE", 0, @@ -436,6 +456,12 @@ parse_opt(int key, char* arg, struct argp_state*) else enqueue_job(key, 1, 12); break; + case OPT_P_PATTERNS: + if (arg) + enqueue_job(key, arg); + else + enqueue_job(key, 1, 20); + break; case OPT_SB_PATTERNS: if (arg) enqueue_job(key, arg); @@ -1142,6 +1168,38 @@ eh_pattern(int n) return spot::relabel(parse_formula(formulas[n - 1]), Pnn); } +static formula +p_pattern(int n) +{ + static const char* formulas[] = { + "G(p0 -> Fp1)", + "(GFp1 & GFp0) -> GFp2", + "G(p0 -> (p1 & (p2 U p3)))", + "F(p0 | p1)", + "GF(p0 | p1)", + "(p0 U p1) -> ((p2 U p3) | Gp2)", + "G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))", + "G(p0 -> (p1 R !p2))", + "G(!p0 -> Fp0)", + "G(p0 -> F(p1 | p2))", + "!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))", + "G!p0 -> G!p1", + "G(p0 -> (G!p1 | (!p2 U p1)))", + "G(p0 -> (p1 R (p1 | !p2)))", + "G((p0 & p1) -> (!p1 R (p0 | !p1)))", + "G(p0 -> F(p1 & p2))", + "G(p0 -> (!p1 U (p1 U (p1 & p2))))", + "G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))", + "GFp0 -> GFp1", + "GF(p0 | p1) & GF(p1 | p2)", + }; + + constexpr unsigned max = (sizeof formulas)/(sizeof *formulas); + if (n < 1 || (unsigned) n > max) + bad_number("--p-patterns", n, max); + return spot::relabel(parse_formula(formulas[n - 1]), Pnn); +} + static formula sb_pattern(int n) { @@ -1488,6 +1546,9 @@ output_pattern(int pattern, int n) case OPT_OR_GF: f = GF_n("p", n, false); break; + case OPT_P_PATTERNS: + f = p_pattern(n); + break; case OPT_R_LEFT: f = bin_n("p", n, op::R, false); break; diff --git a/bin/man/genltl.x b/bin/man/genltl.x index b9f224a71..74fcfb4f2 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -46,6 +46,10 @@ kv O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. .TP +p +R. Pelánek: BEEM: benchmarks for explicit model checkers +Proceedings of Spin'07. LNCS 4595. +.TP rv K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin'07. LNCS 4595. diff --git a/doc/org/genltl.org b/doc/org/genltl.org index 963b0156a..d7952ad1b 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -133,15 +133,15 @@ This is because most tools using =lbt='s syntax require atomic propositions to have the form =pNN=. -Four options provide lists of unrelated LTL formulas, taken from the +Five options provide lists of unrelated LTL formulas, taken from the literature (see the [[./man/genltl.1.html][=genltl=]](1) man page for references): -=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, and -=--sb-patterns=. With these options, the range is used to select a -subset of the list of formulas. Without range, all formulas are used. -Here is the complete list: +=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, =--p-patterns=, +and =--sb-patterns=. With these options, the range is used to select +a subset of the list of formulas. Without range, all formulas are +used. Here is the complete list: #+BEGIN_SRC sh :results verbatim :exports both - genltl --dac --eh --hkrss --sb --format=%F:%L,%f + genltl --dac --eh --hkrss --p --sb --format=%F:%L,%f #+END_SRC #+RESULTS: @@ -268,6 +268,26 @@ hkrss-patterns:52,XG(p0 -> (G!p1 | (!Xp1 U p2))) hkrss-patterns:53,XG((p0 & !p1) -> (G!p1 | (!p1 U p2))) hkrss-patterns:54,XG((p0 & p1) -> ((p1 U p2) | Gp1)) hkrss-patterns:55,Xp0 & G((!p0 & Xp0) -> XXp0) +p-patterns:1,G(p0 -> Fp1) +p-patterns:2,(GFp1 & GFp0) -> GFp2 +p-patterns:3,G(p0 -> (p1 & (p2 U p3))) +p-patterns:4,F(p0 | p1) +p-patterns:5,GF(p0 | p1) +p-patterns:6,(p0 U p1) -> ((p2 U p3) | Gp2) +p-patterns:7,G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1))))) +p-patterns:8,G(p0 -> (p1 R !p2)) +p-patterns:9,G(!p0 -> Fp0) +p-patterns:10,G(p0 -> F(p1 | p2)) +p-patterns:11,!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2)) +p-patterns:12,G!p0 -> G!p1 +p-patterns:13,G(p0 -> (G!p1 | (!p2 U p1))) +p-patterns:14,G(p0 -> (p1 R (p1 | !p2))) +p-patterns:15,G((p0 & p1) -> (!p1 R (p0 | !p1))) +p-patterns:16,G(p0 -> F(p1 & p2)) +p-patterns:17,G(p0 -> (!p1 U (p1 U (p1 & p2)))) +p-patterns:18,G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2)))))) +p-patterns:19,GFp0 -> GFp1 +p-patterns:20,GF(p0 | p1) & GF(p1 | p2) sb-patterns:1,p0 U p1 sb-patterns:2,p0 U (p1 U p2) sb-patterns:3,!(p0 U (p1 U p2)) diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index c5d523401..ae8eb7d2b 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -27,7 +27,7 @@ # commonly use as benchmark change, we want to notice it. set -e -genltl --dac --eh --sb --hkrss --format=%F,%L,%f >pos +genltl --dac --eh --sb --hkrss --p --format=%F,%L,%f >pos (cat pos; ltlfilt --negate pos/3 --format='!%<,%f') | ltlfilt -u -F-/3 >formulas @@ -183,6 +183,24 @@ hkrss-patterns,52, 4,25, 4,25, 5,29, 5,29 hkrss-patterns,53, 3,22, 3,22, 3,22, 3,22 hkrss-patterns,54, 3,22, 3,22, 3,22, 3,22 hkrss-patterns,55, 5,8, 5,8, 5,8, 5,8 +p-patterns,2, 4,36, 4,36, 5,44, 5,44 +p-patterns,3, 2,20, 2,20, 2,20, 2,20 +p-patterns,4, 2,8, 2,8, 2,8, 2,8 +p-patterns,5, 1,4, 1,4, 2,8, 2,8 +p-patterns,6, 4,50, 4,50, 4,50, 4,50 +p-patterns,7, 4,27, 4,27, 4,27, 4,27 +p-patterns,8, 2,10, 2,10, 2,10, 2,10 +p-patterns,9, 1,2, 1,2, 2,4, 2,4 +p-patterns,10, 2,16, 2,16, 2,16, 2,16 +p-patterns,11, 2,20, 2,20, 2,20, 2,20 +p-patterns,12, 3,12, 3,12, 3,12, 3,12 +p-patterns,13, 3,20, 3,20, 3,20, 3,20 +p-patterns,14, 2,13, 2,13, 2,13, 2,13 +p-patterns,15, 2,7, 2,7, 2,7, 2,7 +p-patterns,16, 2,16, 2,16, 2,16, 2,16 +p-patterns,17, 3,20, 3,20, 3,20, 3,20 +p-patterns,18, 5,36, 5,36, 5,36, 5,36 +p-patterns,20, 1,8, 1,8, 3,24, 3,24 !dac-patterns,1, 2,4, 2,4, 2,4, 2,4 !dac-patterns,2, 3,10, 3,10, 3,10, 3,10 !dac-patterns,3, 3,12, 3,12, 3,12, 3,12 @@ -321,6 +339,24 @@ hkrss-patterns,55, 5,8, 5,8, 5,8, 5,8 !hkrss-patterns,53, 4,32, 4,32, 4,32, 4,32 !hkrss-patterns,54, 4,32, 4,32, 4,32, 4,32 !hkrss-patterns,55, 5,12, 6,12, 5,12, 6,12 +!p-patterns,2, 2,15, 2,15, 4,23, 4,23 +!p-patterns,3, 3,41, 3,41, 3,41, 3,41 +!p-patterns,4, 1,1, 1,1, 1,1, 1,1 +!p-patterns,5, 2,6, 2,6, 2,6, 2,6 +!p-patterns,6, 4,42, 4,42, 4,42, 4,42 +!p-patterns,7, 5,34, 5,34, 5,34, 5,34 +!p-patterns,8, 3,24, 3,24, 3,24, 3,24 +!p-patterns,9, 2,4, 2,4, 2,4, 2,4 +!p-patterns,10, 2,11, 2,11, 2,11, 2,11 +!p-patterns,11, 3,48, 3,48, 3,48, 3,48 +!p-patterns,12, 2,4, 2,4, 2,4, 2,4 +!p-patterns,13, 4,32, 4,32, 4,32, 4,32 +!p-patterns,14, 3,24, 3,24, 3,24, 3,24 +!p-patterns,15, 3,12, 3,12, 3,12, 3,12 +!p-patterns,16, 2,17, 2,17, 2,17, 2,17 +!p-patterns,17, 4,31, 4,31, 4,31, 4,31 +!p-patterns,18, 6,43, 6,43, 6,43, 6,43 +!p-patterns,20, 3,16, 3,16, 3,16, 3,16 EOF diff output expected From c90400a1b07c1bf762f5a76a445c99db3e701b4c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 9 Mar 2017 13:52:30 +0100 Subject: [PATCH 17/20] * AUTHORS: Add Thomas Medioni. --- AUTHORS | 1 + 1 file changed, 1 insertion(+) diff --git a/AUTHORS b/AUTHORS index 73a2bb670..d18d865ae 100644 --- a/AUTHORS +++ b/AUTHORS @@ -21,5 +21,6 @@ Souheib Baarir Thibaud Michaud Thomas Badie Thomas Martinez +Thomas Medioni Tomáš Babiak Vincent Tourneur From 88bc78f9e212cfa7c8b787cedcdf2c56e9e54eb8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 7 Apr 2017 20:36:36 +0200 Subject: [PATCH 18/20] * spot/twaalgos/remfin.cc: Typos in comments. --- spot/twaalgos/remfin.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc index 5e5c3bb98..3638161a8 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -95,7 +95,7 @@ namespace spot return sccaut->is_empty(); } // The bits remaining sets in i corresponds to I₁s that have - // been seen with seeing the mathing F₁. In this SCC any state + // been seen with seeing the matching F₁. In this SCC any state // in these I₁ is therefore final. Otherwise we do not know: it // is possible that there is a non-accepting cycle in the SCC // that do not visit Fᵢ. @@ -144,7 +144,7 @@ namespace spot // concerned about *deterministic* automata, but we apply the // algorithm on non-deterministic automata as well: in the worst // case it is possible that a Büchi-type SCC with some - // non-deterministic has one accepting and one rejecting run for + // non-deterministim has one accepting and one rejecting run for // the same word. In this case we may fail to detect the // Büchi-typeness of the SCC, but the resulting automaton should // be correct nonetheless. From e39e5ac586f9d02e8c5ee3653d11e04c613b0be4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 11 Apr 2017 10:43:04 +0200 Subject: [PATCH 19/20] Spot 2.3.3 * NEWS, configure.ac, doc/org/setup.org: Bump version number. --- NEWS | 16 ++++++++-------- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/NEWS b/NEWS index e1a83ff3a..2f844aab0 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.3.2.dev (not yet released) +New in spot 2.3.3 (2017-04-11) Tools: @@ -10,13 +10,13 @@ New in spot 2.3.2.dev (not yet released) (a.k.a. --liberouter-patterns) and --p-patterns (a.k.a. --beem-patterns). - Bug fixes: + Bugs fixed: - - In "lenient" mode the parser would fail to recover from - a missing closing brace. + - In "lenient" mode the formula parser would fail to recover from a + missing closing brace. - - The output of 'genltl --r-left=1 --r-right=1 --format=%F' - had typos. + - The output of 'genltl --r-left=1 --r-right=1 --format=%F' had + typos. - 'ltl2tgba Fa | autfilt --complement' would incorrectly claim that the output is "terminal" because dtwa_complement() failed to reset @@ -25,8 +25,8 @@ New in spot 2.3.2.dev (not yet released) - spot::twa_graph::purge_unreachable_states() was misbehaving on alternating automata. - - In bench/stutter/ the .cc files were not compiling due to warnings being - caught as errors. + - In bench/stutter/ the .cc files were not compiling due to warnings + being caught as errors. - The code in charge of detecting DBA-type Rabin automata is actually written to handle a slightly larger class of acceptance diff --git a/configure.ac b/configure.ac index c1e5fe657..b126e595a 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], [2.3.2.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.3], [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/setup.org b/doc/org/setup.org index cd5ce922b..b60d61ef2 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,8 +1,8 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.3.2 -#+MACRO: LASTRELEASE 2.3.2 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.2.tar.gz][=spot-2.3.2.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-2/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-03-15 +#+MACRO: SPOTVERSION 2.3.3 +#+MACRO: LASTRELEASE 2.3.3 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.3.tar.gz][=spot-2.3.3.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-3/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2017-04-11 From 19602e4bd055194392618b7dfaa7f47e10421e8e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 11 Apr 2017 10:46:40 +0200 Subject: [PATCH 20/20] Bump version number to 2.3.3.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 2f844aab0..ea74dac0e 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.3.3.dev (not yet released) + + Nothing yet. + New in spot 2.3.3 (2017-04-11) Tools: diff --git a/configure.ac b/configure.ac index b126e595a..3e5a3bfe3 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], [2.3.3], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.3.dev], [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])