diff --git a/doc/Makefile.am b/doc/Makefile.am index 3339a67f3..c6fbe19bf 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -116,7 +116,8 @@ ORG_FILES = \ org/upgrade2.org \ org/satmin.org \ org/satmin.tex \ - org/setup.org + org/setup.org \ + org/spot2.svg PICTURES_EXTRA = \ $(srcdir)/org/arch.svg \ diff --git a/doc/org/.gitignore b/doc/org/.gitignore index cbb9e4fa1..709eb9cc5 100644 --- a/doc/org/.gitignore +++ b/doc/org/.gitignore @@ -1,3 +1,4 @@ +!spot2.svg *.png err *.html diff --git a/doc/org/autcross.org b/doc/org/autcross.org index c8095def9..7a09e66ec 100644 --- a/doc/org/autcross.org +++ b/doc/org/autcross.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =autcross= #+DESCRIPTION: Spot command-line tool for cross-comparing the output of automaton processors. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html =autcross= is a tool for cross-comparing the output of tools that diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 85a35dce4..1dca632ae 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =autfilt= #+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting ω-automata. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html The =autfilt= tool can filter, transform, and convert a stream of automata. diff --git a/doc/org/citing.org b/doc/org/citing.org index 9748a3648..b7e5f742f 100644 --- a/doc/org/citing.org +++ b/doc/org/citing.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Citing Spot #+DESCRIPTION: Paper related to Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: index.html * Generic reference diff --git a/doc/org/compile.org b/doc/org/compile.org index dc81dd12c..49bb4c9a6 100644 --- a/doc/org/compile.org +++ b/doc/org/compile.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Compiling against Spot #+DESCRIPTION: How to compile C++14 programs using Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html This page is not about compiling Spot itself (for this, please refer diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 66237fadb..96ae13577 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Concepts #+DESCRIPTION: Informal explanation of various concepts used in Spot. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: index.html This page documents some of the concepts used in Spot, and whose diff --git a/doc/org/csv.org b/doc/org/csv.org index 75bb7a2a8..b4de8e44a 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Reading and writing CSV files #+DESCRIPTION: Examples showing how to read and write CSV files using Spot's command-line tools. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This page discusses features available in Spot's command-line diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 91b79eb40..14b377ded 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =dstar2tgba= #+DESCRIPTION: Spot command-line tool for converting automata into Transition-based Generalized Büchi Automata. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool converts automata into transition-based generalized Büchi diff --git a/doc/org/genaut.org b/doc/org/genaut.org index 74d8fad99..6dc9606f4 100644 --- a/doc/org/genaut.org +++ b/doc/org/genaut.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =genaut= #+DESCRIPTION: Spot command-line tool that generates ω-automata from known patterns -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool outputs ω-automata generated from scalable patterns. diff --git a/doc/org/genltl.org b/doc/org/genltl.org index d7952ad1b..05ee72db8 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =genltl= #+DESCRIPTION: Spot command-line tool that generates LTL formulas from known patterns -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool outputs LTL formulas that either comes from named lists of diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org index b8f4d04ad..13c1bc4df 100644 --- a/doc/org/hierarchy.org +++ b/doc/org/hierarchy.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Exploring the temporal hierarchy of Manna & Pnueli #+DESCRIPTION: Spot command-line tools for exploring the temporal hierarchy of Manna & Pnueli -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html /A hierarchy of temporal properties/ was defined by Manna & Pnueli in diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 12c28e489..0bf4a2bef 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -1,6 +1,6 @@ #+TITLE: Support for the Hanoi Omega Automata (HOA) Format #+DESCRIPTION: Details about support of the HOA format in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/index.org b/doc/org/index.org index dbb5432f4..daf2a2220 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -2,7 +2,7 @@ #+TITLE: Spot: a platform for LTL and ω-automata manipulation #+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata #+KEYWORDS: Spot,C++14,library,platform,framework,tool-suite,LTL,PSL,omega-automata -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_HEAD_EXTRA: Spot is a C++14 library for LTL, ω-automata manipulation and model diff --git a/doc/org/install.org b/doc/org/install.org index d8a9c07e2..49316b601 100644 --- a/doc/org/install.org +++ b/doc/org/install.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Installing Spot #+DESCRIPTION: Different ways to install the Spot package -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: index.html * Installing from a tarball diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 2b26d591b..f2dc6563e 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Common input and output options for LTL/PSL formulas #+DESCRIPTION: Options for input and output of temporal logic formulas in Spot's command-line tools -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html Spot supports different syntaxes for LTL/PSL formulas. This page diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index d3eeae2ec..c36ba72e9 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =ltl2tgba= #+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Büchi Automata. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool translates LTL or PSL formulas into different types of diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index 87b97b9e5..5cb1d345d 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =ltl2tgta= #+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Testing Automata. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool generates various form of Testing Automata, i.e., automata diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 6bef8214b..bb46b4b0d 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlcross= #+DESCRIPTION: Spot command-line tool for cross-comparing the output of LTL translators. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html =ltlcross= is a tool for cross-comparing the output of LTL-to-automata diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 09b31d06d..bdb54b65e 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =ltldo= #+DESCRIPTION: Spot's wrapper for third-party LTL translators -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool is a wrapper for tools that read LTL/PSL formulas and diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index d4bd5d06d..84335a641 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlfilt= #+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting LTL formulas. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool is a filter for LTL formulas. (It will also work with PSL diff --git a/doc/org/ltlgrind.org b/doc/org/ltlgrind.org index 6c33b8d9a..6fbb30976 100644 --- a/doc/org/ltlgrind.org +++ b/doc/org/ltlgrind.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlgrind= #+DESCRIPTION: Spot command-line tool for mutating LTL formulas. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool lists formulas that are similar to but simpler than a given diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index eae52e817..1f5f641b8 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlsynt= #+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html * Basic usage diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 4452bf75e..846ac0064 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Common output options for automata #+DESCRIPTION: Options for input and output of ω-automata in Spot's command-line tools -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html Spot supports different output syntaxes for automata. This page diff --git a/doc/org/randaut.org b/doc/org/randaut.org index 324614948..4e182b817 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =randaut= #+DESCRIPTION: Spot command-line tool for generating random ω-automata. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html The =randaut= tool generates random (connected) automata. diff --git a/doc/org/randltl.org b/doc/org/randltl.org index 110601d6a..3c0c1c4b8 100644 --- a/doc/org/randltl.org +++ b/doc/org/randltl.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: =randltl= #+DESCRIPTION: Spot command-line tool for generating random LTL formulas. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html This tool generates random formulas. By default, it will generate one diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 88ce426fa..53a536653 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: SAT-based Minimization of Deterministic ω-Automata #+DESCRIPTION: Spot command-line tools for minimizing ω-automata -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tools.html #+NAME: version diff --git a/doc/org/setup.org b/doc/org/setup.org index 9536d4320..995cb41aa 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -6,3 +6,6 @@ #+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.5.3.tar.gz][=spot-2.5.3.tar.gz=]] #+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-5-3/NEWS][summary of the changes]] #+MACRO: LASTDATE 2018-04-20 + +#+ATTR_HTML: :id spotlogo +[[file:spot2.svg]] diff --git a/doc/org/spot.css b/doc/org/spot.css index 53828127d..49f4af0c9 100644 --- a/doc/org/spot.css +++ b/doc/org/spot.css @@ -2,7 +2,7 @@ a{color:inherit;background-color:inherit;font:inherit;text-decoration:inherit} a:hover{text-decoration:underline} /* http://paletton.com/#uid=33i0X0kz3BrkeHdpSD1C7r1FAlb */ -body{font-family:Lato, sans-serif;font-size:12pt;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em;background-image:url(/img/spot64.png);background-repeat:no-repeat;background-position:.5em .5em} +body{font-family:Lato, sans-serif;font-size:12pt;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em} body.man{padding:0 .5em 3em .5em} body #content{padding-top:45px} body pre{background:#fbfbfb;border:none;font-family:monospace, courier} @@ -29,17 +29,19 @@ svg.org-svg{width:auto;max-width:100%} #table-of-contents{position:fixed;right:0em;top:0em;max-width:50%;max-height:80%;overflow:auto;z-index:10} #table-of-contents #text-table-of-contents{display:none} #table-of-contents:hover #text-table-of-contents{display:block;padding:0.5em;margin-top:-1.5em} +#spotlogo{position:absolute;top:10px;left:10px;z-index:-1} } @media print{ #table-of-contents{border:1px solid #ffd300} #org-div-home-and-up{visibility:hidden} +#spotlogo{width:2cm;position:absolute;top:0px;left:0px;z-index:-1} } -thead tr {background: #ffe35e;} -#content tbody:nth-child(odd) tr:nth-child(even) {background: #fff0a6;} -#content tbody:nth-child(odd) tr:nth-child(odd) {background: #fff7cf;} -#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;} +thead tr{background:#ffe35e} +#content tbody:nth-child(odd) tr:nth-child(even){background:#fff0a6} +#content tbody:nth-child(odd) tr:nth-child(odd){background:#fff7cf} +#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} @@ -59,3 +61,24 @@ thead tr {background: #ffe35e;} .implem:before{background:#ffe35e;content:"Implementation detail";padding:.5ex;position:relative;top:0;left:0;font-weight:bold} .caveat{background:#ef99c9;padding:0.5ex 1ex 0.5ex 1ex;margin:1ex;border-color:#d70079;border-style:solid none} .caveat:before{background:#d70079;content:"Caveat";padding:.5ex;position:relative;top:0;left:0;font-weight:bold} +.spotlogo{transform-origin:50% 50%;animation-duration:2s;animation-name:animspotlogo} +g.spotlogobg{transform-origin:50% 50%;animation-duration:2s;animation-name:animspotlogobg} +g#version{transform-origin:50% 50%;animation-duration:3s;animation-name:animspotlogover} +@keyframes animspotlogo{ +0%{transform:rotateY(90deg)} +80%{transform:rotateY(0deg)} +100%{transform:rotateY(0deg)} +} +@keyframes animspotlogobg{ +0%{transform:rotateY(90deg)} +50%{transform:rotate(0deg)rotateY(0deg)} +100%{transform:rotate(360deg)rotateY(0deg)} +} +@keyframes animspotlogover{ +0%{transform:scale(.9)} +50%{transform:scale(.9)} +62%{transform:scale(1.1)} +75%{transform:scale(.9)} +88%{transform:scale(1.1)} +100%{transform:scale(1)} +} diff --git a/doc/org/spot2.svg b/doc/org/spot2.svg new file mode 100644 index 000000000..76b76525f --- /dev/null +++ b/doc/org/spot2.svg @@ -0,0 +1,29 @@ + + + diff --git a/doc/org/tools.org b/doc/org/tools.org index 2d0e64eba..57c20ce36 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Command-line tools installed by Spot {{{SPOTVERSION}}} #+DESCRIPTION: List of all the command-line tools installed by Spot {{{SPOTVERSION}}} -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: index.html This document introduces command-line tools that are installed with diff --git a/doc/org/tut.org b/doc/org/tut.org index b712dc7b2..9e7e1bb7e 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Code Examples #+DESCRIPTION: Directory of code examples for using Spot in C++14, Python, and shell. -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 24efd6122..71c6dc307 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Parsing and Printing LTL Formulas #+DESCRIPTION: Code example for parsing and printing formulas in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html Our first task is to read formulas and print them in another syntax. diff --git a/doc/org/tut02.org b/doc/org/tut02.org index ddad6dd33..cbba341ec 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Relabeling Formulas #+DESCRIPTION: Code example for relabeling formulas in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html The task is to read an LTL formula, relabel all (possibly diff --git a/doc/org/tut03.org b/doc/org/tut03.org index 945c4ad0d..156254d00 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Constructing and transforming formulas #+DESCRIPTION: Code example for constructing and transforming formulas in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html This page explains how to build formulas and how to iterate over their diff --git a/doc/org/tut04.org b/doc/org/tut04.org index d6c268b2e..b61ee05f0 100644 --- a/doc/org/tut04.org +++ b/doc/org/tut04.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Testing the equivalence of two formulas #+DESCRIPTION: Code example for testing the equivalence of two LTL or PSL formulas -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html This page shows how to test whether two LTL/PSL formulas are diff --git a/doc/org/tut10.org b/doc/org/tut10.org index 46afe9891..93adbddc9 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Translating an LTL formula into a never claim #+DESCRIPTION: Code example for translating formulas in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html Here is how to translate an LTL (or PSL) formula into a never claim. diff --git a/doc/org/tut11.org b/doc/org/tut11.org index 8a3843663..23f69c09e 100644 --- a/doc/org/tut11.org +++ b/doc/org/tut11.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Translating an LTL formula into a monitor #+DESCRIPTION: Code example for using Spot to translating formulas in monitors -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html A monitor is a special type of automaton that is supposed to /monitor/ diff --git a/doc/org/tut20.org b/doc/org/tut20.org index d83785331..b3793d049 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Converting a never claim into HOA #+DESCRIPTION: Code example for parsing and printing ω-automata in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html The goal is to start from a never claim, as produced by Spin, e.g.: diff --git a/doc/org/tut21.org b/doc/org/tut21.org index ad3e95dbb..54bd98c6f 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Custom print of an automaton #+DESCRIPTION: Code example for iterating over ω-automata in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html This example demonstrates how to iterate over an automaton in C++ and diff --git a/doc/org/tut22.org b/doc/org/tut22.org index 1c2745aaf..50024f908 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Creating an automaton by adding states and transitions #+DESCRIPTION: Code example for constructing ω-automata in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html This example demonstrates how to create an automaton and then print it. diff --git a/doc/org/tut23.org b/doc/org/tut23.org index 78c019fd3..af38981e8 100644 --- a/doc/org/tut23.org +++ b/doc/org/tut23.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Creating an alternating automaton by adding states and transitions #+DESCRIPTION: Code example for constructing alternating ω-automata in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html This example demonstrates how to create the following alternating diff --git a/doc/org/tut24.org b/doc/org/tut24.org index 052bb68bc..1ee5fee77 100644 --- a/doc/org/tut24.org +++ b/doc/org/tut24.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Iterating over alternating automata #+DESCRIPTION: Code example for iterating of alternating ω-automata in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html Alternating automata can be explored in a very similar way as diff --git a/doc/org/tut30.org b/doc/org/tut30.org index 04ae60efe..026392e0a 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it #+DESCRIPTION: Code example for converting ω-automata in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html Consider the following Rabin automaton, generated by =ltl2dstar=: diff --git a/doc/org/tut31.org b/doc/org/tut31.org index ad9603fec..28ffc0bf0 100644 --- a/doc/org/tut31.org +++ b/doc/org/tut31.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Alternation removal #+DESCRIPTION: Code example for removing alternation in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html Consider the following alternating co-Büchi automaton (see [[file:tut23.org][how to diff --git a/doc/org/tut50.org b/doc/org/tut50.org index 88753882f..df925625f 100644 --- a/doc/org/tut50.org +++ b/doc/org/tut50.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Explicit vs. on-the-fly: two interfaces for exploring automata #+DESCRIPTION: Explanation of the explicit and on-the-fly automata interfaces in Spot -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut51.org b/doc/org/tut51.org index 87a880cdf..b630a0cea 100644 --- a/doc/org/tut51.org +++ b/doc/org/tut51.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Implementing an on-the-fly Kripke structure #+DESCRIPTION: Implementing an Kripke structure in C++, allowing on-the-fly exploration -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 110661f41..983239e94 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -1,7 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Upgrading from Spot 1.2.6 #+DESCRIPTION: Help for upgrading code to Spot 2.0 -#+SETUPFILE: setup.org +#+INCLUDE: setup.org #+HTML_LINK_UP: index.html This page is for people who have code written for Spot 1.2.6, and diff --git a/python/ajax/Makefile.am b/python/ajax/Makefile.am index c02413bb7..af8852b94 100644 --- a/python/ajax/Makefile.am +++ b/python/ajax/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2012, 2015, 2016 Laboratoire de Recherche et +## Copyright (C) 2011, 2012, 2015, 2016, 2018 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -20,8 +20,7 @@ nodist_noinst_SCRIPTS = spotcgi.py EXTRA_DIST = $(srcdir)/spotcgi.in README trans.html css/trans.css \ css/tipTip.css js/jquery.tipTip.minified.js js/jquery.ba-bbq.min.js \ - js/jquery.ba-dotimeout.min.js logos/spot64s.png logos/mail.png \ - css/loading.gif protocol.txt + js/jquery.ba-dotimeout.min.js css/loading.gif protocol.txt CLEANFILES = $(nodist_noinst_SCRIPTS) diff --git a/python/ajax/logos/mail.png b/python/ajax/logos/mail.png deleted file mode 100644 index 743a69f61..000000000 Binary files a/python/ajax/logos/mail.png and /dev/null differ diff --git a/python/ajax/logos/spot64s.png b/python/ajax/logos/spot64s.png deleted file mode 100644 index a6d8e91e8..000000000 Binary files a/python/ajax/logos/spot64s.png and /dev/null differ diff --git a/python/ajax/trans.html b/python/ajax/trans.html index 9f18539ba..36ef11a3f 100644 --- a/python/ajax/trans.html +++ b/python/ajax/trans.html @@ -319,9 +319,7 @@ -
- Spot Logo
+ Spot Logo

Translator of LTL to Transition-based Generalized Büchi Automata