From 8edd0648590ba696321d0b95a73a60b147b4a87d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jul 2018 22:19:15 +0200 Subject: [PATCH 01/19] * doc/tl/tl.tex: Convert to utf-8. --- doc/tl/tl.tex | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 5cdde599a..08f597a28 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -2,7 +2,7 @@ \documentclass[a4paper,twoside,10pt,DIV=12]{scrreprt} \usepackage[stretch=10]{microtype} \usepackage[american]{babel} -\usepackage[latin1]{inputenc} +\usepackage[utf8]{inputenc} \usepackage{amsmath} \usepackage{amsfonts} \usepackage[sc]{mathpazo} @@ -983,7 +983,7 @@ right & $\U,\,\W,\,\M,\,\R$ Beware that not all tools agree on the associativity of these operators. For instance Spin, ltl2ba (same parser as spin), Wring, psl2ba, Modella, and NuSMV all have $\U$ and $\R$ as left-associative, -while Goal (hence Büchi store), LTL2AUT, and LTL2Büchi (from +while Goal (hence Büchi store), LTL2AUT, and LTL2Büchi (from JavaPathFinder) have $\U$ and $\R$ as right-associative. Vis and LBTT have these two operators as non-associative (parentheses required). Similarly the tools do not aggree on the associativity of $\IMPLIES$ @@ -1137,13 +1137,13 @@ rules: \node[align=center] (saf) at (1,1) {Safety\\ $\G p$}; \node[align=center] (gua) at (5,1) {Guarantee\\ $\F p$}; - \node[align=right,below left] (det) at (-.2,6.7) {Deterministic\\Büchi\\Automata}; - \node[align=left,below right](weak) at (6.2,6.7) {Weak Büchi\\Automata}; - \node[align=left,right](wdba) at (6.2,4.3) {Weak\\Deterministic\\Büchi\\Automata}; - \node[align=left,above right](ter) at (6.2,1.7) {Terminal\\Büchi\\Automata}; - \node[align=right,above left](occ) at (-.2,2) {Terminal\\co-Büchi\\Automata}; + \node[align=right,below left] (det) at (-.2,6.7) {Deterministic\\Büchi\\Automata}; + \node[align=left,below right](weak) at (6.2,6.7) {Weak Büchi\\Automata}; + \node[align=left,right](wdba) at (6.2,4.3) {Weak\\Deterministic\\Büchi\\Automata}; + \node[align=left,above right](ter) at (6.2,1.7) {Terminal\\Büchi\\Automata}; + \node[align=right,above left](occ) at (-.2,2) {Terminal\\co-Büchi\\Automata}; - \node[above right] (buc) at (3.35,7) {General Büchi Automata}; + \node[above right] (buc) at (3.35,7) {General Büchi Automata}; \draw[annote] (rec) -- (det); \draw[annote] (per) -- (weak); @@ -1961,4 +1961,5 @@ $f_1\AND f_2$ & \bor{f_1}{g}{f_2}{g} & & & %%% Local Variables: %%% mode: latex %%% TeX-master: t +%%% coding: utf-8 %%% End: From 8d475780d29e1d826c695080690005a2e6f17198 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Mon, 9 Jul 2018 11:13:16 +0200 Subject: [PATCH 02/19] * HACKING: typos --- HACKING | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/HACKING b/HACKING index 4d0265ea8..b8a44ff8c 100644 --- a/HACKING +++ b/HACKING @@ -12,9 +12,9 @@ The GIT repository can be cloned with git clone https://gitlab.lrde.epita.fr/spot/spot.git Some files in SPOT's source tree are generated. They are distributed -so that users do not need to tools to rebuild them, but we don't keep -all of them under GIT because it can generate lots of changes or -conflicts. +so that users do not need to install tools to rebuild them, but we +don't keep all of them under GIT because it can generate lots of +changes or conflicts. Here are the tools you need to bootstrap the GIT tree, or more generally if you plan to regenerate some of the generated files. @@ -613,7 +613,7 @@ SPOT macros some header file. See "Assertions" above. * Use SPOT_LIKELY / SPOT_UNLIKELY in case you need to help the - compiler figure out the commont output of a test. Do not abuse + compiler figure out the common output of a test. Do not abuse this without checking the assembly output to make sure the effect is what you desired. @@ -624,7 +624,7 @@ Other style recommandations Feel free to replace these by uses of C++11's nullptr instead. * Limit the scope of local variables by defining them as late as - possible. Do not reuse a local variables for two different things. + possible. Do not reuse a local variable for two different things. * Do not systematically initialize local variables with 0 or other meaningless values. This hides errors to valgrind. From b8aae428e5a5a85b8ef08bcc211cb6b0e964499e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Jul 2018 17:28:43 +0200 Subject: [PATCH 03/19] org: add missing documentation for prop_complete * doc/org/concepts.org: Here. --- doc/org/concepts.org | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 96ae13577..7df9f5880 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1067,6 +1067,7 @@ automaton, and that can be queried or set by algorithms: | =weak= | transitions of an SCC all belong to the same acceptance sets | | =very_weak= | weak automaton where all SCCs have size 1 | | =terminal= | automaton is weak, accepting SCCs are complete, accepting edges may not go to rejecting SCCs | +| =complete= | for any letter â„“, each state has is at least one outgoing transition compatible with â„“ | | =deterministic= | there is at most one run *recognizing* a word, but not necessarily accepting it | | =semi_deterministic= | any nondeterminism occurs before entering an accepting SCC | | =unambiguous= | there is at most one run *accepting* a word (but it might be recognized several time) | From 1edb47ad5b2ad1668f9b9ea10f3f07114fc0863b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 Jul 2018 15:43:01 +0200 Subject: [PATCH 04/19] fix two issues related to jupyter notebook execution * tests/python/ipnbdoctest.py: Invert diffs inputs. * tests/run.in: Run notebooks with PYTHONIOENCODING=utf-8:surrogateescape to avoid exceptions when trying to display utf-8 characters on ascii terminals. --- tests/python/ipnbdoctest.py | 2 +- tests/run.in | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index dc05fce22..a218a2fa8 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -278,7 +278,7 @@ def test_notebook(ipynb): print("output length mismatch (expected {}, got {})".format( len(cell.outputs), len(outs))) failed = True - if not compare_outputs(outs, cell.outputs): + if not compare_outputs(cell.outputs, outs): failed = True print("cell %d: " % i, end="") if failed: diff --git a/tests/run.in b/tests/run.in index 77263f8f9..ecfff458a 100755 --- a/tests/run.in +++ b/tests/run.in @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2014, 2015, 2016 Laboratoire de Recherche et -# Developpement de l'EPITA (LRDE). +# Copyright (C) 2010, 2011, 2014-2016, 2018 Laboratoire de Recherche +# et Developpement 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. @@ -92,6 +92,7 @@ export srcdir case $1 in *.ipynb) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ + PYTHONIOENCODING=utf-8:surrogateescape \ exec $PREFIXCMD @PYTHON@ @abs_srcdir@/python/ipnbdoctest.py "$@";; *.py) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ From b33a88d8bb8074ca681178b09f214194ae524fdc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 18 Jul 2018 17:39:02 +0200 Subject: [PATCH 05/19] escape_rfc4180: document relation with std::quote * spot/misc/escape.hh: Here. --- spot/misc/escape.hh | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/spot/misc/escape.hh b/spot/misc/escape.hh index 4fb777a38..6f76d7bab 100644 --- a/spot/misc/escape.hh +++ b/spot/misc/escape.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2015 Laboratoire de Recherche et +// Copyright (C) 2011-2013, 2015, 2018 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -35,6 +35,15 @@ namespace spot /// /// In CSV files, as defined by RFC4180, double-quoted string that /// contain double-quotes should simply duplicate those quotes. + /// + /// Note that in C++14, + /// ``` + /// os << std::quoted(str, '"', '"'); + /// ``` + /// outputs the same result as + /// ``` + /// escape_rfc4180(os << '"', str) << '"'; + /// ``` SPOT_API std::ostream& escape_rfc4180(std::ostream& os, const std::string& str); From acf254243bb7905399343ef4c54ed48386e197c1 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Fri, 20 Jul 2018 15:55:27 +0200 Subject: [PATCH 06/19] remove useless forward declaration * spot/ta/taexplicit.hh, spot/twaalgos/compsusp.hh, spot/twaalgos/isunamb.hh, spot/twaalgos/word.hh: Here. --- spot/ta/taexplicit.hh | 3 +-- spot/twaalgos/compsusp.hh | 4 +--- spot/twaalgos/isunamb.hh | 4 +--- spot/twaalgos/word.hh | 4 +--- 4 files changed, 4 insertions(+), 11 deletions(-) diff --git a/spot/ta/taexplicit.hh b/spot/ta/taexplicit.hh index 2778d7628..4f833329a 100644 --- a/spot/ta/taexplicit.hh +++ b/spot/ta/taexplicit.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2018 Laboratoire // de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -32,7 +32,6 @@ namespace spot { // Forward declarations. See below. class state_ta_explicit; - class ta_explicit_succ_iterator; class ta_explicit; /// Explicit representation of a spot::ta. diff --git a/spot/twaalgos/compsusp.hh b/spot/twaalgos/compsusp.hh index 08ed354e7..4da48f0e8 100644 --- a/spot/twaalgos/compsusp.hh +++ b/spot/twaalgos/compsusp.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -24,8 +24,6 @@ namespace spot { - class bdd_dict; - /// \brief Compositional translation algorithm with resetable /// suspension. /// diff --git a/spot/twaalgos/isunamb.hh b/spot/twaalgos/isunamb.hh index da243ddc0..4ec9c48f8 100644 --- a/spot/twaalgos/isunamb.hh +++ b/spot/twaalgos/isunamb.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement +// Copyright (C) 2013, 2015, 2018 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -23,8 +23,6 @@ namespace spot { - class tgba; - /// \addtogroup twa_misc /// @{ diff --git a/spot/twaalgos/word.hh b/spot/twaalgos/word.hh index 7372401f0..419b144de 100644 --- a/spot/twaalgos/word.hh +++ b/spot/twaalgos/word.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -23,8 +23,6 @@ namespace spot { - class bdd_dict; - /// \brief An infinite word stored as a lasso. /// /// This is not exactly a word in the traditional sense because we From e0b10d847aa22aa0abc5eda6632176f4e1683950 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Fri, 20 Jul 2018 16:21:01 +0200 Subject: [PATCH 07/19] remove duplicated includes * spot/graph/graph.hh, spot/taalgos/tgba2ta.cc, spot/tl/formula.hh, spot/twaalgos/dot.cc, spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/ndfs_result.hxx, spot/twaalgos/powerset.cc, spot/twaalgos/stutter.cc: Here. --- spot/graph/graph.hh | 1 - spot/taalgos/tgba2ta.cc | 1 - spot/tl/formula.hh | 1 - spot/twaalgos/dot.cc | 1 - spot/twaalgos/ltl2tgba_fm.cc | 1 - spot/twaalgos/ndfs_result.hxx | 2 -- spot/twaalgos/powerset.cc | 2 -- spot/twaalgos/stutter.cc | 2 -- 8 files changed, 11 deletions(-) diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index b1d235123..90df64282 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -28,7 +28,6 @@ #include #include #include -#include namespace spot { diff --git a/spot/taalgos/tgba2ta.cc b/spot/taalgos/tgba2ta.cc index 4df1a8ce8..b2d499e54 100644 --- a/spot/taalgos/tgba2ta.cc +++ b/spot/taalgos/tgba2ta.cc @@ -29,7 +29,6 @@ #include #include -#include #include #include #include diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 53b0a41d1..876480c37 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -55,7 +55,6 @@ #include #include #include -#include #include namespace spot diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 3ee7174d1..86465dc18 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -29,7 +29,6 @@ #include #include #include -#include #include #include #include diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index a3bd4e776..acf67e9e6 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -28,7 +28,6 @@ #include #include #include -#include #include #include #include diff --git a/spot/twaalgos/ndfs_result.hxx b/spot/twaalgos/ndfs_result.hxx index a0a3c49f0..5bf649768 100644 --- a/spot/twaalgos/ndfs_result.hxx +++ b/spot/twaalgos/ndfs_result.hxx @@ -38,8 +38,6 @@ #include #include #include -#include - namespace spot { diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index aedf96d76..e2ceb518d 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -26,13 +26,11 @@ #include #include #include -#include #include #include #include #include #include -#include #include #include #include diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index 47a09454f..1aab344bd 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -32,8 +32,6 @@ #include #include #include -#include -#include #include #include #include From 85eff247b2ea97e967156a65a55ca90918dedc1f Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Fri, 20 Jul 2018 16:56:19 +0200 Subject: [PATCH 08/19] HACKING: directory has moved * HACKING: Here. --- HACKING | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HACKING b/HACKING index b8a44ff8c..6d8ad16c3 100644 --- a/HACKING +++ b/HACKING @@ -350,7 +350,7 @@ Exporting symbols * If a symbol could be used by several modules of the library but should still be private to the library, use a *.hh/*.cc pair of files, but list both files in the _SOURCES variable of that - directory (see for instance weight.hh in tgbaalgos/Makefile.am). + directory (see for instance weight.hh in priv/Makefile.am). This will ensure that the header is not installed. Needless to say, no public header should include such a private header. From d5ffdb60b5e53472e0f9fd279dcade54d63958df Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Jul 2018 09:50:31 +0200 Subject: [PATCH 09/19] * spot/twa/twa.cc: Typo. --- spot/twa/twa.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 7633a8b0f..8c0cb1a7d 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -85,7 +85,7 @@ namespace spot { if (acc().uses_fin_acceptance()) throw std::runtime_error("twa::accepting_run() does not work with " - "Fin acceptance (but twa:is_empty() and " + "Fin acceptance (but twa::is_empty() and " "twa::accepting_word() can)"); auto res = couvreur99_new_check(shared_from_this()); if (!res) From 79a62ae1c9944a061301bb87758ac5774d630412 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Jul 2018 14:52:14 +0200 Subject: [PATCH 10/19] ltlfilt: introduce --suspendable * bin/ltlfilt.cc: Add the option. * tests/core/ltlfilt.test: Use it. * NEWS: Mention it. --- NEWS | 5 ++++- bin/ltlfilt.cc | 7 +++++++ tests/core/ltlfilt.test | 5 +++++ 3 files changed, 16 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 786df0418..41fc89e62 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,9 @@ New in spot 2.6.0.dev (not yet released) - Nothing yet. + Command-line tools: + + - "ltlfilt --suspendable" is now a synonym for + "ltlfilt --universal --eventual". New in spot 2.6 (2018-07-04) diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index f44dfe82d..460d31c13 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -100,6 +100,7 @@ enum { OPT_SIZE_MIN, OPT_SKIP_ERRORS, OPT_STUTTER_INSENSITIVE, + OPT_SUSPENDABLE, OPT_SYNTACTIC_GUARANTEE, OPT_SYNTACTIC_OBLIGATION, OPT_SYNTACTIC_PERSISTENCE, @@ -167,6 +168,8 @@ static const argp_option options[] = { "eventual", OPT_EVENTUAL, nullptr, 0, "match pure eventualities", 0 }, { "universal", OPT_UNIVERSAL, nullptr, 0, "match purely universal formulas", 0 }, + { "suspendable", OPT_SUSPENDABLE, nullptr, 0, + "synonym for --universal --eventual", 0 }, { "syntactic-safety", OPT_SYNTACTIC_SAFETY, nullptr, 0, "match syntactic-safety formulas", 0 }, { "syntactic-guarantee", OPT_SYNTACTIC_GUARANTEE, nullptr, 0, @@ -507,6 +510,10 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_AP_N: ap_n = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_SUSPENDABLE: + universal = true; + eventual = true; + break; case OPT_SYNTACTIC_SAFETY: syntactic_safety = true; break; diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 063c01159..3ab827c3f 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -84,6 +84,11 @@ GFa | FGb F(GFa | Gb) EOF +checkopt --suspendable < Date: Tue, 24 Jul 2018 16:53:30 +0200 Subject: [PATCH 11/19] * .gitlab-ci.yml (debpkg-stable): Typo. --- .gitlab-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8cbdd73bb..e8b4d425a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -164,7 +164,7 @@ debpkg-stable: - docker volume create $vol - exitcode=0 - docker run --rm=true -v $vol:/build/result gadl/spot-debuild:stable ./build-spot.sh $CI_COMMIT_REF_NAME -j${NBPROC-1} || exitcode=$? - - docker run --rm=true -v $vol:/build/result gadl/spot-debuild-i386:stable ./bin-spot.sh -j${NBPROC-1} || exitcode=$ + - docker run --rm=true -v $vol:/build/result gadl/spot-debuild-i386:stable ./bin-spot.sh -j${NBPROC-1} || exitcode=$? - docker run -v $vol:/build/result --name helper-$vol gadl/spot-debuild:stable true || exitcode=$? - docker cp helper-$vol:/build/result _build_stable || exitcode=$? - docker rm helper-$vol || exitcode=$? From b2e51545f9496f995ae55f5b2a5db10569660878 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Jul 2018 14:04:52 +0200 Subject: [PATCH 12/19] scc_info: fix split_on_sets * spot/twaalgos/sccinfo.cc (split_on_sets): Correctly register APs. * tests/python/sccsplit.py: New file. * tests/Makefile.am: Add it. * NEWS: Mention the bug. --- NEWS | 5 +++++ spot/twaalgos/sccinfo.cc | 1 + tests/Makefile.am | 1 + tests/python/sccsplit.py | 30 ++++++++++++++++++++++++++++++ 4 files changed, 37 insertions(+) create mode 100644 tests/python/sccsplit.py diff --git a/NEWS b/NEWS index 41fc89e62..8993cb368 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,11 @@ New in spot 2.6.0.dev (not yet released) - "ltlfilt --suspendable" is now a synonym for "ltlfilt --universal --eventual". + Bugs fixed: + + - scc_info::split_on_sets() did not correctly register the + atomic propositions of the returned automata. + New in spot 2.6 (2018-07-04) Command-line tools: diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index a9597a2dc..23f01c533 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -532,6 +532,7 @@ namespace spot cur.assign(aut_->num_states(), false); auto copy = make_twa_graph(aut_->get_dict()); + copy->copy_ap_of(aut_); copy->copy_acceptance_of(aut_); copy->prop_state_acc(aut_->prop_state_acc()); transform_accessible(aut_, copy, [&](unsigned src, diff --git a/tests/Makefile.am b/tests/Makefile.am index 6e2a48ff3..7de53f77f 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -397,6 +397,7 @@ TESTS_python = \ python/sbacc.py \ python/sccfilter.py \ python/sccinfo.py \ + python/sccsplit.py \ python/semidet.py \ python/setacc.py \ python/setxor.py \ diff --git a/tests/python/sccsplit.py b/tests/python/sccsplit.py new file mode 100644 index 000000000..cf8c0e33d --- /dev/null +++ b/tests/python/sccsplit.py @@ -0,0 +1,30 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2018 Laboratoire de Recherche et Développement de +# l'EPITA. +# +# 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('GF(a <-> Xa) & GF(b <-> XXb)') +si = spot.scc_info(aut) +s = "" +for aut2 in si.split_on_sets(0, [0]): + # This call to to_str() used to fail because split_on_sets had not + # registered the atomic propositions of aut + s += aut2.to_str(); +assert spot.automaton(s).num_states() == 8 From 483b05c5501c161dc235ee48dd0093b0cf36f1a5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Jul 2018 17:02:52 +0200 Subject: [PATCH 13/19] * spot/twaalgos/translate.cc: Typos in comments. --- spot/twaalgos/translate.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index b7e3e13a8..806aa522b 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -163,7 +163,7 @@ namespace spot } if (r2.is_syntactic_obligation() || !r2.is(op::And, op::Or) || // For TGBA/BA we only do conjunction. There is nothing wrong - // with disjunction, but it seems to generated larger automata + // with disjunction, but it seems to generate larger automata // in many cases and it needs to be further investigated. Maybe // this could be relaxed in the case of deterministic output. (r2.is(op::Or) && (type_ == TGBA || type_ == BA))) @@ -189,8 +189,7 @@ namespace spot if (!susp.empty()) { // The only cases where we accept susp and rest to be both - // non-empty is when doing arbitrary acceptance, or when doing - // Generic or TGBA. + // non-empty is when doing Generic acceptance or TGBA. if (!rest.empty() && !(type_ == Generic || type_ == TGBA)) { rest.insert(rest.end(), susp.begin(), susp.end()); From d8419db61818a79cee28cd9bcd0bf2634e6888cf Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Sat, 28 Jul 2018 16:46:41 +0200 Subject: [PATCH 14/19] * spot/twa/acc.hh: fix constness --- spot/twa/acc.hh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index c0c1e410f..291212829 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -729,14 +729,14 @@ namespace spot return *this; } - acc_code operator&(const acc_code& r) + acc_code operator&(const acc_code& r) const { acc_code res = *this; res &= r; return res; } - acc_code operator&(acc_code&& r) + acc_code operator&(acc_code&& r) const { acc_code res = *this; res &= r; @@ -829,14 +829,14 @@ namespace spot return *this; } - acc_code operator|(acc_code&& r) + acc_code operator|(acc_code&& r) const { acc_code res = *this; res |= r; return res; } - acc_code operator|(const acc_code& r) + acc_code operator|(const acc_code& r) const { acc_code res = *this; res |= r; From 126d392355c48e204eb918cd3d174f0637bc6f53 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 1 Aug 2018 15:00:45 +0200 Subject: [PATCH 15/19] tl: add some implication-based rewritings for "<->", "->", and "xor" This prevents an exception from being raised if NNF is not performed on Boolean properties and implication-based checks are used. * NEWS: Mention the issue. * spot/tl/simplify.cc, doc/tl/tl.tex: Add some rules. * tests/python/ltlsimple.py: Test them. --- NEWS | 7 +++ doc/tl/tl.tex | 108 ++++++++++++++++++++------------------ spot/tl/simplify.cc | 34 ++++++++++-- tests/python/ltlsimple.py | 22 +++++++- 4 files changed, 113 insertions(+), 58 deletions(-) diff --git a/NEWS b/NEWS index 8993cb368..0c687ce22 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,13 @@ New in spot 2.6.0.dev (not yet released) - scc_info::split_on_sets() did not correctly register the atomic propositions of the returned automata. + - The spot::tl_simplifier class could raise an exception while + attempting to reduce formulas containing unsimplified <->, -> or + xor, if options nenoform_stop_on_boolean and synt_impl are both + set. (This combinations of options is not available from + command-line tools.) + + New in spot 2.6 (2018-07-04) Command-line tools: diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 08f597a28..7dd243292 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1744,58 +1744,62 @@ are counted as one. \begingroup \allowdisplaybreaks \begin{alignat*}{3} -\text{if~} & f\simp \NOT g && \text{~then~} & f\OR g & \equiv \1 \\ -\text{if~} & f\simp \NOT g && \text{~then~} & f\AND g & \equiv \0 \\ -\text{if~} & \flessg && \text{~then~} & f\OR g & \equiv f \\ -\text{if~} & f\simp g && \text{~then~} & f\OR g & \equiv g \\ -\text{if~} & \glessf && \text{~then~} & f\AND g & \equiv g \\ -\text{if~} & f\simp g && \text{~then~} & f\AND g & \equiv f \\ -\text{if~} & \flessg && \text{~then~} & f\U g & \equiv f \\ -\text{if~} & f\simp g && \text{~then~} & f\U g & \equiv g \\ -\text{if~} & (f\U g)\Simp g && \text{~then~} & f\U g & \equiv g \\ -\text{if~} & (\NOT f)\simp g && \text{~then~} & f\U g & \equiv \F g \\ -\text{if~} & g\simp e && \text{~then~} & e\U g & \equiv \F g \\ -\text{if~} & f\simp g && \text{~then~} & f\U (g \U h) & \equiv g \U h \\ -\text{if~} & f\simp g && \text{~then~} & f\U (g \W h) & \equiv g \W h \\ -\text{if~} & g\simp f && \text{~then~} & f\U (g \U h) & \equiv f \U h \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \U k)) & \equiv g \R (h \U k) \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \R (h \W k)) & \equiv g \R (h \W k) \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \U k)) & \equiv g \M (h \U k) \\ -\text{if~} & f\simp h && \text{~then~} & f\U (g \M (h \W k)) & \equiv g \M (h \W k) \\ -\text{if~} & f\simp h && \text{~then~} & (f\U g) \U h & \equiv g \U h \\ -\text{if~} & f\simp h && \text{~then~} & (f\W g) \U h & \equiv g \U h \\ -\text{if~} & g\simp h && \text{~then~} & (f\U g) \U h & \equiv (f \U g) \OR h \\ -\text{if~} & (\NOT f)\simp g && \text{~then~} & f\W g & \equiv \1 \\ -\text{if~} & \flessg && \text{~then~} & f\W g & \equiv f \\ -\text{if~} & f\simp g && \text{~then~} & f\W g & \equiv g \\ -\text{if~} & (f\W g)\Simp g && \text{~then~} & f\W g & \equiv g \\ -\text{if~} & f\simp g && \text{~then~} & f\W (g \W h) & \equiv g \W h \\ -\text{if~} & g\simp f && \text{~then~} & f\W (g \U h) & \equiv f \W h \\ -\text{if~} & g\simp f && \text{~then~} & f\W (g \W h) & \equiv f \W h \\ -\text{if~} & f\simp h && \text{~then~} & (f\U g) \W h & \equiv g \W h \\ -\text{if~} & f\simp h && \text{~then~} & (f\W g) \W h & \equiv g \W h \\ -\text{if~} & g\simp h && \text{~then~} & (f\W g) \W h & \equiv (f \W g) \OR h \\ -\text{if~} & g\simp h && \text{~then~} & (f\U g) \W h & \equiv (f \U g) \OR h \\ -\text{if~} & \flessg && \text{~then~} & f\R g & \equiv f \\ -\text{if~} & g\simp f && \text{~then~} & f\R g & \equiv g \\ -\text{if~} & g\simp \NOT f && \text{~then~} & f\R g & \equiv \G g \\ -\text{if~} & u\simp g && \text{~then~} & u\R g & \equiv \G g \\ -\text{if~} & g\simp f && \text{~then~} & f\R (g \R h) & \equiv g \R h \\ -\text{if~} & g\simp f && \text{~then~} & f\R (g \M h) & \equiv g \M h \\ -\text{if~} & f\simp g && \text{~then~} & f\R (g \R h) & \equiv f \R h \\ -\text{if~} & h\simp f && \text{~then~} & (f\R g) \R h & \equiv g \R h \\ -\text{if~} & h\simp f && \text{~then~} & (f\M g) \R h & \equiv g \R h \\ -\text{if~} & g\simp h && \text{~then~} & (f\R g) \R h & \equiv (f \AND g) \R h \\ -\text{if~} & g\simp h && \text{~then~} & (f\M g) \R h & \equiv (f \AND g) \R h \\ -\text{if~} & \flessg && \text{~then~} & f\M g & \equiv f \\ -\text{if~} & g\simp f && \text{~then~} & f\M g & \equiv g \\ -\text{if~} & g\simp \NOT f && \text{~then~} & f\M g & \equiv \0 \\ -\text{if~} & g\simp f && \text{~then~} & f\M (g \M h) & \equiv g \M h \\ -\text{if~} & f\simp g && \text{~then~} & f\M (g \M h) & \equiv f \M h \\ -\text{if~} & f\simp g && \text{~then~} & f\M (g \R h) & \equiv f \M h \\ -\text{if~} & h\simp f && \text{~then~} & (f\M g) \M h & \equiv g \M h \\ -\text{if~} & h\simp f && \text{~then~} & (f\R g) \M h & \equiv g \M h \\ -\text{if~} & g\simp h && \text{~then~} & (f\M g) \M h & \equiv (f \AND g) \M h \\ +\text{if~} & f\simp \NOT g & & \text{~then~} & f\OR g & \equiv \1 \\ +\text{if~} & f\simp \NOT g & & \text{~then~} & f\AND g & \equiv \0 \\ +\text{if~} & \flessg & & \text{~then~} & f\OR g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\OR g & \equiv g \\ +\text{if~} & \glessf & & \text{~then~} & f\AND g & \equiv g \\ +\text{if~} & f\simp g & & \text{~then~} & f\AND g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\EQUIV g & \equiv g\IMPLIES f \\ +\text{if~} & f\simp g & & \text{~then~} & f\IMPLIES g & \equiv \1 \\ +\text{if~} & (\NOT f)\simp g & & \text{~then~} & f\XOR g & \equiv g\IMPLIES \NOT f \\ +\text{if~} & f\simp\NOT g & & \text{~then~} & f\XOR g & \equiv (\NOT g)\IMPLIES f \\ +\text{if~} & \flessg & & \text{~then~} & f\U g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (f\U g)\Simp g & & \text{~then~} & f\U g & \equiv g \\ +\text{if~} & (\NOT f)\simp g & & \text{~then~} & f\U g & \equiv \F g \\ +\text{if~} & g\simp e & & \text{~then~} & e\U g & \equiv \F g \\ +\text{if~} & f\simp g & & \text{~then~} & f\U (g \U h) & \equiv g \U h \\ +\text{if~} & f\simp g & & \text{~then~} & f\U (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f & & \text{~then~} & f\U (g \U h) & \equiv f \U h \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \R (h \U k)) & \equiv g \R (h \U k) \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \R (h \W k)) & \equiv g \R (h \W k) \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \M (h \U k)) & \equiv g \M (h \U k) \\ +\text{if~} & f\simp h & & \text{~then~} & f\U (g \M (h \W k)) & \equiv g \M (h \W k) \\ +\text{if~} & f\simp h & & \text{~then~} & (f\U g) \U h & \equiv g \U h \\ +\text{if~} & f\simp h & & \text{~then~} & (f\W g) \U h & \equiv g \U h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\U g) \U h & \equiv (f \U g) \OR h \\ +\text{if~} & (\NOT f)\simp g & & \text{~then~} & f\W g & \equiv \1 \\ +\text{if~} & \flessg & & \text{~then~} & f\W g & \equiv f \\ +\text{if~} & f\simp g & & \text{~then~} & f\W g & \equiv g \\ +\text{if~} & (f\W g)\Simp g & & \text{~then~} & f\W g & \equiv g \\ +\text{if~} & f\simp g & & \text{~then~} & f\W (g \W h) & \equiv g \W h \\ +\text{if~} & g\simp f & & \text{~then~} & f\W (g \U h) & \equiv f \W h \\ +\text{if~} & g\simp f & & \text{~then~} & f\W (g \W h) & \equiv f \W h \\ +\text{if~} & f\simp h & & \text{~then~} & (f\U g) \W h & \equiv g \W h \\ +\text{if~} & f\simp h & & \text{~then~} & (f\W g) \W h & \equiv g \W h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\W g) \W h & \equiv (f \W g) \OR h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\U g) \W h & \equiv (f \U g) \OR h \\ +\text{if~} & \flessg & & \text{~then~} & f\R g & \equiv f \\ +\text{if~} & g\simp f & & \text{~then~} & f\R g & \equiv g \\ +\text{if~} & g\simp \NOT f & & \text{~then~} & f\R g & \equiv \G g \\ +\text{if~} & u\simp g & & \text{~then~} & u\R g & \equiv \G g \\ +\text{if~} & g\simp f & & \text{~then~} & f\R (g \R h) & \equiv g \R h \\ +\text{if~} & g\simp f & & \text{~then~} & f\R (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g & & \text{~then~} & f\R (g \R h) & \equiv f \R h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\R g) \R h & \equiv g \R h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\M g) \R h & \equiv g \R h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\R g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\M g) \R h & \equiv (f \AND g) \R h \\ +\text{if~} & \flessg & & \text{~then~} & f\M g & \equiv f \\ +\text{if~} & g\simp f & & \text{~then~} & f\M g & \equiv g \\ +\text{if~} & g\simp \NOT f & & \text{~then~} & f\M g & \equiv \0 \\ +\text{if~} & g\simp f & & \text{~then~} & f\M (g \M h) & \equiv g \M h \\ +\text{if~} & f\simp g & & \text{~then~} & f\M (g \M h) & \equiv f \M h \\ +\text{if~} & f\simp g & & \text{~then~} & f\M (g \R h) & \equiv f \M h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\M g) \M h & \equiv g \M h \\ +\text{if~} & h\simp f & & \text{~then~} & (f\R g) \M h & \equiv g \M h \\ +\text{if~} & g\simp h & & \text{~then~} & (f\M g) \M h & \equiv (f \AND g) \M h \\ \end{alignat*} \endgroup diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index ddb90c776..422529fc6 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -1775,12 +1775,38 @@ namespace spot trace << "bo: trying inclusion-based rules" << std::endl; switch (o) { - case op::Xor: case op::Equiv: + { + if (c_->implication(a, b)) + return recurse(formula::Implies(b, a)); + if (c_->implication(b, a)) + return recurse(formula::Implies(a, b)); + break; + } case op::Implies: - SPOT_UNIMPLEMENTED(); - break; - + { + if (c_->implication(a, b)) + return formula::tt(); + break; + } + case op::Xor: + { + // if (!a)->b then a xor b = b->!a = a->!b + if (c_->implication_neg(a, b, false)) + { + if (b.is(op::Not)) + return recurse(formula::Implies(a, b[0])); + return recurse(formula::Implies(b, formula::Not(a))); + } + // if a->!b then a xor b = (!b)->a = (!a)->b + if (c_->implication_neg(a, b, true)) + { + if (b.is(op::Not)) + return recurse(formula::Implies(b[0], a)); + return recurse(formula::Implies(formula::Not(a), b)); + } + break; + } case op::U: // if a => b, then a U b = b if (c_->implication(a, b)) diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index 9eb9f909f..96ebcda17 100755 --- a/tests/python/ltlsimple.py +++ b/tests/python/ltlsimple.py @@ -1,6 +1,6 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2015 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2015, 2018 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systemes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -116,3 +116,21 @@ Default for shell: echo 'a U (b U "$strange[0]=name")' | ... LBT for shell: echo 'U "a" U "b" "$strange[0]=name"' | ... Default for CSV: ...,"a U (b U ""$strange[0]=name"")",... Wring, centered: ~~~~~(a=1) U ((b=1) U ("$strange[0]=name"=1))~~~~~""" + + +opt = spot.tl_simplifier_options(False, True, True, + True, True, True, + False, False, False) + +for (input, output) in [('(a&b)<->b', 'b->(a&b)'), + ('b<->(a&b)', 'b->(a&b)'), + ('(a&b)->b', '1'), + ('b->(a&b)', 'b->(a&b)'), + ('(!(a&b)) xor b', 'b->(a&b)'), + ('(a&b) xor !b', 'b->(a&b)'), + ('b xor (!(a&b))', 'b->(a&b)'), + ('!b xor (a&b)', 'b->(a&b)')]: + f = spot.tl_simplifier(opt).simplify(input) + print(input, f, output) + assert(f == output) + assert(spot.are_equivalent(input, output)) From 701a3b1c6a0a208424800eab1d0514c571f520a4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 1 Aug 2018 17:17:25 +0200 Subject: [PATCH 16/19] contains: fix the semantics MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit spot::contains(a, b) should test a⊇b. It was testing a⊆b instead. * NEWS: Mention the bug. * spot/twaalgos/contains.cc, spot/twaalgos/contains.hh: Fix the code and documentation. * tests/python/contains.ipynb: Adjust description and expected results. * python/spot/__init__.py: Also swap the argument of language_containment_checker.contains() * bin/autfilt.cc: Adjust usage. --- NEWS | 5 ++++ bin/autfilt.cc | 2 +- python/spot/__init__.py | 2 +- spot/twaalgos/contains.cc | 12 ++++----- spot/twaalgos/contains.hh | 6 ++--- tests/python/contains.ipynb | 50 ++++++++----------------------------- 6 files changed, 27 insertions(+), 50 deletions(-) diff --git a/NEWS b/NEWS index 0c687ce22..3faf047fc 100644 --- a/NEWS +++ b/NEWS @@ -16,6 +16,11 @@ New in spot 2.6.0.dev (not yet released) set. (This combinations of options is not available from command-line tools.) + - The spot::contains(a, b) function introduced in 2.6 was testing + a⊆b instead of a⊇b as one would expect. Infortunately the + documentation was also matching the code, so this is a backward + incompatible change. + New in spot 2.6 (2018-07-04) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 018086289..71ba08ffc 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1411,7 +1411,7 @@ namespace matched &= !aut->intersects(opt->included_in); if (opt->equivalent_pos) matched &= !aut->intersects(opt->equivalent_neg) - && spot::contains(opt->equivalent_pos, aut); + && spot::contains(aut, opt->equivalent_pos); if (matched && !opt->acc_words.empty()) for (auto& word_aut: opt->acc_words) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 74131f8e5..11e5a8605 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1039,7 +1039,7 @@ def bdd_to_formula(b, dic=_bdd_dict): def language_containment_checker(dic=_bdd_dict): from spot.impl import language_containment_checker as c - c.contains = c.contained + c.contains = lambda this, a, b: c.contained(this, b, a) c.are_equivalent = c.equal return c(dic) diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc index 957aa41b5..a94b3ac40 100644 --- a/spot/twaalgos/contains.cc +++ b/spot/twaalgos/contains.cc @@ -49,25 +49,25 @@ namespace spot bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right) { - return !left->intersects(dualize(ensure_deterministic(right))); + return !right->intersects(dualize(ensure_deterministic(left))); } bool contains(const_twa_graph_ptr left, formula right) { - return !left->intersects(translate(formula::Not(right), left->get_dict())); + auto right_aut = translate(right, left->get_dict()); + return !right_aut->intersects(dualize(ensure_deterministic(left))); } bool contains(formula left, const_twa_graph_ptr right) { - auto left_aut = translate(left, right->get_dict()); - return !left_aut->intersects(dualize(ensure_deterministic(right))); + return !right->intersects(translate(formula::Not(left), right->get_dict())); } bool contains(formula left, formula right) { auto dict = make_bdd_dict(); - auto left_aut = translate(left, dict); - return !left_aut->intersects(translate(formula::Not(right), dict)); + auto right_aut = translate(right, dict); + return !right_aut->intersects(translate(formula::Not(left), dict)); } bool are_equivalent(const_twa_graph_ptr left, const_twa_graph_ptr right) diff --git a/spot/twaalgos/contains.hh b/spot/twaalgos/contains.hh index 758339c73..61c53076a 100644 --- a/spot/twaalgos/contains.hh +++ b/spot/twaalgos/contains.hh @@ -28,14 +28,14 @@ namespace spot { /// \ingroup containment - /// \brief Test if the language of \a left is included in that of \a right. + /// \brief Test if the language of \a right is included in that of \a left. /// /// Both arguments can be either formulas or automata. Formulas /// will be converted into automata. /// /// The inclusion check if performed by ensuring that the automaton - /// associated to \a left does not intersect the automaton - /// associated to the complement of \a right. It helps if \a right + /// associated to \a right does not intersect the automaton + /// associated to the complement of \a left. It helps if \a left /// is a deterministic automaton or a formula (because in both cases /// complementation is easier). /// @{ diff --git a/tests/python/contains.ipynb b/tests/python/contains.ipynb index 5e15a0ba1..0e0022b0f 100644 --- a/tests/python/contains.ipynb +++ b/tests/python/contains.ipynb @@ -17,7 +17,7 @@ "source": [ "# Containement checks\n", "\n", - "The `spot.contains()` function checks whether the language of its left argument is included in the language of its right argument. The arguments may mix automata and formulas; the latter can be given as strings." + "The `spot.contains()` function checks whether the language of its right argument is included in the language of its left argument. The arguments may mix automata and formulas; the latter can be given as strings." ] }, { @@ -38,7 +38,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 3, @@ -58,7 +58,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 4, @@ -78,7 +78,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 5, @@ -98,7 +98,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 6, @@ -118,7 +118,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 7, @@ -145,7 +145,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 8, @@ -165,7 +165,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 9, @@ -272,7 +272,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 14, @@ -344,7 +344,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 17, "metadata": {}, "outputs": [], "source": [ @@ -360,7 +360,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -484,34 +484,6 @@ "source": [ "show_one_difference(aut_f, aut_g)" ] - }, - { - "cell_type": "code", - "execution_count": 36, - "metadata": {}, - "outputs": [ - { - "ename": "NameError", - "evalue": "name 'run' is not defined", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mNameError\u001b[0m Traceback (most recent call last)", - "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mrun\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mget_aut\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", - "\u001b[0;31mNameError\u001b[0m: name 'run' is not defined" - ] - } - ], - "source": [ - "run.get_aut()" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { From 5c8cf1bc47e22244a2fdb04de038efd2e2ce5290 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 2 Aug 2018 23:05:22 +0200 Subject: [PATCH 17/19] fix python bindings for spot::parsed_formula::f getter * python/spot/impl.i: Add a typemap. * tests/python/ltlsimple.py: Add a test case for an issue. * NEWS: Mention the bug. --- NEWS | 4 ++++ python/spot/impl.i | 9 +++++++++ tests/python/ltlsimple.py | 8 ++++++++ 3 files changed, 21 insertions(+) diff --git a/NEWS b/NEWS index 3faf047fc..7349ee5e8 100644 --- a/NEWS +++ b/NEWS @@ -21,6 +21,10 @@ New in spot 2.6.0.dev (not yet released) documentation was also matching the code, so this is a backward incompatible change. + - The Python binding of the getter of spot::parsed_formula::f was + returning a reference instead of a copy, causing issues if the + reference outlasted the parsed_formula struct. + New in spot 2.6 (2018-07-04) diff --git a/python/spot/impl.i b/python/spot/impl.i index 1050c7568..7bdcd1bef 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -384,6 +384,15 @@ namespace swig SWIG_POINTER_IMPLICIT_CONV)); } +// Access to stucture members, such as spot::parsed_formula::f are done via +// the pointer typemap. We want to enforce a copy. +%typemap(out) spot::formula* { + if (!*$1) + $result = SWIG_Py_Void(); + else + $result = SWIG_NewPointerObj(new spot::formula(*$1), $descriptor(spot::formula*), SWIG_POINTER_OWN); +} + %typemap(out) spot::formula { if (!$1) $result = SWIG_Py_Void(); diff --git a/tests/python/ltlsimple.py b/tests/python/ltlsimple.py index 96ebcda17..a8443a357 100755 --- a/tests/python/ltlsimple.py +++ b/tests/python/ltlsimple.py @@ -134,3 +134,11 @@ for (input, output) in [('(a&b)<->b', 'b->(a&b)'), print(input, f, output) assert(f == output) assert(spot.are_equivalent(input, output)) + +def myparse(input): + env = spot.default_environment.instance() + pf = spot.parse_infix_psl(input, env) + return pf.f +# This used to fail, because myparse would return a pointer +# to pf.f inside the destroyed pf. +assert myparse('a U b') == spot.formula('a U b') From d743674729cab04438fd97612ce9d2bbdc7dd0f4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 4 Aug 2018 08:54:45 +0200 Subject: [PATCH 18/19] Release Spot 2.6.1 * NEWS, configure.ac, doc/org/setup.org: Update version number. --- NEWS | 6 +++--- configure.ac | 2 +- doc/org/setup.org | 8 ++++---- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 7349ee5e8..6ac9e6198 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.6.0.dev (not yet released) +New in spot 2.6.1 (2018-08-04) Command-line tools: @@ -13,13 +13,13 @@ New in spot 2.6.0.dev (not yet released) - The spot::tl_simplifier class could raise an exception while attempting to reduce formulas containing unsimplified <->, -> or xor, if options nenoform_stop_on_boolean and synt_impl are both - set. (This combinations of options is not available from + set. (This combination of options is not available from command-line tools.) - The spot::contains(a, b) function introduced in 2.6 was testing a⊆b instead of a⊇b as one would expect. Infortunately the documentation was also matching the code, so this is a backward - incompatible change. + incompatible change, but a short-lived one. - The Python binding of the getter of spot::parsed_formula::f was returning a reference instead of a copy, causing issues if the diff --git a/configure.ac b/configure.ac index 51978ad0f..7af2fa897 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.6.0.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.6.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 08fc2d2ad..444079ceb 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,10 +1,10 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.6 -#+MACRO: LASTRELEASE 2.6 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.6.tar.gz][=spot-2.6.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-6/NEWS][summary of the changes]] +#+MACRO: SPOTVERSION 2.6.1 +#+MACRO: LASTRELEASE 2.6.1 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.6.1.tar.gz][=spot-2.6.1.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-6-1/NEWS][summary of the changes]] #+MACRO: LASTDATE 2018-07-04 #+ATTR_HTML: :id spotlogo From 90f529918b6780c89501d821e079d018fd5d4d54 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 4 Aug 2018 08:56:38 +0200 Subject: [PATCH 19/19] * 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 6ac9e6198..11a6c17ed 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.6.1.dev (not yet released) + + Nothing yet. + New in spot 2.6.1 (2018-08-04) Command-line tools: diff --git a/configure.ac b/configure.ac index 7af2fa897..5d69ccc8e 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.6.1], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.6.1.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])