Commit 21ff2d04 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

org: Add link to the Python notebooks.

Fixes #100.

* doc/org/tut.org: Link to the notebook.
* src/sanity/ipynb.test: New test, to make sure we do not forget
to document ipython notebook when we add some.
* src/sanity/Makefile.am: Add it and run it.
* NEWS: Mention it.
parent 868cabe4
......@@ -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)
......
......@@ -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
## -*- 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
#! /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 <http://www.gnu.org/licenses/>.
#
# 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 (<FD>)
{
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 (<FD>)
{
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;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment