diff --git a/NEWS b/NEWS index e338af9be..6b939fe78 100644 --- a/NEWS +++ b/NEWS @@ -4,7 +4,7 @@ New in spot 1.99.2a (not yet released) for each generated automaton. * The html documentation now includes a HTML copies of the man - pages. + pages, and HTML copies of the Python notebooks. * Bugs fixed - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3) diff --git a/doc/org/tut.org b/doc/org/tut.org index d90530bb7..7251fb43a 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -8,7 +8,6 @@ This section contains code examples for using Spot. This is a work in progress. Feel free to [[mailto:spot@lrde.epita.fr][send]] suggestion of small tasks you would like to see illustrated here. - * Examples with Shell, Python, and C++ All the following pages show how to perform the same task using the @@ -26,3 +25,29 @@ Python (at least at the moment), so they are purely C++ so far. - [[file:tut21.org][Custom print of an automaton]] - [[file:tut22.org][Creating an automaton in C++]] + +* Examples in Python only + +In directory =wrap/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. + +For convenience, the following links offer static HTML renderings of +these notebooks, but we strongly suggest interactively evaluating the +real notebooks instead. + +- [[https://spot.lrde.epita.fr/ipynb/formulas.html][formulas.ipynb]] covers the basics of LTL/PSL formula parsing and + printing, with some light operations +- [[https://spot.lrde.epita.fr/ipynb/automata.html][automata.ipynb]] covers translation from formulas to automata, + automata printing, and some lights transformations +- [[https://spot.lrde.epita.fr/ipynb/automata-io.html][automata-io.ipynb]] shows how to save and read automata from files +- [[https://spot.lrde.epita.fr/ipynb/piperead.html][piperead.ipynb]] shows how to save and read automata output from other + commands, using pipes +- [[https://spot.lrde.epita.fr/ipynb/randaut.html][randaut.ipynb]] shows a simple case where the [[file:randaut.org][=randaut=]] commands + generated random automata, which are displayed in a table before and + after acceptance simplification +- [[https://spot.lrde.epita.fr/ipynb/accparse.html][accparse.ipynb]] exercises the acceptance condition parser +- [[https://spot.lrde.epita.fr/ipynb/randltl.html][randltl.ipynb]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] +- [[https://spot.lrde.epita.fr/ipynb/testingaut.html][testingaut.ipynb]] shows the step necessary to build a testing + automaton diff --git a/src/sanity/Makefile.am b/src/sanity/Makefile.am index d69364e77..121371a4a 100644 --- a/src/sanity/Makefile.am +++ b/src/sanity/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche -## et Développement de l'Epita (LRDE). +## Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +## Recherche et Développement de l'Epita (LRDE). ## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. @@ -37,6 +37,10 @@ check-readme: top_srcdir='$(top_srcdir)' \ $(PERL) $(srcdir)/readme.test +check-ipynb: + top_srcdir='$(top_srcdir)' \ + $(PERL) $(srcdir)/ipynb.test + check-includes: CXX='$(CXX)' \ CPPFLAGS='$(AM_CPPFLAGS) $(CPPFLAGS) $(DEFS)' \ @@ -45,10 +49,8 @@ check-includes: TOPBUILD='$(top_builddir)' \ $(SHELL) $(srcdir)/includes.test $(TESTHEADER) -.PHONY: check-80columns check-style check-readme check-includes -check-local: check-80columns check-style check-readme check-includes - - +.PHONY: check-80columns check-style check-readme check-includes check-ipynb +check-local: check-80columns check-style check-readme check-includes check-ipynb # Ensure we have not forgotten to include an header. check-installed-includes: @@ -68,4 +70,10 @@ check-installed-private: installcheck-local: check-installed-includes check-installed-private CLEANFILES = failures incltest.* -EXTRA_DIST = includes.test 80columns.test style.test readme.test private.test +EXTRA_DIST = \ + 80columns.test \ + includes.test \ + ipynb.test \ + private.test \ + readme.test \ + style.test diff --git a/src/sanity/ipynb.test b/src/sanity/ipynb.test new file mode 100755 index 000000000..c5aee7353 --- /dev/null +++ b/src/sanity/ipynb.test @@ -0,0 +1,76 @@ +#! /usr/bin/perl -w +# -*- cperl; coding: utf-8 -*- +# +# Copyright (C) 2010, 2015 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 . +# +# Check that all the directories documented in README exist, and that +# all directories listed in configure.ac are documented. +# +# Also has an option --list to print directories which are +# documented. + +use strict; +use warnings; + +local $\ = "\n"; +my $top_srcdir = $ENV{top_srcdir} || "../../"; +my $top_srcdir_len = length($top_srcdir) + 1; + +my $tut = "$top_srcdir/doc/org/tut.org"; +my $dir = "$top_srcdir/wrap/python/tests"; +unless (-f $tut) +{ + print STDERR "$tut not found"; + exit 2; +} + +open(FD, "$tut") or die "$!: cannot open $tut"; +my $exit_status = 0; +my %seen; +while () +{ + if (m:\]\[([\w-]+\.ipynb)\]\]:) + { + # print "$1 documented"; + $seen{$1} = 1; + unless (-f "$dir/$1") + { + print STDERR "notebook mentioned in tut.org does not exist"; + $exit_status = 1; + } + } +} +close(FD); + +open(FD, "$dir/Makefile.am") or die $!; +while () +{ + if (m:\s([\w-]+\.ipynb):) + { + # print "$1 exist"; + unless (exists $seen{$1}) + { + print STDERR "notebook $1 is not mentioned in tut.org"; + $exit_status = 1; + } + } +} +close(FD); + +exit $exit_status;