From 5185844d8aff78e573f0a1b66030c3ae22972658 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 11 Apr 2016 09:59:11 +0200 Subject: [PATCH 01/22] * NEWS, configure.ac: Bump version number. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 30dd743e1..2cc4481e4 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.0.0a (not yet released) + + Nothing yet. + New in spot 2.0 (2016-04-11) Command-line tools: diff --git a/configure.ac b/configure.ac index be4ff3fa0..e78e4a11c 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.0], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.0.0a], [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]) From 134982c08b694287c753eb80e744e3b42844f262 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 18 Apr 2016 17:41:41 +0200 Subject: [PATCH 02/22] Typo in --help output * bin/common_aoutput.cc: Fix --help output for -Hk. * NEWS: Mention it. --- NEWS | 4 +++- bin/common_aoutput.cc | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 2cc4481e4..f4124ea60 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 2.0.0a (not yet released) - Nothing yet. + Bug fixes: + + * Typo in documentation of the -H option in --help output. New in spot 2.0 (2016-04-11) diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 086053e1e..a966c40bf 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -101,7 +101,7 @@ static const argp_option options[] = "(+INT) add INT to all set numbers, " "( Date: Mon, 18 Apr 2016 18:38:55 +0200 Subject: [PATCH 03/22] parseaut: fix parsing of /*****/ * spot/parseaut/scanaut.ll: Here. * tests/core/strength.test: Add a test. * NEWS: Mention the bug. --- NEWS | 1 + spot/parseaut/scanaut.ll | 10 +++++----- tests/core/strength.test | 3 ++- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index f4124ea60..c8f1ae425 100644 --- a/NEWS +++ b/NEWS @@ -3,6 +3,7 @@ New in spot 2.0.0a (not yet released) Bug fixes: * Typo in documentation of the -H option in --help output. + * The automaton parser would choke on comments like /******/. New in spot 2.0 (2016-04-11) diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index 6f4f66852..efb9891be 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -76,7 +76,7 @@ identifier [[:alpha:]_][[:alnum:]_.-]* {eol} yylloc->lines(yyleng); yylloc->step(); {eol2} yylloc->lines(yyleng / 2); yylloc->step(); [ \t\v\f]+ yylloc->step(); -"/""*"+ { +"/*" { orig_cond = YY_START; BEGIN(in_COMMENT); comment_level = 1; @@ -281,13 +281,13 @@ identifier [[:alpha:]_][[:alnum:]_.-]* { - "/""*"+ ++comment_level; + "/*" ++comment_level; [^*/\n\r]* continue; "/"[^*\n\r]* continue; - "*"+[^*/\n\r]* continue; - {eol} yylloc->lines(yyleng); yylloc->end.column = 1; + "*" continue; + {eol} yylloc->lines(yyleng); yylloc->end.column = 1; {eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1; - "*"+"/" { + "*/" { if (--comment_level == 0) { yylloc->step(); diff --git a/tests/core/strength.test b/tests/core/strength.test index f9e0eb442..f9fe38811 100755 --- a/tests/core/strength.test +++ b/tests/core/strength.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Developpement +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Developpement # de l'Epita # # This file is part of Spot, a model checking library. @@ -588,3 +588,4 @@ State: 4 EOF diff out expected +autfilt -q expected From 7c7f0df8a847859a76daf2fee48b4a2635178b82 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Apr 2016 15:18:01 +0200 Subject: [PATCH 04/22] check_strength(): also check negated properties The test is in the patch introducing HOA 1.1 output. * spot/twaalgos/strength.cc: Here. * NEWS: Mention the bug. --- NEWS | 1 + spot/twaalgos/strength.cc | 11 +++++------ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index c8f1ae425..657901a2d 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,7 @@ New in spot 2.0.0a (not yet released) * Typo in documentation of the -H option in --help output. * The automaton parser would choke on comments like /******/. + * check_strength() should also set negated properties. New in spot 2.0 (2016-04-11) diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc index 500addeb5..09c29b115 100644 --- a/spot/twaalgos/strength.cc +++ b/spot/twaalgos/strength.cc @@ -84,12 +84,11 @@ namespace spot delete si; if (set) { - if (terminal && is_term && is_weak) - aut->prop_terminal(true); - if (is_weak) - aut->prop_weak(true); - if (is_inweak) - aut->prop_inherently_weak(true); + if (terminal) + aut->prop_terminal(is_term && is_weak); + aut->prop_weak(is_weak); + if (inweak) + aut->prop_inherently_weak(is_inweak); } if (inweak) return is_inweak; From adb99869cc764f842d7feca27410a0c09439570a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Apr 2016 19:41:47 +0200 Subject: [PATCH 05/22] bitvect: tweak to please icc This allows bitvect.hh to compile with icpc 16.0.2, but the whole project does not yet compile due to a bug in 16.0.2 that prevents compilation of unordered_map::emplace() from the STL shipped with GCC 5.3.1. * spot/misc/bitvect.hh: adjust friend declarations. --- spot/misc/bitvect.hh | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/spot/misc/bitvect.hh b/spot/misc/bitvect.hh index ac9175893..cdc4472d7 100644 --- a/spot/misc/bitvect.hh +++ b/spot/misc/bitvect.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -436,17 +436,15 @@ namespace spot return res; } - friend SPOT_API bitvect* - ::spot::make_bitvect(size_t bitcount); + friend SPOT_API bitvect* make_bitvect(size_t bitcount); /// Print a bitvect. friend SPOT_API std::ostream& operator<<(std::ostream&, const bitvect&); private: - friend SPOT_API bitvect_array* - ::spot::make_bitvect_array(size_t bitcount, - size_t vectcount); + friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount, + size_t vectcount); size_t size_; size_t block_count_; @@ -516,9 +514,8 @@ namespace spot return *reinterpret_cast(storage() + index * bvsize_); } - friend SPOT_API bitvect_array* - ::spot::make_bitvect_array(size_t bitcount, - size_t vectcount); + friend SPOT_API bitvect_array* make_bitvect_array(size_t bitcount, + size_t vectcount); /// Print a bitvect_array. From 370ac51b6b5e697d7c3714233c49732006410b26 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Apr 2016 21:39:54 +0200 Subject: [PATCH 06/22] docyment make_emptiness_check_instantiator() Fixes #161, reported by Yann Thierry-Mieg. * spot/twaalgos/emptiness.hh: Here. * NEWS: Mention it. --- NEWS | 5 ++ spot/twaalgos/emptiness.hh | 126 ++++++++++++++++++++++++++++++++++--- 2 files changed, 123 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 657901a2d..140d5c961 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 2.0.0a (not yet released) + Documentation: + + * Add missing documentation for the option string passed to + spot::make_emptiness_check_instantiator(). + Bug fixes: * Typo in documentation of the -H option in --help output. diff --git a/spot/twaalgos/emptiness.hh b/spot/twaalgos/emptiness.hh index 538ecdedc..2b0be3b16 100644 --- a/spot/twaalgos/emptiness.hh +++ b/spot/twaalgos/emptiness.hh @@ -39,11 +39,18 @@ namespace spot /// \addtogroup emptiness_check Emptiness-checks /// \ingroup twa_algorithms /// + /// You can create an emptiness check either by instantiating it + /// explicitly (calling one of the functions of \ref + /// emptiness_check_algorithms "this list"), or indirectly via + /// spot::make_emptiness_check_instantiator(). The latter function + /// allows user-options to influence the choice of the + /// emptiness-check algorithm used, and the intermediate + /// instantiator object can be used to query to properties of the + /// emptiness check selected. + /// /// All emptiness-check algorithms follow the same interface. /// Basically once you have constructed an instance of - /// spot::emptiness_check (by instantiating a subclass, or calling a - /// functions construct such instance; see \ref - /// emptiness_check_algorithms "this list"), you should call + /// spot::emptiness_check, you should call /// spot::emptiness_check::check() to check the automaton. /// /// If spot::emptiness_check::check() returns 0, then the automaton @@ -202,7 +209,7 @@ namespace spot typedef std::shared_ptr emptiness_check_instantiator_ptr; - // Dynamically create emptiness checks. Given their name and options. + /// Dynamically create emptiness checks. Given their name and options. class SPOT_API emptiness_check_instantiator { public: @@ -239,20 +246,123 @@ namespace spot option_map o_; void *info_; }; - /// @} /// \brief Create an emptiness-check instantiator, given the name /// of an emptiness check. /// - /// \a name should have the form \c "name" or \c "name(options)". + /// This is a convenient entry point to instantiate an emptiness + /// check with user-supplied options. /// - /// On error, the function returns 0. If the name of the algorithm - /// was unknown, \c *err will be set to \c name. If some fragment of + /// \param name should have the form \c "name" or \c "name(options)". + /// + /// \return Return an emptiness-check instantiator. On error, the + /// function returns \c nullptr. If the name of the algorithm was + /// unknown, \c *err will be set to \c name. If some fragment of /// the options could not be parsed, \c *err will point to that /// fragment. + /// + /// The following names supported and correspond to different emptiness + /// check algorithms: + /// - `Cou99` uses `spot::couvreur99()`, that works with Fin-less + /// acceptance conditions, with any number of acceptance sets. + /// The following options can be used: + /// - `shy` Compute all successors of each state, then explore already + /// visited states first. This usually helps to merge SCCs, and + /// thus exit sooner. However because all successors have to be + /// computed and stored, it often consume more memory. + /// - `group` Setting this option is meaningful only when shy is + /// used. If set (the default), the successors of all the states + /// that belong to the same SCC will be considered when choosing + /// a successor. Otherwise, only the successor of the topmost + /// state on the DFS stack are considered. + /// - `poprem` Specifies how the algorithm should handle the + /// destruction of non-accepting maximal strongly connected + /// components. If poprem is set, the algorithm will keep a list + /// of all states of a SCC that are fully processed and should be + /// removed once the MSCC is popped. If poprem is unset (the + /// default), the MSCC will be traversed again (i.e. generating + /// the successors of the root recursively) for deletion. This + /// is a choice between memory and speed. + /// + /// Examples: + /// \code + /// Cou99 + /// Cou99(shy !group) + /// Cou99(shy group) + /// Cou99(poprem) + /// Cou99(poprem shy !group) + /// Cou99(poprem shy group) + /// \endcode + /// + /// - `GC04` uses `spot::explicit_gv04_check()` and works on automata + /// with Fin-less acceptance conditions using at most one acceptance + /// set. No options are supported. + /// + /// Example: + /// \code + /// GC04 + /// \endcode + /// + /// - `CVWY90` uses `spot::magic_search()` and work on automata with + /// Fin-less acceptance conditions using at most one acceptance + /// set. Set option `bsh` to the size of a hash-table if you want + /// to activate bit-state hashing. + /// + /// Examples: + /// \code + /// CVWY90 + /// CVWY90(bsh=4M) + /// \endcode + /// + /// - `SE05` uses `spot::se05()` and works on work on automata with + /// Fin-less acceptance conditions using at most one acceptance + /// set. Set option `bsh` to the size of a hash-table if you want + /// to activate bit-state hashing. + /// + /// Examples: + /// \code + /// SE05 + /// SE05(bsh=4M) + /// \endcode + /// + /// - `Tau03` uses `spot::explicit_tau03_search()` and work on automata with + /// Fin-less acceptance conditions using at least one acceptance + /// set. No options are supported. + /// + /// Example: + /// \code + /// Tau03 + /// \endcode + /// + /// - `Tau03_opt` uses `spot::explicit_tau03_opt_search()` and work on + /// automata with any Fin-less acceptance. The following options are + /// supported: + /// - `weights` This option is set by default and activates the usage + /// of weights in the top-level DFS as well as in nested DFSs. + /// - `redweights` This option is set by default, and activates the + /// usage of weights in nested DFSs. It is meaningful only if + /// weights is set. + /// - `condstack` This option is unset by default, and activates + /// the use of the "conditional stack" optimization described by + /// Heikki Tauriainen. + /// - ordering This option is unset by default, and activates the + /// use of the "ordering" heuristic described by Heikki Tauriainen + /// in Research Report A96 from the Helsinki University of Technology. + /// + /// Example: + /// \code + /// Tau03_opt + /// Tau03_opt(!weights) + /// Tau03_opt(!redweights) + /// Tau03_opt(condstack) + /// Tau03_opt(condstack !weights) + /// Tau03_opt(condstack !redweights) + /// \endcode SPOT_API emptiness_check_instantiator_ptr make_emptiness_check_instantiator(const char* name, const char** err); + /// @} + /// \addtogroup emptiness_check_algorithms Emptiness-check algorithms /// \ingroup emptiness_check From 2b5516ba665f2bbab3249309f1583e768c5a8907 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Apr 2016 14:43:32 +0200 Subject: [PATCH 07/22] * bin/autfilt.cc: Typos in --help. --- bin/autfilt.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 5a001ba11..54c9128cf 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -222,11 +222,11 @@ static const argp_option options[] = "in FILENAME", 0 }, { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 }, { "states", OPT_STATES, "RANGE", 0, - "keep automata whose number of states are in RANGE", 0 }, + "keep automata whose number of states is in RANGE", 0 }, { "edges", OPT_EDGES, "RANGE", 0, - "keep automata whose number of edges are in RANGE", 0 }, + "keep automata whose number of edges is in RANGE", 0 }, { "acc-sets", OPT_ACC_SETS, "RANGE", 0, - "keep automata whose number of acceptance sets are in RANGE", 0 }, + "keep automata whose number of acceptance sets is in RANGE", 0 }, { "accept-word", OPT_ACCEPT_WORD, "WORD", 0, "keep automata that accept WORD", 0 }, { "reject-word", OPT_REJECT_WORD, "WORD", 0, From 6acd03a142f39c1c36c0c73bd677e8fe5d435570 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Apr 2016 17:13:13 +0200 Subject: [PATCH 08/22] =?UTF-8?q?doc:=20ltlcross=20is=20not=20only=20about?= =?UTF-8?q?=20B=C3=BCchi=20anymore?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * bin/man/ltlcross.x, doc/org/ltlcross.org, doc/org/tools.org: Fix one-line summaries. --- bin/man/ltlcross.x | 2 +- doc/org/ltlcross.org | 2 +- doc/org/tools.org | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/bin/man/ltlcross.x b/bin/man/ltlcross.x index 30b8b5e81..295fbb195 100644 --- a/bin/man/ltlcross.x +++ b/bin/man/ltlcross.x @@ -1,6 +1,6 @@ .\" -*- coding: utf-8 -*- [NAME] -ltlcross \- cross-compare LTL/PSL translators to Büchi automata +ltlcross \- cross-compare LTL/PSL translators to omega-automata [EXAMPLES] The following commands compare never claims produced by .BR ltl2tgba (1), diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index c0c3a9600..9db0e4e2a 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -3,7 +3,7 @@ #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html -=ltlcross= is a tool for cross-comparing the output of LTL-to-Büchi +=ltlcross= is a tool for cross-comparing the output of LTL-to-automata translators. It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], the /LTL-to-Büchi Translator Testbench/, that essentially performs the same sanity checks. diff --git a/doc/org/tools.org b/doc/org/tools.org index f36d69968..f3dfc641c 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -43,7 +43,7 @@ corresponding commands are hidden. - [[file:genltl.org][=genltl=]] Generate LTL formulas from scalable patterns. - [[file:ltl2tgba.org][=ltl2tgba=]] Translate LTL/PSL formulas into Büchi automata. - [[file:ltl2tgta.org][=ltl2tgta=]] Translate LTL/PSL formulas into Testing automata. -- [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-Büchi translators. +- [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-automata translators. - [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL formula - [[file:dstar2tgba.org][=dstar2tgba=]] Convert automata with any acceptance into variants of From fcbb950c0f1de71eee334488f099a1f00849dee3 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Fri, 22 Apr 2016 14:37:08 +0200 Subject: [PATCH 09/22] Update list of dependencies. * HACKING: Here. --- HACKING | 1 + 1 file changed, 1 insertion(+) diff --git a/HACKING b/HACKING index a46d09792..39ed1da3f 100644 --- a/HACKING +++ b/HACKING @@ -34,6 +34,7 @@ since the generated files they produce are distributed.) liblocale-gettext-perl or p5-locale-gettext in your distribution) A complete LaTeX distribution, including latexmk and extra fonts like dsfont.sty. + ImageMagick Python >= 3.3, IPython >= 2.3 GraphViz From 1d739d766f8085fd84091ad3a7e892a1dd217499 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Apr 2016 18:48:03 +0200 Subject: [PATCH 10/22] python: export tgba_determinize * python/spot/impl.i: Here. * tests/python/automata.ipynb: Use it. * NEWS: Mention it. --- NEWS | 4 + python/spot/impl.i | 2 + tests/python/automata.ipynb | 291 ++++++++++++++++++++++++++++++++---- 3 files changed, 270 insertions(+), 27 deletions(-) diff --git a/NEWS b/NEWS index 140d5c961..b7488181b 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,10 @@ New in spot 2.0.0a (not yet released) * Add missing documentation for the option string passed to spot::make_emptiness_check_instantiator(). + Python: + + * The tgba_determinize() function is now accessible in Python. + Bug fixes: * Typo in documentation of the -H option in --help output. diff --git a/python/spot/impl.i b/python/spot/impl.i index 2a1db01ff..cd895afbd 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -123,6 +123,7 @@ #include #include #include +#include #include #include #include @@ -428,6 +429,7 @@ namespace std { %include %include %include +%include %include %include %include diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 8fda68e28..e470761ee 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:93ecf5f37287bb2a03dcd63d41faa06f0ed9d8bcc403c73b24d1bf10404b3b1c" + "signature": "sha256:29d335e40a65f0ca04a3b2b07bfcbf92f794407b413644546d957487dcbf4bb1" }, "nbformat": 3, "nbformat_minor": 0, @@ -178,7 +178,7 @@ "\n" ], "text": [ - " *' at 0x7f7cfc093810> >" + " *' at 0x7f09a8369240> >" ] } ], @@ -317,7 +317,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -470,7 +470,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -570,7 +570,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ee10> >" + " *' at 0x7f09a8323fc0> >" ] } ], @@ -640,7 +640,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ecc0> >" + " *' at 0x7f09a8323e70> >" ] } ], @@ -716,7 +716,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ed50> >" + " *' at 0x7f09a8323f00> >" ] } ], @@ -839,7 +839,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1029,7 +1029,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1176,7 +1176,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ef60> >" + " *' at 0x7f09a8323f30> >" ] } ], @@ -1277,7 +1277,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ef30> >" + " *' at 0x7f098bff3210> >" ] } ], @@ -1395,7 +1395,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ef00> >" + " *' at 0x7f098bff3240> >" ] } ], @@ -1494,7 +1494,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ed20> >" + " *' at 0x7f098bff3270> >" ] } ], @@ -1964,7 +1964,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ef90> >" + " *' at 0x7f09a8323ed0> >" ] } ], @@ -2161,7 +2161,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2286,7 +2286,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2428,7 +2428,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2579,7 +2579,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ecf0> >" + " *' at 0x7f098bff33f0> >" ] } ], @@ -2735,7 +2735,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37eed0> >" + " *' at 0x7f09a8323c60> >" ] } ], @@ -2805,7 +2805,7 @@ "\n" ], "text": [ - " *' at 0x7f7cef37ecf0> >" + " *' at 0x7f098bff31b0> >" ] } ], @@ -2877,7 +2877,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -2930,7 +2930,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3042,7 +3042,7 @@ "" ], "text": [ - "" + "" ] }, { @@ -3154,20 +3154,257 @@ "" ], "text": [ - "" + "" ] } ], "prompt_number": 23 }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Explicit determinization after translation:" + ] + }, { "cell_type": "code", "collapsed": true, - "input": [], + "input": [ + "a = spot.translate('FGa')\n", + "display(a)\n", + "display(a.is_deterministic())" + ], "language": "python", "metadata": {}, - "outputs": [], - "prompt_number": 23 + "outputs": [ + { + "metadata": {}, + "output_type": "display_data", + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "\u24ff\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f09a82ac5d0> >" + ] + }, + { + "metadata": {}, + "output_type": "display_data", + "text": [ + "False" + ] + } + ], + "prompt_number": 24 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.tgba_determinize(a).show('.ba')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 25, + "svg": [ + "\n", + "\n", + "G\n", + "\n", + "Fin(\n", + "\u24ff\n", + ") & Inf(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u2776\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u2776\n", + "\n", + "\n", + "" + ], + "text": [ + "" + ] + } + ], + "prompt_number": 25 + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Determinization by `translate()`. The `generic` option allows any acceptance condition to be used instead of the default generalized B\u00fcchi." + ] + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "spot.translate('FGa', 'generic', 'deterministic')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 26, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\u2776\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!a\n", + "\u24ff\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\u2776\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f09a82ac480> >" + ] + } + ], + "prompt_number": 26 } ], "metadata": {} From 0b05a8f98b360a0bd5efb0bc443a88bac56e6ee2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Apr 2016 18:49:50 +0200 Subject: [PATCH 11/22] * tests/python/ltsmin.ipynb: Remove some debugging code. --- tests/python/ltsmin.ipynb | 76 +++++++-------------------------------- 1 file changed, 13 insertions(+), 63 deletions(-) diff --git a/tests/python/ltsmin.ipynb b/tests/python/ltsmin.ipynb index c8e84e95c..23c274ae0 100644 --- a/tests/python/ltsmin.ipynb +++ b/tests/python/ltsmin.ipynb @@ -18,7 +18,7 @@ "version": "3.5.1" }, "name": "", - "signature": "sha256:c71f218a80ffc2fb08377daa20d703d7c421278e48d625c4f9fca8ff8f59d80a" + "signature": "sha256:7574bd022ee68fb7411f60cb675c158f5c1e80c5e79e3197073e2abf5d06262f" }, "nbformat": 3, "nbformat_minor": 0, @@ -447,7 +447,7 @@ "\n" ], "text": [ - " *' at 0x7f1de22e1870> >" + " *' at 0x7f2d78243480> >" ] } ], @@ -726,7 +726,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1082,7 +1082,7 @@ "" ], "text": [ - "" + "" ] } ], @@ -1152,7 +1152,7 @@ "\n" ], "text": [ - " *' at 0x7f1dd5f6a630> >" + " *' at 0x7f2d78197fc0> >" ] } ], @@ -1314,7 +1314,7 @@ "\n" ], "text": [ - " *' at 0x7f1de22e17e0> >" + " *' at 0x7f2d78243360> >" ] } ], @@ -1331,74 +1331,24 @@ "cell_type": "code", "collapsed": false, "input": [ - "a = spot.atomic_prop_collect(spot.formula('\"a < 2\" W \"b == 1\"'))\n", - "dir(a)" + "a = spot.atomic_prop_collect(spot.formula('\"a < 2\" W \"b == 1\"')); a" ], "language": "python", "metadata": {}, "outputs": [ { + "latex": [ + "$\\{``\\mathit{a < 2}\\textrm{''}, ``\\mathit{b == 1}\\textrm{''}\\}$" + ], "metadata": {}, "output_type": "pyout", - "prompt_number": 17, + "prompt_number": 14, "text": [ - "['__bool__',\n", - " '__class__',\n", - " '__contains__',\n", - " '__delattr__',\n", - " '__dict__',\n", - " '__dir__',\n", - " '__doc__',\n", - " '__eq__',\n", - " '__format__',\n", - " '__ge__',\n", - " '__getattribute__',\n", - " '__getitem__',\n", - " '__gt__',\n", - " '__hash__',\n", - " '__init__',\n", - " '__iter__',\n", - " '__le__',\n", - " '__len__',\n", - " '__lt__',\n", - " '__module__',\n", - " '__ne__',\n", - " '__new__',\n", - " '__nonzero__',\n", - " '__reduce__',\n", - " '__reduce_ex__',\n", - " '__repr__',\n", - " '__setattr__',\n", - " '__sizeof__',\n", - " '__str__',\n", - " '__subclasshook__',\n", - " '__swig_destroy__',\n", - " '__weakref__',\n", - " 'add',\n", - " 'append',\n", - " 'begin',\n", - " 'clear',\n", - " 'count',\n", - " 'discard',\n", - " 'empty',\n", - " 'end',\n", - " 'equal_range',\n", - " 'erase',\n", - " 'find',\n", - " 'insert',\n", - " 'iterator',\n", - " 'lower_bound',\n", - " 'rbegin',\n", - " 'rend',\n", - " 'size',\n", - " 'swap',\n", - " 'this',\n", - " 'thisown',\n", - " 'upper_bound']" + "{\"a < 2\", \"b == 1\"}" ] } ], - "prompt_number": 17 + "prompt_number": 14 }, { "cell_type": "code", From 4f913c7fb5d90fd0ca06709735488136521455d4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 29 Apr 2016 12:08:32 +0200 Subject: [PATCH 12/22] autfilt: fix simpification of exclusive AP * bin/autfilt.cc: Here. * tests/core/exclusive-tgba.test: Test it. * NEWS: Mention the fix. --- NEWS | 3 +++ bin/autfilt.cc | 11 ++++++++--- tests/core/exclusive-tgba.test | 15 ++++++++++++++- 3 files changed, 25 insertions(+), 4 deletions(-) diff --git a/NEWS b/NEWS index b7488181b..212bd4dad 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,9 @@ New in spot 2.0.0a (not yet released) * Typo in documentation of the -H option in --help output. * The automaton parser would choke on comments like /******/. * check_strength() should also set negated properties. + * Fix autfilt to apply --simplify-exclusive-ap only after + the simplifications of (--small/--deterministic) have + been performed. New in spot 2.0 (2016-04-11) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 54c9128cf..6ef36513d 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -711,12 +711,14 @@ namespace if (opt_mask_acc) aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); - if (!opt->excl_ap.empty()) - aut = opt->excl_ap.constrain(aut, opt_simplify_exclusive_ap); - if (!opt->rem_ap.empty()) aut = opt->rem_ap.strip(aut); + // opt_simplify_exclusive_ap is handled only after + // post-processing. + if (!opt->excl_ap.empty()) + aut = opt->excl_ap.constrain(aut, false); + if (opt_destut) aut = spot::closure(std::move(aut)); if (opt_instut == 1) @@ -755,6 +757,9 @@ namespace aut = post.run(aut, nullptr); + if (opt_simplify_exclusive_ap && !opt->excl_ap.empty()) + aut = opt->excl_ap.constrain(aut, opt_simplify_exclusive_ap); + if (randomize_st || randomize_tr) spot::randomize(aut, randomize_st, randomize_tr); diff --git a/tests/core/exclusive-tgba.test b/tests/core/exclusive-tgba.test index eb7a74263..59e0093f0 100755 --- a/tests/core/exclusive-tgba.test +++ b/tests/core/exclusive-tgba.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -160,3 +160,16 @@ run 0 autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ --simplify-exclusive-ap automaton >out2 cat out2 diff out2 expected-simpl + + +# Example from the paper +test "6,50,14" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' --stats='%s,%t,%e'` +test "6,24,12" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | + autfilt --exclusive-ap=a,b,c --stats='%s,%t,%e'` +test "5,22,10" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | + autfilt --small --exclusive-ap=a,b,c --stats='%s,%t,%e' --ap=3` +# The final automaton has 3 atomic propositions before +# simplifications, but only 2 after that. +ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | + autfilt --small --exclusive-ap=a,b,c --simplify-ex --ap=3 > out +test "5,21,10" = `autfilt out --stats='%s,%t,%e' --ap=2` From dad17b36b81b89a38a856b8e0f04d79e96b20a0c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 29 Apr 2016 18:07:44 +0200 Subject: [PATCH 13/22] honor ap() when counting transitions Fixing this bug alone revealed another bug: parsing never claim or LBTT automata did not register APs. So this fixes both bugs. This is the first part of #170. * spot/twa/twa.hh (register_aps_from_dict): New method. * spot/parseaut/parseaut.yy: Call it for never claim and LBTT files. * spot/twaalgos/stats.cc: Simplify using ap_vars(). * tests/core/ltl2tgba.test: Add a test case. * NEWS: Mention the bugs. --- NEWS | 6 ++++++ spot/parseaut/parseaut.yy | 2 ++ spot/twa/twa.hh | 28 ++++++++++++++++++++++++++++ spot/twaalgos/stats.cc | 19 +------------------ tests/core/ltl2tgba.test | 3 +++ 5 files changed, 40 insertions(+), 18 deletions(-) diff --git a/NEWS b/NEWS index 212bd4dad..865aa8c6a 100644 --- a/NEWS +++ b/NEWS @@ -17,6 +17,12 @@ New in spot 2.0.0a (not yet released) * Fix autfilt to apply --simplify-exclusive-ap only after the simplifications of (--small/--deterministic) have been performed. + * The automaton parser did not fully register atomic propositions + for automata read from never claim or as LBTT. + * The sub_stats_reachable() function used to count the number + of transitions based on the number of atomic propositions + actually *used* by the automaton instead of using the number + of AP declared. New in spot 2.0 (2016-04-11) diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 3f35edb44..46be5e95d 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1529,6 +1529,7 @@ never: "never" // Pretend that we have declared all states. for (auto& p: res.info_states) p.declared = true; + res.h->aut->register_aps_from_dict(); } nc-states: @@ -1750,6 +1751,7 @@ lbtt: lbtt-header lbtt-body ENDAUT res.info_states.resize(res.h->aut->num_states()); for (auto& s: res.info_states) s.declared = true; + res.h->aut->register_aps_from_dict(); } | lbtt-header-states LBTT_EMPTY { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 8d7ec3d7a..c213b9266 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -738,6 +738,34 @@ namespace spot } ///@} + + /// \brief Register all atomic propositions that have + /// already be register by the bdd_dict for this automaton. + /// + /// This method may only be called on an automaton with an empty + /// list of AP. It will fetch all atomic proposition that have + /// been set in the bdd_dict for this particular automaton. + /// + /// The typical use-case for this function is when the labels of + /// an automaton are created by functions such as + /// formula_to_bdd(). This is for instance done in the parser + /// for never claims or LBTT. + void register_aps_from_dict() + { + if (!aps_.empty()) + throw std::runtime_error("register_ap_from_dict() may not be" + " called on an automaton that has already" + " registered some AP"); + auto& m = get_dict()->bdd_map; + unsigned s = m.size(); + for (unsigned n = 0; n < s; ++n) + if (m[n].refs.find(this) != m[n].refs.end()) + { + aps_.push_back(m[n].f); + bddaps_ &= bdd_ithvar(n); + } + } + /// \brief The vector of atomic propositions registered by this /// automaton. const std::vector& ap() const diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index c3a8f14ec..e661e9252 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -62,7 +62,7 @@ namespace spot { public: sub_stats_bfs(const const_twa_ptr& a, twa_sub_statistics& s) - : stats_bfs(a, s), s_(s), seen_(bddtrue) + : stats_bfs(a, s), s_(s), seen_(a->ap_vars()) { } @@ -71,24 +71,7 @@ namespace spot const twa_succ_iterator* it) override { ++s_.edges; - bdd cond = it->cond(); - bdd newvars = bdd_exist(bdd_support(cond), seen_); - if (newvars != bddtrue) - { - seen_ &= newvars; - int count = 0; - while (newvars != bddtrue) - { - ++count; - newvars = bdd_high(newvars); - } - // If we discover one new variable, that means that all - // transitions we counted so far are actually double - // subtransitions. If we have two new variables, they where - // quadruple transitions, etc. - s_.transitions <<= count; - } while (cond != bddfalse) { cond -= bdd_satoneset(cond, seen_, bddtrue); diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index ec556f23c..c907c15d8 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -221,3 +221,6 @@ ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' # test unknown dot options ltl2tgba --dot=@ a 2>stderr && exit 1 grep 'ltl2tgba: unknown option.*@' stderr + +# Make sure the count of AP is correct through never claims or LBTT +ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1 From a1b3b065fa7fe4b3821ccc0c16ee8bb1b413e7f2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 30 Apr 2016 23:54:31 +0200 Subject: [PATCH 14/22] print_hoa: output all registered APs Also introduce twa::unregister_ap() and twa_graph::remove_unused_ap() so that the methods where this behavior is expected can be fixed. And fix ltsmin::kripke() which did not register APs. Part of #170. * spot/twaalgos/hoa.cc: Use apvars() to print all registerd APs. Throw an exception when printing automata using unregistered APs. * spot/ltsmin/ltsmin.cc: Call register_ap(). * spot/twa/twa.cc, spot/twa/twa.hh, spot/twa/twagraph.cc, spot/twa/twagraph.hh (twa::unregister_ap, twa_graph::remove_unused_ap): New methods. * spot/tl/exclusive.cc, spot/twaalgos/postproc.cc, spot/twaalgos/remprop.cc, spot/twaalgos/relabel.cc: Use them. * tests/core/maskacc.test, tests/core/maskkeep.test, tests/core/strength.test: Adjust expected results. * NEWS: Mention those changes. --- NEWS | 15 +++++++++++++++ spot/ltsmin/ltsmin.cc | 9 +++++++-- spot/tl/exclusive.cc | 5 +++-- spot/twa/twa.cc | 11 +++++++++++ spot/twa/twa.hh | 4 ++++ spot/twa/twagraph.cc | 22 ++++++++++++++++++++++ spot/twa/twagraph.hh | 6 ++++++ spot/twaalgos/hoa.cc | 16 +++++++++++++--- spot/twaalgos/postproc.cc | 3 +++ spot/twaalgos/relabel.cc | 6 +++--- spot/twaalgos/remprop.cc | 8 ++++---- tests/core/maskacc.test | 6 +++--- tests/core/maskkeep.test | 4 ++-- tests/core/strength.test | 30 +++++++++++++++--------------- 14 files changed, 111 insertions(+), 34 deletions(-) diff --git a/NEWS b/NEWS index 865aa8c6a..4ba38c360 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 2.0.0a (not yet released) + Library: + + * twa::unregister_ap() and twa_graph::remove_unused_ap() are new + methods introduced to fix some of the bugs below. + Documentation: * Add missing documentation for the option string passed to @@ -19,10 +24,20 @@ New in spot 2.0.0a (not yet released) been performed. * The automaton parser did not fully register atomic propositions for automata read from never claim or as LBTT. + * spot::ltsmin::kripke() had the same issue. * The sub_stats_reachable() function used to count the number of transitions based on the number of atomic propositions actually *used* by the automaton instead of using the number of AP declared. + * print_hoa() will now output all the atomic propositions that have + been registered, not only those that are used in the automaton. + (Note that it will also throw an exception if the automaton uses + an unregistered AP; this is how some of the above bugs were + found.) + * The for Small or Deterministic preference, the postprocessor + will now unregister atomic propositions that are no longer + used in labels. Simplification of exclusive properties + and remove_ap::strip() will do similarly. New in spot 2.0 (2016-04-11) diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index 4f9f2fe7f..86f6f14f2 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1103,8 +1103,13 @@ namespace spot dict->unregister_all_my_variables(iface.get()); throw; } - - return std::make_shared(iface, dict, ps, dead, compress); + auto res = std::make_shared(iface, dict, ps, dead, compress); + // All atomic propositions have been registered to the bdd_dict + // for iface, but we also need to add them to the automaton so + // twa::ap() works. + for (auto ap: *to_observe) + res->register_ap(ap); + return res; } ltsmin_model::~ltsmin_model() diff --git a/spot/tl/exclusive.cc b/spot/tl/exclusive.cc index abeed73a3..cb32b86f6 100644 --- a/spot/tl/exclusive.cc +++ b/spot/tl/exclusive.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -193,6 +193,7 @@ namespace spot res |= cube; cond = res; }); + res->remove_unused_ap(); } else { diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index b3fc0216f..afd4db00d 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -92,6 +92,17 @@ namespace spot return i->second.first; } + void + twa::unregister_ap(int b) + { + auto d = get_dict(); + assert(d->bdd_map[b].type == bdd_dict::var); + auto pos = std::find(aps_.begin(), aps_.end(), d->bdd_map[b].f); + assert(pos != aps_.end()); + aps_.erase(pos); + d->unregister_variable(b, this); + bddaps_ = bdd_exist(bddaps_, bdd_ithvar(b)); + } diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index c213b9266..3664d1ff9 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -738,6 +738,10 @@ namespace spot } ///@} + /// \brief Unregister an atomic proposition. + /// + /// \param num the BDD variable number returned by register_ap(). + void unregister_ap(int num); /// \brief Register all atomic propositions that have /// already be register by the bdd_dict for this automaton. diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 4a1d864ba..85481d4e6 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -287,4 +287,26 @@ namespace spot } g_.defrag_states(std::move(newst), used_states); } + + void twa_graph::remove_unused_ap() + { + if (ap().empty()) + return; + std::set conds; + bdd all = ap_vars(); + for (auto& e: g_.edges()) + { + all = bdd_exist(all, bdd_support(e.cond)); + if (all == bddtrue) // All letters are used. + return; + } + auto d = get_dict(); + while (all != bddtrue) + { + unregister_ap(bdd_var(all)); + all = bdd_high(all); + } + } + + } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index d6daf240e..bf093e168 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -441,6 +441,12 @@ namespace spot /// Remove all unreachable states. void purge_unreachable_states(); + /// \brief Remove unused atomic proposition + /// + /// Remove, from the list of atomic propositions registered by the + /// automaton, those that are not actually used by its labels. + void remove_unused_ap(); + acc_cond::mark_t state_acc_sets(unsigned s) const { assert((bool)prop_state_acc() || num_sets() == 0); diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 74a8bb128..821f1e9cc 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -67,7 +67,7 @@ namespace spot check_det_and_comp(aut); use_implicit_labels = implicit && is_deterministic && is_complete; use_state_labels &= state_labels; - number_all_ap(); + number_all_ap(aut); } std::ostream& @@ -164,12 +164,22 @@ namespace spot assert(state_acc || aut->prop_state_acc() != true); } - void number_all_ap() + void number_all_ap(const const_twa_graph_ptr& aut) { + // Make sure that the automaton uses only atomic propositions + // that have been registered via twa::register_ap() or some + // variant. If that is not the case, it is a bug that should + // be fixed in the function creating the automaton. Since + // that function could be written by the user, throw an + // exception rather than using an assert(). bdd all = bddtrue; for (auto& i: sup) all &= bdd_support(i.first); - all_ap = all; + all_ap = aut->ap_vars(); + if (bdd_exist(all, all_ap) != bddtrue) + throw std::runtime_error("print_hoa(): automaton uses " + "unregistered atomic propositions"); + all = all_ap; while (all != bddtrue) { diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 210b7af51..6c05a795e 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -223,6 +223,7 @@ namespace spot if (m->num_states() < a->num_states()) a = m; } + a->remove_unused_ap(); if (COMP_) a = complete(a); return a; @@ -478,6 +479,8 @@ namespace spot sim = dba ? dba : sim; + sim->remove_unused_ap(); + if (COMP_) sim = complete(sim); if (SBACC_) diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index f72fb0030..0c8fb29fe 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -38,6 +38,6 @@ namespace spot for (auto& t: aut->edges()) t.cond = bdd_replace(t.cond, pairs); for (auto v: vars) - d->unregister_variable(v, aut); + aut->unregister_ap(v); } } diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc index 0a0fa0821..f1d5ca53f 100644 --- a/spot/twaalgos/remprop.cc +++ b/spot/twaalgos/remprop.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -139,7 +139,7 @@ namespace spot if (v >= 0) { exist &= bdd_ithvar(v); - d->unregister_variable(v, res); + res->unregister_ap(v); } } for (auto ap: props_pos) @@ -148,7 +148,7 @@ namespace spot if (v >= 0) { restrict &= bdd_ithvar(v); - d->unregister_variable(v, res); + res->unregister_ap(v); } } for (auto ap: props_neg) @@ -157,7 +157,7 @@ namespace spot if (v >= 0) { restrict &= bdd_nithvar(v); - d->unregister_variable(v, res); + res->unregister_ap(v); } } diff --git a/tests/core/maskacc.test b/tests/core/maskacc.test index f5211ca08..c5eda7fb8 100755 --- a/tests/core/maskacc.test +++ b/tests/core/maskacc.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -95,7 +95,7 @@ cat >expect3 <expect1 < Date: Sun, 1 May 2016 18:35:55 +0200 Subject: [PATCH 15/22] * spot/misc/tmpfile.hh: Disallow copy. --- spot/misc/tmpfile.hh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/spot/misc/tmpfile.hh b/spot/misc/tmpfile.hh index 1a912bfe8..7bf887636 100644 --- a/spot/misc/tmpfile.hh +++ b/spot/misc/tmpfile.hh @@ -52,6 +52,9 @@ namespace spot typedef std::list::iterator cleanpos_t; SPOT_LOCAL temporary_file(char* name, cleanpos_t cp); + + temporary_file(const temporary_file& other) = delete; + virtual ~temporary_file() override; const char* name() const From 5e6d096e0fb566acf10635a54ad0009dcd6f6d2f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 May 2016 10:06:29 +0200 Subject: [PATCH 16/22] * doc/org/tools.org: Minor tweaks. --- doc/org/tools.org | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/doc/org/tools.org b/doc/org/tools.org index f3dfc641c..cb062df47 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -39,17 +39,17 @@ corresponding commands are hidden. * Command-line tools - [[file:randltl.org][=randltl=]] Generate random LTL/PSL formulas. -- [[file:ltlfilt.org][=ltlfilt=]] Filter and convert LTL/PSL formulas. +- [[file:ltlfilt.org][=ltlfilt=]] Filter, convert, and transform LTL/PSL formulas. - [[file:genltl.org][=genltl=]] Generate LTL formulas from scalable patterns. - [[file:ltl2tgba.org][=ltl2tgba=]] Translate LTL/PSL formulas into Büchi automata. - [[file:ltl2tgta.org][=ltl2tgta=]] Translate LTL/PSL formulas into Testing automata. - [[file:ltlcross.org][=ltlcross=]] Cross-compare LTL/PSL-to-automata translators. - [[file:ltlgrind.org][=ltlgrind=]] List formulas similar to but simpler than a given LTL/PSL - formula -- [[file:dstar2tgba.org][=dstar2tgba=]] Convert automata with any acceptance into variants of - Büchi automata. -- [[file:randaut.org][=randaut=]] Generate random automata. -- [[file:autfilt.org][=autfilt=]] Filter and transform automata. + formula. +- [[file:dstar2tgba.org][=dstar2tgba=]] Convert \omega-automata with any acceptance into + variants of Büchi automata. +- [[file:randaut.org][=randaut=]] Generate random \omega-automata. +- [[file:autfilt.org][=autfilt=]] Filter, convert, and transform \omega-automata. - [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]] and [[file:oaut.org][output]] interfaces. From d6e491a761699fd4bc043bbcffff3308e694f6ed Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 May 2016 10:12:32 +0200 Subject: [PATCH 17/22] doc: fix css to not highlight table row in man pages * doc/org/spot.css: Here. --- doc/org/spot.css | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/org/spot.css b/doc/org/spot.css index 49ca7598d..c30fa03c3 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -36,10 +36,10 @@ img{max-width:100%} } thead tr {background: #ffe35e;} -tbody:nth-child(odd) tr:nth-child(even) {background: #fff0a6;} -tbody:nth-child(odd) tr:nth-child(odd) {background: #fff7cf;} -tbody:nth-child(even) tr:nth-child(even) {background: #fff3bc;} -tbody:nth-child(even) tr:nth-child(odd) {background: #fffbe0;} +#content tbody:nth-child(odd) tr:nth-child(even) {background: #fff0a6;} +#content tbody:nth-child(odd) tr:nth-child(odd) {background: #fff7cf;} +#content tbody:nth-child(even) tr:nth-child(even) {background: #fff3bc;} +#content tbody:nth-child(even) tr:nth-child(odd) {background: #fffbe0;} .org-keyword{font-weight:bold} .org-builtin{font-weight:bold} .org-preprocessor{font-weight:bold} From 9149724617cb1c9ba4a38172c97054eb1d545db4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 2 May 2016 10:41:41 +0200 Subject: [PATCH 18/22] doc: add a spot(7) man page Suggested by Akim Demaille. Fixes #171. * bin/man/spot.x, bin/spot.cc: New files. * bin/man/Makefile.am, bin/Makefile.am: Add them. * doc/org/tools.org, NEWS: Mention the new page. --- NEWS | 3 ++ bin/Makefile.am | 13 ++++---- bin/man/Makefile.am | 6 +++- bin/man/spot.x | 28 ++++++++++++++++ bin/spot.cc | 78 +++++++++++++++++++++++++++++++++++++++++++++ doc/org/tools.org | 3 +- 6 files changed, 123 insertions(+), 8 deletions(-) create mode 100644 bin/man/spot.x create mode 100644 bin/spot.cc diff --git a/NEWS b/NEWS index 4ba38c360..55f8695eb 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,9 @@ New in spot 2.0.0a (not yet released) * Add missing documentation for the option string passed to spot::make_emptiness_check_instantiator(). + * There is a now a spot(7) man page listing all installed + command-line tools. + Python: * The tgba_determinize() function is now accessible in Python. diff --git a/bin/Makefile.am b/bin/Makefile.am index e0e4254f8..85e5ca059 100644 --- a/bin/Makefile.am +++ b/bin/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). +## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +## et Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -68,10 +68,10 @@ bin_PROGRAMS = \ randaut \ randltl -# Dummy program used just to generate man/spot-x.7 in a way that is -# consistent with the other man pages (e.g., with a version number that -# is automatically updated). -noinst_PROGRAMS = spot-x +# Dummy programs used just to generate man/spot-x.7 and man/spot.7 in +# a way that is consistent with the other man pages (e.g., with a +# version number that is automatically updated). +noinst_PROGRAMS = spot-x spot autfilt_SOURCES = autfilt.cc ltlfilt_SOURCES = ltlfilt.cc @@ -85,6 +85,7 @@ ltlgrind_SOURCES = ltlgrind.cc ltldo_SOURCES = ltldo.cc dstar2tgba_SOURCES = dstar2tgba.cc spot_x_SOURCES = spot-x.cc +spot_SOURCES = spot.cc ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME) EXTRA_DIST = options.py diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am index 3aa77de5a..b7c9f51bb 100644 --- a/bin/man/Makefile.am +++ b/bin/man/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -37,6 +37,7 @@ dist_man1_MANS = \ randaut.1 \ randltl.1 dist_man7_MANS = \ + spot.7 \ spot-x.7 MAINTAINERCLEANFILES = $(dist_man1_MANS) $(dist_man7_MANS) @@ -75,5 +76,8 @@ randaut.1: $(common_dep) $(srcdir)/randaut.x $(srcdir)/../randaut.cc spot-x.7: $(common_dep) $(srcdir)/spot-x.x $(srcdir)/../spot-x.cc $(convman7) ../spot-x$(EXEEXT) $(srcdir)/spot-x.x $@ +spot.7: $(common_dep) $(srcdir)/spot.x $(srcdir)/../spot.cc + $(convman7) ../spot$(EXEEXT) $(srcdir)/spot.x $@ + ltlgrind.1: $(common_dep) $(srcdir)/ltlgrind.x $(srcdir)/../ltlgrind.cc $(convman) ../ltlgrind$(EXEEXT) $(srcdir)/ltlgrind.x $@ diff --git a/bin/man/spot.x b/bin/man/spot.x new file mode 100644 index 000000000..f46305aa5 --- /dev/null +++ b/bin/man/spot.x @@ -0,0 +1,28 @@ +[NAME] +spot \- Command-line tools installed by Spot. + +[SYNOPSIS] + +Spot is a C++ library for ω-automata and LTL formulas manipulation. +It also comes with Python bindings and a set of command-line tools +that are listed below. + +[DESCRIPTION] +.\" Add any additional description here + +[SEE ALSO] +.BR randltl (1) +.BR genltl (1) +.BR ltlfilt (1) +.BR ltlrind (1) +.BR randaut (1) +.BR ltl2tgba (1) +.BR ltl2tgta (1) +.BR autfilt (1) +.BR ltlcross (1) +.BR ltldo (1) +.BR spot-x (7) + +.UR https://spot.lrde.epita.fr/ +The Spot web page. +.UE diff --git a/bin/spot.cc b/bin/spot.cc new file mode 100644 index 000000000..1478f1234 --- /dev/null +++ b/bin/spot.cc @@ -0,0 +1,78 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014, 2015, 2016 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 . + +#include "common_sys.hh" +#include +#include +#include +#include +#include "common_setup.hh" + +const char argp_program_doc[] ="Command-line tools installed by Spot."; + +#define DOC(NAME, TXT) NAME, 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, TXT, 0 + +static const argp_option options[] = + { + { nullptr, 0, nullptr, 0, "Tools that output LTL/PSL formulas:", 0 }, + { DOC("randltl", "Generate random LTL or PSL formulas.") }, + { DOC("genltl", "Generate LTL formulas from scalable patterns.") }, + { DOC("ltlfilt", "Filter, convert, and transform LTL or PSL formulas.") }, + { DOC("ltlgrind", "Mutate LTL or PSL formulas to generate similar but " + "simpler ones. Use this when looking for shorter formula to " + "reproduce a bug.") }, + { nullptr, 0, nullptr, 0, "Tools that output automata:", 0 }, + { DOC("randaut", "Generate random ω-automata.") }, + { DOC("ltl2tgba", "Convert LTL or PSL into variants of Transition-based " + "Generalized Büchi Automata.") }, + { DOC("ltl2tgta", "Convert LTL or PSL into variants of Transition-based " + "Generalized Testing Automata.") }, + { DOC("autfilt", "Filter, convert, and transform ω-automata.") }, + { DOC("dstar2tgba", "Convert ω-automata into variants of " + "Transition-based Büchi automata.") }, + { nullptr, 0, nullptr, 0, "Tools that run other tools:", 0 }, + { DOC("ltlcross", "Cross-compare translators of LTL or PSL formulas " + "into ω-automata, watch for bugs, and generate statistics.") }, + { DOC("ltldo", "Wrap any tool that inputs LTL or PSL formulas and possibly " + "outputs ω-automata; provides Spot's I/O interface.") }, + { nullptr, 0, nullptr, 0, nullptr, 0 } + }; + +const struct argp_child children[] = + { + { &misc_argp_hidden, 0, nullptr, -1 }, + { nullptr, 0, nullptr, 0 } + }; + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { options, nullptr, nullptr, argp_program_doc, children, + nullptr, nullptr }; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) + exit(err); + + std::cerr << "This binary serves no purpose other than generating" + << " the spot.7 manpage.\n"; + + return 1; +} diff --git a/doc/org/tools.org b/doc/org/tools.org index cb062df47..acdcaa0e9 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -71,7 +71,8 @@ convenience, you can browse their HTML versions: [[./man/ltlfilt.1.html][=ltlfilt=]](1), [[./man/randaut.1.html][=randaut=]](1), [[./man/randltl.1.html][=randltl=]](1), -[[./man/spot-x.7.html][=spot-x=]](7). +[[./man/spot-x.7.html][=spot-x=]](7), +[[./man/spot.7.html][=spot=]](7). * Advanced use-cases From 465fda2b356d3f0a0cdf5d4c57905db2f7157ce5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 May 2016 14:06:01 +0200 Subject: [PATCH 19/22] * bin/man/genltl.x: Typo. --- bin/man/genltl.x | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/bin/man/genltl.x b/bin/man/genltl.x index cd83cbdcb..64e4d9d61 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -17,7 +17,7 @@ J. Geldenhuys and H. Hansen: Larger automata and less work for LTL model checking. Proceedings of Spin'06. LNCS 3925. .TP ccj -J. Cichoń, A. Czubak, and A. Jasiński (DepCoS'09): Minimal Büchi +J. Cichoń, A. Czubak, and A. Jasiński: Minimal Büchi Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS'09. .TP go From 4cc6df102a3d07152b2eebb553dc43f0cef62106 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 May 2016 18:11:46 +0200 Subject: [PATCH 20/22] bench: fix bench/ltl2tgba for new bin location * bench/ltl2tgba/Makefile.am, bench/ltl2tgba/defs.in: Update location of tools. * NEWS: Mention the fix. --- NEWS | 2 ++ bench/ltl2tgba/Makefile.am | 8 ++++---- bench/ltl2tgba/defs.in | 11 ++++++----- 3 files changed, 12 insertions(+), 9 deletions(-) diff --git a/NEWS b/NEWS index 55f8695eb..c44404b37 100644 --- a/NEWS +++ b/NEWS @@ -41,6 +41,8 @@ New in spot 2.0.0a (not yet released) will now unregister atomic propositions that are no longer used in labels. Simplification of exclusive properties and remove_ap::strip() will do similarly. + * bench/ltl2tgba/ was not working since the source code + reorganization of 1.99.7. New in spot 2.0 (2016-04-11) diff --git a/bench/ltl2tgba/Makefile.am b/bench/ltl2tgba/Makefile.am index 74150d0af..9bccb4c63 100644 --- a/bench/ltl2tgba/Makefile.am +++ b/bench/ltl2tgba/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2013 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). +## Copyright (C) 2013, 2016 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -42,13 +42,13 @@ json: $(OUTJSON) deps = $(srcdir)/tools \ $(top_srcdir)/configure.ac \ - $(top_builddir)/src/bin/ltl2tgba + $(top_builddir)/bin/ltl2tgba small.json: $(srcdir)/small $(deps) $(srcdir)/small big.json: $(srcdir)/big $(deps) $(srcdir)/big -known.json: $(srcdir)/known $(srcdir)/formulae.ltl $(deps) +known.json: $(srcdir)/known $(deps) $(srcdir)/known results.tex: $(srcdir)/sum.py $(OUTJSON) diff --git a/bench/ltl2tgba/defs.in b/bench/ltl2tgba/defs.in index ad2de6b6f..ba0dac903 100644 --- a/bench/ltl2tgba/defs.in +++ b/bench/ltl2tgba/defs.in @@ -1,5 +1,5 @@ # -*- mode: shell-script; coding: utf-8 -*- -# Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2013, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -36,13 +36,14 @@ test -f "$srcdir/defs.in" || { top_builddir="@top_builddir@" LBT="@LBT@" -LTLCROSS="$top_builddir/src/bin/ltlcross@EXEEXT@" -LTLFILT="$top_builddir/src/bin/ltlfilt@EXEEXT@" -RANDLTL="$top_builddir/src/bin/randltl@EXEEXT@" +LTLCROSS="$top_builddir/bin/ltlcross@EXEEXT@" +LTLFILT="$top_builddir/bin/ltlfilt@EXEEXT@" +RANDLTL="$top_builddir/bin/randltl@EXEEXT@" +GENLTL="$top_builddir/bin/genltl@EXEEXT@" LTL2BA="@LTL2BA@" LTL3BA="@LTL3BA@" LTL2NBA="@LTL2NBA@" -LTL2TGBA="@top_builddir@/src/bin/ltl2tgba@EXEEXT@" +LTL2TGBA="@top_builddir@/bin/ltl2tgba@EXEEXT@" MODELLA="@MODELLA@" SPIN="@SPIN@" WRING2LBTT="@WRING2LBTT@" From cfd4a1b98d9ba0e4e7e503416039ff21383765ae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 May 2016 09:33:24 +0200 Subject: [PATCH 21/22] Release Spot 2.0.1 * NEWS, configure.ac, doc/org/setup.org: Update. --- NEWS | 10 +++++----- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/NEWS b/NEWS index c44404b37..6f29395f3 100644 --- a/NEWS +++ b/NEWS @@ -1,16 +1,16 @@ -New in spot 2.0.0a (not yet released) +New in spot 2.0.1 (2016-05-09) Library: * twa::unregister_ap() and twa_graph::remove_unused_ap() are new - methods introduced to fix some of the bugs below. + methods introduced to fix some of the bugs listed below. Documentation: * Add missing documentation for the option string passed to spot::make_emptiness_check_instantiator(). - * There is a now a spot(7) man page listing all installed + * There is now a spot(7) man page listing all installed command-line tools. Python: @@ -19,7 +19,6 @@ New in spot 2.0.0a (not yet released) Bug fixes: - * Typo in documentation of the -H option in --help output. * The automaton parser would choke on comments like /******/. * check_strength() should also set negated properties. * Fix autfilt to apply --simplify-exclusive-ap only after @@ -37,12 +36,13 @@ New in spot 2.0.0a (not yet released) (Note that it will also throw an exception if the automaton uses an unregistered AP; this is how some of the above bugs were found.) - * The for Small or Deterministic preference, the postprocessor + * For Small or Deterministic preference, the postprocessor will now unregister atomic propositions that are no longer used in labels. Simplification of exclusive properties and remove_ap::strip() will do similarly. * bench/ltl2tgba/ was not working since the source code reorganization of 1.99.7. + * Various typos and minor documentation fixes. New in spot 2.0 (2016-04-11) diff --git a/configure.ac b/configure.ac index e78e4a11c..8933c0c22 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.0.0a], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.0.1], [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 fea69f133..fc75f5d4c 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.0 -#+MACRO: LASTRELEASE 2.0 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.0.tar.gz][=spot-2.0.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2016-04-11 +#+MACRO: SPOTVERSION 2.0.1 +#+MACRO: LASTRELEASE 2.0.1 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.0.1.tar.gz][=spot-2.0.1.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0-1/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2016-05-09 From bd5ac37e7cd4d3f56a87f965e417ba8e6f0f2c77 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 May 2016 09:42:20 +0200 Subject: [PATCH 22/22] * configure.ac: Bump version number. --- configure.ac | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ac b/configure.ac index 8933c0c22..63ba9b33d 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.0.1], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.0.1a], [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])