From 2402d721a9fa58570d3306d65746ee1d7ea4b2c3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 27 Jun 2018 15:16:48 +0200 Subject: [PATCH] modernize the logo * doc/org/spot2.svg: New file. * doc/Makefile.am: Distribute it. * doc/org/.gitignore: Adjust. * doc/org/setup.org: Display it. * doc/org/autcross.org, doc/org/autfilt.org, doc/org/citing.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/index.org, doc/org/install.org, doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org, doc/org/tut51.org, doc/org/upgrade2.org: Include setup.org instead of declaring it as SETUPFILE. * doc/org/spot.css: Add entries for the logo. * python/ajax/trans.html: Use the new logo. * python/ajax/logos/mail.png, python/ajax/logos/spot64s.png: Delete. * python/ajax/Makefile.am: Adjust. --- doc/Makefile.am | 3 ++- doc/org/.gitignore | 1 + doc/org/autcross.org | 2 +- doc/org/autfilt.org | 2 +- doc/org/citing.org | 2 +- doc/org/compile.org | 2 +- doc/org/concepts.org | 2 +- doc/org/csv.org | 2 +- doc/org/dstar2tgba.org | 2 +- doc/org/genaut.org | 2 +- doc/org/genltl.org | 2 +- doc/org/hierarchy.org | 2 +- doc/org/hoa.org | 2 +- doc/org/index.org | 2 +- doc/org/install.org | 2 +- doc/org/ioltl.org | 2 +- doc/org/ltl2tgba.org | 2 +- doc/org/ltl2tgta.org | 2 +- doc/org/ltlcross.org | 2 +- doc/org/ltldo.org | 2 +- doc/org/ltlfilt.org | 2 +- doc/org/ltlgrind.org | 2 +- doc/org/ltlsynt.org | 2 +- doc/org/oaut.org | 2 +- doc/org/randaut.org | 2 +- doc/org/randltl.org | 2 +- doc/org/satmin.org | 2 +- doc/org/setup.org | 3 +++ doc/org/spot.css | 37 +++++++++++++++++++++++++++------- doc/org/spot2.svg | 29 ++++++++++++++++++++++++++ doc/org/tools.org | 2 +- doc/org/tut.org | 2 +- doc/org/tut01.org | 2 +- doc/org/tut02.org | 2 +- doc/org/tut03.org | 2 +- doc/org/tut04.org | 2 +- doc/org/tut10.org | 2 +- doc/org/tut11.org | 2 +- doc/org/tut20.org | 2 +- doc/org/tut21.org | 2 +- doc/org/tut22.org | 2 +- doc/org/tut23.org | 2 +- doc/org/tut24.org | 2 +- doc/org/tut30.org | 2 +- doc/org/tut31.org | 2 +- doc/org/tut50.org | 2 +- doc/org/tut51.org | 2 +- doc/org/upgrade2.org | 2 +- python/ajax/Makefile.am | 5 ++--- python/ajax/logos/mail.png | Bin 4016 -> 0 bytes python/ajax/logos/spot64s.png | Bin 9398 -> 0 bytes python/ajax/trans.html | 4 +--- 52 files changed, 111 insertions(+), 57 deletions(-) create mode 100644 doc/org/spot2.svg delete mode 100644 python/ajax/logos/mail.png delete mode 100644 python/ajax/logos/spot64s.png 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 743a69f613c234ea17ea42efed935c00b0d39c63..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 4016 zcmeAS@N?(olHy`uVBq!ia0y~yU~m9o4mJh`hEk44ofy`glX=O&z`&N| z?e4D(S#{FuA82m zu>AL=U;F1o=S{9%?Jlo8LjNdFEqYgEscIGKImc_MNT(1(let3^3!{(Rm~ znJa%l?;DGl_{nur3D11}{r9im|NU3#{>Ua>E&Iyv=Vhl{+Ro|xFCs96U4yk(oj z3AOIij7q^5=C58=_2$NJ`IvjF>L#tt__A02|4~P$6ZQr?i|=p!t+{Pm-t9}WyJ9-^ z{x1&k&23=H>zDrjclG}XwsQRLnzmk=e>Xo?_gn36!r*@Yw>O)}`yj9SD_1YO&#(Pf z+4k5%VAHL<5E>7Ge5j+l1za6A9Um+H$!BPYE(vFXpD z&fs*lc^VA&?0@z38a%1D=*zDC+q->dQxlWNB$hytg{!i{mVUNmXPAAKt@$8BAkTxz z{r;!rw%=a6;?%v#%k6gUm8?xSzjfea@_Q?Zwx4sJ|D3kH?t}ZBlPOLrLX8?-r}^?^ zyN;(W4B(g&Bq9=V;qv9CnT1dtA?o<;)j1H8GWxem7874ljLJ@FJkT{(U;LG)v-LhB-F>9tX80 z?z`}sxAcDf>-IT*%bgVj989EQ&7X!d>4O71{mKN1Z*wlDtf~6jd;j^CC|wpu2OY87BB{l9``s3I98L06h`HQ$c;R7b z#>BG>bF4nbnI1NXpLzD#rttXc?#GpKO$rK9y?IhkKeH}eytsR(oz)`V_CxKze(gHX z$H%vOyGR4SpWNDHiD%lYw{H0HG(7IPiIlI?&$A(ATYq275SgU1aKi=xYip~S(%0R$ zE)4ik5TE~DpS`^;Hk#=``|`eN#yrLu+pXuc_wAXr=ueo|?AJCzoeq;!ZseG4+4?>u zukY@I=7SF=-n;j1K0hySwYg}+WqFy+Mm)b;Z^i@^{&;%bqVMs8@4t(!_N*;vy7}(- z%!JK1H!R*dcW2E{CHd~7eBZv6{LOjsr}e}#hJs&*zi;I^{HN==X|8_#d)~h1KU+Ta z2i=^y%)@h1!uH!2Z{0e^!^1b>a5yuic-Y>#yTr*v#dS&QSCE z!^GQOjw=USvw-Wzjlp$GKRYNeG#_MGewlOk-M)zvv(JC|R&w9ozUJel zSqwjZoawyJT<~nRel54?)X)wWr4PUV_QxKqdB@$v(0#P&(WIaaI^8Evc22L_WxZcc zZlA?WafbOdC7)cKPT1S-eJ|~k9Bi!O*>wH2Z{*e7t-kq7ctb-KIheS(xdQ_OS@)ms z-np~={=0XtEUarDUi#C;Q1k2K%A!LC^UF(0KF^Ka>k=Be!12BbGj|Q*y7K` z;KZS^G(d!Pk;b8yC5yIgn|EjCoD>$vA8XgGn`^(f;9-!?a^Vz-XYX@b&2sba=dm%w z=!uKC-rT?(y;}Ip)pbLlz7lX{{lMVj%c3+*nKC<8cIahg&-}2_uPn&d3_g`HW8tQ5x)26^NW9H0* zM~<-kxh#C6&GL)2$ea8Pi+8S)m}6wfy@vnSUFjMCC*Cy5Q*GX#V~8`5gu1x_wV?>Pax*a1?m(u|nZj?Tux^ z7vDSxe6_(TdBd`I$tMFFELytcmc>Z~z!?%TJmnGG&lzf(^ zeqh?tcWT{v2kd!&q&IdjY}wQBYLn8O-TN9=oMl@ZHk;|dmoFx-UcLJ8nmsO|t&L5K z;ioJ^{Uip5(5ta?WA`ewsLZ(+7Gx*YtLAp|ZJDyzhXpr94%Y4F>nqZZsEvIkpk<_R zhG}1ZB>y|Zjtzvq?b&7G4*c3O{1OEj+_%c5_6tqdj z{i7eVqW-H>bAD8vVV!-JZQk?XU|#R@uS<4`JU_2%+}$L=H2EY;|8eHH!|P{%`ZzVp zK%(XP>(=9s8HGP3v|F~twKHCu|MJPO%lMx*k1x)Dpj7C&L2I5KVpE z<1fwzHZbjJJHKkjs#P5>N}SK1eym97+jTK1aKrJ$mX-JT3S4K(_OgoS-Zba!&}+y` z+LoQh;`7+h+XVb*FWzOVb-WE9g?5z%q# z)G3p@9(=+c{*r=C>*mJ(DEi;rt<0J=xx0oFl7S&VSd#sdG8qx8)z=xUz5Vv@XVlN3XEc0zn!(2f8E0KGHjjxq5YF?t@dkS z5nog7c&2PhPWI^w$vv*?(uSUv)fU(9-2*ixIZm7Ysg!=T z`}@-?inE1NHW@0|rpw!xeSg=Qu;Re~Pr1=w3s3GkWm;@5wqTOE*Ha6 zPPP_n+S7E`5>u%ihPK`9pkIYhhAP6yd@A2uwlv~r=r9?Ul>FV9X#k7xM!`t{;l+n|0L6n zt_^=#5*b@6`-jnfnVe7Jjh*b)&-Wi|Nwv25CG@1|tIGL=Q>V8&9L`D%YF_d3#`b6X zmbD)$St`4**W}*4JA8&JhhBevRP=LmfCl4vqZez|vK%jBIPoa^l8jL7CbwNGi>4@v z@F_|Nd^n))5Fj$+iGkFtaV23qKri zoZ*|s(0%{s@4x>rui@Rbyq^2A$FDSNdQ58hwd&WOO#cbiB5|FJFE{-* z{%&Yz+BdCDY)f7~>tTZhQewtG;V@+<$(VT-v{&Jq^>S=q`wx@2!M7yu+ zUN9Gx=H(>u)E(?+{>``GLevbSSDSS5J1^Z#as8$w!RvNsS21_8aB{|)T$a+!dsoWp9Dj7|39rYd zDgB%&@qFu3{wD<-`Ej?fWNZ1t6B}oIoR}(Ew_kpeO0GuTjTa%uHt9%ZOBp_&b@;5c z`NfFKGfw0_v*lf-edGV0YPp3O9OrHS%9u#;GAKy!C<$<^u~fUSvvl*+BzHp}H(|AR z{tK3^VXK;JcYV{06yKhd#dn%_vTNvTx<`9PC!PELv!>%{l7Gvkmq%BaFWR_E@Vnf- z=F87oJo8VP3wXWlS)@_$GbSTDui0;P^qkMm3wzePn`Ikro!Ocid1c!5qsRA;pfkvy0cHog&Mx?Q zUYW5%?X}H}iQ*fg)>twxIy=pluk6Vk!Clstodp&w7k<20x@@9mtdeKZ^N9k-9(!E) zF-xg(we3s(v)h=RGv8H-Xg;4gyWHfpap&tJpS#s3PZpkO*N}K);qC3mf92hmJAGoY zzShhV-%LNrSSQV;y%rO)|NN}^b5~O^;nwa)?~iqDI-@b^>5hdK4FCCmq-9>nvvx0M QU|?YIboFyt=akR{00YFB1^@s6 diff --git a/python/ajax/logos/spot64s.png b/python/ajax/logos/spot64s.png deleted file mode 100644 index a6d8e91e8e6dccdabc34c614a04c4ba72f04dcc8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 9398 zcmeAS@N?(olHy`uVBq!ia0y~yU~m9o4mJh`hEF<~;+^X0sQq35=_6xCBn| zJiSRO*RbS~)XCh*!t&|K>;22#`qo_YToUVkO>0|fblmqN(^9;rq#WCnGHH>A*OG_> zT#LTPvCX)*|NU)yHVGb&leWK)@3Saoo562<|IYKh-*=wh`~ElAtYsfxA3Jg2!CdwF zZ-<1JY-X(OeEVh9-01z6Z*6<0zDOnY$Nz*A``;~EmicMx_49u`Cugl#y<(N(Qmx(V zWGnab_I`QgD?LxB?)Ptwu0=DFH_osZ;d=S}`Sa`UivxqTrYcQ8t$5lfZL{R+tFsEM z=1%wa@-hlrUFtPy3Cn`N-?sl$W@gC9@;f=xMKVNm_QfN|x}<*Zyng=Q^;gG!37hS% zef0L;3XQJRtSqeyH*fBIdS_>G_4=5dLK2danX~51nR58y2JP7=J$AlS(Cg#8UQ7j8Sv7l5{@#bVuPKU9s+<*jU@`+1J;t{(i6e{pRTHd9_C$ zf8_bo&S+q78(jbN%*|?*y>VGN(VutSOp>(ub5%V)VtIK^@lM+pK5lKzn^VGB?RM3^ zpZ8vGZ+=Eb#$Ds{HlHV^&#Qcv;O_38sx_6#VN&Ui(^;G*xkuivKln`N=(8_L+8-0Q zSznYslM=-FXrjW!3pyJw=uB+QY?|!cQxdOWVcN4Qh0$PUIdxr^EP<^J4kWM;1u z;9yzzH<0ndg(czh>fZfsdv}rFDpv2;<%=u7e!u^dQ+M)g%kTN;>&kmKZ@K#X^F>?R z#?0Hd`19{={p>z@^5pFLABW}bek_*%`vT-J)`oi-3r#Ng{Jk~TB!9B_I9%kHA#k+z8n?mB z*-BD*w&%jj(uOl~PFTrKTH-wAs7*lk``{v}ix+s3_fEI?d+GbmvR~p$galmzQ=Xrj zTRZ>fnRL1Ruh;FKcj@)l;`#!PIkt6=4z|Yc{rI-Dw0BaDQDI_YQQB>G{x@b4JO|fl zhkxh)`t84G=WWx1CqFixT5tF9NbJRokSmftTXJrle)s*4>RIW0_k0tveKmTMl}*gg zd6ZipzAN6rqTcD+!(bnOM*Rj z>B&6Z`h4Dk-;Y*5G17cfw)@w`{<<$8p4)xj`TyPb-|PRxF=%ux>ULXv&ByAk<+r`^ z^?UWy-)n!Leo=0=^rzgY&woFD%l>Y0`Bl{Rt9bz?p}Wm)=-2!YZ}E!hr{)|D?dLIZ+w%VSTD!m z8hA!M?#K6fj;}oLgx5Y>v3T99l$4rPilRKZa{aAmuez-+-Mju&#^wkI5kVJ5M}Zkp zGoGJ#Ve*pq{n8~m4XX~F$1rEL{eY8^hcyxH*>RlqyD}`?^ za5sB#VyV%QXHGsPJOVQFoP1a7^qd!(8_B@S;&>!B?6mIhd*{EE|F@j?$%=)MC7~{D z&h)wu{d@kszwdZ5HDYU4=$ntn<^M0Q{r%0B>yO(;wTxMA1!>#fo!DRVyH_@pcWKkf z14nmup5$eJw=X>{tLpOs@AY=Owr;w&>henm0Rb05M*#sB#=t2ZDoKBeQl`yZr5j^c z-eS&IKmFy!JO(c0K(AD!80d|tTeKoFmBOO1@4;MSuVNAkB9R@O93 zv)|qOd*2tsu={&?S08WOaDtO{)7349&SdLUH!RCs(70rJ;SZZ5&5Fya+dW&9jyNmM zVbsrlcdPAYW^!IZ)6I#DyUxiw<{Jb@?iY((zI;!fY2!0rp1AtSCpR+Qy}3Dk`}VC{ zeXm}*67yp#LrSsb=Btlqc|`FXPQG}dBj91B?@X?|n75y%b1mZF=>Dd!_Hj|Vqre3d z-t~t&7p`f!)Sh=V@S$U{X~5R0ZTgaHK2AHPA1jc`S-rA7!oVd-(dpYOJ7d*zyhrh(w_!-G9-IXd_wODexeZ%rS^VWTKpE*n7V(iYM)VuR+tJm$m z`|jU%mIv$qJ<>OqtA2G;U0tv2PbgpS+V6LM+N-cQzLx(#;~=jbGgxTUP`Cc-aO{2u%+p)cc#Mhvy;5j14Uaue321b-hAnpREZk%!G(oh zf8uI1^XZt$&^H!|c%Kh=ms)wyRT{5zkothp{K1(e5zuI+uuJ%3RPv&o) zsWZ1o!ui0|?+uS;rgOHqvV=*@m!Ij<_3~b#n_l_Eh>nCUQ5^o~7Om3yym&Ilq6Y1N zwuXj_Y0Ju@wVMW&JmAd-V3w*Vh&| zDXe+G{L=sX{_l);pZrlRxqQ9WS!<&>H=ydH-E^F!Fp_IN{8a zmsg%$G_9D{d!?&KzwGBxpQdFKd5+I`C6};gasQ2}f=>#jT{?Sq$7?MCmd4hNnMFHg z%=(49FZXG5Wz1?@Gnq3d$4P+2?RK@~>)lOjj05(kS#R?5Uyy3N`SIVLuknIaRaIek z3y;grt=qr9n3W;^->LAlUB7?-Nq+bE|q+}$7d^&Ix% z7hs(@Gozz#lgu-%>t|DrZ~DkIf%9nR7k|U6)x!c89E4t32DsxM*ej!*$#iwV@%`)*nqUdHC&m z;ny#T%hcU?KUVDd7yG{I`e&=TdT|U7E*{@!^m4_z9eMdH>^8payX*hu>$kNhzx3S+ zk9#z!i%~YTBe)uzC4ME#ke{r%Is z?0Q@K1bJRFh2&(qzMcO(uUPqOoPFO-le@*jONuSO`Az@87q5J-vejF;_C?m6jE5#0 z&v6#r)M1<6+htnH!md8^l~l@><#XG%-JMc#dgJbzBTmI%;%nzFT&Q?|TkdVQSFc~6 z7iHK{eEr@3vcF4{<2!kK>o=4aB;3{Kli#=d>a%Z^Z&fo|Z|-mW(dAM2Qr^Y!!KX6< zw(C^fcDFwGVDT|Q!hL0Xjap-l)#;M=0u!fO{}6s26*ir9#r5e1Rz`l?Znhf9rsiJj zyqa=I>7~THSt@EPbIijYZHU--x~gjVv6)`(H!f&zwhnT7bx9*wj5T|!c)l}hbGj90 zU+=;vMr-c<(o2~u7oKT4H$6VFuFUC7icxC${o3!`-f;?VSFHK{(Jb9HH92zW&cBzA zhU&{&KiXOT*eplQ*n8oAo8NcVu#4?=2n}6#eEG$_n_0_aSoR zGKa;jJlv9}9PhpJFrSr?XH$=a&xPf#7q0F&S#~z)`G-Z*Q>qpjpSd=3gI_Ag4cjBh zh3j4~K2jvfH!W|$wb#d|3GSFP&r!TUQA0{fN?E*WhV1L*%SyHPbyewzBujZVr=9dLNj;O_(uP+oqk%- zMAIXUxwBOx_-=EGkf+mRFDsCCl|G{eD}r zc3NfK8>8jwza=j(H3->Vd0GB3du{%Qnl0=PuSLySd$s4N_=yau=92=O?l+bdb(rp- zl^(xr3fK1b6q_?2)Aze6$+0>ne71r|E;RwXYQR;^NFcquRc_tT574;{Zx z-KhBd`uzG^8W{!ukL5=6ENf!lBg(IHzV6?yRV%h=UtYoM*LE(BRWv5F?peEf;8dBd z(bpcV(sG`pI_ad!wv8&He)_9cDP$RJF>qdVwDZkYBeB`(896+wm6Bz<9(sBmG1gp^ z#Amp6!e);-vagmDr}dmHE!z^ro&DS8Ug+j&YMW=@Y^~Je`EF=$>y-Mp>Qr`kqRH(U zlCRS@JT{r=ab$P>|9{ipl>J`v<;eE=d!qKI9{w!e{`;H1h<=pN$oOAN? zH(#584OOiC98C_tJ@kW*iFCFaY>mGDaLt#=eMbdV1Sj8hD^c?>n|UncVNy*6Q+`nU z=_Kc1k#+6MIV@ejsJq|X8gOXeC9!Q)S(%%EM5cbal=kuRvd=-%<`3k&olVXz5pa$Q zW}DPd@3eH?k|`xxzUw6t4TO^tbEG`4Z7h4f_k>kvjM?dcV)#YFN3K{b36jJ&e+%D^iE8`gqK&;QJDK>?#o>&T~oTkmWc?sO#C^K zQ)it}(r3jtcIF2ka;E)qH;C|wh~X=FT2)u`l_}R)?#rSh9j4AVcUHdpyyjTy=EbYD zR;^mJ@~4%P$N>#0Ln+=VR&%!eWIE&O98+D|rB~hcd4&(3d*D==oz_{Ak8d4(vDA*u z`n=Grxd)=-d_y0z**q=v;f)pdn`g80aU;9jiRtOw+}xsX-@eUe)Czl_;3b$5DiR?g zqa(E{vs-Y(5#~pmb}(jasE|0NGLb3uOuvuOP1BCen?&k^bvc;61(|!PdF#zq7VI(z z)if|M?>LvTL?y&58HfXM8j>lA7Zhqf@d)Nhs#o5!IkG((6}g_1-JWNnhUScRqM~t!>q2!SYhe zMSgA~tX`+~>|lEO;}vsAe$LXu=WesUSz&siLn(@a4=SfzOWZUnQkFed+H*hEwKrt(ly8^9!F#;Ij4W*XJZ8BrN7I zu(5g5?V{wi`EIBEg{IugyDiqv;BZs!VEwsnVWyV1#*_c&_HUcQS+ePj_20Eq__SA8 zih8O~_D$tlRbW~C0pN1RKLsD zuW$FgV$yr@;>AmUT-Dh&i<)>W75ek$O!lA8`gO-@bY}G*R`T7D;_`6g3&B;Zf*yY? zo*&@+Agb$4&Kd>zX*TW=Q;v9xt9UA{O7%!H5}Cwf9yZ6k>OfJ1PU`Zd8#c^1vnF`X zj7w5(vuB1Vc`1o89mv?0xW$5@<=?-5MS>Ta4lZCy(Eh0O`jcvbj)}X~+($Pm%=LX^ z)Tf>k>6*!;zQWZeK&3Avbm6I|PZx%6-~4Tt+nYBEJ9F}OwzdSkV9bcxXDsvW)r@X; z0aio(gRM{1dNw%K78y%$Xxp$axb*CZP@ut$Gfy^2CO!N!snIY0NYo=%1qq(4MT<0+ zr5I(hZ?L#?!m3uT;e*VqS%-sOsq9$Y)4lnyw#|YFO}*w#Z&bThJ=zepb9)){?q9u6 z>Tdd4NoZeTJ$hA1YQ@vAU&))ba}ry-#drTXyI%ad#w-T2#hmd$ZVXdmru|T2*mSPp z=sP9_sa~%ntGRmp#~-g{2y18eoaE3PkzqFfero5Wv!yYsFU^SH5aWu@)%^DPVEhr* z(`)rZLno?CTzl1bkAL2=&!;RVzJA=TxLHPM)~cj0)-Md)IF2T9GjU~?>*NLgl{-0#F zoL}I?GNa0$uZj)!o;v4HP_=P+e2l`~GtAoSpI07CxKQkVH|kr@?UQ@V9P$KNe3^YO zZV0K~@yN3vH>cpDL}6=SzH3!$+FM?J-VZlqEPTWSmbzAdvOTV9w;@8Od65FgtgBg} zjE^Q(7TvT-3TqeloaEV-eB_xEhtv!+)*V`H9?Okgb=Ply+$g=idD%*irUSaBXW#Vf z@Q9JnY?-tylcT9)%hs;L+dS(o-aeO8!Fa+vx@GpB2Wu}UZB%~}(z<4m!bz(&W#5$; zGKD6xGR*N?uE5pQaQ(ID=OgCcdb8uNZ=Y5%;j3FxapJE2`N~$pF6rimdk=bk|C2IN zT%>dHc8~6S_c_~HW<}U9QnwRYvO#1`CWjU0<8M-W`IkN~PGQ&Qi&>DLHOEJ-TcwMm z>4#Zn;nFez*2V;#Q%*KraruWHePEd2tIjR=;PX!b#XE2ENHi*j6 zxG6KUqU~Y#T%R)Dq>OLHp7LrNcQ7WkS|rWn=)RqBdRF33-X?_t?@ZZe>jb>~G$&n` zYGRwFW&UVhlvVkSierYS_|?x9maUi_qBb{w^W6#m@|c`NBgo$;u$|&68Z7 z$$l<^ERNZEd3O3tA>rZiMiM+r9!+G5j+$#1vy}15951U`Zuv$=b!)|agFEu|mKG-# zwOU-tQ#mTVvmxm{L+Is#n{Tch_g&I-(dqEY50R^8@mp`_J^d_8={J+irru9;y^qhB zF+ZB8TeUoXmEg4bqP~xBy%1Qn?BTa?@uGSi8+R?qqe*7jTeogyR&vPAeLLm$TR*iV z?w&7On%TsnIeT+=GtSs$*Ry}8SbVJL#+w3>?R}SD8Xo!>(HP0Sd7aqD1H5w=KML9T zgq3lzu;L7sk8Nv}yX7bQF5~b&JF!o7!I?u({KW0O%ZxV)oXPImUQq8S(78M~M)G97 zYF1RewOY5RZ}Y=-pO-uew26D~yufO44^CKPpPtT;>=i>k2`)I`t?`aLiQfH4WZ)#co?2~umLy4I# zlVa4ojbu{4WSJjaXsBlO+u`a5Q#OyBZ-qJQ*j)p|CfpaY^jhTc{)$EHV`T}Suvunz z`V_cQf;4yC?q`%*9llHB2Zw4tN9fZ3ekNfFoQ z&6_=*$wc`%hF-0?C&serCC@V<>(sNQDu)7>{ch9noRU-&CAoG+azb90TD@x5qO~sq zGNtxZy%k#MGRNU_+Nsyq8r%{eiypYPHd=r7*=Lc4|K%Ka|NVBmf5zEocMhG=aGsm) z$T0h|v-9m-hLSyB)F!U1Wbt$naaD;_iphN7k_i#^jhycJ3HHdUF`0%n9!n*9=6r+$5X?QWiPyZ*^L zNzvLRsPoV|(ZDGZvt~XzuHL^OOKSH0kIO^0=ddKK`OkIt?QsE?#@+At{ho68p+q!e zg969SzrVl#->_+uk(s^inU&)6T~4M>EV0Vl`+c%SZKzM2{F6(Y)eFOZ6o&np_@$_B z;-)jlo^Dd{_lxjWjA2z{-A0Addzrt0OZYT3>X`{Ey`mW@NV7`o$Nt(-kx6OPf zd+brkgZyrrnQAnr=Hcv?=V~ifuIzkwfB*mZ$UCM%3=9jlZvFbBk(s@ZA;#hxkMs5O%mIP> zXXTdvwah5^w{r29J!KmwtTOs2vRHig2DUvb-bWvwI8Dc%x2&LQ&-8sWImMI&pB++E zYbuVJE%EH=LhnD>pRDHI)`>7@J@IVQ8NMFFs-@i}Hja_Sx~aOQH*EZ-``urQyW)L@1#e6HY<}^q zTNUJ`W!n??)-B&G=vqv>hPTA_8y#!Ciu5F$=XNT(HJ_N&(&ct7(?PFP`L-{|N|VdA zhh5U2PyAZ7XDg$Qp8Gz*=o{V)R?Yi5o^+W%D> z?%OTzBH(hV)8hF2zgizXCcJv}>O{N!pNILLlcq#%iUf_m?r^IAQM2!(hsvd@S65bE zEuP%$v>;RXpM$d6YUcU`(Y@3AjExOW{CQ#G)-D*SAGmRsraWKw?Ie}CJZ_Q~bKT;f zyRIrzWS`^V$2~J-($0m3&)SYNGM0y0zI#>FBNjYyg;tB|#-9RKlLfm^2c9tSo}@Y1 zC)ikBG1b)W`(E{o_wSdPTsZUF{x|QRt7kcwV(h*a*L|H_&*pp8?)S~}cA);|`p!i& zs-qcP0?(M5nwHMDD17v9;zGyYZz|+_U*{ixRq*&zXwajTOFsV*Tvpx2;m;CTeSYl> z@0=q|iY%T^lT^fxEuXpLo_j`8TZ%^4n#r8LXAExJJEfG#?LFDDew$EutNh-ZM=sgj z60KGh@9jNzZn5zT!<%beB~|8szZxR8(fGvw%7>PHF?Q{1j~xH~@ALJHn>*N9W=QNg z=fD4#xsFf&hT`YvHoD7IKACJbJ9pC$Gjm3UgzdMV?}=Og=alyPJ65K*^xM;pXWsk4 z$K%Gmv{6mvro;WGlXZH|3dqcHG3#=9-sH0EbLo*g7bND*^19PlbZD~inSNhI4kpz) z{du#v-Yk9hhmE}}BypleRGqJ~7?0xX5{b9hQd3Tt+dOMuR`F}L{lhz7`M$Urf3JPx zeP`2qW{xI@l)72V<$jCQPWOLMwtI5F?YA3;UteGU|7Y*EeX0x%Ve#?z=lLz4?KjtI zYg*P4?-Oa4Omc7Zt}za{x? z=(?A(WYbp0#b=v#+$f3`a~Fx&`(vxBsU)|a!pjsNv+Ts|-ep-lbKX68vESx&#eWI0 z-LtFZ{wQs~``9_8-W#cTbDFM=o={qq#Vsv-d#3#Sgk9M@a}PRX7MpsRIagHm9dVix zVbHRC8PndITVnKeqT>wyxm}N!`q*l)NFhn@D>j|Y*TCc7J+}+c8a-m;Z+i!`Q&sM_M*)~q!wQ-lM zN0nsx0-5g1fmhh#i#{s}biHm?nkLTDSfQ~g;=zd$`Q0ZzuD3n@b^7^<-l;3%%eCMC zKVzPGcN4#($jK#>W$eH3#{GIY{lpTXJEhlS_x9WW`w{=MX5Z@k^vCO285S&Al9KWH z+1YUYxIH_HH|)QDwfdvQN|zpo&uU+m{W*5zS#LQ5)4`L9Y3%MV>iJN3Jkebx!kxGO%9#_(ZCwLr$j(^s{)p(gzqbQ#&9`+-sbXy3-4px0cGCBM zNB=KbRAz45TbNlXBq-A85l$6~0 zx6;4%)$R5Beq}W)bgkL{cJH3&lldR7&SKydaZTLuS!TWMf0l5+y>#Y>Zx7dqURc zFUYE8-gnGvO&mMhYRmar+!0THv+m5PJ6w`ucBbSzM{+ou#O^!ZDO&dr8%NJwbN{bg z+1>x1t7e-${pr%M@?jod?c@BNe|~W<$h=eee6B4hn2yhyJ=_1E+U~k+28On_wzB$f zo9F+1w$QmfDkOAi+1Ijn|9{wDx=^OQN$-Byxn;p$Vr&jd|Nke;W_50Zfic??@0i7B zTW+Qve^r)HcJq^xyU2x*sX1ECHFjP$5^8qxsE?x%mF!vk}v|JKY52Il71f89v#uYLJC z{{OGP4+|nTS=i*<`OC2T-EWquy{`qAE|pD`e73wz@=cBLdIf7gV|!aCy~%Eu@0EQv zYf@NvS-Rlo>Xp%(o1gWT2VAb=es_uC)1rr~78zZtZJexcck<}l`Pj&6 z;|I%COu@=?_tgE^J;(Y}@}c6N$=$Qfa;1JB65sdXhwb+}pJgMbiPwoo*Xc7%JNDqg zgKzmYkEQGXHp~BcaBt>JNnwY~P~+U)@0M3ymJPYKJ+XM&Itz=fCMLZ{jhVTcG@kY! zx^rOSPv&5)i>;Dw)%q7pA8JhZw>$r)LY^TtHMO%{uIj~6|C&d_|E&c$_Wb;P;{!V* z!vc-2hi7IQzyE#j`@Zid54ZE*H?pRSEj@Kk7lvJsB#>D-K zTJuiC)%D~u@$lkw$(Q>a%73rsDVdX&wq|;c)p_o^{r1)OYrpUPdBK^#Hv9B6-SZub zepJs-{@2VHA$2q7TIt6}M}N<+`}LApfB&CP&*sgOi#MAc-z=;;Q^=o{Z@YZ=;pU_7 z4uw5B{O(iomK&Z&54$}3tSH!jPMG_=AfKPmtho-spC9?Izkd179h=(cbIa%1SA2Nj zZ=Q4G!=v}F-u++5pu_8Xxkp%7xHo^#$765Z`(!H9tADp{YixA9f9O!t!}6WeH8?C{ z*M;QfzCANdH(Kxg-QC}xzP-JDe^^-9HSQ(#ulaw~^E!MC2)$}zZ7u!c-Mf1=KR-Q< zwzjsG{{8EhO>%Pb>qj4VOz=_TUVhwHO<1hkb?vHEyDr_hA(4}r`7$p%yL#`=oj>qWHDFe(~(%|5=;Qly)3C&tZ35qQDFQ}?uw-&Wldr**w_u0LU7c$6sQyKBYM R90mpk22WQ%mvv4FO#lRWHPrwB 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