From 8f7a0c2f7a0e78f6e5bf0292d14781d50fde6dcc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Feb 2019 21:56:15 +0100 Subject: [PATCH 01/11] python: improve kripke_graph bindings Related to issue #376. * spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the benefit of Swig. * python/spot/impl.i: Add bindings for iterators over kripke_graph states and edges. * tests/python/kripke.py: New file. * tests/Makefile.am: Add it. * NEWS: Update. --- NEWS | 6 ++- python/spot/impl.i | 33 +++++++++++++++++ spot/kripke/kripkegraph.hh | 75 +++++++++++++++++++++++++++++++++++--- tests/Makefile.am | 3 +- tests/python/kripke.py | 75 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 184 insertions(+), 8 deletions(-) create mode 100644 tests/python/kripke.py diff --git a/NEWS b/NEWS index d916a7795..973116ec6 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.7.1.dev (not yet released) - Nothing yet. + Python: + + - Improved support for explicit Kripke structure. It is now + possible to iterate over a kripke_graph object in a way similar to + twa_graph. New in spot 2.7.1 (2019-02-14) diff --git a/python/spot/impl.i b/python/spot/impl.i index 38bdeb916..c8b86a160 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -549,19 +549,29 @@ namespace std { %nodefaultctor spot::internal::killer_edge_iterator; %nodefaultctor spot::internal::all_trans; %nodefaultctor spot::internal::universal_dests; +%traits_swigtype(spot::internal::distate_storage >); +%fragment(SWIG_Traits_frag(spot::internal::distate_storage >)); %traits_swigtype(spot::internal::edge_storage >); %fragment(SWIG_Traits_frag(spot::internal::edge_storage >)); +%traits_swigtype(spot::internal::edge_storage >); +%fragment(SWIG_Traits_frag(spot::internal::edge_storage >)); %typemap(out, optimal="1") spot::internal::all_trans> { $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, SWIG_POINTER_OWN); } +%typemap(out, optimal="1") spot::internal::all_trans> { + $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, + SWIG_POINTER_OWN); +} + %typemap(out, optimal="1") spot::internal::const_universal_dests { $result = SWIG_NewPointerObj(new $1_ltype($1), $&1_descriptor, SWIG_POINTER_OWN); } +%noexception spot::kripke_graph::edges; %noexception spot::twa_graph::edges; %noexception spot::twa_graph::univ_dests; @@ -681,6 +691,13 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%template(kripke_graph_state_out) spot::internal::state_out>; +%template(kripke_graph_all_trans) spot::internal::all_trans>; +%template(kripke_graph_edge_boxed_data) spot::internal::boxed_label; +%template(kripke_graph_edge_storage) spot::internal::edge_storage >; +%template(kripke_graph_state_boxed_data) spot::internal::boxed_label; +%template(kripke_graph_state_storage) spot::internal::distate_storage >; +%template(kripke_graph_state_vector) std::vector>>; %include @@ -949,6 +966,14 @@ static void* ptr_for_bdddict(PyObject* obj) } } +%extend spot::internal::state_out> { + swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) + { + return swig::make_forward_iterator(self->begin(), self->begin(), + self->end(), *PYTHON_SELF); + } +} + %extend spot::internal::killer_edge_iterator> { spot::internal::edge_storage >& current() @@ -966,6 +991,14 @@ static void* ptr_for_bdddict(PyObject* obj) } } +%extend spot::internal::all_trans> { + swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) + { + return swig::make_forward_iterator(self->begin(), self->begin(), + self->end(), *PYTHON_SELF); + } +} + %extend spot::internal::all_trans> { swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF) { diff --git a/spot/kripke/kripkegraph.hh b/spot/kripke/kripkegraph.hh index a8bde37a0..348e1ccf5 100644 --- a/spot/kripke/kripkegraph.hh +++ b/spot/kripke/kripkegraph.hh @@ -152,7 +152,28 @@ namespace spot { public: typedef digraph graph_t; - typedef graph_t::edge_storage_t edge_storage_t; + // We avoid using graph_t::edge_storage_t because graph_t is not + // instantiated in the SWIG bindings, and SWIG would therefore + // handle graph_t::edge_storage_t as an abstract type. + typedef internal::edge_storage> + edge_storage_t; + static_assert(std::is_same::value, "type mismatch"); + + typedef internal::distate_storage> + state_storage_t; + static_assert(std::is_same::value, "type mismatch"); + typedef std::vector state_vector; + + // We avoid using graph_t::state for the very same reason. + typedef unsigned state_num; + static_assert(std::is_same::value, + "type mismatch"); + protected: graph_t g_; mutable unsigned init_number_; @@ -177,7 +198,7 @@ namespace spot return g_.num_edges(); } - void set_init_state(graph_t::state s) + void set_init_state(state_num s) { if (SPOT_UNLIKELY(s >= num_states())) throw std::invalid_argument @@ -185,7 +206,7 @@ namespace spot init_number_ = s; } - graph_t::state get_init_state_number() const + state_num get_init_state_number() const { // If the kripke has no state, it has no initial state. if (num_states() == 0) @@ -218,7 +239,7 @@ namespace spot } - graph_t::state + state_num state_number(const state* st) const { auto s = down_cast(st); @@ -226,13 +247,13 @@ namespace spot } const kripke_graph_state* - state_from_number(graph_t::state n) const + state_from_number(state_num n) const { return &g_.state_data(n); } kripke_graph_state* - state_from_number(graph_t::state n) + state_from_number(state_num n) { return &g_.state_data(n); } @@ -282,6 +303,48 @@ namespace spot { return g_.new_edge(src, dst); } + + +#ifndef SWIG + const state_vector& states() const + { + return g_.states(); + } +#endif + + state_vector& states() + { + return g_.states(); + } + +#ifndef SWIG + internal::all_trans + edges() const noexcept + { + return g_.edges(); + } +#endif + + internal::all_trans + edges() noexcept + { + return g_.edges(); + } + +#ifndef SWIG + internal::state_out + out(unsigned src) const + { + return g_.out(src); + } +#endif + + internal::state_out + out(unsigned src) + { + return g_.out(src); + } + }; typedef std::shared_ptr kripke_graph_ptr; diff --git a/tests/Makefile.am b/tests/Makefile.am index 2f42108f7..4b332e243 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -372,7 +372,6 @@ TESTS_python = \ python/bugdet.py \ python/complement_semidet.py \ python/declenv.py \ - python/_word.ipynb \ python/decompose_scc.py \ python/dualize.py \ python/except.py \ @@ -380,6 +379,7 @@ TESTS_python = \ python/genem.py \ python/implies.py \ python/interdep.py \ + python/kripke.py \ python/ltl2tgba.test \ python/ltlf.py \ python/ltlparse.py \ @@ -417,6 +417,7 @@ TESTS_python = \ python/tra2tba.py \ python/twagraph.py \ python/toweak.py \ + python/_word.ipynb \ $(TESTS_ipython) endif diff --git a/tests/python/kripke.py b/tests/python/kripke.py new file mode 100644 index 000000000..30f07a81f --- /dev/null +++ b/tests/python/kripke.py @@ -0,0 +1,75 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2019 Laboratoire de Recherche et Développement de l'Epita +# (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +import spot +import buddy +bdict = spot.make_bdd_dict() +k = spot.make_kripke_graph(bdict) +p1 = buddy.bdd_ithvar(k.register_ap("p1")) +p2 = buddy.bdd_ithvar(k.register_ap("p2")) +cond1 = p1 & p2 +cond2 = p1 & -p2 +cond3 = -p1 & -p2 +s2 = k.new_state(cond1) +s1 = k.new_state(cond2) +s3 = k.new_state(cond3) +k.new_edge(s1, s2) +k.new_edge(s2, s2) +k.new_edge(s1, s3) +k.new_edge(s3, s3) +k.new_edge(s3, s2) +k.set_init_state(s1) + +hoa="""HOA: v1 +States: 3 +Start: 0 +AP: 2 "p1" "p2" +acc-name: all +Acceptance: 0 t +properties: state-labels explicit-labels state-acc +--BODY-- +State: [0&!1] 0 "1" +1 2 +State: [0&1] 1 "0" +1 +State: [!0&!1] 2 "2" +2 1 +--END--""" +assert hoa == k.to_str('HOA') +assert k.num_states() == 3 +assert k.num_edges() == 5 + +res = [] +for e in k.out(s1): + res.append((e.src, e.dst)) +assert res == [(1, 0), (1, 2)] + +res = [] +for e in k.edges(): + res.append((e.src, e.dst)) +assert res == [(1, 0), (0, 0), (1, 2), (2, 2), (2, 0)] + +res = [] +for s in k.states(): + res.append(s.cond()) +assert res == [cond1, cond2, cond3] + +assert k.states()[0].cond() == cond1 +assert k.states()[1].cond() == cond2 +assert k.states()[2].cond() == cond3 From 25133cac2893e13f7e5d972e60b6e58fea9fdaad Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Feb 2019 15:35:42 +0100 Subject: [PATCH 02/11] org: add explicit Kripke structure example Fixes #376. * doc/org/tut52.org: New file. * doc/org/tut.org, doc/org/tut51.org: Link to it. * doc/Makefile.am: Add it. --- doc/Makefile.am | 3 +- doc/org/tut.org | 1 + doc/org/tut51.org | 19 +-- doc/org/tut52.org | 305 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 319 insertions(+), 9 deletions(-) create mode 100644 doc/org/tut52.org diff --git a/doc/Makefile.am b/doc/Makefile.am index c6fbe19bf..de8eac0ab 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010-2011, 2013-2018 Laboratoire de Recherche et +## Copyright (C) 2010-2011, 2013-2019 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -113,6 +113,7 @@ ORG_FILES = \ org/tut31.org \ org/tut50.org \ org/tut51.org \ + org/tut52.org \ org/upgrade2.org \ org/satmin.org \ org/satmin.tex \ diff --git a/doc/org/tut.org b/doc/org/tut.org index a68751a92..7e812b2f3 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -36,6 +36,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut22.org][Creating an automaton by adding states and transitions]] - [[file:tut23.org][Creating an alternating automaton by adding states and transitions]] - [[file:tut24.org][Iterating over alternating automata]] +- [[file:tut52.org][Creating an explicit Kripke structure]] * Examples in C++ only diff --git a/doc/org/tut51.org b/doc/org/tut51.org index 884cd3272..3ad26467c 100644 --- a/doc/org/tut51.org +++ b/doc/org/tut51.org @@ -13,11 +13,14 @@ represent the state space of the model to verify. * Implementing a toy Kripke structure In this example, our goal is to implement a Kripke structure that -constructs its state space on the fly. The states of our toy model -will consist of a pair of modulo-3 integers $(x,y)$; and at any state -the possible actions will be to increment any one of the two integer -(nondeterministicaly). That increment is obviously done modulo 3. -For instance state $(1,2)$ has two possible successors: +constructs its state space on the fly. ([[file:tut52.org][Another page]] shows how to +implement this Kripke structure using an explicit graph instead.) + +The states of our toy model will consist of a pair of modulo-3 +integers $(x,y)$; and at any state the possible actions will be to +increment any one of the two integer (nondeterministicaly). That +increment is obviously done modulo 3. For instance state $(1,2)$ has +two possible successors: - $(2,2)$ if =x= was incremented, or - $(1,0)$ if =y= was incremented. Initially both variables will be 0. The complete state space is @@ -396,6 +399,9 @@ $txt [[file:kripke-1.svg]] * Checking a property on this state space + :PROPERTIES: + :CUSTOM_ID: prop-check + :END: Let us pretend that we want to verify the following property: if =odd_x= infinitely often holds, then =odd_y= infinitely often holds. @@ -412,7 +418,6 @@ counterexample: #+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim #include #include -#include #include <> int main() @@ -469,7 +474,6 @@ We also pass option "~A~" to hide the acceptance condition (which is #include #include #include - #include #include <> int main() @@ -521,7 +525,6 @@ figure: #include #include #include - #include #include <> int main() diff --git a/doc/org/tut52.org b/doc/org/tut52.org new file mode 100644 index 000000000..f75865f3f --- /dev/null +++ b/doc/org/tut52.org @@ -0,0 +1,305 @@ +# -*- coding: utf-8 -*- +#+TITLE: Playing with explicit Kripke structures +#+DESCRIPTION: Kripke structures that are fully stored in memory, as explicit graphs. +#+INCLUDE: setup.org +#+HTML_LINK_UP: tut.html + +Kripke structures, can be defined as ω-automata in which labels are on +states, and where all runs are accepting (i.e., the acceptance +condition is =t=). They are typically used by model checkers to +represent the state space of the model to verify. + +On [[file:tut51.org][another page]] we have described how to implement a Kripke structure +that can be explored on the fly, by implementing a function that take +the current state, and produce its successor states. While +implementing an on-the-fly Kripke structure is good for large example, +it requires some implementation effort we are not always willing to +put for a toy example. + +This document shows how to create a Kripke structure that is stored as +an explicit graph. The class for those is =spot::kripke_graph= and +works in a similar way as the class =spot::twa_graph= used for +automata. The main difference between those two classes is that +Kripke structures labels the states instead of the transitions. Using +=spot::kripke_graph= instead of =spot::twa_graph= saves a bit of +memory. + +Our Kripke structure represent a model whose states consist of pairs +of modulo-3 integers $(x,y)$. At any state the possible actions +will be to increment any one of the two integer (nondeterministicaly). +That increment is obviously done modulo 3. For instance state $(1,2)$ +has two possible successors: + - $(2,2)$ if =x= was incremented, or + - $(1,0)$ if =y= was incremented. +Initially both variables will be 0. The complete state space has +9 states, that we will store explicitly as a graph. + +In addition, we would like to label each state by atomic propositions +=odd_x= and =odd_y= that are true only when the corresponding +variables are odd. Using such variables, we could try to verify +whether if =odd_x= infinitely often holds, then =odd_y= infinitely +often holds as well. + + +* C++ implementation +** Building the state space + +Here is how we could create the Kripke structure: + +#+NAME: create-kripke +#+BEGIN_SRC C++ + #include + + spot::kripke_graph_ptr create_kripke(spot::bdd_dict_ptr dict, + bool named_states = false) + { + spot::kripke_graph_ptr k = spot::make_kripke_graph(dict); + + bdd odd_x = bdd_ithvar(k->register_ap("odd_x")); + bdd odd_y = bdd_ithvar(k->register_ap("odd_y")); + + unsigned x0y0 = k->new_state((!odd_x) & !odd_y); + unsigned x0y1 = k->new_state((!odd_x) & odd_y); + unsigned x0y2 = k->new_state((!odd_x) & !odd_y); + unsigned x1y0 = k->new_state(odd_x & !odd_y); + unsigned x1y1 = k->new_state(odd_x & odd_y); + unsigned x1y2 = k->new_state(odd_x & !odd_y); + unsigned x2y0 = k->new_state((!odd_x) & !odd_y); + unsigned x2y1 = k->new_state((!odd_x) & odd_y); + unsigned x2y2 = k->new_state((!odd_x) & !odd_y); + + k->set_init_state(x0y0); + + k->new_edge(x0y0, x0y1); k->new_edge(x0y0, x1y0); + k->new_edge(x0y1, x0y2); k->new_edge(x0y1, x1y1); + k->new_edge(x0y2, x0y0); k->new_edge(x0y2, x1y2); + k->new_edge(x1y0, x1y1); k->new_edge(x1y0, x2y0); + k->new_edge(x1y1, x1y2); k->new_edge(x1y1, x2y1); + k->new_edge(x1y2, x1y0); k->new_edge(x1y2, x2y2); + k->new_edge(x2y0, x2y1); k->new_edge(x2y0, x0y0); + k->new_edge(x2y1, x2y2); k->new_edge(x2y1, x0y1); + k->new_edge(x2y2, x2y0); k->new_edge(x2y2, x0y2); + + if (named_states) + { + auto names = new std::vector + { "x0y0", "x0y1", "x0y2", + "x1y0", "x1y1", "x1y2", + "x2y0", "x2y1", "x2y2" }; + k->set_named_prop("state-names", names); + } + return k; + } +#+END_SRC + +To display this Kripke structure, we can call the =print_dot()= +function: + +#+NAME: print-dot +#+BEGIN_SRC C++ :noweb strip-export :results verbatim :export code + #include + <> + int main() + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::print_dot(std::cout, create_kripke(dict)); + } +#+END_SRC + +=print_dot()= will output the graph in [[https://graphviz.gitlab.io/][GraphViz's syntax]], and you just +have to pass it to GraphViz's =dot= command to render it: + +#+BEGIN_SRC dot :file kripke-52.svg :cmd circo :var txt=print-dot :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52.svg]] + +By default, states are just numbered. If you want to name them, for +instance for debugging, you should define the ="state-names"= +properties to a vector of names. Our =create_kripke()= function does +that when passed a true argument. + +#+NAME: print-dot-2 +#+BEGIN_SRC C++ :noweb strip-export :results verbatim :export code + #include + <> + int main() + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::print_dot(std::cout, create_kripke(dict, true)); + } +#+END_SRC + +#+BEGIN_SRC dot :file kripke-52b.svg :cmd circo :var txt=print-dot-2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52b.svg]] + +** Checking a property on this state space + +Let us pretend that we want to verify the following property: if +=odd_x= infinitely often holds, then =odd_y= infinitely often holds. + +In LTL, that would be =GF(odd_x) -> GF(odd_y)=. + +To check this formula, we translate its negation into an automaton, +build the product of this automaton with our Kripke structure, and +check whether the output is empty. If it is not, that means we have +found a counterexample. Here is some code that would show this +counterexample: + +#+NAME: demo-2 +#+BEGIN_SRC C++ -r :exports code :noweb strip-export :results verbatim +#include +#include +#include +<> +int main() +{ + auto d = spot::make_bdd_dict(); + + // Parse the input formula. + spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)"); + if (pf.format_errors(std::cerr)) + return 1; + + // Translate its negation. + spot::formula f = spot::formula::Not(pf.f); + spot::twa_graph_ptr af = spot::translator(d).run(f); + + // Find a run of our Kripke structure that intersects af. + auto k = create_kripke(d, true); (ref:ck) + if (auto run = k->intersecting_run(af)) + std::cout << "formula is violated by the following run:\n" << *run; + else + std::cout << "formula is verified\n"; +} +#+END_SRC + +# temporary fix for an issue in Org 9.2, see +# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html +#+BEGIN_SRC text :noweb yes +<> +#+END_SRC + +Note that this main function is similar to the main function we used +for [[file:tut51.org::#check-prop][the on-the-fly version]] except for [[(ck)][the line that creates the Kripke +structure]]. You can modify it to display the counterexample in a +similar way. + +* Python implementation +** Building the state space + +#+NAME: create-kripke-py +#+BEGIN_SRC python -r + import spot + from buddy import bdd_ithvar + + def create_kripke(bdddict, name_states=False): + k = spot.make_kripke_graph(bdddict) + odd_x = bdd_ithvar(k.register_ap("odd_x")) + odd_y = bdd_ithvar(k.register_ap("odd_y")) + + x0y0 = k.new_state(-odd_x & -odd_y); + x0y1 = k.new_state(-odd_x & odd_y); + x0y2 = k.new_state(-odd_x & -odd_y); + x1y0 = k.new_state(odd_x & -odd_y); + x1y1 = k.new_state(odd_x & odd_y); + x1y2 = k.new_state(odd_x & -odd_y); + x2y0 = k.new_state(-odd_x & -odd_y); + x2y1 = k.new_state(-odd_x & odd_y); + x2y2 = k.new_state(-odd_x & -odd_y); + + k.set_init_state(x0y0); + + k.new_edge(x0y0, x0y1); k.new_edge(x0y0, x1y0); + k.new_edge(x0y1, x0y2); k.new_edge(x0y1, x1y1); + k.new_edge(x0y2, x0y0); k.new_edge(x0y2, x1y2); + k.new_edge(x1y0, x1y1); k.new_edge(x1y0, x2y0); + k.new_edge(x1y1, x1y2); k.new_edge(x1y1, x2y1); + k.new_edge(x1y2, x1y0); k.new_edge(x1y2, x2y2); + k.new_edge(x2y0, x2y1); k.new_edge(x2y0, x0y0); + k.new_edge(x2y1, x2y2); k.new_edge(x2y1, x0y1); + k.new_edge(x2y2, x2y0); k.new_edge(x2y2, x0y2); + + if name_states: + k.set_state_names(["x0y0", "x0y1", "x0y2", (ref:ns) + "x1y0", "x1y1", "x1y2", + "x2y0", "x2y1", "x2y2"]) + return k; +#+END_SRC + +To display this structure, we would just call =to_str('dot')= (and +convert the resulting textual output into graphical form using the +=dot= command). + +#+NAME: print-dot-py +#+BEGIN_SRC python :noweb strip-export :results output :export code +<> +k = create_kripke(spot.make_bdd_dict()) +print(k.to_str('dot')) +#+END_SRC + +=print_dot()= will output the graph in [[https://graphviz.gitlab.io/][GraphViz's syntax]], and you just +have to pass it to GraphViz's =dot= command to render it: + +#+BEGIN_SRC dot :file kripke-52c.svg :cmd circo :var txt=print-dot-py :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52c.svg]] + +Again, states may be named if that can help. This is done by passing +a vector of names (indexed by state numbers) to the =set_name_states()= method, +[[(ns)][as done conditionally in our =create_kripke()= function]]. + + +#+NAME: print-dot-py-2 +#+BEGIN_SRC python :noweb strip-export :results output :export code +<> +k = create_kripke(spot.make_bdd_dict(), True) +print(k.to_str('dot')) +#+END_SRC + +#+BEGIN_SRC dot :file kripke-52d.svg :cmd circo :var txt=print-dot-py-2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52d.svg]] + + +** Checking a property on this state space + +Here is the Python code equivalent to our C++ check. Please +read the C++ description for details. + +#+NAME: demo-2py +#+BEGIN_SRC python -r :exports code :noweb strip-export :results output + <> + + d = spot.make_bdd_dict() + + # Translate the negation of the formula + f = spot.formula.Not("GF(odd_x) -> GF(odd_y)") + af = spot.translate(f, dict=d) + + # Find a run of our Kripke structure that intersects af. + k = create_kripke(d, True) + run = k.intersecting_run(af) + if run: + print("formula is violated by the following run:\n", run) + else: + print("formula is verified") +#+END_SRC + +# temporary fix for an issue in Org 9.2, see +# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html +#+BEGIN_SRC text :noweb yes +<> +#+END_SRC From 8512a2d52606db3520fa1cda465071a6e2cb8147 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Feb 2019 16:17:29 +0100 Subject: [PATCH 03/11] org: improve Python formating * doc/org/spot.css: Use bold for "def", "from", "import". * doc/org/init.el.in: Prevent tabs from being inserted when the code is indented before export. --- doc/org/init.el.in | 3 +++ doc/org/spot.css | 8 ++------ 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/doc/org/init.el.in b/doc/org/init.el.in index b515d31a7..cfa43eefd 100644 --- a/doc/org/init.el.in +++ b/doc/org/init.el.in @@ -54,6 +54,9 @@ ;; conditions when doing concurrent builds. (setq org-publish-timestamp-directory "@abs_top_builddir@/.org-timestamps/") +;; Prevent tabs from being inserted when org-mode reindent some code. +(setq-default indent-tabs-mode nil) + (org-babel-do-load-languages 'org-babel-load-languages `((,(if (version< org-version "8.3") 'sh 'shell) . t) diff --git a/doc/org/spot.css b/doc/org/spot.css index ef1dfe6de..0dbe505ae 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -43,18 +43,14 @@ thead tr{background:#ffe35e} #content tbody:nth-child(even) tr:nth-child(even){background:#fff3bc} #content tbody:nth-child(even) tr:nth-child(odd){background:#fffbe0} .org-svg{max-width:100%;width:auto} -.org-keyword{font-weight:bold} -.org-builtin{font-weight:bold} -.org-preprocessor{font-weight:bold} +.org-keyword,.org-builtin,.org-preprocessor,.org-py-import-from,.org-py-def-class{font-weight:bold} .org-string{font-weight:bold;color:#00adad} .src-hoa .org-string{font-weight:bold;color:#d70079} .org-function-name{font-weight:bold;color:#d70079} .org-type{font-weight:bold;color:#00adad} .org-comment-delimiter{font-weight:bold;color:#a13672} .org-comment{font-style:italic;color:#a13672} -.org-hoa-keyword{font-weight:bold} -.org-hoa-builtin{font-weight:bold} -.org-hoa-acceptance-set{font-weight:bold} +.org-hoa-keyword,.org-hoa-builtin,.org-hoa-acceptance-set{font-weight:bold} .org-hoa-header-uppercase{font-weight:bold;color:#00adad} .org-hoa-header-lowercase{color:#00adad} .org-hoa-ap-number{color:#d70079} From e3b5552fb8524e60fcb34f629debf82a4a54ec0d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Feb 2019 17:35:49 +0100 Subject: [PATCH 04/11] * NEWS: Add missing entry for previous patch. --- NEWS | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/NEWS b/NEWS index 973116ec6..983e88e24 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,10 @@ New in spot 2.7.1.dev (not yet released) + Documentation: + + - A new page shows how to create explicit Kripke structures in C++ + and Python. See https://spot.lrde.epita.fr/tut52.html + Python: - Improved support for explicit Kripke structure. It is now From c25a75ea8e5e58c94951c5dff28644ce3495ac4e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 26 Feb 2019 22:36:56 +0100 Subject: [PATCH 05/11] * tests/python/twagraph-internals.ipynb: Fix a typo. --- tests/python/twagraph-internals.ipynb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/python/twagraph-internals.ipynb b/tests/python/twagraph-internals.ipynb index 815d35006..0e255a9b8 100644 --- a/tests/python/twagraph-internals.ipynb +++ b/tests/python/twagraph-internals.ipynb @@ -5218,7 +5218,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "This properties also need to be updated by algorithms. They can be reset with:" + "These properties also need to be updated by algorithms. They can be reset with:" ] }, { From 262668bbad3ba137a6984d000703e829e09d815d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 14 Mar 2019 22:55:45 +0100 Subject: [PATCH 06/11] org: add an example for dealing with LTLf formulas Related to issue #377. * doc/org/tut12.org: New file. * doc/org/tut.org, doc/Makefile.am, NEWS: Add the new file. --- NEWS | 3 + doc/Makefile.am | 1 + doc/org/tut.org | 1 + doc/org/tut12.org | 222 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 227 insertions(+) create mode 100644 doc/org/tut12.org diff --git a/NEWS b/NEWS index 983e88e24..c9e36f4e0 100644 --- a/NEWS +++ b/NEWS @@ -4,6 +4,9 @@ New in spot 2.7.1.dev (not yet released) - A new page shows how to create explicit Kripke structures in C++ and Python. See https://spot.lrde.epita.fr/tut52.html + - Another new page shows how to deal with LTLf formulas (i.e., LTL + with finite semantics) and how to translate those. + See https://spot.lrde.epita.fr/tut12.html Python: diff --git a/doc/Makefile.am b/doc/Makefile.am index de8eac0ab..cfbd13c73 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -104,6 +104,7 @@ ORG_FILES = \ org/tut04.org \ org/tut10.org \ org/tut11.org \ + org/tut12.org \ org/tut20.org \ org/tut21.org \ org/tut22.org \ diff --git a/doc/org/tut.org b/doc/org/tut.org index 7e812b2f3..60b8f0344 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -25,6 +25,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut04.org][Testing the equivalence of two LTL formulas]] - [[file:tut10.org][Translating an LTL formula into a never claim]] - [[file:tut11.org][Translating an LTL formula into a monitor]] +- [[file:tut12.org][Working with LTL formula with finite semantics]] - [[file:tut20.org][Converting a never claim into HOA]] - [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]] - [[file:tut31.org][Removing alternation]] diff --git a/doc/org/tut12.org b/doc/org/tut12.org new file mode 100644 index 000000000..e2f3ac4b5 --- /dev/null +++ b/doc/org/tut12.org @@ -0,0 +1,222 @@ +# -*- coding: utf-8 -*- +#+TITLE: Working with LTL formula with finite semantics +#+DESCRIPTION: Code example for using Spot to translate LTLf formulas +#+INCLUDE: setup.org +#+HTML_LINK_UP: tut.html + +The LTL operators used by Spot are defined over infinite words, and +the various type of automata supported are all \omega-automata, i.e., +automata over infinite words. + +However there is a trick we can use in case we want to use Spot to +build a finite automaton that recognize some LTLf (i.e. LTL with +finite semantics) property. The plan is as follows: + +#+name: from_ltlf +#+begin_src sh :results verbatim :exports none :var f="bug" +ltlfilt --from-ltlf -f "$f" +#+end_src + +1. Have Spot read the input formula as if it were LTL. +2. Rewrite this formula in a way that embeds the semantics of LTLf in + LTL. First, introduce a new atomic proposition =alive= that will + be true initially, but that will eventually become false forever. + Then adjust all original LTL operators so that they have to be + satisfied during the =alive= part of the word. For instance the + formula =(a U b) & Fc= would be transformed into + call_from_ltlf(f="(a U b) & Fc"). +3. Convert the resulting formula into a Büchi automaton: + #+name: tut12a + #+begin_src sh :results verbatim :exports none + ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B -d + #+end_src + #+BEGIN_SRC dot :file tut12a.svg :var txt=tut12a :exports results + $txt + #+END_SRC + #+RESULTS: + [[file:tut12a.svg]] +4. Remove the =alive= property, and, while we are at it, simplify the + Büchi automaton: + #+name: tut12b + #+begin_src sh :results verbatim :exports none + ltlfilt --from-ltlf -f "(a U b) & Fc" | ltl2tgba -B | autfilt --remove-ap=alive -B --small -d + #+end_src + #+BEGIN_SRC dot :file tut12b.svg :var txt=tut12b :exports results + $txt + #+END_SRC + #+RESULTS: + [[file:tut12b.svg]] +5. Interpret the above automaton as finite automaton. (This part is + out of scope for Spot.) + +The above sequence of operations was described by De Giacomo & Vardi +in their [[https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf][IJCAI'13 paper]] and by Dutta & Vardi in their [[https://www.cs.rice.edu/~vardi/papers/memocode14a.pdf][Memocode'14 +paper]]. However, beware that the LTLf to LTL rewriting suggested in +theorem 1 of the [[https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf][IJCAI'13 paper]] has a typo (=t(φ₁ U φ₂)= should be +equal to =t(φ₁) U t(φ₂ & alive)=) that is fixed in the [[https://www.cs.rice.edu/~vardi/papers/memocode14a.pdf][Memocode'14 +paper]], but that second paper forgets to ensure that =alive= holds +initially, as required in the first paper... + +* Shell version + +The first four steps of the the above sequence of operations can be +executed as follows. Interpreting the resulting Büchi automaton as a +finite automaton is out of scope for Spot. + +#+begin_src sh :exports both :results verbatim +ltlfilt --from-ltlf -f "(a U b) & Fc" | + ltl2tgba -B | + autfilt --remove-ap=alive -B --small +#+end_src + +#+RESULTS: +#+begin_example +HOA: v1 +States: 4 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak +--BODY-- +State: 0 +[!2] 0 +[2] 3 +State: 1 +[0&!2] 0 +[!0&1&!2] 1 +[!0&1&2] 2 +[0&2] 3 +State: 2 +[!0&1] 2 +[0] 3 +State: 3 {0} +[t] 3 +--END-- +#+end_example + +Use =-B -D= instead of =-B= if you want to ensure that a deterministic +automaton is output. + +* Python version + +In Python, we need to the =remove_ap()= object, which we must first +setup with some atomic propositions to remove. + + +#+begin_src python :results output :exports both +import spot +# Translate LTLf to Büchi. +aut = spot.from_ltlf('(a U b) & Fc').translate('ba') +# Remove "alive" atomic proposition +rem = spot.remove_ap() +rem.add_ap('alive') +aut = rem.strip(aut) +# Simplify result and print it. Use postprocess('ba', 'det') +# if you always want a deterministic automaton. +aut = spot.postprocess(aut, 'ba') +print(aut.to_str('hoa')) +#+end_src + +#+RESULTS: +#+begin_example +HOA: v1 +States: 4 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak +--BODY-- +State: 0 +[!2] 0 +[2] 3 +State: 1 +[0&!2] 0 +[!0&1&!2] 1 +[!0&1&2] 2 +[0&2] 3 +State: 2 +[!0&1] 2 +[0] 3 +State: 3 {0} +[t] 3 +--END-- +#+end_example + +* C++ version + +#+begin_src cpp :results verbatim :exports both + #include + #include + #include + #include + #include + #include + + int main() + { + spot::parsed_formula pf = spot::parse_infix_psl("(a U b) & Fc"); + if (pf.format_errors(std::cerr)) + return 1; + + spot::translator trans; + trans.set_type(spot::postprocessor::BA); + trans.set_pref(spot::postprocessor::Small); + spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.f)); + + spot::remove_ap rem; + rem.add_ap("alive"); + aut = rem.strip(aut); + + spot::postprocessor post; + post.set_type(spot::postprocessor::BA); + post.set_pref(spot::postprocessor::Small); // or ::Deterministic + aut = post.run(aut); + + print_hoa(std::cout, aut) << '\n'; + return 0; + } +#+end_src + +#+RESULTS: +#+begin_example +HOA: v1 +States: 4 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +properties: very-weak +--BODY-- +State: 0 +[!2] 0 +[2] 3 +State: 1 +[0&!2] 0 +[!0&1&!2] 1 +[!0&1&2] 2 +[0&2] 3 +State: 2 +[!0&1] 2 +[0] 3 +State: 3 {0} +[t] 3 +--END-- +#+end_example + +* Final note + +Spots only deal with infinite behaviors, so if you plan to use Spot to +perform some LTLf model checking, you should stop at step 3. Keep the +=alive= proposition in your property automaton, and also add it to the +Kripke structure representing your system. + +Alternatively, if your Kripke structure is already equiped with some +=dead= property (as introduced by default in our [[https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html][=ltsmin= interface]]), +you could replace =alive= by =!dead= by using ~ltlfilt +--from-ltl="!dead"~ (from the command-line), a running +=from_ltlf(f, "!dead")= in Python or C++. From 936990a42719aa96f1f49b22bf7dd3779273cd2d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 15 Mar 2019 14:05:36 +0100 Subject: [PATCH 07/11] org: more hyperlinks * doc/org/ltlfilt.org, doc/org/tut12.org: Add links. --- doc/org/ltlfilt.org | 3 +++ doc/org/tut12.org | 25 ++++++++++++++++++++----- 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 84335a641..d1b92a41c 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -285,6 +285,9 @@ ltldo ltl3ba -f '"proc@loc1" U "proc@loc2"' --spin This case also relabels the formula before calling =ltl3ba=, and it then rename all the atomic propositions in the output. +An example showing how to use the =--from-ltlf= option is on [[file:tut12.org][a +separate page]]. + * Filtering =ltlfilt= supports many ways to filter formulas: diff --git a/doc/org/tut12.org b/doc/org/tut12.org index e2f3ac4b5..10641558b 100644 --- a/doc/org/tut12.org +++ b/doc/org/tut12.org @@ -60,8 +60,13 @@ initially, as required in the first paper... * Shell version The first four steps of the the above sequence of operations can be -executed as follows. Interpreting the resulting Büchi automaton as a -finite automaton is out of scope for Spot. +executed as follows. Transforming LTLf to LTL can be done using +[[file:ltlfilt.org][=ltlfilt=]]'s =--from-ltlf= option, translating the resulting formula +into a Büchi automaton is obviously done with [[file:ltl2tgba.org][=ltl2tgba=]], and removing +an atomic proposition from an automaton can be done using [[file:autfilt.org][=autfilt=]]'s +=--remove-ap= option (adding =--small= will also simplify the +automaton). Interpreting the resulting Büchi automaton as a finite +automaton is out of scope for Spot. #+begin_src sh :exports both :results verbatim ltlfilt --from-ltlf -f "(a U b) & Fc" | @@ -101,9 +106,14 @@ automaton is output. * Python version -In Python, we need to the =remove_ap()= object, which we must first -setup with some atomic propositions to remove. - +In Python, we use the =from_ltlf()= function to convert from LTLf to +LTL and translate the result into a Büchi automaton using +=translate()= [[file:tut10.org][as usual]]. Then we need to use the =remove_ap()= object, +which we must first setup with some atomic propositions to remove. +Finally we call the =postprocess()= function for automata +simplifications. (Note that =postprocess()= is already called by +=translate()=, but in this case removing the atomic proposition allows +more simplification opportunities.) #+begin_src python :results output :exports both import spot @@ -148,6 +158,11 @@ State: 3 {0} * C++ version +The C++ version is straightforward adaptation of the Python version. +The Python functions =translate()= and =postprocess()= are convenient +wrappers around the =spot::translator= and =spot::postprocessor= +objects that we need to use here. + #+begin_src cpp :results verbatim :exports both #include #include From bb51499b118858728835066baa0556fa1b24ca78 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 17 Mar 2019 15:19:35 +0100 Subject: [PATCH 08/11] org: typos * doc/org/tut.org, doc/org/tut12.org: Here. --- doc/org/tut.org | 4 ++-- doc/org/tut12.org | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/org/tut.org b/doc/org/tut.org index 60b8f0344..d15063356 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -13,7 +13,7 @@ If you have difficulties compiling the C++ examples, check out [[file:compile.or instructions]]. Reading the [[file:concepts.org][concepts page]] might help if you are not familiar with some -of the objects manipulated here. +of the objects or concepts used here. * Examples with Shell, Python, and C++ @@ -25,7 +25,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut04.org][Testing the equivalence of two LTL formulas]] - [[file:tut10.org][Translating an LTL formula into a never claim]] - [[file:tut11.org][Translating an LTL formula into a monitor]] -- [[file:tut12.org][Working with LTL formula with finite semantics]] +- [[file:tut12.org][Working with LTL formulas with finite semantics]] - [[file:tut20.org][Converting a never claim into HOA]] - [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]] - [[file:tut31.org][Removing alternation]] diff --git a/doc/org/tut12.org b/doc/org/tut12.org index 10641558b..741053597 100644 --- a/doc/org/tut12.org +++ b/doc/org/tut12.org @@ -1,5 +1,5 @@ # -*- coding: utf-8 -*- -#+TITLE: Working with LTL formula with finite semantics +#+TITLE: Working with LTL formulas with finite semantics #+DESCRIPTION: Code example for using Spot to translate LTLf formulas #+INCLUDE: setup.org #+HTML_LINK_UP: tut.html From c63521d67af30be1ca5734d192c0c8c87d485ec7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 17 Mar 2019 17:11:24 +0100 Subject: [PATCH 09/11] work around potential null dereference warning * spot/twaalgos/ltl2taa.cc: Here. * NEWS: Mention the issue. --- NEWS | 5 +++++ spot/twaalgos/ltl2taa.cc | 9 +++++++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/NEWS b/NEWS index c9e36f4e0..01b168b0d 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,11 @@ New in spot 2.7.1.dev (not yet released) possible to iterate over a kripke_graph object in a way similar to twa_graph. + Build: + + - Work around a spurious null dereference warning when compiling + with --coverage and g++ 8.3.0-3 from Debian unstable. + New in spot 2.7.1 (2019-02-14) Build diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc index 49c3880ee..6430f43cb 100644 --- a/spot/twaalgos/ltl2taa.cc +++ b/spot/twaalgos/ltl2taa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2010, 2012-2016, 2018 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2009-2010, 2012-2016, 2018-2019 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -20,6 +20,7 @@ #include "config.h" #include #include +#include #include #include #include @@ -340,6 +341,10 @@ namespace spot for (unsigned i = 0; i < vs.size(); ++i) pos[i] = vs[i].succ_.size(); + // g++ (Debian 8.3.0-3) 8.3.0 in --coverage mode, + // reports a "potential null pointer dereference" on the next + // line without this assert... + assert(pos.size() > 0); while (pos[0] != 0) { std::vector u; // Union From cf8d7113869600bc1ae85d233eab5b6a9f3b07b6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 17 Mar 2019 15:22:39 +0100 Subject: [PATCH 10/11] Release Spot 2.7.2 * NEWS, configure.ac, doc/org/setup.org: Bump version. --- NEWS | 14 +++++++------- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/NEWS b/NEWS index 01b168b0d..ff3a03074 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,10 @@ -New in spot 2.7.1.dev (not yet released) +New in spot 2.7.2 (2019-03-17) + + Python: + + - Improved support for explicit Kripke structures. It is now + possible to iterate over a kripke_graph object in a way similar to + twa_graph. Documentation: @@ -8,12 +14,6 @@ New in spot 2.7.1.dev (not yet released) with finite semantics) and how to translate those. See https://spot.lrde.epita.fr/tut12.html - Python: - - - Improved support for explicit Kripke structure. It is now - possible to iterate over a kripke_graph object in a way similar to - twa_graph. - Build: - Work around a spurious null dereference warning when compiling diff --git a/configure.ac b/configure.ac index ca222c678..e4840a2f4 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.7.1.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.7.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 d03324286..d6ba75962 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,11 +1,11 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.7.1 -#+MACRO: LASTRELEASE 2.7.1 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.1.tar.gz][=spot-2.7.1.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-1/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2019-02-14 +#+MACRO: SPOTVERSION 2.7.2 +#+MACRO: LASTRELEASE 2.7.2 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.2.tar.gz][=spot-2.7.2.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-2/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2019-03-17 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] From 489444aa4d0a8e6efc92c16fdc04a2527d43b902 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 17 Mar 2019 15:24:29 +0100 Subject: [PATCH 11/11] * NEWS, configure.ac: Bump version to 2.7.2.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index ff3a03074..3595c6f1a 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.7.2.dev (not yet released) + + Nothing yet. + New in spot 2.7.2 (2019-03-17) Python: diff --git a/configure.ac b/configure.ac index e4840a2f4..0c87413bf 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.7.2], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.7.2.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])