From d4c1db287b70d63116e00252a28fce43623badb0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 May 2016 13:13:02 +0200 Subject: [PATCH 01/18] * NEWS: Update for next version. --- NEWS | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/NEWS b/NEWS index 6f29395f3..5b9fa68f6 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,8 @@ +New in spot 2.0.1a (not yet released) + + Nothing yet. + + New in spot 2.0.1 (2016-05-09) Library: From e75605529adfa4ae9f2636c3e7aa2ff2831aed59 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 9 May 2016 22:01:57 +0200 Subject: [PATCH 02/18] attempt to fix clang++ compilation error Seen on arch linux when clang++ 3.7.1 uses GCC's 6.1.1 tuple header. * spot/twaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::succ): Build the return type explicitly. * NEWS: Mention the issue. --- NEWS | 4 +++- spot/twaalgos/ltl2tgba_fm.cc | 12 ++++++++++-- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 5b9fa68f6..3f9c05021 100644 --- a/NEWS +++ b/NEWS @@ -1,7 +1,9 @@ New in spot 2.0.1a (not yet released) - Nothing yet. + Bug fixes: + * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1 + headers. New in spot 2.0.1 (2016-05-09) diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 05bb7a53b..0c006ec93 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -1047,14 +1047,22 @@ namespace spot else a = translate(f); + // Using return std::make_tuple(nullptr, nullptr, nullptr) works + // with GCC 6.1.1, but breaks with clang++ 3.7.1 when using the + // same header file for . So let's use the output type + // explicitly. + typedef std::tuple res_t; + // If a is null, f has an empty language. if (!a.first) - return std::forward_as_tuple(nullptr, nullptr, nullptr); + return res_t{nullptr, nullptr, nullptr}; auto namer = a.second; assert(namer->has_state(f)); auto st = a.first->state_from_number(namer->get_state(f)); - return std::forward_as_tuple(a.first, namer, st); + return res_t{a.first, namer, st}; } // The rewrite rules used here are adapted from Jean-Michel From bb2c6970727386176223eae7d70eb76002f89cee Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 May 2016 08:37:09 +0200 Subject: [PATCH 03/18] org: add a description for each page Part of #176. * doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genltl.org, doc/org/hoa.org, doc/org/install.org, doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut30.org, doc/org/upgrade2.org: Here. * doc/org/index.org: Also add keywords in case it is useful, and use a more descripting title for search engines. --- doc/org/autfilt.org | 1 + doc/org/compile.org | 1 + doc/org/concepts.org | 1 + doc/org/csv.org | 1 + doc/org/dstar2tgba.org | 1 + doc/org/genltl.org | 1 + doc/org/hoa.org | 1 + doc/org/index.org | 16 +++++++++------- doc/org/install.org | 1 + doc/org/ioltl.org | 1 + doc/org/ltl2tgba.org | 1 + doc/org/ltl2tgta.org | 1 + doc/org/ltlcross.org | 1 + doc/org/ltldo.org | 1 + doc/org/ltlfilt.org | 1 + doc/org/ltlgrind.org | 1 + doc/org/oaut.org | 1 + doc/org/randaut.org | 1 + doc/org/randltl.org | 1 + doc/org/satmin.org | 1 + doc/org/tools.org | 1 + doc/org/tut.org | 1 + doc/org/tut01.org | 1 + doc/org/tut02.org | 1 + doc/org/tut03.org | 1 + doc/org/tut10.org | 1 + doc/org/tut20.org | 1 + doc/org/tut21.org | 1 + doc/org/tut22.org | 1 + doc/org/tut30.org | 1 + doc/org/upgrade2.org | 1 + 31 files changed, 39 insertions(+), 7 deletions(-) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 65e445dfb..316ce6eed 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =autfilt= +#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting ω-automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/compile.org b/doc/org/compile.org index f9627b7bb..5aa47111a 100644 --- a/doc/org/compile.org +++ b/doc/org/compile.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Compiling against Spot +#+DESCRIPTION: How to compile C++11 programs using Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 847975308..ea86e9e18 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Concepts +#+DESCRIPTION: Informal explanation of various concepts used in Spot. #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/csv.org b/doc/org/csv.org index 6ae9cc65b..4a4d6e37d 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Reading and writing CSV files +#+DESCRIPTION: Examples showing how to read and write CSV files using Spot's command-line tools. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 70122ed3e..7a64539e8 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =dstar2tgba= +#+DESCRIPTION: Spot command-line tool for converting automata into Transition-based Generalized Büchi Automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/genltl.org b/doc/org/genltl.org index 026872a9f..cfe2ee203 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =genltl= +#+DESCRIPTION: Spot command-line tool that generates LTL formulas from known patterns #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 72c61b790..3c37ecf25 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -1,4 +1,5 @@ #+TITLE: Support for the Hanoi Omega Automata (HOA) Format +#+DESCRIPTION: Details about support of the HOA format in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/index.org b/doc/org/index.org index d79945db9..bffc627ae 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -1,9 +1,11 @@ # -*- coding: utf-8 -*- -#+TITLE: Spot +#+TITLE: Spot: a platform for LTL and ω-automata manipulation +#+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata +#+KEYWORDS: Spot,C++11,library,platform,framework,tool-suite,LTL,PSL,omega-automata #+SETUPFILE: setup.org #+HTML_HEAD_EXTRA: -Spot is a C++11 library for ω-automata manipulation and model +Spot is a C++11 library for LTL, ω-automata manipulation and model checking. It has the following notable features: - Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and @@ -22,11 +24,11 @@ checking. It has the following notable features: weak-DBA, removal of useless SCCs, acceptance-condition transformations, determinization, etc. - In addition to the C++ interface, most of its algorithms are usable - via [[file:tools.org][command-line tools]], and via Python bindings. -- One command-line tool, called [[file:ltlcross.org][=ltlcross=]], is a rewrite of - [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but with support for PSL and arbitrary acceptance conditions. - It could for instance be used to test tools that translate LTL into - Rabin automata. + via [[file:tools.org][command-line tools]], and via [[file:tut.org][Python bindings]]. +- One command-line tool, called [[file:ltlcross.org][=ltlcross=]], is a rewrite of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but + with support for PSL and automata with arbitrary acceptance + conditions. It can be used to test tools that translate LTL into + ω-automata, or benchmark them. * Latest version diff --git a/doc/org/install.org b/doc/org/install.org index f96a7410d..c60d5c64d 100644 --- a/doc/org/install.org +++ b/doc/org/install.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Installing Spot +#+DESCRIPTION: Different ways to install the Spot package #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 3873aaf16..be7d10695 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Common input and output options for LTL/PSL formulas +#+DESCRIPTION: Options for input and output of temporal logic formulas in Spot's command-line tools #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index b75a7ddaf..d85e2cead 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltl2tgba= +#+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Büchi Automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index ff290d87f..a7e3d6fdb 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltl2tgta= +#+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Testing Automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 9db0e4e2a..1616930a0 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlcross= +#+DESCRIPTION: Spot command-line tool for cross-comparing the output of LTL translators. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 1b5d4b481..37bd1efa3 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltldo= +#+DESCRIPTION: Spot's wrapper for third-party LTL translators #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 7f48010f7..cf5bca47d 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlfilt= +#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting LTL formulas. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltlgrind.org b/doc/org/ltlgrind.org index d1729f737..6c33b8d9a 100644 --- a/doc/org/ltlgrind.org +++ b/doc/org/ltlgrind.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlgrind= +#+DESCRIPTION: Spot command-line tool for mutating LTL formulas. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 5ad6aa41a..88909faf0 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Common output options for automata +#+DESCRIPTION: Options for input and output of ω-automata in Spot's command-line tools #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/randaut.org b/doc/org/randaut.org index e2064a432..f05cb74d1 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =randaut= +#+DESCRIPTION: Spot command-line tool for generating random ω-automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/randltl.org b/doc/org/randltl.org index 839dc066b..110601d6a 100644 --- a/doc/org/randltl.org +++ b/doc/org/randltl.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =randltl= +#+DESCRIPTION: Spot command-line tool for generating random LTL formulas. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 92586c76f..bdd0240c2 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: SAT-based Minimization of Deterministic ω-Automata +#+DESCRIPTION: Spot command-line tools for minimizing ω-automata #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/tools.org b/doc/org/tools.org index acdcaa0e9..81acd065c 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Command-line tools installed by Spot {{{SPOTVERSION}}} +#+DESCRIPTION: List of all the command-line tools installed by Spot {{{SPOTVERSION}}} #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/tut.org b/doc/org/tut.org index 457fc1f4e..609dc981e 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Code Examples +#+DESCRIPTION: Directory of code examples for using Spot in C++11, Python, and shell. #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 9fdfda015..d2641f62a 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Parsing and Printing LTL Formulas +#+DESCRIPTION: Code example for parsing and printing formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut02.org b/doc/org/tut02.org index d9e307a51..c02510ae1 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Relabeling Formulas +#+DESCRIPTION: Code example for relabeling formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut03.org b/doc/org/tut03.org index 7240243fb..68cebe292 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Constructing and transforming formulas +#+DESCRIPTION: Code example for constructing and transforming formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut10.org b/doc/org/tut10.org index b25f55bff..7772d2794 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Translating an LTL formula into a never claim +#+DESCRIPTION: Code example for translating formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut20.org b/doc/org/tut20.org index f138f5419..c0b6dcf8e 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Converting a never claim into HOA +#+DESCRIPTION: Code example for parsing and printing ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 2140063d1..a0b3ebedc 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Custom print of an automaton +#+DESCRIPTION: Code example for iterating over ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut22.org b/doc/org/tut22.org index da6ca6d7f..35f68416b 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Creating an automaton by adding states and transitions +#+DESCRIPTION: Code example for constructing ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut30.org b/doc/org/tut30.org index bd82228cb..118c7a6f4 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it +#+DESCRIPTION: Code example for converting ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 9c4bdfbf2..e2618e4f5 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Upgrading from Spot 1.2.6 +#+DESCRIPTION: Help for upgrading code to Spot 2.0 #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html From 86287be2ef282e87c9cbf52643dc160cfb54b268 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 May 2016 10:37:34 +0200 Subject: [PATCH 04/18] org: disable postamble in html export * doc/org/init.el.in, doc/org/.dir-locals.el.in: Here. --- doc/org/.dir-locals.el.in | 1 + doc/org/init.el.in | 2 ++ 2 files changed, 3 insertions(+) diff --git a/doc/org/.dir-locals.el.in b/doc/org/.dir-locals.el.in index ca511e3d0..98b70ad22 100644 --- a/doc/org/.dir-locals.el.in +++ b/doc/org/.dir-locals.el.in @@ -32,6 +32,7 @@ (org-babel-python-command . "@PYTHON@") (org-babel-C++-compiler . "./g++wrap") (shell-file-name . "@SHELL@") + (org-export-html-postamble . nil) (org-publish-project-alist . (("spot-html" :base-directory "." diff --git a/doc/org/init.el.in b/doc/org/init.el.in index 467b4d0a3..99900103e 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -52,6 +52,8 @@ UP | HOME ") +(setq org-export-html-postamble nil) + (setq org-publish-project-alist `(("spot-html" :base-directory "@abs_top_srcdir@/doc/org/" From 1780208961dfedba1d0a0ab14ca03fb3bfd2c952 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 May 2016 10:44:38 +0200 Subject: [PATCH 05/18] ajax: add

title Final part of #176. * python/ajax/trans.html: Here. --- python/ajax/trans.html | 2 ++ 1 file changed, 2 insertions(+) diff --git a/python/ajax/trans.html b/python/ajax/trans.html index 74e2bb038..d985484f0 100644 --- a/python/ajax/trans.html +++ b/python/ajax/trans.html @@ -24,6 +24,7 @@ $(".tabs").tabs(); $("#send").button(); $("#results").hide(); + $("h1").hide(); $("abbr").tipTip({maxWidth: "300px", delay: 1000, edgeOffset: 3, defaultPosition: "below"}); @@ -326,6 +327,7 @@
+

Translator of LTL to Transition-based Generalized Büchi Automata

From c94787b7d9ad38f863bbd29f1f9111de3abc989a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 11 May 2016 16:19:13 +0200 Subject: [PATCH 06/18] * doc/org/ltlcross.org: Fix explanation. --- doc/org/ltlcross.org | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 1616930a0..8dd8587ce 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -616,12 +616,12 @@ positive and negative formulas by the ith translator). followed by a cycle that should be repeated infinitely often. The cycle part is denoted by =cycle{...}=. - - Complemented intersection check. If $P_i$ and $P_j$ are + - Complemented intersection check. If $P_i$ and $N_i$ are deterministic, =ltlcross= builds their complements, $Comp(P_i)$ - and $Comp(P_j)$, and then ensures that $Comp(P_i)\otimes - Comp(P_j)$ is empty. If only one of them is deterministic, - for instance $P_i$, we check that $P_j\otimes Comp(P_i)$ for all - $j \ne i$; likewise if it's $N_i$ that is deterministic. + and $Comp(N_i)$, and then ensures that $Comp(P_i)\otimes + Comp(N_i)$ is empty. If only one of them is deterministic, for + instance $P_i$, we check that $P_j\otimes Comp(P_i)$ for all $j + \ne i$; likewise if it's $N_i$ that is deterministic. By default this check is only done for deterministic automata, because complementation is relatively cheap is that case (at least From 0605181c7a78d4b457084be2c0a4ae754e8eb152 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 May 2016 15:40:40 +0200 Subject: [PATCH 07/18] * spot/twaalgos/postproc.cc: Typo. --- spot/twaalgos/postproc.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 6c05a795e..d1181c2cf 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -382,7 +382,7 @@ namespace spot { if (type_ == Generic) throw std::runtime_error - ("postproc() no yet updated to mix sat-minimize and Generic"); + ("postproc() not yet updated to mix sat-minimize and Generic"); unsigned target_acc; if (type_ == BA) target_acc = 1; From 2d304f3dcf850dc3340df8e8657bfcbb899521b3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 May 2016 20:57:14 +0200 Subject: [PATCH 08/18] org: fix never claim example * doc/org/concepts.org: Enlarge the width of the output of pr so that the output is not truncated. It add a missing closing brace. --- doc/org/concepts.org | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/doc/org/concepts.org b/doc/org/concepts.org index ea86e9e18..0d6576a01 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -569,30 +569,30 @@ $txt #+BEGIN_SRC sh :results verbatim :exports results ltl2tgba -s 'p0 | GFp1' > tmp.$$ -ltl2tgba -s6 'p0 | GFp1' | pr -m -t tmp.$$ - +ltl2tgba -s6 'p0 | GFp1' | pr -w80 -m -t tmp.$$ - #+END_SRC #+RESULTS: #+begin_example -never { /* p0 | GFp1 */ never { /* p0 | GFp1 */ -T0_init: T0_init: - if do - :: (p0) -> goto accept_all :: atomic { (p0) -> assert(!(p0)) - :: (!(p0)) -> goto accept_S2 :: (!(p0)) -> goto accept_S2 - fi; od; -accept_S2: accept_S2: - if do - :: (p1) -> goto accept_S2 :: (p1) -> goto accept_S2 - :: (!(p1)) -> goto T0_S3 :: (!(p1)) -> goto T0_S3 - fi; od; -T0_S3: T0_S3: - if do - :: (p1) -> goto accept_S2 :: (p1) -> goto accept_S2 - :: (!(p1)) -> goto T0_S3 :: (!(p1)) -> goto T0_S3 - fi; od; -accept_all: accept_all: - skip skip -} } +never { /* p0 | GFp1 */ never { /* p0 | GFp1 */ +T0_init: T0_init: + if do + :: (p0) -> goto accept_all :: atomic { (p0) -> assert(!(p0)) } + :: (!(p0)) -> goto accept_S2 :: (!(p0)) -> goto accept_S2 + fi; od; +accept_S2: accept_S2: + if do + :: (p1) -> goto accept_S2 :: (p1) -> goto accept_S2 + :: (!(p1)) -> goto T0_S3 :: (!(p1)) -> goto T0_S3 + fi; od; +T0_S3: T0_S3: + if do + :: (p1) -> goto accept_S2 :: (p1) -> goto accept_S2 + :: (!(p1)) -> goto T0_S3 :: (!(p1)) -> goto T0_S3 + fi; od; +accept_all: accept_all: + skip skip +} } #+end_example #+NAME: never-ex1 From 1f9b18f54a094feff9547e4370beb32fa3040d0b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 May 2016 20:58:19 +0200 Subject: [PATCH 09/18] org: fix sat-minimize example Fixes #178. * doc/org/satmin.org: Use a different example, where tba-det does not work. Also adjust the text to automatically adjust to the size of the produced automata. --- doc/org/satmin.org | 58 ++++++++++++++++++++++++++-------------------- 1 file changed, 33 insertions(+), 25 deletions(-) diff --git a/doc/org/satmin.org b/doc/org/satmin.org index bdd0240c2..c81a46981 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -73,7 +73,7 @@ deterministic automaton for =GF(a <-> XXb)=. Instead we get a 9-state non-deterministic automaton. #+BEGIN_SRC sh :results verbatim :exports both -ltl2tgba -D "GF(a <-> XXb)" --stats='states=%s, det=%d' +ltl2tgba -D 'GF(a <-> XXb)' --stats='states=%s, det=%d' #+END_SRC #+RESULTS: : states=9, det=0 @@ -88,7 +88,7 @@ On our example, =-x tba-det= successfully produces a deterministic TBA, but a non-minimal one: #+BEGIN_SRC sh :results verbatim :exports both -ltl2tgba -D -x tba-det "GF(a <-> XXb)" --stats='states=%s, det=%d' +ltl2tgba -D -x tba-det 'GF(a <-> XXb)' --stats='states=%s, det=%d' #+END_SRC #+RESULTS: : states=7, det=1 @@ -97,7 +97,7 @@ Option =-x sat-minimize= will turn-on SAT-based minimization. It also implies =-x tba-det=, so there is no need to supply both options. #+BEGIN_SRC sh :results verbatim :exports both -ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" --stats='states=%s, det=%d' +ltl2tgba -D -x sat-minimize 'GF(a <-> XXb)' --stats='states=%s, det=%d' #+END_SRC #+RESULTS: : states=4, det=1 @@ -106,7 +106,7 @@ We can draw it: #+NAME: gfaexxb3 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" -d +ltl2tgba -D -x sat-minimize 'GF(a <-> XXb)' -d #+END_SRC #+RESULTS: gfaexxb3 #+begin_example @@ -148,14 +148,14 @@ $txt #+RESULTS: [[file:gfaexxb3.png]] -Clearly this is automaton benefits from the transition-based +Clearly this automaton benefits from the transition-based acceptance. If we want a traditional Büchi automaton, with state-based acceptance, we only need to add the =-B= option. The result will of course be slightly bigger. #+NAME: gfaexxb4 #+BEGIN_SRC sh :results verbatim :exports code -ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -d +ltl2tgba -BD -x sat-minimize 'GF(a <-> XXb)' -d #+END_SRC #+RESULTS: gfaexxb4 #+begin_example @@ -207,10 +207,10 @@ There are cases where =ltl2tgba='s =tba-det= algorithm fails to produce a determ In that case, SAT-based minimization is simply skipped. For instance: #+BEGIN_SRC sh :results verbatim :exports both -ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d' +ltl2tgba -D -x sat-minimize 'G(F(!b & (X!a M (F!a & F!b))) U !b)' --stats='states=%s, det=%d' #+END_SRC #+RESULTS: -: states=5, det=1 +: states=5, det=0 The question, of course, is whether there exist a deterministic automaton for this formula, in other words: is this a recurrence @@ -224,10 +224,10 @@ without being syntactic recurrences.) [[file:ltlfilt.org][=ltlfilt=]] can be in print only formulas that are syntactic recurrences: #+BEGIN_SRC sh :results verbatim :exports both -ltlfilt --syntactic-recurrence -f "Ga R (F!b & (c U b))" +ltlfilt --syntactic-recurrence -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' #+END_SRC #+RESULTS: -: Ga R (F!b & (c U b)) +: G(F(!b & (X!a M (F!a & F!b))) U !b) Since our input formula was output, it expresses a recurrence property. @@ -237,35 +237,43 @@ output is guaranteed to be deterministic if and only if the input DRA expresses a recurrence property. #+BEGIN_SRC sh :results verbatim :exports both -ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' #+END_SRC #+RESULTS: : input(states=11) output(states=9, acc-sets=1, det=1) -In the above command, =ltlfilt= is used to convert the LTL formula -into =ltl2dstar='s syntax. Then =ltl2dstar= creates a deterministic -Rabin automaton (using =ltl2tgba= as an LTL to BA translator), and the -resulting 11-state DRA is converted into a 9-state DTBA by -=dstar2tgba=. Since that result is deterministic, we can conclude -that the formula was a recurrence. +#+NAME: size +#+BEGIN_SRC sh :exports none +ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l | +ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | +dstar2tgba -D --stats=$arg +#+END_SRC + +In the above command, =ltldo= is used to convert the LTL formula into +=ltl2dstar='s syntax. Then =ltl2dstar= creates a deterministic Rabin +automaton (using =ltl2tgba= as an LTL to BA translator), and the +resulting call_size(arg="%S")[:results raw]-state DRA is converted +into a call_size(arg="%s")[:results raw]-state DTBA by =dstar2tgba=. +Since that result is deterministic, we can conclude that the formula +was a recurrence. As far as SAT-based minimization goes, =dstar2tgba= will take the same options as =ltl2tgba=. For instance we can see that the smallest DTBA -has 6 states: +has call_size(arg="%s -x sat-minimize")[:results raw] states: #+BEGIN_SRC sh :results verbatim :exports both -ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' #+END_SRC #+RESULTS: -: input(states=11) output(states=6, acc-sets=1, det=1) +: input(states=11) output(states=4, acc-sets=1, det=1) * More acceptance sets -The formula "=Ga R (F!b & (c U b))=" can in fact be minimized into an +The formula "=G(F(!b & (X!a M (F!a & F!b))) U !b)=" can in fact be minimized into an even smaller automaton if we use multiple acceptance sets. Unfortunately because =dstar2tgba= does not know the formula being @@ -276,12 +284,12 @@ number of acceptance sets can however be specified on the command-line with option =-x sat-acc=M=. For instance: #+BEGIN_SRC sh :results verbatim :exports both -ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' #+END_SRC #+RESULTS: -: input(states=11) output(states=5, acc-sets=2, det=1) +: input(states=11) output(states=3, acc-sets=2, det=1) Beware that the size of the SAT problem is exponential in the number of acceptance sets (adding one acceptance set, in the input automaton @@ -370,7 +378,7 @@ For our example, let us first generate a deterministic Rabin automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]]. #+BEGIN_SRC sh :results silent :exports both -ltlfilt -f "FGa | FGb" -l | +ltlfilt -f 'FGa | FGb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa #+END_SRC @@ -769,7 +777,7 @@ its iterations in this file. #+BEGIN_SRC sh :results verbatim :exports both rm -f stats.csv export SPOT_SATLOG=stats.csv -ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltlfilt -f 'Ga R (F!b & (c U b))' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' cat stats.csv From 1c8c86914fb0ed3021036792ab24e3c02ef47f11 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 May 2016 11:05:16 +0200 Subject: [PATCH 10/18] * doc/org/tut.org: Typo. --- doc/org/tut.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/org/tut.org b/doc/org/tut.org index 609dc981e..b34ab01ce 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -34,7 +34,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. * Examples in Python only -In directory the, =python/tests= [[file:install.org][Spot tarball]] contains a small +In directory =python/tests=, the [[file:install.org][Spot tarball]] contains a small collection of IPython notebooks. As the name of the directory implies, these are part of the test suite for the Python bindings, however they can be interesting to look at if you want to see more code examples. From dc5237c7e74fb4b8e4743113f0f28a37af814269 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Jun 2016 09:56:17 +0200 Subject: [PATCH 11/18] relabel: fix infinite recursion in relabel_bse() MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by František Blahoudek. * spot/tl/relabel.cc: Fix. * tests/core/ltlrel.test: Add test case. * NEWS: Mention the bug. --- NEWS | 1 + spot/tl/relabel.cc | 3 ++- tests/core/ltlrel.test | 14 +++++++++++++- 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index 3f9c05021..32099ec68 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,7 @@ New in spot 2.0.1a (not yet released) * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1 headers. + * Fix an infinite recursion in relabel_bse(). New in spot 2.0.1 (2016-05-09) diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc index 05270453e..90e2a6f0a 100644 --- a/spot/tl/relabel.cc +++ b/spot/tl/relabel.cc @@ -433,13 +433,14 @@ namespace spot /// it as ((a & b) & Xc) in the graph to isolate the /// Boolean operands as a single node. formula b = f.boolean_operands(&i); - if (b) + if (b && b != f) { res.reserve(sz - i + 1); res.push_back(visit(b)); } else { + i = 0; res.reserve(sz); } for (; i < sz; ++i) diff --git a/tests/core/ltlrel.test b/tests/core/ltlrel.test index 13c4de3a0..4f403ef66 100755 --- a/tests/core/ltlrel.test +++ b/tests/core/ltlrel.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013 Laboratoire de Recherche et Dévelopement to +# Copyright (C) 2013, 2016 Laboratoire de Recherche et Dévelopement to # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -77,3 +77,15 @@ t < b p2 -> c EOF + +# This one used to stack overflow due to an infinite recursion +# in the relabeling function. Reported by František Blahoudek. +t <p1 -> ((p0 -> (!p1 U (!p1 && p3 && !p5 && X((!p1 && !p5) U p4)))) U p1) +Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & p3 & X((!p0 & p3) U p4)))) U p0) + p0 -> p1 + p1 -> p0 + p2 -> p3 + p3 -> !p5 + p4 -> p4 +EOF From bb47d13fcd2dd2b3701f1e210e662ff25e1d929c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Jun 2016 11:32:26 +0200 Subject: [PATCH 12/18] fix a few copyright headers * tests/core/ltlcrossgrind.test, tests/core/ltlgrind.test, tests/core/ltlrel.test: Here. --- tests/core/ltlcrossgrind.test | 2 +- tests/core/ltlgrind.test | 4 ++-- tests/core/ltlrel.test | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/core/ltlcrossgrind.test b/tests/core/ltlcrossgrind.test index a9f7b1eb9..1814bcd15 100755 --- a/tests/core/ltlcrossgrind.test +++ b/tests/core/ltlcrossgrind.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014 Laboratoire de Recherche et Dévelopement to +# Copyright (C) 2014 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. diff --git a/tests/core/ltlgrind.test b/tests/core/ltlgrind.test index abc95285c..0cbc0dae4 100755 --- a/tests/core/ltlgrind.test +++ b/tests/core/ltlgrind.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Dévelopement to -# l'Epita (LRDE). +# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # diff --git a/tests/core/ltlrel.test b/tests/core/ltlrel.test index 4f403ef66..b734bee18 100755 --- a/tests/core/ltlrel.test +++ b/tests/core/ltlrel.test @@ -1,7 +1,7 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2016 Laboratoire de Recherche et Dévelopement to -# 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. # From 91e8ced372ffdc753ce301ad8af1050dda7feb75 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Jun 2016 12:02:41 +0200 Subject: [PATCH 13/18] * tests/Makefile.am: Distribute elevator2.1.pm. --- tests/Makefile.am | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/Makefile.am b/tests/Makefile.am index 5e90ddbf4..5c4f69564 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -363,7 +363,8 @@ TESTS_ltsmin = \ ltsmin/finite2.test \ ltsmin/kripke.test -EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/finite.dve ltsmin/finite.pm +EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/elevator2.1.pm \ + ltsmin/finite.dve ltsmin/finite.pm ltlsmin/kripke.log: core/kripkecat$(EXEEXT) From 125ca7df7aa290288d0e82e457c2000dca54a4aa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Jun 2016 14:39:53 +0200 Subject: [PATCH 14/18] tests: reset CFLAGS * tests/run.in: Here. This helps when spins is installed an the tests actually compile code; we do not want to inherit the -std=c11 -fvisibility=hidden set for compiling Spot. --- tests/run.in | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/run.in b/tests/run.in index 8aedf320e..b7ae3b7ae 100755 --- a/tests/run.in +++ b/tests/run.in @@ -48,6 +48,11 @@ test -z "$1" && PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec $PREFIXCMD @PYTHON@ srcdir="@srcdir@" +# Reset CFLAGS, because some tests call the compiler, and we do not +# want to inherit parameters likes -std=c11 -fvisibility=hidden +CFLAGS= +export CFLAGS + case $1 in */*) dir=${1%/*} From b2a306c8d3dc7dfc64aedcb318f3fecfecd1f922 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Jun 2016 14:18:48 +0200 Subject: [PATCH 15/18] python: add the examples from the ATVA'16 paper * tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb: New files. * tests/Makefile.am, doc/org/tut.org: Add them. --- doc/org/tut.org | 2 + tests/Makefile.am | 2 + tests/python/atva16-fig2a.ipynb | 261 ++++++++++++++++++++++++ tests/python/atva16-fig2b.ipynb | 340 ++++++++++++++++++++++++++++++++ 4 files changed, 605 insertions(+) create mode 100644 tests/python/atva16-fig2a.ipynb create mode 100644 tests/python/atva16-fig2b.ipynb diff --git a/doc/org/tut.org b/doc/org/tut.org index b34ab01ce..0932621b1 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -67,3 +67,5 @@ real notebooks instead. - [[https://spot.lrde.epita.fr/ipynb/word.html][=word.ipynb=]] example for the =twa_run= and =twa_word= classes. - [[https://spot.lrde.epita.fr/ipynb/highlighting.html][=highlighting.ipynb=]] shows how to highlight states or edges in automata. +- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2a.html][=atva16-fig2a.ipynb=]] first example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]]. +- [[https://spot.lrde.epita.fr/ipynb/atva16-fig2b.html][=atva16-fig2b.ipynb=]] second example from our [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][ATVA'16 tool paper]]. diff --git a/tests/Makefile.am b/tests/Makefile.am index 5c4f69564..d4e7f7072 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -290,6 +290,8 @@ if USE_PYTHON TESTS_ipython = \ python/acc_cond.ipynb \ python/accparse.ipynb \ + python/atva16-fig2a.ipynb \ + python/atva16-fig2b.ipynb \ python/automata-io.ipynb \ python/automata.ipynb \ python/decompose.ipynb \ diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb new file mode 100644 index 000000000..8e2b789aa --- /dev/null +++ b/tests/python/atva16-fig2a.ipynb @@ -0,0 +1,261 @@ +{ + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.5.2rc1" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This example is the left part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"." + ] + }, + { + "cell_type": "code", + "collapsed": true, + "input": [ + "import spot\n", + "spot.setup(show_default='.abr')" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f = spot.formula('GFa <-> GFb'); f" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "latex": [ + "$\\mathsf{G} \\mathsf{F} a \\leftrightarrow \\mathsf{G} \\mathsf{F} b$" + ], + "metadata": {}, + "output_type": "pyout", + "prompt_number": 2, + "text": [ + "GFa <-> GFb" + ] + } + ], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "f.translate()" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")&Inf(\n", + "\u2776\n", + ")\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & b\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a & !b\n", + "\u24ff\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!a & !b\n", + "\u24ff\n", + "\u2776\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!a & !b\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f77f87ba300> >" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "code", + "collapsed": true, + "input": [ + "def implies(f, g):\n", + " f = spot.formula(f)\n", + " g = spot.formula_Not(spot.formula(g))\n", + " return spot.product(f.translate(), g.translate()).is_empty()\n", + "def equiv(f, g):\n", + " return implies(f, g) and implies(g, f)" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 4 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "equiv('a U (b U a)', 'b U a')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 5, + "text": [ + "True" + ] + } + ], + "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "equiv('!(a U b)', '!a U !b')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 6, + "text": [ + "False" + ] + } + ], + "prompt_number": 6 + } + ], + "metadata": {} + } + ] +} diff --git a/tests/python/atva16-fig2b.ipynb b/tests/python/atva16-fig2b.ipynb new file mode 100644 index 000000000..59023578d --- /dev/null +++ b/tests/python/atva16-fig2b.ipynb @@ -0,0 +1,340 @@ +{ + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.5.2rc1" + }, + "name": "" + }, + "nbformat": 3, + "nbformat_minor": 0, + "worksheets": [ + { + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "This example is the right part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"." + ] + }, + { + "cell_type": "code", + "collapsed": true, + "input": [ + "import spot\n", + "import spot.ltsmin\n", + "spot.setup(show_default='.abr', max_states=10)\n", + "# This extra line ensures that our test-suite skips this test if divine is not installed.\n", + "spot.ltsmin.require('divine')" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 1 + }, + { + "cell_type": "code", + "collapsed": true, + "input": [ + "%%dve adding\n", + "int c=1, x1, x2;\n", + "process a1 {\n", + " state Q, R, S; init Q;\n", + " trans Q -> R { guard c<20; effect x1 = c; },\n", + " R -> S { effect x1 = x1 + c; },\n", + " S -> Q { effect c = x1; };\n", + "}\n", + "process a2 {\n", + " state Q, R, S; init Q;\n", + " trans Q -> R { guard c<20; effect x2 = c; },\n", + " R -> S { effect x2 = x2 + c; },\n", + " S -> Q { effect c = x2; };\n", + "}\n", + "system async;" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 2 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "adding" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 3, + "text": [ + "ltsmin model with the following variables:\n", + " c: int\n", + " x1: int\n", + " x2: int\n", + " a1: ['Q', 'R', 'S']\n", + " a2: ['Q', 'R', 'S']" + ] + } + ], + "prompt_number": 3 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "adding.kripke(['a1.Q', 'c==17'])" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 4, + "svg": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "G\n", + "\n", + "t\n", + "\n", + "\n", + "0\n", + "\n", + "c=1, x1=0, x2=0, a1=0, a2=0\n", + "a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "c=1, x1=1, x2=0, a1=1, a2=0\n", + "!a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "c=1, x1=0, x2=1, a1=0, a2=1\n", + "a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "c=1, x1=2, x2=0, a1=2, a2=0\n", + "!a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "c=1, x1=1, x2=1, a1=1, a2=1\n", + "!a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "c=1, x1=0, x2=2, a1=0, a2=2\n", + "a1.Q & !"c==17" & !dead\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "c=2, x1=2, x2=0, a1=0, a2=0\n", + "...\n", + "\n", + "\n", + "3->6\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "c=1, x1=2, x2=1, a1=2, a2=1\n", + "...\n", + "\n", + "\n", + "3->7\n", + "\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "c=1, x1=1, x2=2, a1=1, a2=2\n", + "...\n", + "\n", + "\n", + "4->8\n", + "\n", + "\n", + "\n", + "\n", + "5->8\n", + "\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "c=2, x1=0, x2=2, a1=0, a2=0\n", + "...\n", + "\n", + "\n", + "5->9\n", + "\n", + "\n", + "\n", + "\n", + "u6\n", + "\n", + "...\n", + "\n", + "\n", + "6->u6\n", + "\n", + "\n", + "\n", + "\n", + "u7\n", + "\n", + "...\n", + "\n", + "\n", + "7->u7\n", + "\n", + "\n", + "\n", + "\n", + "u8\n", + "\n", + "...\n", + "\n", + "\n", + "8->u8\n", + "\n", + "\n", + "\n", + "\n", + "u9\n", + "\n", + "...\n", + "\n", + "\n", + "9->u9\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text": [ + " *' at 0x7f3406f6f5d0> >" + ] + } + ], + "prompt_number": 4 + }, + { + "cell_type": "code", + "collapsed": true, + "input": [ + "def model_check(model, f):\n", + " f = spot.formula(f)\n", + " ss = model.kripke(spot.atomic_prop_collect(f))\n", + " nf = spot.formula_Not(f).translate()\n", + " return spot.otf_product(ss, nf).is_empty()" + ], + "language": "python", + "metadata": {}, + "outputs": [], + "prompt_number": 5 + }, + { + "cell_type": "code", + "collapsed": false, + "input": [ + "model_check(adding, 'F(\"c==2\")')" + ], + "language": "python", + "metadata": {}, + "outputs": [ + { + "metadata": {}, + "output_type": "pyout", + "prompt_number": 6, + "text": [ + "True" + ] + } + ], + "prompt_number": 6 + } + ], + "metadata": {} + } + ] +} From 5f3cc5225541738844150b7f269657a46d6bcdd9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Jun 2016 15:06:15 +0200 Subject: [PATCH 16/18] org: add a citing page With a reference to the "to appear" ATVA'16 paper. * doc/org/citing.org: New file. * doc/Makefile.am: Add it. * doc/org/index.org, doc/org/tools.org: Link to it. --- doc/Makefile.am | 1 + doc/org/citing.org | 79 ++++++++++++++++++++++++++++++++++++++++++++++ doc/org/index.org | 8 ++++- doc/org/tools.org | 30 +++--------------- 4 files changed, 92 insertions(+), 26 deletions(-) create mode 100644 doc/org/citing.org diff --git a/doc/Makefile.am b/doc/Makefile.am index 9f9f46512..3a2307f5e 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -74,6 +74,7 @@ ORG_FILES = \ $(srcdir)/org/arch.png \ org/autfilt.org \ org/csv.org \ + org/citing.org \ org/compile.org \ org/concepts.org \ org/dstar2tgba.org \ diff --git a/doc/org/citing.org b/doc/org/citing.org new file mode 100644 index 000000000..8f9e4dc06 --- /dev/null +++ b/doc/org/citing.org @@ -0,0 +1,79 @@ +# -*- coding: utf-8 -*- +#+TITLE: Citing Spot +#+DESCRIPTION: Paper related to Spot +#+SETUPFILE: setup.org +#+HTML_LINK_UP: index.html + +* Generic reference + +If you need to cite the Spot project in some academic paper, please +use the following reference: + +- *Spot 2.0 –- a framework for LTL and ω-automata manipulation*, + /Alexandre Duret-Lutz/, /Alexandre Lewkowicz/, /Amaury Fauchille/, + /Thibaud Michaud/, /Etienne Renault/, and /Laurent Xu/. To appear + in Proc. of ATVA'16. Chiba, Japan, Oct. 2016. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.16.atva2][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.16.atva2.pdf][pdf]]) + + This provides a quick overview of the entire project (the features + of the library, [[file:tools.org][the tools]], the Python bindings), and provides many + references detailing more specific aspects. + + +* Other, more specific, references + +Alternatively, you may also like to reference these papers to +be more specific about a particular aspect of Spot. + +- *Manipulating LTL formulas using Spot 1.0*, /Alexandre Duret-Lutz/. + In Proc. of ATVA'13, LNCS 8172, pp. 442--445. Hanoi, Vietnam, + Oct. 2013. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.13.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.slides.pdf][slides]]) + + This focuses on the tools [[file:ltlfilt.org][=ltlfilt=]], [[file:randltl.org][=randltl=]], and [[file:ltlcross.org][=ltlcross=]]. + +- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/. + Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014. + ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]]) + + This describes the translation from LTL to TGBA used by the + [[file:ltl2tgba.org][=ltl2tgba=]] tool. + +- *Model checking using generalized testing automata*, /Ala Eddine Ben + Salem/, /Alexandre Duret-Lutz/, and /Fabrice Kordon/. In + Transactions on Petri Nets and Other Models of Concurrency (ToPNoC + VI), 7400:94--112, 2012. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#bensalem.12.topnoc][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/bensalem.12.topnoc.pdf][pdf]]) + + This describes the generalized testing automata produced by the + [[file:ltl2tgta.org][=ltl2tgta=]] tool. + +- *SAT-based minimization of deterministic ω-automata*, /Souheib + Baarir/ and /Alexandre Duret-Lutz/. In Proc. of LPAR'15, LNCS 9450, + pp. 79--87. Nov. 2015. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#baarir.15.lpar][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/baarir.15.lpar.pdf][pdf]]) + + This describes our [[file:satmin.org][SAT-based minimization technique]], working with + deterministic automata of arbitrary acceptance condition. + +- *Practical stutter-invariance checks for ω-regular languages*, + /Thibaud Michaud/ and /Alexandre Duret-Lutz/. In Proc. of SPIN'15, + LNCS 9232, pp. 84--101. Aug. 2015. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#michaud.15.spin][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/michaud.15.spin.pdf][pdf]]) + + Explains how the stutter-invariance checks of Spot are implemented. + +- *The Hanoi Omega-Automata format*, /Tomáš Babiak/, /František + Blahoudek/, /Alexandre Duret-Lutz/, /Joachim Klein/, /Jan + Křetínský/, /David Müller/, /David Parker/, and /Jan Strejček/. In + Proc. of CAV'15, LNCS 9206, pp. 479--486. July 2015. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#babiak.15.cav][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.15.cav.pdf][pdf]] | + [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.15.cav.slides.pdf][slides]] | [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.15.cav.poster.pdf][poster]]) + + Presents the automaton format [[file:hoa.org][supported by Spot 2.0]] and [[http://adl.github.io/hoaf/support.html][several other + tools]]. + + +* Obsolete reference + +- *Spot: an extensible model checking library using transition-based + generalized Büchi automata*, /Alexandre Duret-Lutz/ and /Denis + Poitrenaud/. In Proc. of MASCOTS'04, pp. 76--83. Volendam, The + Netherlands, Oct. 2004. Volendam. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.04.mascots][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.04.mascots.draft.pdf][pdf]]) + + For a while, this used to be the only paper presenting Spot as a + model-checking library. diff --git a/doc/org/index.org b/doc/org/index.org index bffc627ae..53eb4fc59 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -57,7 +57,8 @@ The latest version is *{{{LASTRELEASE}}}* and was released on Spot is distributed under a [[http://www.gnu.org/licenses/gpl-3.0.html][GNU GPL v3 license]]. A consequence is that if you distribute a tool built using Spot, you -*must* make the source code of that tool available as well. +*must* make the source code of that tool available as well, under a +compatible license. * Staying in touch @@ -68,3 +69,8 @@ informed about future releases of Spot, we invite you to [[https://lists.lrde.ep [[mailto:spot@lrde.epita.fr][=spot@lrde.epita.fr=]] is a list for general discussions and questions about Spot. [[https://lists.lrde.epita.fr/listinfo/spot][Subscribe here]] if you want to join, but feel free to send in any question (in English) or bug report without subscribing. + +* Citing + +Our [[file:citing.org][citing page]] has a list of papers you could cite if you need to +reference Spot in an academic publication. diff --git a/doc/org/tools.org b/doc/org/tools.org index 81acd065c..9b1ccd10e 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -82,32 +82,12 @@ convenience, you can browse their HTML versions: * Citing -If you want to refer to these tools in an article, please cite one of -the following articles: +If some of these tools have played a significant role in a work that +lead to some academic publication, please consider citing Spot. Our +[[file:citing.org][citing page]] has a list of papers you could cite. -- *Manipulating LTL formulas using Spot 1.0*, /Alexandre Duret-Lutz/. - In Proc. of ATVA'13, LNCS 8172, pp. 442--445. Hanoi, Vietnam, - Oct. 2013. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.13.atva][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.13.atva.slides.pdf][slides]]) - - This focuses on =ltlfilt=, =randltl=, and =ltlcross=. - -- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/. - Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014. - ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]]) - - This describes the translation from LTL to TGBA used by =ltl2tgba= - and =ltl2tgta=. - -- *Model checking using generalized testing automata*, /Ala Eddine Ben - Salem/, /Alexandre Duret-Lutz/, and /Fabrice Kordon/. In - Transactions on Petri Nets and Other Models of Concurrency (ToPNoC - VI), 7400:94--112, 2012. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#bensalem.12.topnoc][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/bensalem.12.topnoc.pdf][pdf]]) - - This describes the generalized testing automata produced by =ltl2tgta=. - - -Check the man page for each tool for additional references about the -algorithms or data sources used. +Additionally, the man pages of these tools also contains additional +references about the algorithms or data sources used. # LocalWords: num toc helloworld SRC LTL PSL randltl ltlfilt genltl # LocalWords: scalable ltl tgba Büchi automata tgta ltlcross eval From 1cce09bc807f04698bef88264694b64f62ce9eb8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Jun 2016 16:33:30 +0200 Subject: [PATCH 17/18] Release Spot 2.0.2 * NEWS: Update. * configure.ac, doc/org/setup.org: Bump version. --- NEWS | 10 +++++++++- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 15 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 32099ec68..5ab1fc495 100644 --- a/NEWS +++ b/NEWS @@ -1,10 +1,18 @@ -New in spot 2.0.1a (not yet released) +New in spot 2.0.2 (2016-06-17) + + Documentation: + + * We now have a citing page at https://spot.lrde.epita.fr/citing.html + providing a list of references about Spot. + * The Python examples have been augmented with the two examples + from our ATVA'16 tool paper. Bug fixes: * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1 headers. * Fix an infinite recursion in relabel_bse(). + * Various small typos and cosmetic cleanups. New in spot 2.0.1 (2016-05-09) diff --git a/configure.ac b/configure.ac index 63ba9b33d..c723349e7 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.1a], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.0.2], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/setup.org b/doc/org/setup.org index fc75f5d4c..db227b7b2 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.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 +#+MACRO: SPOTVERSION 2.0.2 +#+MACRO: LASTRELEASE 2.0.2 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.0.2.tar.gz][=spot-2.0.2.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-0-2/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2016-06-17 From 01e71d108ae139d828714da5f5cd8ea56d0ed829 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Jun 2016 16:40:51 +0200 Subject: [PATCH 18/18] * 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 5ab1fc495..47bc514b9 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.0.2a (Not yet released) + + Nothing yet. + New in spot 2.0.2 (2016-06-17) Documentation: diff --git a/configure.ac b/configure.ac index c723349e7..3cd608570 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.2], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.0.2a], [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])