1#!/bin/sh 2# -*- coding: utf-8 -*- 3# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement 4# de l'Epita (LRDE). 5# 6# This file is part of Spot, a model checking library. 7# 8# Spot is free software; you can redistribute it and/or modify it 9# under the terms of the GNU General Public License as published by 10# the Free Software Foundation; either version 3 of the License, or 11# (at your option) any later version. 12# 13# Spot is distributed in the hope that it will be useful, but WITHOUT 14# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 15# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 16# License for more details. 17# 18# You should have received a copy of the GNU General Public License 19# along with this program. If not, see <http://www.gnu.org/licenses/>. 20 21. ./defs 22set -e 23 24# Skip this test if we don't find a sufficiently complete LaTeX 25# installation 26 27(latexmk --version) || exit 77 28(pdflatex --version) || exit 77 29(kpsewhich txfonts.sty) || exit 77 30(kpsewhich amsmath.sty) || exit 77 31 32cat >input <<\EOF 33XGFa <-> FGX(!b & !c) | (b ^ a) 34a U b W c R (d & e) M f 35{a;b[=2];((c:d*) && f*);e[*2..]}<>-> {((a | [*0])*;b[+]) & (c1[->2])}[]-> h 36{a;b;c} []=> {d*;e} <>=> !f 37!{a;b*;c}! -> d 38{a*;(b;c)[:*3..4];(c;d)[:+];d}! 39G(uglyname->Fuglierlongname42) 40"#foo/$bar$" U "baz~yes^no" 41EOF 42 43( 44cat <<\EOF 45\documentclass{article} 46\usepackage{amsmath} 47\usepackage{spotltl} 48\begin{document} 49\begin{tabular}{ll} 50EOF 51( ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\'; 52 genltl --go-theta=1..3 --latex \ 53 --format='\texttt{--%F:%L} & $%f$ \\') 54cat <<\EOF 55\end{tabular} 56\end{document} 57EOF 58) > output.tex 59 60TEXINPUTS=$top_srcdir/doc/tl: \ 61latexmk -f -silent -pdf -ps- -dvi- -pvc- output.tex 62 63# latexmk will have a non-zero exit status on failure, so we will 64# detect that. However the file output.pdf really ought to be 65# controled by eye... 66