alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Merge branch 'master' into next

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2019-03-17 17:28:10 +01:00
commit 0c1da2a0ea
6 changed files with 38 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

37
NEWS
View file

@ -1,18 +1,4 @@
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
- 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:
- 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.2.dev (not yet released)
Library:
@ -29,6 +15,27 @@ New in spot 2.7.1.dev (not yet released)
'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1
state instead of 4.)
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:
- 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
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

2
configure.ac
View file

@ -21,7 +21,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>.
AC_PREREQ([2.61])
AC_INIT([spot], [2.7.1.dev], [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])

10
doc/org/setup.org
View file

@ -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]]

4
doc/org/tut.org
View file

@ -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]]

2
doc/org/tut12.org
View file

@ -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

9
spot/twaalgos/ltl2taa.cc
View file

@ -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 <utility>
#include <algorithm>
#include <cassert>
#include <spot/tl/unabbrev.hh>
#include <spot/tl/nenoform.hh>
#include <spot/tl/contain.hh>
@ -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<formula> u; // Union