From 0f7008d98ce60ba8bc18412dbdd4904f0251c201 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 27 Feb 2017 22:27:47 +0100 Subject: [PATCH 01/26] * spot/priv/satcommon.cc: Fix include. --- spot/priv/satcommon.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spot/priv/satcommon.cc b/spot/priv/satcommon.cc index 9af7d887b..999086616 100644 --- a/spot/priv/satcommon.cc +++ b/spot/priv/satcommon.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita. +// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -20,7 +20,7 @@ #include #include -#include +#include #include #include #include From 6c218e48285e1a86a8acebd2a2ab260fe436c5e6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 28 Feb 2017 14:06:26 +0100 Subject: [PATCH 02/26] bin: --stats=%x to count atomic propositions * bin/common_aoutput.cc, bin/common_aoutput.hh: Implement %x and %X. * tests/core/remprop.test: Test them. * NEWS: Mention them. --- NEWS | 6 +++++- bin/common_aoutput.cc | 16 ++++++++++++++-- bin/common_aoutput.hh | 6 ++++-- tests/core/remprop.test | 5 +++-- 4 files changed, 26 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 4a583c01b..ec5426fed 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.3.1.dev (not yet released) - Nothing yet. + Tools: + + - In tools that output automata the number of atomic propositions + can be output using --stats=%x (output automaton) or --stats=%X + (input automaton). New in spot 2.3.1 (2017-02-20) diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index ce0944b2c..e8011b30f 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -193,6 +193,8 @@ static const argp_option io_options[] = "wall-clock time elapsed in seconds (excluding parsing)", 0 }, { "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "one word accepted by the automaton", 0 }, + { "%X, %x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of atomic propositions declared in the automaton", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -228,6 +230,8 @@ static const argp_option o_options[] = "number of transitions", 0 }, { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "number of acceptance sets", 0 }, + { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of acceptance sets", 0 }, { "%g", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "acceptance condition (in HOA syntax)", 0 }, { "%c, %[LETTERS]c", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -250,6 +254,8 @@ static const argp_option o_options[] = "wall-clock time elapsed in seconds (excluding parsing)", 0 }, { "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "one word accepted by the output automaton", 0 }, + { "%x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "number of atomic propositions declared in the automaton", 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { nullptr, 0, nullptr, 0, nullptr, 0 } @@ -361,6 +367,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('S', &haut_states_); declare('T', &haut_trans_); declare('W', &haut_word_); + declare('X', &haut_ap_size_); } declare('<', &csv_prefix_); declare('>', &csv_suffix_); @@ -372,6 +379,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('h', &output_aut_); declare('m', &aut_name_); declare('w', &aut_word_); + declare('x', &aut_ap_size_); } std::ostream& @@ -467,6 +475,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, haut_word_.val().clear(); } } + if (has('X')) + haut_ap_size_ = haut->aut->ap().size(); } if (has('m')) @@ -490,6 +500,8 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, aut_word_.val().clear(); } } + if (has('x')) + aut_ap_size_ = aut->ap().size(); auto& res = this->spot::stat_printer::print(aut, f, run_time); // Make sure we do not store the automaton until the next one is diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 9a10b0745..f22244242 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -144,6 +144,8 @@ private: spot::printable_value haut_edges_; spot::printable_value haut_trans_; spot::printable_value haut_acc_; + spot::printable_value haut_ap_size_; + spot::printable_value aut_ap_size_; spot::printable_scc_info haut_scc_; spot::printable_value haut_deterministic_; spot::printable_value haut_nondetstates_; diff --git a/tests/core/remprop.test b/tests/core/remprop.test index 09e28d7ce..e423c4784 100755 --- a/tests/core/remprop.test +++ b/tests/core/remprop.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. @@ -47,6 +47,7 @@ EOF cat >expected <1" States: 4 Start: 0 AP: 1 "c" @@ -68,7 +69,7 @@ State: 3 --END-- EOF -run 0 autfilt -H --remove-ap=a,b automaton >out +run 0 autfilt -H --remove-ap=a,b --name='%X->%x' automaton >out cat out diff out expected From 905af9045916a83117692e2cbbe65cd8e4143855 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 28 Feb 2017 16:05:59 +0100 Subject: [PATCH 03/26] skip divine tests when divine does not understand compile --help Fixes #235, reported by Henrich Lauko. * python/spot/ltsmin.i: Catch CalledProcessError. * NEWS: Mention the bug. * THANKS: Add Henrich. --- NEWS | 5 +++++ THANKS | 1 + python/spot/ltsmin.i | 11 ++++++++--- 3 files changed, 14 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index ec5426fed..084e873c4 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,11 @@ New in spot 2.3.1.dev (not yet released) can be output using --stats=%x (output automaton) or --stats=%X (input automaton). + Bugs fixed: + + - The tests using LTSmin's patched version of divine would fail + if the current (non-patched) version of divine was installed. + New in spot 2.3.1 (2017-02-20) Tools: diff --git a/THANKS b/THANKS index 3d7c104d7..b182df63f 100644 --- a/THANKS +++ b/THANKS @@ -14,6 +14,7 @@ Felix Klaedtke František Blahoudek Gerard J. Holzmann Heikki Tauriainen +Henrich Lauko Jan Strejček Jean-Michel Couvreur Jean-Michel Ilié diff --git a/python/spot/ltsmin.i b/python/spot/ltsmin.i index ae81916b8..c70da47f9 100644 --- a/python/spot/ltsmin.i +++ b/python/spot/ltsmin.i @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016 Laboratoire de Recherche et Développement de +// Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -120,8 +120,13 @@ def require(*tools): if shutil.which("divine") == None: print("divine not available", file=sys.stderr) sys.exit(77) - out = subprocess.check_output(['divine', 'compile', '--help'], - stderr=subprocess.STDOUT) + try: + out = subprocess.check_output(['divine', 'compile', '--help'], + stderr=subprocess.STDOUT) + except (subprocess.CalledProcessError): + print("divine does not understand 'compile --help'", + file=sys.stderr) + sys.exit(77) if b'LTSmin' not in out: print("divine available but no support for LTSmin", file=sys.stderr) From e0d32918815ad57535dfcb21539052ff6bddeebe Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 28 Feb 2017 16:39:54 +0100 Subject: [PATCH 04/26] correct handling of --stats=%P Fixes #236. * bin/common_aoutput.cc: Fix it. * tests/core/format.test: Improve test cases. * NEWS: Mention the bug. --- NEWS | 3 +++ bin/common_aoutput.cc | 2 +- tests/core/format.test | 18 +++++++++++++----- 3 files changed, 17 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 084e873c4..a399c2ac5 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,9 @@ New in spot 2.3.1.dev (not yet released) - The tests using LTSmin's patched version of divine would fail if the current (non-patched) version of divine was installed. + - Because of a typo, the output of --stats='...%P...' was correct + only if %p was used as well. + New in spot 2.3.1 (2017-02-20) Tools: diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index e8011b30f..c1805f3c7 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -453,7 +453,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, haut_deterministic_ = is_deterministic(haut->aut); } - if (has('p')) + if (has('P')) haut_complete_ = is_complete(haut->aut); if (has('G')) diff --git a/tests/core/format.test b/tests/core/format.test index 67a7ce0b3..a91026130 100644 --- a/tests/core/format.test +++ b/tests/core/format.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -51,11 +51,19 @@ for i in 1 2 3 4 5 6; do cmp ap-$i.ltl ap-$i.ltl2 || exit 1 done -out=`ltl2tgba -f 'GFa' | autfilt --stats='%W,%w' --complement` +ltl2tgba GFa > GFa +out=` FGa +test "0,1,0,1" = "` Date: Wed, 1 Mar 2017 16:02:09 +0100 Subject: [PATCH 05/26] add options to %x to list atomic propositions * bin/common_aoutput.cc, bin/common_aoutput.hh, bin/common_output.cc, bin/common_output.hh: Add options to %x to list atomic propositions with various quoting scheme. Deprecate --format=%a in favor of the new --format=%x for consistency with --stats=%x. * tests/core/format.test, tests/core/remprop.test: Adjust and add more tests. * NEWS: Mention these changes. --- NEWS | 12 +++- bin/common_aoutput.cc | 120 ++++++++++++++++++++++++++++++++-------- bin/common_aoutput.hh | 37 ++++++++++++- bin/common_output.cc | 10 ++-- bin/common_output.hh | 18 +++++- tests/core/format.test | 8 +-- tests/core/remprop.test | 3 +- 7 files changed, 169 insertions(+), 39 deletions(-) diff --git a/NEWS b/NEWS index a399c2ac5..d6cd1ee4e 100644 --- a/NEWS +++ b/NEWS @@ -4,7 +4,9 @@ New in spot 2.3.1.dev (not yet released) - In tools that output automata the number of atomic propositions can be output using --stats=%x (output automaton) or --stats=%X - (input automaton). + (input automaton). Additional options can be passed to list + atomic propositions instead of conting them. Tools that output + formulas also support --format=%x for this purpose. Bugs fixed: @@ -14,6 +16,14 @@ New in spot 2.3.1.dev (not yet released) - Because of a typo, the output of --stats='...%P...' was correct only if %p was used as well. + Deprecation notices: + + - Using --format=%a to print the number of atomic propositions in + ltlfilt, genltl, and randltl still works, but it is not documented + anymore and should be replaced by the newly-introduced --format=%x + for consistency with tools producing automata. + + New in spot 2.3.1 (2017-02-20) Tools: diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index c1805f3c7..862cc70b5 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -20,12 +20,15 @@ #include "common_sys.hh" #include "error.h" #include "argmatch.h" +#include "common_output.hh" #include "common_aoutput.hh" #include "common_post.hh" #include "common_cout.hh" #include #include +#include +#include #include #include #include @@ -193,8 +196,9 @@ static const argp_option io_options[] = "wall-clock time elapsed in seconds (excluding parsing)", 0 }, { "%W, %w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "one word accepted by the automaton", 0 }, - { "%X, %x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of atomic propositions declared in the automaton", 0 }, + { "%X, %x, %[LETTERS]X, %[LETTERS]x", 0, nullptr, + OPTION_DOC | OPTION_NO_USAGE, + COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, @@ -254,8 +258,9 @@ static const argp_option o_options[] = "wall-clock time elapsed in seconds (excluding parsing)", 0 }, { "%w", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "one word accepted by the output automaton", 0 }, - { "%x", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, - "number of atomic propositions declared in the automaton", 0 }, + { "%x, %[LETTERS]x", 0, nullptr, + OPTION_DOC | OPTION_NO_USAGE, + COMMON_X_OUTPUT_SPECS(declared in the automaton), 0 }, { "%%", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, { nullptr, 0, nullptr, 0, nullptr, 0 } @@ -367,7 +372,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('S', &haut_states_); declare('T', &haut_trans_); declare('W', &haut_word_); - declare('X', &haut_ap_size_); + declare('X', &haut_ap_); } declare('<', &csv_prefix_); declare('>', &csv_suffix_); @@ -379,7 +384,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('h', &output_aut_); declare('m', &aut_name_); declare('w', &aut_word_); - declare('x', &aut_ap_size_); + declare('x', &aut_ap_); } std::ostream& @@ -476,7 +481,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, } } if (has('X')) - haut_ap_size_ = haut->aut->ap().size(); + haut_ap_ = haut->aut->ap(); } if (has('m')) @@ -501,7 +506,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, } } if (has('x')) - aut_ap_size_ = aut->ap().size(); + aut_ap_ = aut->ap(); auto& res = this->spot::stat_printer::print(aut, f, run_time); // Make sure we do not store the automaton until the next one is @@ -625,6 +630,19 @@ void printable_automaton::print(std::ostream& os, const char* pos) const print_hoa(os, val_, options.c_str()); } + +namespace +{ + static void percent_error(const char* beg, const char* pos) + { + std::ostringstream tmp; + const char* end = std::strchr(pos, ']'); + tmp << "unknown option '" << *pos << "' in '%" + << std::string(beg, end + 2) << '\''; + throw std::runtime_error(tmp.str()); + } +} + void printable_timer::print(std::ostream& os, const char* pos) const { double res = 0; @@ -652,20 +670,9 @@ void printable_timer::print(std::ostream& os, const char* pos) const bool children = false; const char* beg = pos; - auto error = [&](std::string str) - { - std::ostringstream tmp; - const char* end = std::strchr(pos, ']'); - tmp << "unknown option '" << str << "' in '%" << std::string(beg, end + 2) - << '\''; - throw std::runtime_error(tmp.str()); - }; - do - { - ++pos; - switch (*pos) - { + switch (*++pos) + { case 'u': user = true; break; @@ -685,9 +692,9 @@ void printable_timer::print(std::ostream& os, const char* pos) const case ']': break; default: - error(std::string(pos, pos + 1)); - } - } while (*pos != ']'); + percent_error(beg, pos); + } + while (*pos != ']'); if (!parent && !children) parent = children = true; @@ -697,3 +704,68 @@ void printable_timer::print(std::ostream& os, const char* pos) const res = val_.get_uscp(user, system, children, parent); os << res / clocks_per_sec; } + +void printable_varset::print(std::ostream& os, const char* pos) const +{ + if (*pos != '[') + { + os << val_.size(); + return; + } + char qstyle = 's'; // quote style + bool parent = false; + std::string sep; + + const char* beg = pos; + do + switch (int c = *++pos) + { + case 'p': + parent = true; + break; + case 'c': + case 'd': + case 's': + case 'n': + qstyle = c; + break; + case ']': + break; + default: + if (isalnum(c)) + percent_error(beg, pos); + sep += c; + } + while (*pos != ']'); + + if (sep.empty()) + sep = " "; + + bool first = true; + for (auto f: val_) + { + if (first) + first = false; + else + os << sep; + if (parent) + os << '('; + switch (qstyle) + { + case 's': + os << f; + break; + case 'n': + os << f.ap_name(); + break; + case 'd': + spot::escape_str(os << '"', f.ap_name()) << '"'; + break; + case 'c': + spot::escape_rfc4180(os << '"', f.ap_name()) << '"'; + break; + } + if (parent) + os << ')'; + } +} diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index f22244242..83a774438 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -31,6 +31,7 @@ #include #include #include +#include // Format for automaton output @@ -107,6 +108,38 @@ struct printable_timer final: void print(std::ostream& os, const char* pos) const override; }; +struct printable_varset final: public spot::printable +{ +protected: + std::vector val_; + void sort() + { + std::sort(val_.begin(), val_.end(), + [](spot::formula f, spot::formula g) + { + return strverscmp(f.ap_name().c_str(), g.ap_name().c_str()) < 0; + }); + } +public: + + template + void set(T begin, T end) + { + val_.clear(); + val_.insert(val_.end(), begin, end); + sort(); + } + + printable_varset& operator=(const std::vector& val) + { + val_ = val; + sort(); + return *this; + } + + void print(std::ostream& os, const char* pos) const override; +}; + /// \brief prints various statistics about a TGBA /// /// This object can be configured to display various statistics @@ -144,8 +177,8 @@ private: spot::printable_value haut_edges_; spot::printable_value haut_trans_; spot::printable_value haut_acc_; - spot::printable_value haut_ap_size_; - spot::printable_value aut_ap_size_; + printable_varset haut_ap_; + printable_varset aut_ap_; spot::printable_scc_info haut_scc_; spot::printable_value haut_deterministic_; spot::printable_value haut_nondetstates_; diff --git a/bin/common_output.cc b/bin/common_output.cc index 2a6a92060..abe85a819 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -19,6 +19,7 @@ #include "common_sys.hh" #include "common_output.hh" +#include "common_aoutput.hh" #include #include #include @@ -203,13 +204,14 @@ namespace formula_printer(std::ostream& os, const char* format) : format_(format) { - declare('a', &ap_num_); + declare('a', &ap_); // deprecated in 2.3.2 declare('b', &bool_size_); declare('f', &fl_); declare('F', &filename_); declare('L', &line_); declare('s', &size_); declare('h', &class_); + declare('x', &ap_); declare('<', &prefix_); declare('>', &suffix_); set_output(os); @@ -225,10 +227,10 @@ namespace prefix_ = fl.prefix ? fl.prefix : ""; suffix_ = fl.suffix ? fl.suffix : ""; auto f = fl_.val()->f; - if (has('a')) + if (has('a') || has('x')) { auto s = spot::atomic_prop_collect(f); - ap_num_ = s->size(); + ap_.set(s->begin(), s->end()); delete s; } if (has('b')) @@ -250,7 +252,7 @@ namespace spot::printable_value size_; printable_formula_class class_; spot::printable_value bool_size_; - spot::printable_value ap_num_; + printable_varset ap_; }; } diff --git a/bin/common_output.hh b/bin/common_output.hh index 8e61811cf..cff7222a5 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -36,9 +36,18 @@ extern output_format_t output_format; extern bool full_parenth; extern bool escape_csv; +#define COMMON_X_OUTPUT_SPECS(where) \ + "number of atomic propositions " #where "; " \ + " add LETTERS to list atomic propositions with " \ + "(n) no quoting, " \ + "(s) occasional double-quotes with C-style escape, " \ + "(d) double-quotes with C-style escape, " \ + "(c) double-quotes with CSV-style escape, " \ + "(p) between parentheses, " \ + "any extra non-alphanumeric character will be used to " \ + "separate propositions" + #define COMMON_LTL_OUTPUT_SPECS \ - { "%a", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ - "number of atomic propositions used in the formula", 0 }, \ { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ "the length (or size) of the formula", 0 }, \ { "%b", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ @@ -47,7 +56,10 @@ extern bool escape_csv; { "%h, %[vw]h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, \ "the class of the formula is the Manna-Pnueli hierarchy " \ "([v] replaces abbreviations by class names, [w] for all " \ - "compatible classes)", 0 } + "compatible classes)", 0 }, \ + { "%x, %[LETTERS]X, %[LETTERS]x", 0, nullptr, \ + OPTION_DOC | OPTION_NO_USAGE, \ + COMMON_X_OUTPUT_SPECS(used in the formula), 0 } extern const struct argp output_argp; diff --git a/tests/core/format.test b/tests/core/format.test index a91026130..5b5073241 100644 --- a/tests/core/format.test +++ b/tests/core/format.test @@ -23,7 +23,7 @@ set -e -genltl --dac=1..10 --format='%s,%b,%a,%f' > output +genltl --dac=1..10 --format='%s,%b,%x,%f' > output cat >expected < (!p1 U p0) @@ -38,7 +38,7 @@ cat >expected < FGa test "0,1,0,1" = "`expected <(c)" States: 3 Start: 0 AP: 1 "c" @@ -90,7 +91,7 @@ State: 2 --END-- EOF -run 0 autfilt -H --remove-ap=a=1,b=0 automaton >out +run 0 autfilt -H --remove-ap=a=1,b=0 --name='%[d, ]X->%[p]x' automaton >out cat out diff out expected From e826710cf16b51810ea46dfed075a0ed51781e30 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 1 Mar 2017 16:17:05 +0100 Subject: [PATCH 06/26] remove options -! and -" from genltl Fixes #237. * bin/genltl.cc: Fix the numbering of options. * NEWS: Mention the bugs. --- NEWS | 3 +++ bin/genltl.cc | 9 +++++---- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index d6cd1ee4e..0c14ae062 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,9 @@ New in spot 2.3.1.dev (not yet released) - Because of a typo, the output of --stats='...%P...' was correct only if %p was used as well. + - genltl was never meant to have (randomly attributed) short + options for --postive and --negative. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/bin/genltl.cc b/bin/genltl.cc index 8fc105046..4c1fc995c 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -167,7 +167,8 @@ const char argp_program_doc[] ="\ Generate temporal logic formulas from predefined patterns."; enum { - OPT_AND_F = 1, + FIRST_CLASS = 256, + OPT_AND_F = FIRST_CLASS, OPT_AND_FG, OPT_AND_GF, OPT_CCJ_ALPHA, @@ -203,7 +204,7 @@ enum { OPT_NEGATIVE, }; -const char* const class_name[LAST_CLASS] = +const char* const class_name[LAST_CLASS - FIRST_CLASS] = { "and-f", "and-fg", @@ -1445,12 +1446,12 @@ output_pattern(int pattern, int n) if (opt_positive || !opt_negative) { - output_formula_checked(f, class_name[pattern - 1], n); + output_formula_checked(f, class_name[pattern - FIRST_CLASS], n); } if (opt_negative) { std::string tmp = "!"; - tmp += class_name[pattern - 1]; + tmp += class_name[pattern - FIRST_CLASS]; output_formula_checked(spot::formula::Not(f), tmp.c_str(), n); } } From 57ea6d9634b6c848dfc4c82a592690ea3e4a5681 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Mar 2017 11:36:41 +0100 Subject: [PATCH 07/26] sbacc: fix a typo and remove some useless code * spot/twaalgos/sbacc.cc: Do not assign to one_in twice, and fix the value of init_acc. * tests/core/sbacc.test: Add a test case. * NEWS: Mention the bug. --- NEWS | 4 ++++ spot/twaalgos/sbacc.cc | 7 ++++--- tests/core/sbacc.test | 34 ++++++++++++++++++++++++++++++++-- 3 files changed, 40 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index 0c14ae062..0b11c818f 100644 --- a/NEWS +++ b/NEWS @@ -19,6 +19,10 @@ New in spot 2.3.1.dev (not yet released) - genltl was never meant to have (randomly attributed) short options for --postive and --negative. + - a typo in the code for transformating transition-based acceptance + to state-based acceptance could cause a superfluous initial state + to be output in some cases (the result was still correct). + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index b4df91026..93acc554c 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -37,21 +37,22 @@ namespace spot unsigned ns = old->num_states(); acc_cond::mark_t all = old->acc().all_sets(); + // Marks that are common to all ingoing or outgoing transitions. std::vector common_in(ns, all); std::vector common_out(ns, all); + // Marks that label one incoming transition from the same SCC. std::vector one_in(ns, 0U); for (auto& e: old->edges()) if (si.scc_of(e.src) == si.scc_of(e.dst)) { common_in[e.dst] &= e.acc; common_out[e.src] &= e.acc; - one_in[e.dst] = e.acc; } for (unsigned s = 0; s < ns; ++s) common_out[s] |= common_in[s]; for (auto& e: old->edges()) if (si.scc_of(e.src) == si.scc_of(e.dst)) - one_in[e.dst] = (e.acc - common_out[e.src]); + one_in[e.dst] = e.acc - common_out[e.src]; auto res = make_twa_graph(old->get_dict()); res->copy_ap_of(old); @@ -83,7 +84,7 @@ namespace spot if (!si.is_rejecting_scc(si.scc_of(old_init))) // Use any edge going into the initial state to set the first // acceptance mark. - init_acc = one_in[old_init] | common_out[init_acc]; + init_acc = one_in[old_init] | common_out[old_init]; res->set_init_state(new_state(old_init, init_acc)); while (!todo.empty()) diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 156c2250a..fedc228bd 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -76,6 +76,22 @@ State: 1 {0} State: 2 [0] 0 {1} --END-- +/* The following example used to be converted into a + 3-state automaton instead of just 2 states, due to + a typo in the code. */ +HOA: v1 +States: 2 +Start: 1 +AP: 2 "a" "b" +Acceptance: 2 Fin(0) & Inf(1) +--BODY-- +State: 0 +[t] 0 {0} +State: 1 +[1] 0 +[0&!1] 1 {1} +--END-- + EOF run 0 $autfilt --state-based-acceptance in.hoa -H > out.hoa @@ -96,6 +112,20 @@ State: 1 {0} State: 2 {0 1} [0] 0 --END-- +HOA: v1 +States: 2 +Start: 0 +AP: 2 "a" "b" +acc-name: Rabin 1 +Acceptance: 2 Fin(0) & Inf(1) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 {1} +[0&!1] 0 +[1] 1 +State: 1 +[t] 1 +--END-- EOF diff out.hoa expected @@ -103,7 +133,7 @@ diff out.hoa expected $autfilt --sba -H expected > out.hoa diff out.hoa expected -$autfilt --strip-acc -H expected > out.hoa +$autfilt --strip-acc -H expected -n1 > out.hoa cat >expected < Date: Fri, 3 Mar 2017 14:29:10 +0100 Subject: [PATCH 08/26] postproc: fix monitor code Fixes #240. * spot/twaalgos/postproc.cc: Do not call do_simul on the output of minimize_monitor(), and do not skip complete() when PREF_==Any. * tests/core/monitor.test: Add a test case. * NEWS: Mention the bug. * doc/org/ltl2tgba.org: Document complete monitors. --- NEWS | 2 ++ doc/org/ltl2tgba.org | 49 ++++++++++++++++++--------------------- spot/twaalgos/postproc.cc | 25 ++++++++++---------- tests/core/monitor.test | 29 ++++++++++++++++++----- 4 files changed, 61 insertions(+), 44 deletions(-) diff --git a/NEWS b/NEWS index 0b11c818f..977f5afd5 100644 --- a/NEWS +++ b/NEWS @@ -23,6 +23,8 @@ New in spot 2.3.1.dev (not yet released) to state-based acceptance could cause a superfluous initial state to be output in some cases (the result was still correct). + - 'ltl2tgba --any -C -M ...' would not complete automata. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 8381adc3f..118809f3d 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -921,32 +921,6 @@ $txt ltl2tgba -MD '(Xa & Fb) | Gc' -d #+END_SRC -#+RESULTS: monitor2 -#+begin_example -digraph G { - rankdir=LR - node [shape="circle"] - fontname="Lato" - node [fontname="Lato"] - edge [fontname="Lato"] - node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] - I [label="", style=invis, width=0] - I -> 3 - 0 [label=<0>] - 0 -> 0 [label=<1>] - 1 [label=<1>] - 1 -> 0 [label=] - 2 [label=<2>] - 2 -> 2 [label=] - 3 [label=<3>] - 3 -> 1 [label=] - 3 -> 4 [label=] - 4 [label=<4>] - 4 -> 0 [label=] - 4 -> 2 [label=] -} -#+end_example - #+BEGIN_SRC dot :file monitor2.png :cmdline -Tpng :var txt=monitor2 :exports results $txt #+END_SRC @@ -959,6 +933,29 @@ match the formula, monitor cannot be used to check for eventualities such as =F(a)=: indeed, any finite execution can be extended to match =F(a)=. + +Because Monitors accept every recognized run (in other words, they +only reject words that are not recognized), it makes little sense to +use option =-C= to request /complete/ monitors. If uou combine =-C= +with =-M=, the result will output as a Büchi automaton if (and only +if) a sink state had to be added. For instance, here is the +"complete" version of the previous monitor. + +#+NAME: monitor3 +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -C -M -D '(Xa & Fb) | Gc' -d +#+END_SRC + +#+BEGIN_SRC dot :file monitor3.png :cmdline -Tpng :var txt=monitor3 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:monitor3.png]] + + + + # LocalWords: ltl tgba num toc PSL Büchi automata SRC GFb invis Acc # LocalWords: ltlfilt filenames GraphViz vectorial pdf Tpdf dotex # LocalWords: sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 2191b8924..5b3f2ca29 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -227,20 +227,21 @@ namespace spot else strip_acceptance_here(a); - if (PREF_ == Any) - return a; - - a = do_simul(a, simul_); - - // For Small,High we return the smallest between the output of - // the simulation, and that of the deterministic minimization. - if (PREF_ == Small && level_ == High && simul_) + if (PREF_ != Any) { - auto m = minimize_monitor(a); - if (m->num_states() < a->num_states()) - a = m; + if (PREF_ != Deterministic) + a = do_simul(a, simul_); + + // For Small,High we return the smallest between the output of + // the simulation, and that of the deterministic minimization. + if (PREF_ == Small && level_ == High && simul_) + { + auto m = minimize_monitor(a); + if (m->num_states() < a->num_states()) + a = m; + } + a->remove_unused_ap(); } - a->remove_unused_ap(); if (COMP_) a = complete(a); return a; diff --git a/tests/core/monitor.test b/tests/core/monitor.test index 504721c28..d21fb3c9d 100755 --- a/tests/core/monitor.test +++ b/tests/core/monitor.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -44,7 +44,7 @@ digraph G { } EOF -expect ltl2tgba --monitor a --hoa< Date: Fri, 3 Mar 2017 17:36:31 +0100 Subject: [PATCH 09/26] doc: add an example about how to build monitor in shell/python/C++ Part of #239. * doc/org/tut11.org: New file. * doc/org/ltl2tgba.org, doc/org/hierarchy.org: Add some anchors we can link to in tut11.org. * doc/org/tut.org, doc/Makefile.am: Add tut11.org. * NEWS: Mention the new page. --- NEWS | 5 + doc/Makefile.am | 1 + doc/org/hierarchy.org | 3 + doc/org/ltl2tgba.org | 5 + doc/org/tut.org | 1 + doc/org/tut11.org | 289 ++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 304 insertions(+) create mode 100644 doc/org/tut11.org diff --git a/NEWS b/NEWS index 977f5afd5..79559b92f 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,11 @@ New in spot 2.3.1.dev (not yet released) atomic propositions instead of conting them. Tools that output formulas also support --format=%x for this purpose. + Documentation: + + - https://spot.lrde.epita.fr/tut11.html is a new page describing + how to build monitors in Shell, Python, or C++. + Bugs fixed: - The tests using LTSmin's patched version of divine would fail diff --git a/doc/Makefile.am b/doc/Makefile.am index c98f07661..917a50afe 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -105,6 +105,7 @@ ORG_FILES = \ org/tut03.org \ org/tut04.org \ org/tut10.org \ + org/tut11.org \ org/tut20.org \ org/tut21.org \ org/tut22.org \ diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index d8e656c11..4bbde1e82 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -427,6 +427,9 @@ $txt ** Safety + :PROPERTIES: + :CUSTOM_ID: safety + :END: /Safety/ properties also form a subclass of /obligation/ properties, and again there is no code specific to them in the translation. diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 118809f3d..f2f04185e 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -870,6 +870,9 @@ more restricted labels. files are on a separate page]]. * Building Monitors + :PROPERTIES: + :CUSTOM_ID: monitors + :END: In addition to TGBA and BA, =ltl2tgba= can output /monitor/ using the =-M= option. These are finite automata that accept all prefixes of a @@ -933,6 +936,8 @@ match the formula, monitor cannot be used to check for eventualities such as =F(a)=: indeed, any finite execution can be extended to match =F(a)=. +For more discussion and examples about monitor, see also our [[file:tut11.org][separate +page showing how to build them in Python and C++]]. Because Monitors accept every recognized run (in other words, they only reject words that are not recognized), it makes little sense to diff --git a/doc/org/tut.org b/doc/org/tut.org index d799d0cdc..1afad5011 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -24,6 +24,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut02.org][Relabeling Formulas]] - [[file:tut04.org][Testing the equivalence of two LTL formulas]] - [[file:tut10.org][Translating an LTL formula into a never claim]] +- [[file:tut11.org][Translating an LTL formula into a monitor]] - [[file:tut20.org][Converting a never claim into HOA]] - [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]] - [[file:tut31.org][Removing alternation]] diff --git a/doc/org/tut11.org b/doc/org/tut11.org new file mode 100644 index 000000000..beb9433ec --- /dev/null +++ b/doc/org/tut11.org @@ -0,0 +1,289 @@ +# -*- coding: utf-8 -*- +#+TITLE: Translating an LTL formula into a monitors +#+DESCRIPTION: Code example for using Spot to translating formulas in monitors +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +A monitor is a special type of automaton that is supposed to /monitor/ +a running system and move accordingly. A monitor detects an error +when it cannot move: i.e., the system as performed some action, or +reached some state that is not supposed to happen. + +For instance here is a monitor that checks that *yellow* never occurs +immediately after *red*. + +#+NAME: tut11a +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -D -M '!F(red & Xyellow)' -d +#+END_SRC + +#+BEGIN_SRC dot :file tut11a.png :cmdline -Tpng :var txt=tut11a :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:tut11a.png]] + +This monitor stays in the initial state until *red* becomes true, it +can then wait in the second state while *red* holds and *yellow* does +not,, and will only move back to the initial state when both *red* and +*yellow* are false. The only way this monitor would not be able to +progress is if *yellow* becomes true while in the second state; in +that case a violation should be reported. + + +* Building a deterministic monitor + +** Shell + +To build the above deterministic monitor using [[file:ltl2tgba.org][=ltl2tgba=]], we simply +pass option =-M= (for monitor) and =-D= (for deterministic). + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -D -M '!F(red & X(yellow))' +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +name: "G(!red | X!yellow)" +States: 2 +Start: 0 +AP: 2 "red" "yellow" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[!0&!1] 0 +[0&!1] 1 +--END-- +#+end_example + +** Python + +The code is very similar to [[file:tut10.org][our previous example of building a never +claim]] except that we explicitly require a deterministic monitor and +output in the [[file:hoa.org][HOA format]]. + +#+BEGIN_SRC python :results output :exports both +import spot +print(spot.translate('!F(red & X(yellow))', 'monitor', 'det').to_str('HOA')) +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 2 +Start: 0 +AP: 2 "red" "yellow" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[!0&!1] 0 +[0&!1] 1 +--END-- +#+end_example + +** C++ + +The code very similar to [[file:tut10.org][the never claim example]]. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include + #include + + int main() + { + spot::parsed_formula pf = spot::parse_infix_psl("!F(red & X(yellow))"); + if (pf.format_errors(std::cerr)) + return 1; + spot::translator trans; + trans.set_type(spot::postprocessor::Monitor); + trans.set_pref(spot::postprocessor::Deterministic); + spot::twa_graph_ptr aut = trans.run(pf.f); + print_hoa(std::cout, aut) << '\n'; + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 2 +Start: 0 +AP: 2 "red" "yellow" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic weak +--BODY-- +State: 0 +[!0] 0 +[0] 1 +State: 1 +[!0&!1] 0 +[0&!1] 1 +--END-- +#+end_example + + +* Non-deterministic monitors + +If you drop the =-D= option from =ltl2tgba=, or the =det= argument +from =spot.translate()=, or the +=set_pref(spot::postprocessor::Deterministic)= in C++, then a +non-deterministic monitor can be output. By default Spot will build +both a deterministic and a non-deterministic monitor, it will output +the smallest one. + +* Details + +** Expressiveness + +In the [[file:hierarchy.org][hierarchy of temporal properties]], the properties that are +monitorable correspond to the class of [[file:hierarchy.org::#safety][safety properties]]. You can +check that an LTL formula is a safety by using: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt --count --safety -f '!F(red & X(yellow))' +#+END_SRC + +#+RESULTS: +: 1 + +(This asks [[file:ltlfilt.org][=ltlfilt=]] to count the number of safety formulas among +those---only one here---that were passed.) + +For properties that are not safety properties, the monitors built +recognize the smallest safety property that contain the original +languages. + +For instance if we want to ensure that whenever we press a button, the +red light will be on until the green light is on, we would use the +following formula: =G(press -> red U green)=. Unfortunately it is not +a safety property: + +#+BEGIN_SRC sh :results verbatim :exports code +ltlfilt --count --safety -f 'G(press -> red U green)' +#+END_SRC + +#+BEGIN_SRC sh :results verbatim :exports results +ltlfilt --count --safety -f 'G(press -> red U green)' +true +#+END_SRC + +#+RESULTS: +: 0 + +Nonetheless, we can still build a monitor for it: + +#+NAME: tut11b +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -D -M 'G(press -> red U green)' -d +#+END_SRC +#+BEGIN_SRC dot :file tut11b.png :cmdline -Tpng :var txt=tut11b :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:tut11b.png]] + + +This monitor will report violations if both *red* and *green* are off +when the button is pressed, and also if *red* goes off without *green* +going on. However note that in the original formula, =red U green= +implies that *green* will eventually become true, and the monitor +cannot ensure that: a system where *red* is continuously on, and +*green* is continuously off would not trigger any violation. The +monitor that has been built here actually represents the safety +property =G(press -> red W green)=, and accepts a bit more than +our original property =G(press -> red U green)=. + +** Construction & References + +The construction of deterministic monitors in Spot follows the +construction of M. d'Amorim and G. Roşu ([[https://www.ideals.illinois.edu/bitstream/handle/2142/10975/Efficient%20Monitoring%20of%20%CF%89-languages.pdf][Efficient monitoring of +ω-languages]]. CAV’05) as described by D. Tabakov and M. Y. Vardi +([[https://www.cs.rice.edu/~vardi/papers/rv10rj.pdf][Optimized Temporal Monitors for SystemC]]. RV’10) with a minor +optimization: instead of starting from a Büchi automaton we start from +a Transition-based Generalized Büchi automaton. + +The construction steps are: +1. translate the LTL formula into a TGBA +2. remove SCCs that cannot reach an accepting cycle +3. strip the acceptance condition +4. determinize the automaton (using a classical powerset) +5. minimize the automaton (using standard DFA minimization) + +When non-deterministic monitors are required, the last two steps +are replaced by a pass of simulation-based reductions. + + +The following code shows how to implement the above five steps in C++ +without using =spot::translator=. Unless you plan to customize some +of these steps, we recommend you use =spot::translator= instead. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include + #include + #include + #include + #include + #include + + int main() + { + spot::parsed_formula pf = spot::parse_infix_psl("G(press -> red U green)"); + if (pf.format_errors(std::cerr)) + return 1; + // 1. translate LTL formula into TGBA + spot::twa_graph_ptr aut = spot::ltl_to_tgba_fm(pf.f, spot::make_bdd_dict()); + // 2. remove "dead" SCCs + aut = spot::scc_filter(aut); + // 3. strip the acceptance condition (in place) + spot::strip_acceptance_here(aut); + // 4. & 5. determinize and minimize the automaton + aut = spot::minimize_monitor(aut); + // output the result. + print_hoa(std::cout, aut) << '\n'; + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 2 +Start: 1 +AP: 3 "press" "red" "green" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +properties: stutter-invariant weak +--BODY-- +State: 0 +[1&!2] 0 +[2] 1 +State: 1 +[0&1&!2] 0 +[!0 | 2] 1 +--END-- +#+end_example + +* Further reading + +If your application requires monitors and you plan to build them with +Spot, it is very likely that you will want to convert the resulting +automata to your own data structure. See [[file:tut21.org][how to print an automaton in +a custom format]] to learn all you need to iterate over Spot's automata. From 28f4e4b9a5e2a39df732d3fc44c0dc2680a00f69 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Mar 2017 17:58:31 +0100 Subject: [PATCH 10/26] doc: simplify a C++ example * doc/org/tut10.org: Remove a couple of useless includes. --- doc/org/tut10.org | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/doc/org/tut10.org b/doc/org/tut10.org index f30f807b0..46afe9891 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -128,17 +128,14 @@ various preferences (like small or deterministic) or characteristic output as a never claim is done via the =print_never_claim= function. #+BEGIN_SRC C++ :results verbatim :exports both - #include #include #include - #include #include #include int main() { - std::string input = "[]<>p0 || <>[]p1"; - spot::parsed_formula pf = spot::parse_infix_psl(input); + spot::parsed_formula pf = spot::parse_infix_psl("[]<>p0 || <>[]p1"); if (pf.format_errors(std::cerr)) return 1; spot::translator trans; From 0621e0e9c57748f39e6c6ae63635b63e75ea4001 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Mar 2017 18:23:57 +0100 Subject: [PATCH 11/26] monitor: fix -MD/-M difference in property output Fixes #241. * spot/twaalgos/postproc.cc: Use the deterministic monitor if it has as many states as the non-deterministic one. * spot/twaalgos/minimize.cc (minimize_monitor): Quickly check for terminal automata. * spot/twaalgos/stripacc.cc: Set the weak property. * spot/twaalgos/stripacc.hh: Improve documentation. * tests/core/monitor.test, tests/core/sbacc.test: Update. * NEWS: Mention the issue. --- NEWS | 5 +++++ spot/twaalgos/minimize.cc | 7 +++++++ spot/twaalgos/postproc.cc | 3 ++- spot/twaalgos/stripacc.cc | 3 ++- spot/twaalgos/stripacc.hh | 6 ++++-- tests/core/monitor.test | 19 ++++++++++++++++--- tests/core/sbacc.test | 2 +- 7 files changed, 37 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 79559b92f..b68c93c4a 100644 --- a/NEWS +++ b/NEWS @@ -30,6 +30,11 @@ New in spot 2.3.1.dev (not yet released) - 'ltl2tgba --any -C -M ...' would not complete automata. + - while not incorrect, the HOA properties output by 'ltl2tgba -M' + could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D' + would always report 'weak' automata. Both variants now report the + most precise between 'weak' or 'terminal'. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 4a199fbd5..355f13fc3 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -490,6 +490,13 @@ namespace spot res->prop_deterministic(true); res->prop_weak(true); res->prop_state_acc(true); + // Quickly check if this is a terminal automaton + for (auto& e: res->edges()) + if (e.src == e.dst && e.cond == bddtrue) + { + res->prop_terminal(true); + break; + } return res; } diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 5b3f2ca29..367757e33 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -234,10 +234,11 @@ namespace spot // For Small,High we return the smallest between the output of // the simulation, and that of the deterministic minimization. + // Prefer the deterministic automaton in case of equality. if (PREF_ == Small && level_ == High && simul_) { auto m = minimize_monitor(a); - if (m->num_states() < a->num_states()) + if (m->num_states() <= a->num_states()) a = m; } a->remove_unused_ap(); diff --git a/spot/twaalgos/stripacc.cc b/spot/twaalgos/stripacc.cc index 5010f1711..a4018035a 100644 --- a/spot/twaalgos/stripacc.cc +++ b/spot/twaalgos/stripacc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2014, 2015, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -30,5 +30,6 @@ namespace spot t.acc = 0U; a->set_generalized_buchi(0); a->release_named_properties(); + a->prop_weak(true); } } diff --git a/spot/twaalgos/stripacc.hh b/spot/twaalgos/stripacc.hh index b94d5558c..df673d7ff 100644 --- a/spot/twaalgos/stripacc.hh +++ b/spot/twaalgos/stripacc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012-2014, 2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,7 +26,9 @@ namespace spot /// \ingroup twa_misc /// \brief Remove all acceptance sets from a twa_graph. /// - /// This is equivalent to marking all states/transitions as accepting. + /// This will also set the acceptance condition to true, and mark + /// the automaton as weak. Doing so obviously makes all recognized + /// infinite runs accepting. SPOT_API void strip_acceptance_here(twa_graph_ptr a); } diff --git a/tests/core/monitor.test b/tests/core/monitor.test index d21fb3c9d..e2a251b1f 100755 --- a/tests/core/monitor.test +++ b/tests/core/monitor.test @@ -44,7 +44,7 @@ digraph G { } EOF -expect ltl2tgba --monitor a GFa --hoa< Date: Tue, 7 Mar 2017 13:36:49 +0100 Subject: [PATCH 12/26] twa_graph: fix set_univ_init_state() with initializer_list Reported by Thomas Medioni. * spot/twa/twagraph.hh (set_univ_init_state): Remove the bogus template parameter. * tests/core/twagraph.cc, tests/core/tgbagraph.test: Test the method. * NEWS: Mention the bug. --- NEWS | 3 +++ spot/twa/twagraph.hh | 1 - tests/core/tgbagraph.test | 20 ++++++++++++++++++-- tests/core/twagraph.cc | 22 ++++++++++++++++++++-- 4 files changed, 41 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index b68c93c4a..7e4ec555a 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,9 @@ New in spot 2.3.1.dev (not yet released) would always report 'weak' automata. Both variants now report the most precise between 'weak' or 'terminal'. + - spot::twa_graph::set_univ_init_state() could not be called with + an initializer list. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 18732b7f0..24d4c8552 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -277,7 +277,6 @@ namespace spot init_number_ = g_.new_univ_dests(dst_begin, dst_end); } - template void set_univ_init_state(const std::initializer_list& il) { set_univ_init_state(il.begin(), il.end()); diff --git a/tests/core/tgbagraph.test b/tests/core/tgbagraph.test index 1b4afad69..37aa4e0f8 100755 --- a/tests/core/tgbagraph.test +++ b/tests/core/tgbagraph.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -254,6 +254,22 @@ State: 1 State: 2 [t] 1 --END-- +HOA: v1.1 +States: 3 +Start: 2&0 +AP: 0 +acc-name: all +Acceptance: 0 t +properties: univ-branch trans-labels explicit-labels state-acc complete +properties: deterministic +--BODY-- +State: 0 +[t] 0 +State: 1 +[t] 0 +State: 2 +[t] 0&1 +--END-- EOF diff stdout expected diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index 5d066455a..c3cf98b20 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -129,9 +129,27 @@ static void f3() spot::print_hoa(std::cout, tg, "1.1") << '\n'; } +// Test creation of universal edges via initializer-list +static void f4() +{ + auto d = spot::make_bdd_dict(); + auto tg = make_twa_graph(d); + + auto s1 = tg->new_state(); + auto s2 = tg->new_state(); + auto s3 = tg->new_state(); + tg->set_univ_init_state({s3, s1}); + tg->new_univ_edge(s3, {s1, s2}, bddtrue); + tg->new_univ_edge(s2, {s1}, bddtrue); + tg->new_edge(s1, s1, bddtrue); + + spot::print_hoa(std::cout, tg, "1.1") << '\n'; +} + int main() { f1(); f2(); f3(); + f4(); } From 61924aec3726ed3926656fa754c25ee54aff799a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Mar 2017 14:06:29 +0100 Subject: [PATCH 13/26] postproc/translate: more doc and references Fixes #239. * spot/twaalgos/postproc.hh, spot/twaalgos/translate.hh: Here. --- spot/twaalgos/postproc.hh | 64 +++++++++++++++++++++++++++----------- spot/twaalgos/translate.hh | 21 +++++++++++-- 2 files changed, 64 insertions(+), 21 deletions(-) diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 7572119c5..3266fe2a3 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -33,10 +33,10 @@ namespace spot /// /// This class is a shell around scc_filter(), /// minimize_obligation(), simulation(), iterated_simulations(), - /// degeneralize(), to_generalized_buchi() and tgba_determinize(). - /// These different algorithms will be combined depending on the - /// various options set with set_type(), set_pref(), and - /// set_level(). + /// degeneralize(), to_generalized_buchi(), tgba_determinize(), and + /// other algorithms. These different algorithms will be combined + /// depending on the various options set with set_type(), + /// set_pref(), and set_level(). /// /// This helps hiding some of the logic required to combine these /// simplifications efficiently (e.g., there is no point calling @@ -59,7 +59,10 @@ namespace spot /// than its input. pref=Small,level=Low will only run /// simulation(). /// - /// + /// The handling of alternating automata should change in the + /// future, but currently \c Generic, \c Low, \c Any is the only + /// configuration where alternation is preserved. In any other + /// configuration, \c remove_alternation() will be called. class SPOT_API postprocessor { public: @@ -76,14 +79,28 @@ namespace spot /// \c TGBA requires transition-based generalized Büchi acceptance /// while \c BA requests state-based Büchi acceptance. In both /// cases, automata with more complex acceptance conditions will - /// be converted into these simpler acceptance. \c Monitor - /// requests an automaton with the "all paths are accepting - /// condition": this is less expressive, and may output automata - /// that recognize a larger language than the input. Finally \c - /// Generic remove all constraints about the acceptance condition. - /// Using \c Generic can be needed to force the determinization of - /// some automata (e.g., not all TGBA can be degeneralized, using - /// \c Generic will allow parity acceptance to be used instead). + /// be converted into these simpler acceptance. For references + /// about the algorithms used behind these options, see section 5 + /// of "LTL translation improvements in Spot 1.0" (Alexandre + /// Duret-Lutz. Int. J. on Critical Computer-Based Systems, + /// 5(1/2), pp. 31–54, March 2014). + /// + /// \c Monitor requests an automaton where all paths are + /// accepting: this is less expressive than Büchi automata, and + /// may output automata that recognize a larger language than the + /// input (the output recognizes the smallest safety property + /// containing the input). The algorithm used to obtain monitors + /// comes from "Efficient monitoring of ω-languages" (Marcelo + /// d’Amorim and Grigoire Roşu, Proceedings of CAV’05, LNCS 3576) + /// but is better described in "Optimized Temporal Monitors for + /// SystemC" (Deian Tabakov and Moshe Y. Vardi, Proceedings of + /// RV’10, LNCS 6418). + /// + /// Finally \c Generic remove all constraints about the acceptance + /// condition. Using \c Generic can be needed to force the + /// determinization of some automata (e.g., not all TGBA can be + /// degeneralized, using \c Generic will allow parity acceptance + /// to be used instead). /// /// If set_type() is not called, the default \c output_type is \c TGBA. void @@ -121,15 +138,24 @@ namespace spot /// set_type(postprocessor::Generic); /// set_pref(postprocessor::Deterministic); /// \endcode - /// if you absolutely want a deterministic automaton. + /// if you absolutely want a deterministic automaton. The + /// resulting deterministic automaton may have generalized Büchi + /// acceptance or parity acceptance. /// /// The above options can be combined with \c Complete and \c /// SBAcc, to request a complete automaton, and an automaton with /// state-based acceptance. /// - /// Note: the postprocessor::Unambiguous option is not actually - /// supported by spot::postprocessor; it is only honored by - /// spot::translator. + /// Note 1: the \c Unambiguous option is not actually supported by + /// spot::postprocessor; it is only honored by spot::translator. + /// + /// Note 2: for historical reasons, option \c SBAcc is implied + /// when the output type is set to \c BA. + /// + /// Note 3: while setting the output type to \c Monitor requests + /// automata with \c t as acceptance condition, combining \c + /// Monitor with \c Complete may produce Büchi automata in case a + /// sink state (which should be rejecting) is added. /// /// If set_pref() is not called, the default \c output_type is \c Small. void diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index a1cfc5706..545474ba7 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2013-2017 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -44,6 +44,23 @@ namespace spot /// The semantic of these three methods is inherited from the /// spot::postprocessor class, but the optimization level is /// additionally used to select which LTL simplifications to enable. + /// + /// Most of the techniques used to produce TGBA or BA are described + /// in "LTL translation improvements in Spot 1.0" (Alexandre + /// Duret-Lutz. Int. J. on Critical Computer-Based Systems, 5(1/2), + /// pp. 31–54, March 2014). + /// + /// Unambiguous automata are produced using a trick described in + /// "LTL Model Checking of Interval Markov Chains" (Michael Benedikt + /// and Rastislav Lenhardt and James Worrell, Proceedings of + /// TACAS'13, pp. 32–46, LNCS 7795). + /// + /// For reference about formula simplifications, see + /// https://spot.lrde.epita.fr/tl.pdf (a copy of this file should be + /// in the doc/tl/ subdirectory of the Spot sources). + /// + /// For reference and documentation about the post-processing step, + /// see the documentation of the spot::postprocessor class. class SPOT_API translator: protected postprocessor { public: From cd4c326f7b2f445f7dcfc46a50be96d2506cefaa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 7 Mar 2017 17:24:14 +0100 Subject: [PATCH 14/26] twa_graph: more test coverage The goal is to improve coverage stats, but I discovered two issues while doing so. * tests/python/twagraph.py: New test case. * tests/Makefile.am: Add it. * spot/twa/twagraph.hh: Add fix typos in error messages. * python/spot/impl.i: Fix broken wrappers for state_from_number and state_acc_sets. --- NEWS | 3 ++ python/spot/impl.i | 4 +- spot/twa/twagraph.hh | 4 +- tests/Makefile.am | 1 + tests/python/twagraph.py | 90 ++++++++++++++++++++++++++++++++++++++++ 5 files changed, 98 insertions(+), 4 deletions(-) create mode 100644 tests/python/twagraph.py diff --git a/NEWS b/NEWS index 7e4ec555a..50593c9f3 100644 --- a/NEWS +++ b/NEWS @@ -38,6 +38,9 @@ New in spot 2.3.1.dev (not yet released) - spot::twa_graph::set_univ_init_state() could not be called with an initializer list. + - the Python wrappers for spot::twa_graph::state_from_number and + spot::twa_graph::state_acc_sets were broken in 2.3. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/python/spot/impl.i b/python/spot/impl.i index 8dfefa14e..3ff4f3073 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -487,12 +487,12 @@ def out(self, src: 'unsigned int'): return $action(self, src) %} %feature("shadow") spot::twa_graph::state_from_number %{ -def state_from_number(self, s: 'unsigned int') -> "spot::twa_graph_state const *": +def state_from_number(self, src: 'unsigned int') -> "spot::twa_graph_state const *": self.report_univ_dest(src) return $action(self, src) %} %feature("shadow") spot::twa_graph::state_acc_sets %{ -def state_acc_sets(self, s: 'unsigned int') -> "spot::acc_cond::mark_t": +def state_acc_sets(self, src: 'unsigned int') -> "spot::acc_cond::mark_t": self.report_univ_dest(src) return $action(self, src) %} diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 24d4c8552..0594ab092 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -257,7 +257,7 @@ namespace spot { if (SPOT_UNLIKELY(s >= num_states())) throw std::invalid_argument - ("set_init_state() called with nonexisiting state"); + ("set_init_state() called with nonexisting state"); init_number_ = s; } @@ -273,7 +273,7 @@ namespace spot for (I i = dst_begin; i != dst_end; ++i) if (SPOT_UNLIKELY(*i >= ns)) throw std::invalid_argument - ("set_univ_init_state() called with nonexisiting state"); + ("set_univ_init_state() called with nonexisting state"); init_number_ = g_.new_univ_dests(dst_begin, dst_end); } diff --git a/tests/Makefile.am b/tests/Makefile.am index b8cf1f2ea..44f5cecf4 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -350,6 +350,7 @@ TESTS_python = \ python/sccfilter.py \ python/setxor.py \ python/trival.py \ + python/twagraph.py \ $(TESTS_ipython) endif diff --git a/tests/python/twagraph.py b/tests/python/twagraph.py new file mode 100644 index 000000000..b87cfdb45 --- /dev/null +++ b/tests/python/twagraph.py @@ -0,0 +1,90 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 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 . + + +# This file tests various error conditions on the twa API + +import spot +from buddy import bddtrue + +aut = spot.make_twa_graph(spot.make_bdd_dict()) + +try: + print(aut.to_str()) + exit(2) +except RuntimeError as e: + assert "no state" in str(e) + +try: + aut.set_init_state(2) +except ValueError as e: + assert "nonexisting" in str(e) + +try: + aut.set_univ_init_state([2, 1]) +except ValueError as e: + assert "nonexisting" in str(e) + +aut.new_states(3) +aut.set_init_state(2) +assert aut.get_init_state_number() == 2 +e = aut.set_univ_init_state([2, 1]) +assert [2, 1] == list(aut.univ_dests(aut.get_init_state_number())) + +try: + aut.get_init_state() +except RuntimeError as e: + s = str(e) + assert "abstract interface" in s and "alternating automata" in s + +all = aut.set_buchi() +aut.new_acc_edge(0, 1, bddtrue, True) + +try: + s = aut.state_acc_sets(0) +except RuntimeError as e: + assert "state-based acceptance" in str(e) + +try: + s = aut.state_is_accepting(0) +except RuntimeError as e: + assert "state-based acceptance" in str(e) + +aut.prop_state_acc(True) + +assert aut.state_acc_sets(0) == all +assert aut.state_is_accepting(0) == True + +aut.set_init_state(0) +aut.purge_unreachable_states() +i = aut.get_init_state() +assert aut.state_is_accepting(i) == True + +it = aut.succ_iter(i) +it.first() +assert aut.edge_number(it) == 1 +assert aut.state_number(it.dst()) == 1 +assert aut.edge_storage(it).src == 0 +assert aut.edge_storage(1).src == 0 +assert aut.edge_data(it).cond == bddtrue +assert aut.edge_data(1).cond == bddtrue +aut.release_iter(it) + +aut.purge_dead_states() +assert aut.state_is_accepting(i) == False From d1d3ee38e699746547dbd3cec39ff8df5b97cf42 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 8 Mar 2017 15:18:49 +0100 Subject: [PATCH 15/26] python: add bindings for bdd_to_formula() Follow-up to an email from Ayrat Khalimov. * python/spot/impl.i: Include twa/formula2bdd.hh. * python/spot/__init__.py: Make the dictionnary optional. * spot/twa/formula2bdd.cc: Throw an exception instead of asserting. * tests/python/bdditer.py: New file. * tests/Makefile.am: Add it. * NEWS: Update. --- NEWS | 4 +++ python/spot/__init__.py | 3 ++ python/spot/impl.i | 2 ++ spot/twa/formula2bdd.cc | 9 ++++-- tests/Makefile.am | 1 + tests/python/bdditer.py | 62 +++++++++++++++++++++++++++++++++++++++++ 6 files changed, 78 insertions(+), 3 deletions(-) create mode 100644 tests/python/bdditer.py diff --git a/NEWS b/NEWS index 50593c9f3..1217356e1 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,10 @@ New in spot 2.3.1.dev (not yet released) atomic propositions instead of conting them. Tools that output formulas also support --format=%x for this purpose. + Python: + + - The bdd_to_formula() function can now be called in Python. + Documentation: - https://spot.lrde.epita.fr/tut11.html is a new page describing diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 0f34693d8..2fb595b7c 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -891,6 +891,9 @@ def parse_word(word, dic=_bdd_dict): from spot.impl import parse_word as pw return pw(word, dic) +def bdd_to_formula(b, dic=_bdd_dict): + from spot.impl import bdd_to_formula as bf + return bf(b, dic) def language_containment_checker(dic=_bdd_dict): from spot.impl import language_containment_checker as c diff --git a/python/spot/impl.i b/python/spot/impl.i index 3ff4f3073..3c700f73c 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -108,6 +108,7 @@ #include #include +#include #include #include #include @@ -428,6 +429,7 @@ namespace std { /* these must come before apcollect.hh */ %include %include +%include %include %implicitconv spot::acc_cond::mark_t; %implicitconv spot::acc_cond::acc_code; diff --git a/spot/twa/formula2bdd.cc b/spot/twa/formula2bdd.cc index dd1106ee9..f10f53ad4 100644 --- a/spot/twa/formula2bdd.cc +++ b/spot/twa/formula2bdd.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2014, 2015 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. @@ -39,7 +39,10 @@ namespace spot { int var = bdd_var(b); const bdd_dict::bdd_info& i = d->bdd_map[var]; - assert(i.type == bdd_dict::var); + if (SPOT_UNLIKELY(i.type != bdd_dict::var)) + throw std::runtime_error("bdd_to_formula() was passed a bdd" + " with a variable that is not in " + "the dictionary"); formula res = i.f; bdd high = bdd_high(b); diff --git a/tests/Makefile.am b/tests/Makefile.am index 44f5cecf4..895a2934b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -330,6 +330,7 @@ TESTS_python = \ python/alarm.py \ python/alternating.py \ python/bddnqueen.py \ + python/bdditer.py \ python/bugdet.py \ python/implies.py \ python/interdep.py \ diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py new file mode 100644 index 000000000..eea25a761 --- /dev/null +++ b/tests/python/bdditer.py @@ -0,0 +1,62 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 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 . + + +# Tests different ways to explore a BDD label, as discussed in +# http://lists.lrde.epita.fr/pipermail/spot/2017q1/000117.html + +import spot +import buddy +import sys + +run = spot.translate('a & !b').accepting_run() +b = run.prefix[0].label +c = buddy.bdd_satone(b) +assert c != buddy.bddfalse +res = [] +while c != buddy.bddtrue: + var = buddy.bdd_var(c) + h = buddy.bdd_high(c) + if h == buddy.bddfalse: + res.append(-var) + c = buddy.bdd_low(c) + else: + res.append(var) + c = h + +assert res == [0, -1] + +res2 = [] +for i in run.aut.ap(): + res2.append((i, run.aut.register_ap(i))) +assert str(res2) == '[(a, 0), (b, 1)]' + + +f = spot.bdd_to_formula(b) +assert f._is(spot.op_And) +assert f[0]._is(spot.op_ap) +assert f[1]._is(spot.op_Not) +assert f[1][0]._is(spot.op_ap) +assert str(f) == 'a & !b' + +try: + f = spot.bdd_to_formula(b, spot.make_bdd_dict()) + sys.exit(2) +except RuntimeError as e: + assert "not in the dictionary" in str(e) From cd89983ca50aeaf3df101375275f106c71fffcd0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 8 Mar 2017 16:10:47 +0100 Subject: [PATCH 16/26] typos: dictionnary -> dictionary * doc/org/upgrade2.org, tests/python/prodexpt.py, tests/python/product.ipynb, NEWS: Fix typos. * tests/sanity/style.test: Add a check for this. --- NEWS | 2 +- doc/org/upgrade2.org | 4 ++-- tests/python/prodexpt.py | 6 +++--- tests/python/product.ipynb | 4 ++-- tests/sanity/style.test | 8 ++++++-- 5 files changed, 14 insertions(+), 10 deletions(-) diff --git a/NEWS b/NEWS index 1217356e1..3223e7e3e 100644 --- a/NEWS +++ b/NEWS @@ -3499,7 +3499,7 @@ New in spot 0.0f (2003-08-01): * Tgba's output algorithms (save(), dotty()) now non-recursive. * During products, succ_iter will optimize its set of successors using information computed from the current product state. - * BDD dictionnaries are now shared between automata and. This + * BDD dictionaries are now shared between automata and. This gets rid of all the BDD-variable translating machinery. New in spot 0.0d (2003-07-13): diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 8df4ff21c..942b05eaf 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -46,7 +46,7 @@ experience of updating a couple of projects that are using Spot. used to require visitors. 5. Allocated object that are large or expected to have a long life - (such as automata, BDD dictionnaries, accepting runs) are now + (such as automata, BDD dictionaries, accepting runs) are now [[#shared_ptr][returned using shared pointers]]. 6. Spot used to be centered around the concept of TGBA @@ -587,7 +587,7 @@ for (auto i: aut->succ(s)) } #+END_SRC -- Each =twa= now has a BDD dictionnary, so the =get_dict()= method is +- Each =twa= now has a BDD dictionary, so the =get_dict()= method is implemented once for all in =twa=, and should not be implemented anymore in sub-classes. diff --git a/tests/python/prodexpt.py b/tests/python/prodexpt.py index 2b11d4e61..020bc9d71 100644 --- a/tests/python/prodexpt.py +++ b/tests/python/prodexpt.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement -# de l'Epita +# Copyright (C) 2016-2017 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). # # This file is part of Spot, a model checking library. # @@ -20,7 +20,7 @@ import spot # make sure that we are not allowed to build the product of two automata with -# different dictionnaries. +# different dictionaries. aut1 = spot.translate('Xa') aut2 = spot.translate('Xb', dict=spot.make_bdd_dict()) diff --git a/tests/python/product.ipynb b/tests/python/product.ipynb index 320e9d543..2d3478552 100644 --- a/tests/python/product.ipynb +++ b/tests/python/product.ipynb @@ -732,7 +732,7 @@ "\n", "We will build an automaton of type `twa_graph`, i.e., an automaton represented explicitely using a graph. In those automata, states are numbered by integers, starting from `0`. (Those states can also be given a different name, which is why the the `product()` shows us something that appears to be labeled by pairs, but the real identifier of each state is an integer.)\n", "\n", - "We will use a dictionnary to keep track of the association between a pair `(ls,rs)` of input states, and its number in the output." + "We will use a dictionary to keep track of the association between a pair `(ls,rs)` of input states, and its number in the output." ] }, { @@ -2064,4 +2064,4 @@ "metadata": {} } ] -} \ No newline at end of file +} diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 59577015f..2cd2b0987 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.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) 2004, 2005 Laboratoire d'Informatique de Paris 6 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université # Pierre et Marie Curie. @@ -84,6 +84,10 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do $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 'version 2 of the License' $file && diag 'license text should refer to version 2' $GREP -i 'Temple Place' $file && From 4a160cb644bed091c4d8e0ec1b4ca184eb649e2e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 8 Mar 2017 16:52:46 +0100 Subject: [PATCH 17/26] * spot/twaalgos/remfin.cc: Typos in comment. --- 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 87d8c90ef..69fc04486 100644 --- a/spot/twaalgos/remfin.cc +++ b/spot/twaalgos/remfin.cc @@ -86,8 +86,8 @@ namespace spot auto sccaut = mask_keep_accessible_states(aut, keep, states.front()); // Force SBA to false. It does not affect the emptiness // check result, however it prevent recurring into this - // procedure, because empty() will call to_tgba() which will - // call remove_fin()... + // procedure, because is_empty() will call + // to_generalized_buchi() which will call remove_fin()... sccaut->prop_state_acc(false); // If SCCAUT is empty, the SCC is BA-type (and none // of its states are final). If SCCAUT is nonempty, the SCC From 4c08e7ec00366539c022258bdd8dfc90bd69cf08 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 8 Mar 2017 17:33:51 +0100 Subject: [PATCH 18/26] python: add bindings for to_generalized_buchi() * python/spot/impl.i: Here. * NEWS: Mention it. --- NEWS | 3 ++- python/spot/impl.i | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 3223e7e3e..3c4df348f 100644 --- a/NEWS +++ b/NEWS @@ -10,7 +10,8 @@ New in spot 2.3.1.dev (not yet released) Python: - - The bdd_to_formula() function can now be called in Python. + - The bdd_to_formula(), and to_generalized_buchi() functions can now + be called in Python. Documentation: diff --git a/python/spot/impl.i b/python/spot/impl.i index 3c700f73c..8c1f11018 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -134,6 +134,7 @@ #include #include #include +#include #include #include #include @@ -535,6 +536,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include From d6d987bd96a8d57a8dffc929ac061fef575afe20 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Mar 2017 14:19:09 +0100 Subject: [PATCH 19/26] emptiness checks: replace assert-preconditions by exceptions * spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc, spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance condition is not satisfied. * tests/python/misc-ec.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the change. --- NEWS | 5 ++++ spot/twaalgos/couvreurnew.cc | 5 ++++ spot/twaalgos/gv04.cc | 8 ++++-- spot/twaalgos/magic.cc | 8 ++++-- spot/twaalgos/se05.cc | 9 ++++--- spot/twaalgos/tau03.cc | 8 +++--- spot/twaalgos/tau03opt.cc | 4 ++- tests/Makefile.am | 1 + tests/python/misc-ec.py | 47 ++++++++++++++++++++++++++++++++++++ 9 files changed, 84 insertions(+), 11 deletions(-) create mode 100644 tests/python/misc-ec.py diff --git a/NEWS b/NEWS index 3c4df348f..46f162f12 100644 --- a/NEWS +++ b/NEWS @@ -46,6 +46,11 @@ New in spot 2.3.1.dev (not yet released) - the Python wrappers for spot::twa_graph::state_from_number and spot::twa_graph::state_acc_sets were broken in 2.3. + - instantiating an emptiness check on an automaton with unsupported + acceptance condition should throw an exception. This used to be + just an assertion, disabled in release builds; the difference + matters for the Python bindings. + Deprecation notices: - Using --format=%a to print the number of atomic propositions in diff --git a/spot/twaalgos/couvreurnew.cc b/spot/twaalgos/couvreurnew.cc index e38c208fc..ee0e91de5 100644 --- a/spot/twaalgos/couvreurnew.cc +++ b/spot/twaalgos/couvreurnew.cc @@ -540,12 +540,17 @@ namespace spot : emptiness_check(a, o) , ecs_(std::make_shared>(a)) { + if (a->acc().uses_fin_acceptance()) + throw std::runtime_error + ("couvreur99_new requires Fin-less acceptance"); } virtual emptiness_check_result_ptr check() override { + if (ecs_->aut->acc().get_acceptance().is_f()) + return nullptr; return check_impl(); } diff --git a/spot/twaalgos/gv04.cc b/spot/twaalgos/gv04.cc index ea3508cef..45e496954 100644 --- a/spot/twaalgos/gv04.cc +++ b/spot/twaalgos/gv04.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2011, 2013, 2014, 2015, 2016 Laboratoire de +// Copyright (C) 2008, 2010, 2011, 2013-2017 Laboratoire de // recherche et développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -67,7 +67,11 @@ namespace spot gv04(const const_twa_ptr& a, option_map o) : emptiness_check(a, o) { - assert(a->num_sets() <= 1); + if (!(a->prop_weak().is_true() + || a->num_sets() == 0 + || a->acc().is_buchi())) + throw std::runtime_error + ("gv04 requires Büchi or weak automata"); } ~gv04() diff --git a/spot/twaalgos/magic.cc b/spot/twaalgos/magic.cc index 705329818..24820aac4 100644 --- a/spot/twaalgos/magic.cc +++ b/spot/twaalgos/magic.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de recherche et +// Copyright (C) 2011, 2013-2017 Laboratoire de recherche et // développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -59,7 +59,11 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->num_sets() <= 1); + if (!(a->prop_weak().is_true() + || a->num_sets() == 0 + || a->acc().is_buchi())) + throw std::runtime_error + ("magic_search requires Büchi or weak automata"); } virtual ~magic_search_() diff --git a/spot/twaalgos/se05.cc b/spot/twaalgos/se05.cc index ee77ff4f1..ec24263b7 100644 --- a/spot/twaalgos/se05.cc +++ b/spot/twaalgos/se05.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -59,7 +59,10 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->num_sets() <= 1); + if (!(a->prop_weak().is_true() + || a->num_sets() == 0 + || a->acc().is_buchi())) + throw std::runtime_error("se05 requires Büchi or weak automata"); } virtual ~se05_search() diff --git a/spot/twaalgos/tau03.cc b/spot/twaalgos/tau03.cc index d69a66b3b..8e07a2fac 100644 --- a/spot/twaalgos/tau03.cc +++ b/spot/twaalgos/tau03.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche -// et Developpement de l'Epita (LRDE). +// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -58,7 +58,9 @@ namespace spot : emptiness_check(a, o), h(size) { - assert(a->num_sets() > 0); + if (!(a->num_sets() > 0 && a->acc().is_generalized_buchi())) + throw std::runtime_error + ("tau03 requires generalized Büchi with at least one set"); } virtual ~tau03_search() diff --git a/spot/twaalgos/tau03opt.cc b/spot/twaalgos/tau03opt.cc index fd3d2acc6..9b9907605 100644 --- a/spot/twaalgos/tau03opt.cc +++ b/spot/twaalgos/tau03opt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2017 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -74,6 +74,8 @@ namespace spot use_weights(o.get("weights", 1)), use_red_weights(use_weights && o.get("redweights", 1)) { + if (a->acc().uses_fin_acceptance()) + throw std::runtime_error("tau03opt requires Fin-less acceptance"); } virtual ~tau03_opt_search() diff --git a/tests/Makefile.am b/tests/Makefile.am index 895a2934b..efc77fe19 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -339,6 +339,7 @@ TESTS_python = \ python/ltlparse.py \ python/ltlsimple.py \ python/minato.py \ + python/misc-ec.py \ python/optionmap.py \ python/otfcrash.py \ python/parsetgba.py \ diff --git a/tests/python/misc-ec.py b/tests/python/misc-ec.py new file mode 100644 index 000000000..4c01e345f --- /dev/null +++ b/tests/python/misc-ec.py @@ -0,0 +1,47 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2017 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 . + +import spot +aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'BA') +ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut) +n = 0 +while True: + res = ec.check() + if not res: + break + print(res.accepting_run()) + n += 1 +assert n == 2 + +for name in ['SE05', 'CVWY90', 'GV04']: + aut = spot.translate("GFa && GFb") + try: + ec = spot.make_emptiness_check_instantiator(name)[0].instantiate(aut) + print(ec.check().accepting_run()) + except RuntimeError as e: + assert "Büchi or weak" in str(e) + +aut = spot.translate("a", 'monitor') +try: + ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut) +except RuntimeError as e: + assert "at least one" in str(e) + +aut = spot.translate("a", 'ba') +ec = spot.make_emptiness_check_instantiator('Tau03')[0].instantiate(aut) From d0f92d75a19be7ea4b0569fc483f4d092db1c093 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 13 Mar 2017 18:09:44 +0100 Subject: [PATCH 20/26] tl: fix incorrect comment about {r} vs. cl(r) Fixes #242. * doc/tl/tl.tex: Remove incorrect claim that {r} does not match the PSL semantics. --- doc/tl/tl.tex | 7 ------- 1 file changed, 7 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 1b9d5701b..56f3e4ce9 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -867,13 +867,6 @@ is not a model of \samp{$\sere{a\PLUS{}\CONCAT\NOT a\CONCAT(a\STAR{}\ANDALT(a\STAR{}\CONCAT\NOT a\CONCAT a\STAR{}))}$} because this SERE does not accept any word. -Note that the semantics of $\sere{r}$ comes from the -$\mathsf{cl}(\cdot)$ operator defined by~\citet{dax.09.atva}. This -differs from the interpretation of a SERE $r$ in the context of a -temporal formula given by the PSL standard~\citep[Appendix~B.3.1.1.2, -item~7]{psl.04.lrm}: the $\sere{r}$ semantics used here corresponds to -$r!\lor r$ in the PSL standard. - \subsection{Syntactic Sugar}\label{sec:pslsugar} The syntax on the left is equivalent to the syntax on the right. From 7ee52041ddca70290c4c19fb4d79f0f421e63a98 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 13 Mar 2017 22:17:49 +0100 Subject: [PATCH 21/26] [buddy] remove useless #include * src/bddio.c, src/bddop.c, src/imatrix.c, src/pairs.c: Here. --- buddy/src/bddio.c | 1 - buddy/src/bddop.c | 1 - buddy/src/imatrix.c | 1 - buddy/src/pairs.c | 1 - 4 files changed, 4 deletions(-) diff --git a/buddy/src/bddio.c b/buddy/src/bddio.c index c7f3ab983..eaa1fde6b 100644 --- a/buddy/src/bddio.c +++ b/buddy/src/bddio.c @@ -37,7 +37,6 @@ #include #include #include -#include #include #include "kernel.h" diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index c01513e81..1a90e53bd 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -38,7 +38,6 @@ #include #include #include -#include #include "kernel.h" #include "cache.h" diff --git a/buddy/src/imatrix.c b/buddy/src/imatrix.c index 9e482941f..c7073b89e 100644 --- a/buddy/src/imatrix.c +++ b/buddy/src/imatrix.c @@ -34,7 +34,6 @@ DATE: (C) february 2000 *************************************************************************/ #include -#include #include #include "kernel.h" #include "imatrix.h" diff --git a/buddy/src/pairs.c b/buddy/src/pairs.c index 5c95f05a9..5677e6b62 100644 --- a/buddy/src/pairs.c +++ b/buddy/src/pairs.c @@ -36,7 +36,6 @@ *************************************************************************/ #include #include -#include #include "kernel.h" /*======================================================================*/ From b7afef3643aea703f6125ea46232d7e9ae6643d5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Mar 2017 10:44:30 +0100 Subject: [PATCH 22/26] org: misc cosmetics * doc/org/tut24.org: Add missing section title. * doc/org/spot.css: Style h3 headings, and remove some useless lines. --- doc/org/spot.css | 9 +++------ doc/org/tut24.org | 1 + 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/doc/org/spot.css b/doc/org/spot.css index c30fa03c3..99472710b 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -1,7 +1,7 @@ a{color:inherit;background-color:inherit;font:inherit;text-decoration:inherit} a:hover{text-decoration:underline} /* http://paletton.com/#uid=33i0X0kz3BrkeHdpSD1C7r1FAlb */ -body{font-family:Arial, sans-serif;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em;background-image:url(/img/spot64.png);background-repeat:no-repeat;background-position:25px 25px} +body{font-family:Arial, sans-serif;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em;background-image:url(/img/spot64.png);background-repeat:no-repeat;background-position:.5em .5em} body.man{padding:0 .5em 3em .5em} body #content{padding-top:45px} body pre{background:#fbfbfb;border:none;font-family:monospace, courier} @@ -12,11 +12,9 @@ body a{color:#008181} #table-of-contents h2{font-size:100%;font-weight:normal;padding-left:0.5em;padding-right:0.5em;padding-top:0.05em;padding-bottom:0.05em} #table-of-contents #text-table-of-contents{text-align:left} #org-div-home-and-up{text-align:center;font-size:100%} -.done{color:SpringGreen} -.WAIT{color:Orange} -.timestamp-kwd{color:DeepPink} -div#postamble{visibility:hidden} .outline-2 h2{border-bottom-style:solid;border-color:#ffe35e} +.outline-3 h3{position:relative;z-index:1} +.outline-3 h3:before{content:"";position:absolute;z-index:-1;left:-.2em;bottom:-.05em;height:1.2em;width:1.2em;background-color:#ffe35e;border-radius:5px} pre.src{padding-top:8px;border-left-style:solid;border-color:#00adad;overflow:auto} pre.src-hoa{padding-top:8px;border-left-style:solid;border-color:#d70079;overflow:auto} pre.example{border-left-style:solid;border-color:#d70079} @@ -34,7 +32,6 @@ img{max-width:100%} #table-of-contents{border:1px solid #ffd300} #org-div-home-and-up{visibility:hidden} } - thead tr {background: #ffe35e;} #content tbody:nth-child(odd) tr:nth-child(even) {background: #fff0a6;} #content tbody:nth-child(odd) tr:nth-child(odd) {background: #fff7cf;} diff --git a/doc/org/tut24.org b/doc/org/tut24.org index 220ff2796..4dc646596 100644 --- a/doc/org/tut24.org +++ b/doc/org/tut24.org @@ -47,6 +47,7 @@ autfilt --dot=.a tut24.hoa #+RESULTS: [[file:tut24in.png]] +* C++ Let us assume that this automaton has been loaded in variable =aut=, and that we run the following code, similar to what we did in the From 880131a0c304e2e2ac38f36de0d087d907db7325 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Mar 2017 12:03:10 +0100 Subject: [PATCH 23/26] [buddy] add -Wno-gnu if supported * m4/gccwarns.m4: Add -Wno-gnu to workaround a diagnostic from clang 3.9.1 on arch Linux. clang was complaining whtat assert() is using a GNU extension. --- buddy/m4/gccwarns.m4 | 1 + 1 file changed, 1 insertion(+) diff --git a/buddy/m4/gccwarns.m4 b/buddy/m4/gccwarns.m4 index 6a91d7e2b..fb90308e1 100644 --- a/buddy/m4/gccwarns.m4 +++ b/buddy/m4/gccwarns.m4 @@ -41,6 +41,7 @@ EOF Wnull-dereference \ Wsuggest-override \ Wpedantic \ + Wno-gnu \ Wno-long-long do CFLAGS="$cf_save_CFLAGS $ac_cv_prog_gcc_warn_flags -$cf_opt" From 2f7d5cfd0034c2af94e410d76745fa70a54a03b7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Mar 2017 14:37:23 +0100 Subject: [PATCH 24/26] tl.pdf: adjust syntactic hierarchy class to match code Fixes #243. * doc/tl/tl.tex: Here. --- doc/tl/tl.tex | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 56f3e4ce9..62eab9f40 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1175,30 +1175,32 @@ page~\pageref{property-methods}). The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$, $\varphi_R$ denote any formula belonging respectively to the Guarantee, Safety, Obligation, Persistence, or Recurrence classes. -$\varphi_F$ denotes a finite LTL formula (the unnamed class at the -intersection of Safety and Guarantee formulas on -Fig.~\ref{fig:hierarchy}). $v$ denotes any variable, $r$ any SERE, -$r_F$ any bounded SERE (no loops), and $r_I$ any unbounded SERE. +Additionally $\varphi_B$ denotes a finite LTL formula (the unnamed +class at the intersection of Safety and Guarantee formulas, at the +\textbf{b}ottom of Fig.~\ref{fig:hierarchy}). $v$ denotes any +variable, $r$ any SERE, $r_F$ any bounded SERE (no loops), and $r_I$ +any unbounded SERE. \begin{align*} - \varphi_F ::={}& \0\mid\1\mid v\mid\NOT\varphi_F\mid\varphi_F\AND\varphi_F - \mid(\varphi_F\OR\varphi_F)\mid\varphi_F\EQUIV\varphi_F - \mid\varphi_F\XOR\varphi_F\mid\varphi_F\IMPLIES\varphi_F - \mid\X\varphi_F\\ - \varphi_G ::={}& \varphi_F\mid \NOT\varphi_S\mid + \varphi_B ::={}& \0\mid\1\mid v\mid\NOT\varphi_B\mid\varphi_B\AND\varphi_B + \mid(\varphi_B\OR\varphi_B)\mid\varphi_B\EQUIV\varphi_B + \mid\varphi_B\XOR\varphi_B\mid\varphi_B\IMPLIES\varphi_B + \mid\X\varphi_B\\ + \mid{}& \sere{r_F}\mid \nsere{r_F}\\ + \varphi_G ::={}& \varphi_B\mid \NOT\varphi_S\mid \varphi_G\AND \varphi_G\mid (\varphi_G\OR \varphi_G) \mid\varphi_S\IMPLIES\varphi_G\mid \X\varphi_G \mid \F\varphi_G\mid \varphi_G\U\varphi_G\mid \varphi_G\M\varphi_G\\ - \mid{}& \sere{r_F}\mid + \mid{}& \nsere{r}\mid \sere{r}\Esuffix \varphi_G\mid \sere{r_F}\Asuffix \varphi_G \\ - \varphi_S ::={}& \varphi_F\mid \NOT\varphi_G\mid + \varphi_S ::={}& \varphi_B\mid \NOT\varphi_G\mid \varphi_S\AND \varphi_S\mid (\varphi_S\OR \varphi_S) \mid\varphi_G\IMPLIES\varphi_S\mid \X\varphi_S \mid \G\varphi_S\mid \varphi_S\R\varphi_S\mid \varphi_S\W\varphi_S\\ - \mid{}& \nsere{r_F}\mid + \mid{}& \sere{r}\mid \sere{r_F}\Esuffix \varphi_S\mid \sere{r}\Asuffix \varphi_S\\ \varphi_O ::={}& \varphi_G \mid \varphi_S\mid \NOT\varphi_O\mid From 696eba8a292d00541749d608de07289239653d47 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Mar 2017 09:17:10 +0100 Subject: [PATCH 25/26] Release Spot 2.3.2 * configure.ac, NEWS, doc/org/setup.org: Bump version to 2.3.2. --- NEWS | 17 +++++++++-------- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/NEWS b/NEWS index 46f162f12..73b9745fe 100644 --- a/NEWS +++ b/NEWS @@ -1,11 +1,11 @@ -New in spot 2.3.1.dev (not yet released) +New in spot 2.3.2 (2017-03-15) Tools: - - In tools that output automata the number of atomic propositions + - In tools that output automata, the number of atomic propositions can be output using --stats=%x (output automaton) or --stats=%X (input automaton). Additional options can be passed to list - atomic propositions instead of conting them. Tools that output + atomic propositions instead of counting them. Tools that output formulas also support --format=%x for this purpose. Python: @@ -35,7 +35,7 @@ New in spot 2.3.1.dev (not yet released) - 'ltl2tgba --any -C -M ...' would not complete automata. - - while not incorrect, the HOA properties output by 'ltl2tgba -M' + - While not incorrect, the HOA properties output by 'ltl2tgba -M' could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D' would always report 'weak' automata. Both variants now report the most precise between 'weak' or 'terminal'. @@ -43,20 +43,21 @@ New in spot 2.3.1.dev (not yet released) - spot::twa_graph::set_univ_init_state() could not be called with an initializer list. - - the Python wrappers for spot::twa_graph::state_from_number and + - The Python wrappers for spot::twa_graph::state_from_number and spot::twa_graph::state_acc_sets were broken in 2.3. - - instantiating an emptiness check on an automaton with unsupported + - Instantiating an emptiness check on an automaton with unsupported acceptance condition should throw an exception. This used to be just an assertion, disabled in release builds; the difference matters for the Python bindings. - Deprecation notices: + Deprecation notice: - Using --format=%a to print the number of atomic propositions in ltlfilt, genltl, and randltl still works, but it is not documented anymore and should be replaced by the newly-introduced --format=%x - for consistency with tools producing automata. + for consistency with tools producing automata, where %a means + something else. New in spot 2.3.1 (2017-02-20) diff --git a/configure.ac b/configure.ac index 4283d528a..622b42ef9 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.1.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.2], [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 ca62b121d..cd5ce922b 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.1 -#+MACRO: LASTRELEASE 2.3.1 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.3.1.tar.gz][=spot-2.3.1.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-3-1/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-02-20 +#+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 From 6b339a37122a432ebefd15bd7cf5f9a6d8e09c21 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Mar 2017 09:21:59 +0100 Subject: [PATCH 26/26] Bump version to 2.3.2.dev * NEWS, configure.ac: Here. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 73b9745fe..76faccc9b 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.3.2.dev (not yet released) + + Nothing yet. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/configure.ac b/configure.ac index 622b42ef9..c1e5fe657 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], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.3.2.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])