alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

update some URLs to skip permanent redirections

Browse source 
* doc/org/concepts.org, doc/org/ltlcross.org, doc/org/ltldo.org,
python/ajax/trans.html, tools/man2html.pl: Update URLs.
This commit is contained in:
Alexandre Duret-Lutz 2016-04-10 12:16:28 +02:00
parent 868f2634f8
commit 5e47d4df38
5 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
doc/org/concepts.org
View file

@ -54,7 +54,7 @@ Andersen's lecture notes]].
In Spot, BDDs are one way to represent Boolean formulas, and in In Spot, BDDs are one way to represent Boolean formulas, and in
particular, they are used to labels the edges of [[#buchi][automata]]. Spot uses a particular, they are used to labels the edges of [[#buchi][automata]]. Spot uses a
customized version of [[http://sourceforge.net/projects/buddy/][the BuDDy library]] for manipulating BDDs. customized version of [[https://sourceforge.net/projects/buddy/][the BuDDy library]] for manipulating BDDs.
* ω-word * ω-word
:PROPERTIES: :PROPERTIES:

2
doc/org/ltlcross.org
View file

@ -101,7 +101,7 @@ No problem detected.
=ltlcross= can only read four kinds of output: =ltlcross= can only read four kinds of output:
- Never claims (only if they are restricted to representing an - Never claims (only if they are restricted to representing an
automaton using =if=, =goto=, and =skip= statements) such as those automaton using =if=, =goto=, and =skip= statements) such as those
output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. The output by [[http://spinroot.com/][=spin=]], [[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/][=ltl2ba=]], [[https://sourceforge.net/projects/ltl3ba/][=ltl3ba=]], or =ltl2tgba --spin=. The
newer syntax introduced by Spin 6.24, using =do= instead of =if=, newer syntax introduced by Spin 6.24, using =do= instead of =if=,
is also supported. is also supported.
- [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with - [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT's format]], which supports generalized Büchi automata with

2
doc/org/ltldo.org
View file

@ -19,7 +19,7 @@ any other tool.
* Example: computing statistics for =ltl3ba= * Example: computing statistics for =ltl3ba=
As a motivating example, consider a scenario where we want to run As a motivating example, consider a scenario where we want to run
[[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file. For each formula [[https://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file. For each formula
we would like to compute compute the number of states and edges in the we would like to compute compute the number of states and edges in the
Büchi automaton produced by =ltl3ba=. Büchi automaton produced by =ltl3ba=.

2
python/ajax/trans.html
View file

@ -616,7 +616,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
</label><br> </label><br>
</div> </div>
<div id="tabs-tl3"> <div id="tabs-tl3">
Use <a href="http://sourceforge.net/projects/ltl3ba/" id="ltl3ba-link">LTL3BA</a> to build: Use <a href="https://sourceforge.net/projects/ltl3ba/" id="ltl3ba-link">LTL3BA</a> to build:
<label class="rtip" title="Stop LTL3BA once it has built a Transition-based Generalized Büchi Automaton. Spot will take it from here and optionally apply more optimizations."> <label class="rtip" title="Stop LTL3BA once it has built a Transition-based Generalized Büchi Automaton. Spot will take it from here and optionally apply more optimizations.">
<INPUT id="ltl3ba-T" type="radio" name="lo" value="T" checked> <INPUT id="ltl3ba-T" type="radio" name="lo" value="T" checked>
a TGBA a TGBA

4
tools/man2html.pl
View file

@ -1,6 +1,6 @@
#!/usr/bin/perl #!/usr/bin/perl
## -*- coding: utf-8 -*- ## -*- coding: utf-8 -*-
## Copyright (C) 2015 Laboratoire de Recherche et Développement de ## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
## l'Epita (LRDE). ## l'Epita (LRDE).
## ##
## This file is part of Spot, a model checking library. ## This file is part of Spot, a model checking library.
@ -42,7 +42,7 @@ while (my $file = readdir(DIR))
my $html = `(echo '.HEAD <LINK REL="stylesheet" TYPE="text/css" HREF="../spot.css">' my $html = `(echo '.HEAD <LINK REL="stylesheet" TYPE="text/css" HREF="../spot.css">'
echo '.HEAD <meta name="viewport" content="width=device-width, initial-scale=1">' echo '.HEAD <meta name="viewport" content="width=device-width, initial-scale=1">'
cat $file) | groff -Kutf8 -mandoc -Thtml - -P -r`; cat $file) | groff -Kutf8 -mandoc -Thtml - -P -r`;
$html =~ s|GNU GPL version 3 or later.*http://gnu.org/licenses/gpl.html&gt;|<a href="http://gnu.org/licenses/gpl.html">GNU GPL version 3 or later</a>|s; $html =~ s|GNU GPL version 3 or later.*http://gnu.org/licenses/gpl.html&gt;|<a href="http://www.gnu.org/licenses/gpl.html">GNU GPL version 3 or later</a>|s;
$html =~ s|<h2>.*?</h2>|<div class="outline-2">$&</div>|smg; $html =~ s|<h2>.*?</h2>|<div class="outline-2">$&</div>|smg;
$html =~ s|(<a href="#.*?">.*?</a><br>\n)+|<div id="table-of-contents"><h2>Table of Contents</h2><div id="text-table-of-contents"><ul>\n$&</ul></div></div>|sm; $html =~ s|(<a href="#.*?">.*?</a><br>\n)+|<div id="table-of-contents"><h2>Table of Contents</h2><div id="text-table-of-contents"><ul>\n$&</ul></div></div>|sm;
$html =~ s|(<a href="#.*?">.*?</a>)<br>|<li>$1</li>|g; $html =~ s|(<a href="#.*?">.*?</a>)<br>|<li>$1</li>|g;